Lambda calculus
Cálculo lambda
- Date
- 1932-1936 · confidence high
- Place
- Princeton, New Jersey, United States
- Credited to
- Alonzo Church
- Field
- Knowledge & symbols
What was discovered
American logician Alonzo Church introduced at Princeton, between 1932 and 1936, lambda calculus, a formal system for expressing functions and their application through abstraction and substitution, originally conceived within a broader program on the foundations of mathematical logic.
The original 1932-1933 system turned out to be logically inconsistent (the Kleene-Rosser paradox, 1935); in 1936 Church isolated and published the portion relevant to computation, now known as the untyped lambda calculus.
What it led to
- a formalization of computability, shown equivalent to the Turing machine (the Church-Turing thesis)
- the theoretical foundation of functional programming languages
- a direct influence on languages such as Lisp and Haskell