What is the Lambda Calculus?
In 1936, Alonzo Church wanted to answer a deceptively simple question: what does it mean to compute something? Before computers existed, he needed a precise mathematical language for describing computation itself.
He discovered something remarkable. You only need three constructs — variables, functions, and function application. Everything else — numbers, booleans, data structures, loops, recursion — can be built from these three building blocks.
Around the same time, Alan Turing invented his Turing machine. The two models look nothing alike, yet Church and Turing proved they are equivalent. Anything a Turing machine can compute, the lambda calculus can compute — and vice versa. This equivalence is the Church-Turing thesis.
The lambda calculus is the foundation of functional programming — Haskell, ML, Lisp, and countless modern languages are built on its ideas. Understanding it gives you a window into the deep structure of computation.
This essay is interactive. Each section has live steppers, sliders, and evaluators. Use the sidebar to navigate. When you reach the Playground, you can type any lambda expression and watch it reduce step by step.
Three Constructs
The entire syntax of the lambda calculus fits in three lines. There is nothing else.
| λx. e
| e₁ e₂
Variables like x, y, f are just names. They stand for something — we'll substitute in values during reduction.
Abstraction creates a function. λx. e means "a function that takes x and returns e." The λ (lambda) marks the start of the function; the variable after it is the parameter; everything after the dot is the body.
λx. λy. x — constant (ignores y)
λf. λx. f x — apply f once
Application calls a function. f x means "apply f to x." Application is left-associative: f x y means (f x) y, not f (x y).
One important restriction: functions take exactly one argument. To handle multiple arguments, we return a function. This technique is called currying, after mathematician Haskell Curry.
— takes x, returns (λy. x + y)
— apply that to y to get x + y
A variable can be bound (it's the parameter of an enclosing λ) or free (it refers to something outside). In λx. x y, x is bound and y is free.
The One Rule
Computation in the lambda calculus happens through a single rule called β-reduction. When you apply an abstraction to an argument, substitute the argument for the parameter everywhere in the body.
A redex (reducible expression) is any subterm of the form (λx. e) v. Reducing it means performing the substitution. We keep reducing until no redexes remain — that's normal form.
Step through two examples:
Two other rules exist. α-conversion says you can rename bound variables freely — λx. x and λy. y are the same function. η-reduction says λx. f x simplifies to f when x doesn't appear free in f.
Numbers from Nothing
We have no numbers — no built-in 0 or 1. Can we represent them anyway? Church's insight was brilliant: a number is how many times you apply a function.
Zero means "apply f zero times to x." One means "apply f once." Two means apply it twice. Every natural number becomes a pattern of applications.
1 = λf. λx. f x
2 = λf. λx. f (f x)
3 = λf. λx. f (f (f x))
n = λf. λx. fⁿ x
Use the slider to explore. Each teal tile represents one application of f; the gold tile is x.
Arithmetic follows naturally. The successor of n wraps one more f around the result. Addition chains the applications of two numerals. Multiplication nests one numeral inside another.
ADD = λm. λn. λf. λx. m f (n f x)
MUL = λm. λn. λf. m (n f)
True, False, and Choice
Booleans in the lambda calculus are functions that make a choice. TRUE picks its first argument; FALSE picks its second. A boolean is a selector.
FALSE = λt. λf. f
This makes if-then-else trivially simple. IF b t f just applies b to the two branches — b selects which one to return.
AND = λp. λq. p q FALSE
OR = λp. λq. p TRUE q
NOT = λp. p FALSE TRUE
Toggle the inputs below to see each operation live:
The Building Blocks
A combinator is a lambda expression with no free variables — completely self-contained. Several fundamental combinators appear again and again. Click any card to explore it.
This is SKI combinatory logic — a system where every lambda term can be translated into combinations of just S, K, and I (though I itself is derivable from S and K: S K K = I). It's Turing-complete with no variables at all.
Recursion from Nothing
Here's a puzzle. In the lambda calculus, functions are anonymous. You can't write fact n = n * fact(n-1) because the function has no name to call itself with.
Church solved this with one of the most mind-bending constructs in mathematics: the Y combinator. It computes the fixed point of any function.
With Y, we can define factorial. We write a helper that takes a "recursive call" as a parameter. Y hands that helper itself as an argument — creating the loop.
FACT = Y STEP
FACT THREE → Y STEP THREE → STEP (Y STEP) THREE → ...
Explore the Y combinator computing factorial for small n:
Live Lambda Evaluator ⚡
Type any lambda expression below. Use \x. body for lambda (backslash). Named constants like TRUE, FALSE, AND, OR, NOT, SUCC, ADD, MUL, ONE, TWO, THREE, K, S, I, B, C, W are pre-defined. Press Enter or click REDUCE.
Named constants are expanded lazily. Diverging terms (Ω, Y applied directly) hit the step limit.