Lambda Calculus Reducer

Lambda calculus is the universal model of computation: variables, abstraction (λx.e), and application (f x). β-reduction substitutes arguments: (λx.e) v → e[x:=v]. Every computable function has a lambda encoding — Church numerals, booleans, pairs, and even recursion via the Y combinator.

Reduction order: Max steps:
Identity K combinator Y combinator (diverges) succ(2) = 3 add(2,3) mul(2,3) = 6? if true then a else b Ω (diverges) Y combinator
Enter an expression and click Reduce
Church numerals: 0 = λf.λx.x | 1 = λf.λx.f x | 2 = λf.λx.f(f x) | n = λf.λx.fⁿx
Booleans: true = λt.λf.t | false = λt.λf.f | and = λp.λq.p q p
Syntax: use \x.e or λx.e | application is left-associative | parentheses for grouping