April 1936
Church defines effective calculability with lambda calculus
Alonzo Church's April 1936 paper in the American Journal of Mathematics used lambda calculusA formal system of functions and application — Church's 1930s model of computation alongside Turing machines. to prove the EntscheidungsproblemHilbert's decision problem — whether every mathematical statement can be proved or disproved algorithmically. unsolvable — the same year TuringAlan Turing — mathematician who defined computability, broke Enigma, and posed the imitation game. published his machine model.
What it was for
Church's lambda calculusA formal system of functions and application — Church's 1930s model of computation alongside Turing machines. became the theoretical basis for Lisp, functional programmingA style emphasizing functions and immutable data over step-by-step state changes — influences Haskell, Lisp, and modern languages., and type theory. Together with TuringAlan Turing — mathematician who defined computability, broke Enigma, and posed the imitation game.'s 1936 work, it established the Church–TuringAlan Turing — mathematician who defined computability, broke Enigma, and posed the imitation game. thesis: anything effectively computable can be computed by these equivalent models.
People
- Alonzo Church — researcher
Why it's here
lambda calculusA formal system of functions and application — Church's 1930s model of computation alongside Turing machines. is one of two independent 1936 definitions of computation.
Why it mattered
It linked logic to programming language design decades before computers were widespread.
What it solved
HilbertDavid Hilbert — posed foundational questions for mathematics, including the Entscheidungsproblem.'s EntscheidungsproblemHilbert's decision problem — whether every mathematical statement can be proved or disproved algorithmically. asked for a general procedure to decide mathematical truth — Church proved no such procedure exists.