In 1983 or 1984, when Alonzo Church was about 80 years old, he was invited to speak at the Center for the Study of Language and Information at Stanford University, and was taken on a little tour featuring CSLI's Xerox Dandelion computers. These computers were running LISP, a programming language developed by John McCarthy (b. 1927). Church was told how LISP was based on the lambda calculus that Church had invented some 50 years earlier.
Church confessed that he didn't know anything about computers, but that he once had a student who did.1 By that time, of course, everyone knew who Alan Turing was.
The lambda calculus developed by Alonzo Church in the early 1930s provided a means for Church to prove that that there is no general decision procedure for first-order predicate logic. Alan Turing learned of this proof prior to the publication of his own paper on computable numbers and the Entscheidungsproblem. He was then obliged to add an appendix to his paper that described how his approach and Church's approach were basically equivalent. That appendix is the subject of this chapter.
If the concepts behind the lambda calculus seem familiar, it is because they have been quite influential in the development of programming languages. Fairly early it was noticed that a structural relationship existed between the lambda calculus and programming languages classified as procedural or imperative, such as the early programming language ALGOL,2 from which languages such ...