Joachim Breitner's Homepage
For a course at the IIT Bombay on functional programing, I was preparing a presentation on Alonzo Church’s theorem, based on his original 1936 paper “An Unsolvable Problem of Elementary Number Theory” where he first showed that the Entscheidungsproblem is not solvable. In that paper, he states a theorem (Theorem II) “If a formula has a normal form […] any sequence of reductions of the formula must (if continued) terminate in the normal form”. This seems to be wrong. Consider the lambda expression KIΩ, where K=(λxy.x), I=(λx.x) and Ω=(λx.xx)(λx.xx). This has a normal form I. But because Ω reduces to Ω, there is a non-terminating sequence KIΩ → KIΩ → ⋯, in contradiction to Church’s claim. The same example contradicts his Theorem III: “If a formula has a normal form, every well-formed part of it has a normal form.”, which is used in the very proof of his main result, Theorem XVIII.
There is no proof for Theorem II in this paper. He cites it from the then forthcoming paper “Some properties of Conversion” by him and J. B. Rosser. There, proofs are given (see Theorem 2 and its Corollary) but they are quite impenetrable to me. So I was searching for some correction paper, or any other discussion of this issue, but could not find any. Does any reader of this blog know more? What happened in that times when a paper had an error in some proof? What would happen now? Or is this not an error after all, but just a subtle difference between the definitions of λ-calculus as we know and as they introduced it?
Unrelated to this question: The professor asked me to write down a summary of (my interpretation of) the importance and impact of Church’s paper with regard to Gödel and Hilbert’s program, and how that relates to Böhm’s theorem. In the spirit of sharing, I have uploaded my thoughts on Church and Böhm, comments are welcome.
Update: Christian von Essen solved the riddle in a comment to this post: Church only considers lambda abstractions as well-formed when the bound variable actually occurs (freely) in the abstracted term. This does not allow for the K combinator and thus there is no problem.