Structure and Interpretation of Computer Programs

Alonzo Church

Figure P.3: Alonzo Church, 1943.

Alonzo Church was born in Washington, D.C. in 1903.¹ 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.² 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 Kuczinski³ -- 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;⁴ 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:

1. Known paradoxes entailed by Bertrand Russell's theory of types ⁵
2. David Hilbert's Entscheidungsproblem, and
3. 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 ⁶. 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.⁷ In this the λ‑calculus was an unparalleled success, allowing Church to solve the Entscheidungsproblem using the concept of recursive functions.

Syntactically, Church's λ‑notation made a significant improvement upon that found in the Principia Mathematica ⁸. Given the Principia phrase $$\phi x̂$$ and the λ‑calculus equivalent, $$\lambda x \phi x$$, one benefits from the use of the latter by virtue of the fact that it unambiguously states that the variable $$x$$ is bound by the term-forming operator $$\lambda$$. This innovation was necessary for Church's work and a powerful tool that was put to use by John McCarthy when he built the first programming language which used the λ‑calculus: Lisp.