The Hidden Origins of Lisp: Alonzo Church
Alonzo Church: Creator of the λ‑calculus and articulator of the Church–Turing thesis.
This is one of a series of posts tracing the origins of Lisp through four brief biographical vignettes of individuals whose contributions to mathematics ultimately supported the creation of Lisp:
- Introduction
- Giuseppe Peano
- Bertrand Russell
- Alonzo Church
- John McCarthy
- The Place of Lisp in the 21st Century
The material presented in these posts has been taken from early drafts of the new preface for the LFE edition of Structure and Interpretation of Computer Programs (book, source) and shared here for the purpose of community feedback and review – as well as to expose Lisp's pre-history to a wider audience!
If you find any issues or have questions, concerns, etc., about this preface material, you may share these via the ticket which has been dedicated to tracking feedback.
The Hidden Origins of Lisp: Alonzo Church
Alonzo Church was born in Washington, D.C. in 1903.1 His great-grandfather (originally from Vermont) was not only a professor of mathematics and astronomy at the University of Georgia, but later became its president.2 Church graduated from a Connecticut prep-school in 1920 and then enrolled in Princeton to study mathematics. He published his first paper as an undergraduate and then continued at Princeton, earning his Ph.D. in just three years.
While a graduate student, Church was hit by a trolley car and spent time in a hospital where he met Julia Kuczinski3 – they were married a year later and remained inseparable until her death, 51 years later. Church had a reputation for being a bit quirky: he never drove a car or typed; he was extremely neat and fastidious; he walked everywhere and often hummed to himself while he did so; he loved reading science fiction magazines;4 a nightowl, he often did his best work late at night. Though he had solitary work habits, his list of Ph.D. students is impressive, including the likes of Turing, Kleene, and Rosser.
Perhaps one of Church's more defining characteristics was his drive: he deliberately focused on prominent problems in mathematics and attacked them with great force of will. A few of the problems he had focused on in the early 1930s were:
- Known paradoxes entailed by Bertrand Russell's theory of types 5
- David Hilbert's Entschiedungsproblem, and
- The implications of Gödel's completeness theorem.
These were some of the most compelling challenges in mathematics at that time. All of them ended up meeting at the cross-roads of the λ‑calculus.
Church had started working on the λ‑calculus when attempting to address the Russell Paradox 6. However, it was not that goal toward which the λ‑calculus was ultimately applied. Instead, it became useful – essential, even – in his efforts to define what he called "calculability" and what is now more commonly referred to as computability.7 In this the λ‑calculus was an unparalleled success, allowing Church to solve the Entschiedungsproblem using the concept of recursive functions.
Syntactically, Church's λ‑-notation made a significant improvement upon that found in the Principia Mathematica 8. Given the Principia phrase and the λ‑calculus equivalent, , one benefits from the use of the latter by virtue of the fact that it unambiguously states that the variable is bound by the term-forming operator . This innovation was necessary for Church's work and was a powerful tool put to use by John McCarthy when he built the first programming language which used the λ‑calculus: Lisp.
-
The majority of the material for this section has been adapted from the Introduction to the Collected Works of Alonzo Church, MIT Press (not yet published). ↩
-
This was when the University of Georgia was still called Franklin College. ↩
-
She was there in training to become a nurse. ↩
-
He would also write letters to the editors when the science fiction writers got their science wrong. ↩
-
These complications were known and discussed by Russell himself at the time of Principia's publication. ↩
-
See Russell's paradox. ↩
-
"Computability" was the term which Turing used. ↩
-
See the discussion of "Propositional Functions" in the section "The Notation in Principia Mathematica": http://plato.stanford.edu/entries/pm-notation/#4. Note that the section of the Principia Mathematica which they reference in that linked discussion on the Stanford site is at the beginning of "Section B: Theory of Apparent Variables" in the Principia. ↩