Alonzo Church
Alonzo Church (14 June 1903 – 11 August 1995) was the Princeton logician who gave computing its first precise definition — and then proved, with it, that mathematics itself has limits no machine can cross. He invented the Lambda calculus, answered Hilbert's Entscheidungsproblem before Turing's machines were ink, founded the Journal of Symbolic Logic, and supervised a generation of doctoral students that reads like a hall of fame of computing. He did all of it at a blackboard, one hand writing, the other erasing, in a voice so steady his students measured the centuries by it.
Early life
Church was born in Washington, D.C., in 1903 — named for his great-grandfather, a professor of mathematics and astronomy who had become president of the University of Georgia. His father was a municipal court judge, and something of the law's precision seems to have lodged in the son: colleagues would spend a lifetime remarking on a mind that moved slowly, exactly, and never twice over the same ground.
He entered Princeton in 1920, took his degree in mathematics in 1924, and stayed for a doctorate under Oswald Veblen — the geometer who was then building Princeton into a mathematical power. The 1927 dissertation concerned the foundations of set theory; the real education was Princeton itself, which was assembling — in Veblen, von Neumann shortly after, and the Institute for Advanced Study to come — the capital of twentieth-century mathematics.
A fellowship took him to Harvard, then to Europe in 1928–29: Göttingen, still the Rome of mathematics under Hilbert, and Amsterdam, where L.E.J. Brouwer's intuitionism was challenging logic's foundations. Church came home to a Princeton assistant professorship in 1929 — a chair he would hold for thirty-eight years.
In 1925 he had married Mary Julia Kuczinski; they raised three children and stayed married for the rest of his life — a domestic fact that mattered, because Church's working habits were monastic and Mary Julia ran everything else.
The impossible system — and the λ that survived it
Church's ambition in the early 1930s was the largest one logic offered: a complete formal foundation for all of mathematics, built not on sets but on functions. His "set of postulates" papers (1932–33) erected a grand system whose atoms were unnamed functions written in a new notation — λx.M, "the function that takes x and yields M."
In 1935 the grand system collapsed: his own graduate students, Stephen Kleene and J. Barkley Rosser, showed it inconsistent — the Kleene–Rosser paradox. Lesser ambitions would have died with the postulates. Church's did not, because carved out of the wreckage was a perfect surviving fragment: the pure calculus of λ-terms, free of the logic that had been bolted onto it. What remained was not a foundation for mathematics.
It was a foundation for computation — though nobody yet had that word for it. The full story of the calculus itself is told on its own page.
1936 — the year everything answered at once
A single Princeton year produced three of the century's foundational results:
- April 1936 — "An Unsolvable Problem of Elementary Number Theory." Church defined "effectively calculable" as λ-definable, exhibited a problem no such function could solve, and thereby proved Hilbert's Entscheidungsproblem unsolvable: there is no mechanical procedure that decides every mathematical question. It was the first great impossibility theorem of the computer age — Church's theorem — and it appeared months before Turing's machines.
- 1936 — with Rosser, "Some Properties of Conversion" — the Church–Rosser theorem: the λ-calculus is confluent. However you reduce a term, every path rejoins; computation under his rules is deterministic in outcome even when free in order. Every functional language still breathes through this theorem.
- 1936 — Church founded the Journal of Symbolic Logic, the field's first journal, and edited it himself for over forty years — building, almost single-handedly, the institutional home formal logic had never had.
The teacher — and the students
Church's teaching was legend, and legend of a specific kind. He lectured in a flat, careful monotone, filling the blackboard in dense, immaculate script — writing with one hand while erasing with the other — so that by the end of the hour the board held exactly one hour of completed logic and nothing else. Students described the experience variously as soporific and sublime; several took the same course twice to catch what the monotone concealed.
What the board produced was better measured in people than in theorems:
- Stephen Kleene (1934) — founded recursion theory as a discipline; regular expressions and the
*of every regex engine are his. - J. Barkley Rosser (1934) — co-author of the paradox and of Church–Rosser; the Rosser trick repaired Gödel's own proof.
- Alan Turing (1938) — sailed to Princeton after proving his machines equivalent to Church's λ; wrote his doctorate on ordinal logics under the man whose formalism his own had just vindicated. Temperamental opposites — Turing rough and improvising, Church formal to the cufflink — they gave each other the century's deepest idea in duplicate.
- Leon Henkin (1947) — the completeness proofs; the Henkin construction logic students still learn.
- Martin Davis (1950) — a third of the solution to Hilbert's Tenth Problem; Computability and Unsolvability taught the subject to generations.
- Hartley Rogers (1952) — wrote the recursion-theory textbook.
- Michael Rabin (1957) and Dana Scott (1958) — nondeterministic automata; joint Turing Award, 1976.
- Raymond Smullyan (1959) — logician, magician, and the most beloved puzzle-writer the field ever produced.
- Peter Andrews (1965) — carried Church's typed logic into the Q0 system and its provers.
The war, and the book that waited
During the war years Church did what Princeton mathematicians did — classified and applied work for the war effort — and then returned to logic, to the JSL desk, and to a second major creation: in 1940 he had published the simply typed λ-calculus, his untyped system fitted with a type discipline. It could no longer express the self-eating Ω — a limitation that turned out to be a foundation. Typed λ-calculi are the grammar of nearly every modern type system, and of the proof assistants that now verify mathematics itself.
In 1956 came Introduction to Mathematical Logic, Volume I — five hundred pages of the most careful logic textbook ever written, with footnotes of legendary density and a bibliography maintained like a state archive. Volume II was announced, awaited, anticipated — and never written, becoming a running half-century joke in a field that adored its author enough to wait for him.
The man
Colleagues preserved the small facts because the large ones seemed impossible in a person so ordinary:
- The files. Church kept an indexed card file of everything — correspondence, references, reviews — and could produce any letter on demand. The JSL's bibliography was, for decades, essentially his private system.
- The lectures at eight in the morning, monotone, perfect, unforgettable-in-hindsight.
- The ice cream. He was a large, unhurried man with a devotion to ice cream that his obituaries felt honor-bound to record; students remembered the cones — plural.
- The pulp science fiction. The most rigorous mind in logic kept a large collection of SF magazines and read them with the same completeness he brought to Frege.
- The monotone that concealed the kindness — former students, writing his memorials, kept reaching for the same discovery: behind the formalism was a shy, gentle, unfailingly generous man who answered every serious letter seriously.
UCLA — the long second act
Princeton retired him in 1967 — mandatory retirement, sixty-four years old, still writing. UCLA hired him that year into a joint chair of mathematics and philosophy, and he taught there for twenty-three more years, running a logic seminar past his eightieth birthday and retiring a second time only in 1990.
His late work returned to the problem of meaning itself — the intensional logic of sense and denotation, a decades-long project refining Frege's semantics into a formal calculus — and to Church's problem (1957): whether a desired input–output behavior can automatically be synthesized into a circuit. Büchi and Landweber solved it in 1969; its descendants are the program-synthesis tools of today. Even his open problems had grandchildren.
Recognition and the last years
Elected to the National Academy of Sciences in 1978; honored across mathematics and philosophy; the steady, late-arriving recognition that the man who defined computability had also built its institutions. He left UCLA in 1990, moved to Ohio to be near his son, and died in Hudson on 11 August 1995, at ninety-two — six months after his paper's sixty-year-old subject had become, via the Web, the busiest concept on Earth.
Legacy
- The Lambda calculus — the field's other great formalism, and the skeleton under every functional language.
- The Church-Turing thesis — the load-bearing axiom of computing: "computable" means λ-definable / Turing-computable.
- Church's theorem and Church–Rosser — impossibility and confluence, the twin pillars.
- The JSL — forty-three years of his editorship; the journal that gave logic a home.
- The students — ten doctorates that became a century of the field.
- And, in every editor, every language, every
lambdaand=>— the notation itself, chosen, he said, because it was easy and distinctive.