The lambda calculus is a formal system, introduced by Alonzo Church in the 1930s, for expressing computation in terms of functions. As the Stanford Encyclopedia of Philosophy puts it, “the lambda-calculus is, at heart, a simple notation for functions and application.” Two operations do the work: abstraction, which defines an anonymous function, and application, which feeds an argument to a function.
Computation in the lambda calculus proceeds by reduction. The central rule is beta-reduction, which substitutes an argument into the body of a function and simplifies it step by step. The handling of bound and free variables and the rules of substitution make this rewriting precise. The Church-Rosser theorem guarantees that the order of reduction does not change the final result when one exists.
Despite its minimal syntax, the lambda calculus is a universal model of computation: it can represent any computable function. Church’s account of effective calculability in terms of lambda-definability was proven equivalent to Turing’s machine model, which is why the two are paired in the Church-Turing thesis.
The lambda calculus is the direct theoretical foundation of functional programming. Its notion of functions as values, applied and composed without side effects, shaped languages from LISP onward, and typed extensions connect it to logic through the Curry-Howard correspondence.