Alonzo Church and Lambda Calculus

The Princeton Logician

Alonzo Church was born in Washington, D.C., on June 14, 1903, the son of a judge. He showed early mathematical gifts and enrolled at Princeton, where he studied under Oswald Veblen and earned his doctorate in 1927 with a thesis titled “Alternatives to Zermelo’s Assumption,” exploring set theories in which the axiom of choice is false. He then spent two years as a National Research Fellow, a period that took him to Harvard, Göttingen, and Amsterdam, where the atmosphere of Hilbert’s program and the emerging crisis in foundations left a permanent mark. By 1929, he was back at Princeton as a faculty member; he stayed on its mathematics faculty until 1967, when he moved to UCLA.

Church was an unusual personality. Haskell Curry, reviewing his textbook, praised the “meticulous precision which characterizes the author’s work generally.” He wrote precisely and revised obsessively. His lectures were dense and formal, rewarding for students who followed every step and hard going for those who wanted intuition first. Behind the reserve he was generous with his 31 doctoral students, who included Alan Turing, Stephen Kleene, Barkley Rosser, Michael Rabin, and Dana Scott.

Princeton in the 1930s was one of the world’s great intellectual environments. The newly founded Institute for Advanced Study brought Einstein, von Neumann, and shortly thereafter Gödel to within walking distance of Church’s office. The question animating everyone in mathematical logic was Hilbert’s: Could mathematics be fully formalized? If so, could every mathematical truth be decided by a mechanical procedure? Church set out to answer it.

Inventing Lambda Calculus

Church’s approach was not to build a machine but to build a notation. Starting in 1932, he developed what he called lambda calculus, a formal system in which every mathematical object was a function, and every operation was function application.

The idea was simple: computation is the successive application of functions to arguments, and any computable process can be expressed this way. Church introduced the Greek letter lambda (λ) to denote function definition. The expression λx. x denotes the identity function, the function that takes an input x and returns it unchanged. The expression λx. λy. x denotes the function that takes two arguments and returns the first, ignoring the second. By encoding natural numbers as functions, booleans as functions, and recursion as a special self-referential construction, Church showed that lambda calculus could express any computation that could be described precisely.

The system had no built-in data types, no numbers, no loops, no conditionals, only functions and application. That so little could express universal computation was not obvious. To show it, Church had to encode arithmetic, logical connectives, and recursive definitions entirely as lambda terms, the same encodings that functional programmers later studied as the basis of their field.

The Kleene-Rosser Crisis

Church’s original ambition for lambda calculus was foundational: he hoped it could serve as a complete formal basis for all of mathematics, replacing or supplementing the set-theoretic foundations that Russell and Whitehead had attempted in Principia Mathematica. If successful, this would have realized a version of Hilbert’s program.

The dream collapsed in 1935, when two of Church’s own doctoral students (Stephen Kleene and Barkley Rosser) proved that Church’s original system of logic, built on the untyped lambda calculus, was inconsistent. In any inconsistent system, every statement is provable, which means the system proves nothing meaningful. The Kleene-Rosser paradox showed that Church’s logical ambitions exceeded what the system could support.

Kleene and Rosser had sunk their advisor’s foundational program, and both stayed with the computational side of the work. Kleene developed the theory of recursive functions and, later, regular expressions. Rosser proved results about lambda calculus reduction, among them the Church-Rosser theorem with Church in 1936.

Proving the Undecidable

Despite the foundational crisis, Church pressed forward with the computational questions that had motivated his work from the beginning. By 1936, he had proved the central negative result: there is no algorithm that can decide, for an arbitrary statement in first-order predicate logic, whether that statement is provable. Hilbert’s Entscheidungsproblem had no solution.

Church’s proof was subtle. He first defined “effectively computable” to mean “expressible in lambda calculus”, a definition that later became half of the Church-Turing Thesis. He then showed that the question of whether two lambda expressions are equivalent under reduction (the conversion problem) was undecidable. Finally, he showed that the Entscheidungsproblem could be reduced to the conversion problem: a solution to the decision problem would yield a solution to conversion. Since conversion was undecidable, so was the Entscheidungsproblem.

The undecidability result, “An Unsolvable Problem of Elementary Number Theory,” appeared in April 1936 in the American Journal of Mathematics; a short follow-up, “A Note on the Entscheidungsproblem,” in the first volume of the new Journal of Symbolic Logic, applied it to Hilbert’s problem. In May 1936, Alan Turing submitted his paper “On Computable Numbers, with an Application to the Entscheidungsproblem” to the Proceedings of the London Mathematical Society, arriving at the same conclusion through the device of abstract computing machines and the halting problem. The two papers, from different directions, converged on the same frontier: the boundary of what mechanical computation could and could not do.

Turing at Princeton

In September 1936, Alan Turing arrived at Princeton to study under Church. The relationship was, on the surface, an odd pairing. Church worked in formal logic, building formal systems with the care of a watchmaker. Turing thought more intuitively and more physically; his machines were concrete devices with tapes and read-write heads, not notational formalisms. The two men respected each other, and Turing’s two years at Princeton shaped his later work.

Through exchanges with each other and with Kleene, Church and Turing came to understand that their approaches were equivalent. Lambda calculus and Turing machines computed the same class of functions. From this came what Church stated in 1936 and Turing elaborated in 1937: the thesis that any function computable by an effective procedure is computable by a Turing machine (equivalently, expressible in lambda calculus). The Church-Turing Thesis is not a theorem, because “effective procedure” is an intuitive concept, not a formal one. In more than eighty years, no formalization of computation has ever exceeded the boundary it draws.

Turing received his Princeton PhD under Church in 1938, with a thesis on ordinal logics, systems that could transcend Gödelian incompleteness by adding stronger axioms, at the cost of losing full formalization. For more on Turing’s later career, see Alan Turing and the Enigma.

Lambda Calculus and the Birth of Functional Programming

For two decades after 1936, lambda calculus was primarily a tool of mathematical logicians, not computer scientists. The shift came with John McCarthy. In the late 1950s, McCarthy was working on artificial intelligence at MIT and needed a programming language that could handle symbolic computation, the manipulation of expressions and rules as well as numbers. Drawing on his background in mathematical logic, he designed LISP (List Processing) and borrowed Church’s lambda notation to write functions. By his own account he took little else: “I didn’t understand the rest of his book, so I wasn’t tempted to try to implement his more general mechanism for defining functions.”

LISP treated functions as first-class values: functions could be passed as arguments, returned as results, and stored in data structures. It supported recursive definitions by default. McCarthy kept the keyword lambda in LISP’s syntax for anonymous function definition, a usage that persists in Python, Ruby, and many other modern languages. For the full story of McCarthy and LISP, see John McCarthy and LISP.

The influence broadened as programming language theory matured. Robin Milner’s ML language (1973), Haskell (1990), and a proliferating family of typed functional languages built on typed lambda calculi: ML on the Hindley-Milner type system, a restricted form of polymorphic lambda calculus, and Haskell’s main compiler GHC on an internal language derived from System F, the polymorphic lambda calculus developed independently by Jean-Yves Girard (1972) and John Reynolds (1974). The parametric polymorphism of Java generics and Rust traces back to the same line of work. The full story of this tradition is explored in The Rise of Functional Programming.

Simply Typed Lambda Calculus and Type Theory

Church’s answer to the Kleene-Rosser paradox, adding types to restore consistency, ended up mattering more than the untyped system. In the simply typed lambda calculus (1940), every term has a type, and functions can only be applied to arguments whose types match the expected input type. This restriction prevents self-referential paradoxes and guarantees that well-typed terms always terminate, a property called strong normalization.

The connection between type theory and logic, discovered by Haskell Curry and William Howard in the 1950s and 1960s, is now known as the Curry-Howard correspondence: types correspond to logical propositions, and programs correspond to proofs. A function from type A to type B is a proof that proposition A implies proposition B. This correspondence shaped the design of proof assistants (computer programs that check mathematical proofs) and of dependently typed programming languages like Agda and Coq, which blur the boundary between programs and mathematical proofs.

The Quiet Scholar

Church was not a public intellectual and sought neither fame nor controversy. He published carefully and slowly, preferring precision to speed. He was a founding editor of the Journal of Symbolic Logic in 1936 and ran its reviews section for 43 years, until 1979, which made him the person who decided what the central venue of mathematical logic considered worth noticing. His textbook Introduction to Mathematical Logic (1944, revised 1956) defined the subject for a generation of students.

He left Princeton in 1967 for UCLA, where he was Kent Professor of Philosophy and Professor of Mathematics until 1990. He died on August 11, 1995, in Hudson, Ohio, at the age of ninety-two, long enough to see functional programming, built on his calculus, take hold in the software industry. Most modern programming languages now have a lambda notation. In Python, lambda x: x + 1 is a direct descendant of λx. x+1. In JavaScript, x => x + 1 is the same thing under different clothing.

The notation was worked out with pencil and paper in 1932, sixteen years before a stored-program computer ran anywhere.

---

📚 Sources

• Alonzo Church: An Unsolvable Problem of Elementary Number Theory (1936), American Journal of Mathematics
• Alonzo Church: A Note on the Entscheidungsproblem (1936), Journal of Symbolic Logic
• Alonzo Church: Introduction to Mathematical Logic (1956), Princeton University Press
• Hendrik P. Barendregt: The Lambda Calculus: Its Syntax and Semantics (1984), North-Holland
• John P. Seldin & J. Roger Hindley (eds.): To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism (1980), Academic Press
• Paul Hudak et al.: A History of Haskell: Being Lazy with Class (2007), HOPL III
• Felice Cardone & J. Roger Hindley: History of Lambda-calculus and Combinatory Logic (2006), in Handbook of the History of Logic, Vol. 5
• Alonzo Church — MacTutor History of Mathematics Archive
• Herbert B. Enderton: “In Memoriam: Alonzo Church, 1903–1995” (1995), Bulletin of Symbolic Logic 1(4)
• John McCarthy: “History of LISP” (1978), HOPL I, ACM
• B. Jack Copeland: “The Church-Turing Thesis” — Stanford Encyclopedia of Philosophy