> Just because something can be formally and precisely described doesn't necessarily mean it's
> ... (aesthetically)
The 'aesthetics' part is an interesting argument I didn't see, and yes, I agree that a particular concept arising in different areas of math is 'aesthetically pleasing'.
> ... "mathematical"
That's the part I have a problem with, mathematical objects are (more or less) exactly those that can be precisely and formally described. "Lambda calculus is a more elegant mathematical object" is not a statement I have a problem with, "Turing machines have a lesser status as mathematical entities", on the other hand, is sort of weird.
> So for Turing machines, maybe a question we might ask is, "how can we ensure Turing machines always terminate?" This is a much harder question than say, imposing a type system on untyped lambda calculus which unconditionally makes all terms terminate, while still retaining the ability to do recursion and useful work.
You can bound the number of steps or the size of the tape :)
That's not a "well, actually", the point I'm making is that other computational models (TMs, pointer machines, RAMs, counter machines) are more natural formalisms to think about some problems. Sure, logic/proof theory is intimately related to lambda calculi and it would be extremely unnatural to formulate the same ideas using Turing machines, but for things like analysis of algorithms, complexity theory or numerical analysis it would be similarly unnatural to use lambda calculus as the computational model instead.
They certainly aren't lesser forms of math, even though one might find them less aesthetically pleasing.
> ... it feels remarkable that both Turing and Church came up with their constructions to describe computation formally!
It is. It completely blew my mind when I first learned about that fact. If computation can be exactly described by different formalisms resulting in the exact same set of computable functions, then it must be a very fundamental feature of how "things" work!
> That's the part I have a problem with, mathematical objects are (more or less) exactly those that can be precisely and formally described. "Lambda calculus is a more elegant mathematical object" is not a statement I have a problem with, "Turing machines have a lesser status as mathematical entities", on the other hand, is sort of weird.
I agree as well. I don't think Turing machines have any lesser status (it's literally equivalent to lambda calculus, after all!)
> but for things like analysis of algorithms, complexity theory or numerical analysis it would be similarly unnatural to use lambda calculus as the computational model instead.
That's a good point as well. Because of the nature of hardware, neither lambda calculus nor Turing machines are very good fits, so RAMs and pointer machines essentially take over.
> I don't think Turing machines have any lesser status (it's literally equivalent to lambda calculus, after all!)
"Equivalence" has a specific meaning here, though. The term "Turing tarpit" was invented to point out the limits of that equivalence, and any attempts to define computations for Turing machines quickly run into that.
The sense in which I consider Turing machines to be "rather unmathematical" is closely related to this. You can write useful mathematical proofs in lambda calculus - as I've pointed out elsewhere, there are automated proof assistants based on this fact. There's no such equivalent for Turing machines. Theoretically, there could be, due to Turing equivalence, but in practice, no-one wants to exploit that.
Given one formalism that has actively been used for such mathematical purposes, and another that has been actively avoided, I call the latter rather unmathematical by comparison to the former.
People can quibble with my word choice, but it's describing a real, measurable phenomenon, the effects of which have played out predictably over the last 70 years.
> ... (aesthetically)
The 'aesthetics' part is an interesting argument I didn't see, and yes, I agree that a particular concept arising in different areas of math is 'aesthetically pleasing'.
> ... "mathematical"
That's the part I have a problem with, mathematical objects are (more or less) exactly those that can be precisely and formally described. "Lambda calculus is a more elegant mathematical object" is not a statement I have a problem with, "Turing machines have a lesser status as mathematical entities", on the other hand, is sort of weird.
> So for Turing machines, maybe a question we might ask is, "how can we ensure Turing machines always terminate?" This is a much harder question than say, imposing a type system on untyped lambda calculus which unconditionally makes all terms terminate, while still retaining the ability to do recursion and useful work.
You can bound the number of steps or the size of the tape :) That's not a "well, actually", the point I'm making is that other computational models (TMs, pointer machines, RAMs, counter machines) are more natural formalisms to think about some problems. Sure, logic/proof theory is intimately related to lambda calculi and it would be extremely unnatural to formulate the same ideas using Turing machines, but for things like analysis of algorithms, complexity theory or numerical analysis it would be similarly unnatural to use lambda calculus as the computational model instead.
They certainly aren't lesser forms of math, even though one might find them less aesthetically pleasing.
> ... it feels remarkable that both Turing and Church came up with their constructions to describe computation formally!
It is. It completely blew my mind when I first learned about that fact. If computation can be exactly described by different formalisms resulting in the exact same set of computable functions, then it must be a very fundamental feature of how "things" work!