Nope. Turing machines are arbitrary and rather unmathematical. The lambda calculus is a much better computational formalism, more mathematically grounded and oriented, with far more direct practical applications.
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.
Wikipedia provides a partial list of these correspondences at https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon... :
* 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.
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!
Thank you, this is exactly what I was getting at.
> ... (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!
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.
"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.
Computing science cares a lot about building efficient processes. Thus to create real working programs, a better basis is a combination of lambda calculus for defining mathematical structures and (Von Neumann based) agent-based models for defining stateful processes.
Modern programming languages are evolving to be capable of representing either model, to adapt themselves to the style more suited to the problem at hand.
For seeing whether a given statement holds true, minimizing complexity is the most important.
Precisely, and that's the main difference between computer science and the rest of mathematics.
Typically CS cares about the process to find a result, and not just its value nor the possibility or impossibility to find it.
Typically, programmers care about the process to find the result. Some programmers are computer scientists. You can not conclude that all computer scientists are programmers, so your statement is based on logical fallacy.
There are results in theoretical computer science that don't care about the efficiency in the process; the most essential are the computability theorems exploring what parts of mathematics can be computed, and what we mean by computation anyway.
But the most essential part -the halting problem- was resolved long ago, so the lion's share of applications of computing science is in finding practical ways to use computers, which again needs to take efficiency into account.
Efficiency and tractability of representation is also an issue, though, and mathematicians (and programmers) do care about that, a great deal. That's why the lambda calculus has been used as the basis for proof assistants such as Coq, whereas Turing machines have not.
Sometimes that could mean using the lambda calculus, particularly in study of language theory and type systems. Other times that could mean some sort of black box model, such as when proving lower bounds for solving problems using specific operations (see e.g. the sorting lower bound). Yet other times, like when establishing the ground-zero of some new variety of computational hardness, I can't think of many more suitable models to cut up into pieces and embed into the substrate of some other problem than those based upon Turing machines.
As I said above, it may very well be that the best usage for Turing machines is using them in mathematical proofs; where the efficiency of the computation is not a concern.
This response might come off as a little facetious, but seriously, I think the idea of "founding" industrial computing languages/platforms upon theoretical research models of computation misunderstands the relationship between theory and practice. There is a relationship for sure, the research on these models usually does want to translate into real-world implications somehow, but your functional programming language is not the literal lambda calculus.
Each time a new theoretical model is created to represent a particular programming problem, entirely new languages are created to ease the practical approaches of building systems for the underlying problem.
And it is worth keeping track of which models are good for which problems. So no, theoretical models are not good just for doing math with them, also for guiding practical usage.
My original comment certainly reads that way, but my intent was really to point out that it doesn't make sense to privilege the Turing machine model in the study of computation. I wrote more about why in this comment: https://news.ycombinator.com/item?id=27334163
That was a claim someone made, but it turned out to be a misunderstanding, and is incorrect.
I've covered this here: https://news.ycombinator.com/item?id=27338055 (see the parent comment for quotes from Godel & Church that I'm referring to.)
I'd be interested in a source for this.
Lambda calculi are used as the basis for several functional programming languages, which seems to argue against the idea that they're less easy to reason about.
They're also used as the basis for proof assistants such as Coq. Coq is based on the calculus of constructions, which is a typed lambda calculus. Again, this would be a mystifying choice if lambda calculi are difficult to reason about.
> I disagree with your statement that it is more mathematically grounded.
I've provided more support for my position here: https://news.ycombinator.com/item?id=27334163
https://plato.stanford.edu/entries/church-turing/
"In his review of Turing’s work, Church himself acknowledged the superiority of Turing’s analysis of effectiveness, saying:
computability by a Turing machine … has the advantage of making the identification with effectiveness in the ordinary (not explicitly defined) sense evident immediately. (Church 1937a: 43)"
Moreover, Gödel himself (as well as other mathematicians) found Turing machines and Turing's thesis to be more persuasive:
Gödel also found Turing’s analysis superior. Kleene related that Gödel was unpersuaded by Church’s thesis until he saw Turing’s formulation:
According to a November 29, 1935, letter from Church to me, Gödel “regarded as thoroughly unsatisfactory” Church’s proposal to use λ-definability as a definition of effective calculability. … It seems that only after Turing’s formulation appeared did Gödel accept Church’s thesis. (Kleene 1981: 59, 61)
Gödel described Turing’s analysis of computability as “most satisfactory” and “correct … beyond any doubt” (Gödel 1951: 304 and *193?: 168)."
For what it's worth, I do think you've started an interesting discussion!
You're allowed to have an opinion that you prefer lambda calculus over LCMs (logical computing machines -- a better term for Turing machine's that Turing favoured) for conceptualizing and reasoning about computation mathematically.
Myself, I find Conway's game of life to be the superior framework over both lambda calculus and Turing's Logical Computing Machine :-P
However, those quotes are not saying "that Turing machines are a more elegant basis for computations, since they are much easier to mathematically reason about." I still consider that statement to be false, and I've substantiated that in my comments.
The quotes from Church and Gödel are saying that Turing's formalism was the more helpful in making the case that it had captured the notion of effective calculability. That's understandable - it's much like e.g. Cantor's diagonal, in that it makes its subject very concrete.
But that doesn't tell us anything about the usability of the formalism as an actual mechanism for computation, or analysis of computation. In that respect, lambda calculus has proved far more useful, as shown by the examples I mentioned, and many more. Another example is denotational semantics, which maps programming language semantics to lambda calculus.
In fact, one of the inventors of denotational semantics, Dana Scott, developed the first non-trivial model of the lambda calculus, in terms of complete lattices. That model addressed the concreteness issue, albeit decades later, in the early 1970s. It's possible Gödel, Church etc. might still have preferred the Turing tape as an intuition-friendly proof for effective calculability, but it would no longer be possible to reasonably make Gödel's "thoroughly unsatisfactory" claim about the lambda calculus.
Coming back to denotational semantics, I'm pretty sure no-one has ever provided a non-trivial language semantics in terms of a Turing machine - and if you wanted to do that, one of the easiest ways to do it would probably be to implement a compiler from lambda calculus to Turing tape, and generate the Turing representation automatically from that.
More generally, my position could be simply refuted with counterexamples of tractable Turing machine solutions to any of the various problems that lambda calculus has been used to address, like programming language implementations, programming language semantics, duals of logical systems, and proof assistants. To my knowledge, no such examples exist, and the reason for that is because what I'm saying is a fact, not an opinion.
> Myself, I find Conway's game of life to be the superior framework over both lambda calculus and Turing's Logical Computing Machine :-P
I'll agree that the game of life is only slightly less useful than the Turing machine as a model of computation!
I also agree that the absence of such a refutation is a pretty solid argument that your position is simply a fact and not an opinion as I argued.
Cheers friend!
This is what I primarily meant with my controversial statement, sorry I didn’t articulate it well enough. Of course lambda calculus is very useful and has plenty of applications, never meant to say otherwise!
In case it helps, I've provided some substantiation for my position here: https://news.ycombinator.com/item?id=27334163
I should also clarify that I didn't intend to argue that lambda calculus should be the only way of understanding computation, but rather that it doesn't make sense to privilege the Turing machine model, as the comment I was replying to suggested.
The Turing machine model is arbitrary, and it is unmathematical in the sense I've described in my comment linked above. A different culture (or species!) would be likely to come up with a different computational machine-like model, but any culture that develops formal logics would be likely to discover the lambda calculus as a consequence of that.
Thus proving the point that a field that studies them cannot be considered a branch of mathematics.