A More Immediate Intuitive Appeal | Veit's Blog
Veit's Blog
A More Immediate Intuitive Appeal
2026-08-04
Alonzo Church published The<br>Calculi of Lambda-Conversion in 1941. On page 41, weighing up the<br>formalisms that had been proposed for the intuitive notion of an<br>effective procedure (a bit of a fight between him and Turing), he grants<br>that Turing’s has “a more immediate intuitive appeal” than his own.
It’s a generous sentence, and broadly correct (although I find<br>Church’s construction, the lambda calculus, more appealing), and it<br>makes me sad every time I think about it.
I should say where this comes from, because I am not a logician and<br>the foundational crisis is not my day job. I don’t really have a<br>business reading these books. But when I was eighteen I read Logicomix, a graphic<br>novel about Bertrand Russell and the search for a secure foundation for<br>mathematics, and it handed me a story I’ve been unravelling ever since.<br>The names and stories in the book fascinated me, and so I read Frege,<br>then Russell and Whitehead (I gave up on the Principia Mathematica,<br>admittedly), then Hilbert, Wittgenstein (his Tractatus is a big ol’<br>letdown in my opinion), Gödel, and eventually Turing and Church. I tried<br>to read the real literature, badly and out of order, because noone was<br>grading me and I would just find papers and books more or less randomly<br>over time.
Fifteen years of that, and I’d struggle to tell you what it’s for.<br>It’s fun and gratifying, but most of it is over my head, and the<br>notation is arcane and archaic (though Frege’s Grundgesetze der<br>Arithmetik is a real notational gem, even if you take nothing else<br>away from it).
Church’s sentence made me cry, which is both a sign that I’m a huge<br>nerd, and that I’m too far into the bikeshed to turn around now.
What he actually gave away
The concession didn’t start in 1941, and it wasn’t small. Church had<br>already reviewed<br>Turing’s On<br>Computable Numbers for the Journal of Symbolic Logic in<br>1937 (they both published their systems in 1936), and it was in that<br>review that he coined the phrase “Turing machine”. He named the thing<br>that would eclipse his own for the years to come. In the same review he<br>wrote that computability by a Turing machine “has the advantage of<br>making the identification with effectiveness in the ordinary (not<br>explicitly defined) sense evident immediately”.
For completeness’ sake (no pun intended), there’s a third party in<br>this, and in my opinion he matters more than is commonly understood.<br>Gödel had not accepted lambda-definability as a definition of effective<br>calculability at all. Kleene later reported that he regarded the<br>proposal as “thoroughly unsatisfactory” (ouch!), and it seems he only<br>came around to the thesis once Turing’s formulation appeared. Of that<br>one he said it was “correct […] beyond any doubt” (OUCH!), and later<br>that “we had not perceived the sharp concept of mechanical procedures<br>sharply before Turing, who brought us to the right<br>perspective”1.
That’s likely why Church stated his thesis in terms of recursiveness<br>rather than in terms of the calculus he had built (though the SEP<br>treats it as a bit of a puzzle still). Gödel wasn’t buying what he<br>was selling, and although I don’t know if this is a reflection of a<br>broader sentiment, it was clear enough that Church came to believe<br>Turing’s method to be more intuitive himself.
Why can’t we just get along?
There’s more to this that I personally find strange and sad,<br>though.
By the time Church wrote that sentence, the question of<br>power was closed. Kleene had shown in 1936 that the<br>lambda-definable functions are exactly the general recursive ones.<br>Turing had shown in 1937 that his computable functions are exactly the<br>lambda-definable ones. The three formalisms were provably equivalent for<br>the application that people were arguing about.
Nothing was at stake mathematically. Every remaining disagreement was<br>about which story a person could be brought to believe more quickly. And<br>on that question, the tape and the head and the little machine that<br>shuffles along it beat an algebra of substitution, even for mathematical<br>geniuses amongst themselves.
I find that a bit deflating. I personally find lambda prettier (more<br>on that below), but there’s also something structural at play.
For the longest time, I believed that in mathematics (and science at<br>large) the argument ends when the proof is formalized. Here it did not<br>end, even though everyone knew that the proofs were equivalent, and<br>people quibbled over, basically, rhetoric, personal taste, and,<br>honestly, a bit of ego.
But back to Turing machines and lambda calculus.
Why I still like lambda
I should define beauty, because the whole problem here is basically<br>that it’s famously in the eye of the beholder.
Turing’s model persuades his readers by metaphor. It creates a<br>picture of a clerk with a paper tape, and you check the picture against<br>your own sense of what following a rule is like, and it matches. You can<br>even do your own...