Lambda Calculus

Step through beta-reduction — Church numerals, combinators, Y combinator

Reference:   0 = λf.λx.x  |  1 = λf.λx.f x  |  2 = λf.λx.f(f x)  |  SUCC = λn.λf.λx.f(n f x)  |  TRUE = λt.λf.t  |  FALSE = λt.λf.f

Beta reduction substitutes the argument for the bound variable: (λx.M) N → M[x:=N]. Church numerals encode natural numbers as higher-order functions; the Y combinator enables recursion without self-reference.

Lambda calculus is the mathematical foundation of functional programming. Every computable function can be expressed as nested abstractions and applications; Church numerals prove that integers themselves are just functions.