> I believe I’ve read that even Church himself said that Turing machines are a more elegant basis for computations, since they are much easier to mathematically reason about.
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.
"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!
> 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.
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!
I think you've demonstrated far more familiarity with the subject matter than me (and my own understanding is admittedly pretty basic), and just wanted to say I really appreciate your thoughtful response. You're right that those quotes don't really fit for what you were asking for evidence of.
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.
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