Lambda Calculus
The lambda calculus is a minimal formal system of functions that is equivalent in power to the Turing machine.
A calculus of functions
The lambda calculus, invented by Alonzo Church in the 1930s, models computation entirely through function definition and application. There are no numbers, loops, or data types built in; everything is expressed as functions of functions. Despite this austerity, it can compute anything a Turing machine can.
The three constructs
- Variables: x, y, z
- Abstraction: (lambda x. e) defines an anonymous function of x with body e
- Application: (f a) applies function f to argument a
Beta reduction
Computation happens by beta reduction: applying a function substitutes the argument for the bound variable in the body. For example (lambda x. x x) applied to y reduces to (y y). Repeated reduction is the entire mechanism of evaluation; a term that reduces no further is in normal form.
Encoding everything
Numbers, booleans, pairs, and recursion are all encoded as pure functions. Church numerals represent the number n as a function that applies its argument n times. The Y combinator achieves recursion without any named self-reference, showing that even repetition emerges from function application alone.
Equivalence to Turing machines
Church and Turing proved their models compute exactly the same functions, which is the foundation of the Church-Turing thesis. The lambda calculus takes the functional view of computation; the Turing machine takes the mechanical, tape-based view. Their equivalence is a deep unifying result.
Influence on programming
The lambda calculus is the theoretical root of functional programming. Lisp, Haskell, ML, and the lambda expressions now in most mainstream languages descend from it. Type theory, which underpins modern language design and proof assistants, grew from typed variants of the lambda calculus.