Textbook of AI

1903–1995, Mathematician, logician

Also known as: A. Church

Alonzo Church was an American mathematical logician whose lambda calculus, introduced in the early 1930s, is the second great model of computation alongside Alan Turing's machine. Church's 1936 paper An Unsolvable Problem of Elementary Number Theory proved the undecidability of first-order logic, answering Hilbert's Entscheidungsproblem, months before Turing's independent proof using a different formalism. The two formalisms were quickly shown to be equivalent in power; the Church–Turing thesis is the (unprovable) claim that they capture exactly what is meant by an "effectively computable" function.

The lambda calculus is a minimalist formal system for defining and applying anonymous functions. From the three primitives of variables, abstraction (λx. M) and application (M N), one can build all of computable mathematics. Lambda calculus is the direct ancestor of every functional programming language, LISP, Scheme, ML, Haskell, OCaml, Clojure, and of the type theories that underlie modern proof assistants such as Coq and Lean.

Church spent most of his career at Princeton (1929–1967) and later at UCLA. His doctoral students included Alan Turing (whose 1938 PhD Church supervised), Stephen Kleene, J. Barkley Rosser, Dana Scott, Hartley Rogers Jr., Michael Rabin, John Kemeny and Raymond Smullyan, a notable lineage that shaped twentieth-century logic and the theory of computation. He founded the Journal of Symbolic Logic in 1936 and edited it for nearly four decades.