This reads like total nonsense to me. Why would Turing machines be 'arbitrary and unmathematical'? What's 'unmathematical' about them? They can be formally and precisely described and I don't know of any mathematician who wouldn't accept TMs as a sound definition.
Turing machines are arbitrary in that they don't derive from some mathematical basis. You could easily reformulate the abstraction in many different ways, replacing "tape" or a "read/write head" with some other quasi-physical concept that don't normally appear in mathematics. Those concepts are spurious, just provided for their analogy to real-world machines.
You can provide formal descriptions for many things - the Perl programming language, for example. I would also call that language unmathematical. You can study such objects mathematically, but they are essentially external objects of study which one is using mathematics to make more tractable.
In contrast, Curry and Howard discovered direct correspondences between logic and lambda calculus. For example, intuitionistic natural deduction is isomorphic to typed lambda calculus. The internal languages of Cartesian closed categories are lambda calculi.
If Church hadn't discovered lambda calculi, they would have eventually been discovered via one of these correspondences.
* Girard-Reynolds System F as a common language for both second-order propositional logic and polymorphic lambda calculus
* higher-order logic and Girard's System Fω
* inductive types as algebraic data type
* necessity in modal logic and staged computation
* possibility in modal logic and monadic types for effects
* The λI calculus corresponds to relevant logic.
* The local truth (∇) modality in Grothendieck topology or the equivalent "lax" modality (◯) of Benton, Bierman, and de Paiva (1998) correspond to CL-logic describing "computation types".
As such, lambda calculi are inextricably embedded in mathematics and logic, and their core features (ignoring superficial choices such as syntax) are a discovery, rather than an invention. We can't change the equivalences described above, they are facts that arise from the formalisms developed to address subjects like logic and categorical analysis. The same is not true of Turing machines.
> They can be formally and precisely described and I don't know of any mathematician who wouldn't accept TMs as a sound definition.
Just because something can be formally and precisely described doesn't necessarily mean it's (aesthetically) "mathematical". Another example that comes to mind now is the notion of an applicative functor (Applicative in Haskell) — sure, you can give the categorical definition for it but it's quite an oddly specific structure (if anyone reading this knows where they arise in non-FP contexts, I'd really like to know!).
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.
A good yardstick to judge the "mathematicality" of a construction often amounts to looking at its compositional properties. That is, could you re-use the concepts over and over again, and could variants of the structure be uniformly described? While Turing machines and lambda calculus are both equivalent and can be both formally described, one does win over the other in terms of having a simpler, more compositional structure.
This is quite subjective, and in any case it feels remarkable that both Turing and Church came up with their constructions to describe computation formally!
> 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.
