Definition
The lambda calculus is a formal system devised by Alonzo Church in the 1930s for studying computation. Its entire syntax: variables x, abstractions λx.M (a function with parameter x and body M), and applications M N (apply function M to argument N). The single reduction rule β-reduction replaces (λx.M) N with M[x := N]. Despite its minimal syntax, the lambda calculus is Turing-complete — anything computable can be expressed in it.
Why it matters
How it works
Write a lambda term using only variables, abstractions, and applications. Reduce by β-reduction (substitute argument for parameter when applying). Numbers, booleans, pairs, lists, and recursion can all be encoded purely in lambda terms (Church encodings). Evaluation strategies (call-by-value, call-by-name, lazy) differ in when to reduce; the Church-Rosser theorem guarantees that whichever order succeeds, the result is the same (in the pure untyped calculus, on terminating terms).