Beta Reduction and Normal Forms
We have a language of three forms and a notion of substitution that respects binding. Now we make the
language compute. There is a single rewrite rule, β-reduction, and running a
program means applying it over and over until no rule applies. The term you are left with — if you are
left with one — is the answer, its normal form. This lesson pins down the one-step
relation, its transitive closure, what "no rule applies" means precisely, and the unsettling fact that
some terms reduce forever.
The β-rule and redexes
A β-redex ("reducible expression") is any application whose operator is an
abstraction: a term of the shape (\lambda x.\, M)\ N. It is the pattern
"a function meeting an argument," and the β-rule says how to fire it — substitute the argument for the
parameter throughout the body. The result is the redex's contractum:
(\lambda x.\, M)\ N \;\longrightarrow_\beta\; M[x := N].
Crucially, a redex may occur anywhere inside a term, not only at the top. So the one-step
relation \to_\beta is the compatible closure of the β-rule: it lets
you contract a redex sitting under an abstraction, or in the operator or operand of an application.
Formally, on top of the axiom above,
\dfrac{M \to_\beta M'}{\lambda x.\, M \to_\beta \lambda x.\, M'} \qquad
\dfrac{M \to_\beta M'}{M\ N \to_\beta M'\ N} \qquad
\dfrac{N \to_\beta N'}{M\ N \to_\beta M\ N'} .
These three congruence rules simply say "you may reduce a subterm in place." A single
\to_\beta step contracts exactly one redex; a term with
several redexes therefore has several possible next steps, and choosing between them is the subject of
the next lesson.
Multi-step reduction
Running a program is repeated single-stepping. We write \twoheadrightarrow_\beta
for the reflexive–transitive closure of \to_\beta: the
smallest relation containing \to_\beta that is reflexive
(M \twoheadrightarrow_\beta M) and transitive. Read
M \twoheadrightarrow_\beta N as "M reduces to
N in zero or more steps." Its symmetric closure gives
β-equivalence =_\beta, the equational theory in which two
terms are considered "the same computation."
-
A term is a redex iff it has the form (\lambda x.\, M)\ N.
-
A term is in β-normal form iff it contains no redex as a subterm — there
is nowhere left to apply the β-rule.
-
M has a normal form iff
M \twoheadrightarrow_\beta N for some normal N;
such an M is called weakly normalising. If
every reduction path terminates, M is
strongly normalising.
Be careful: "no redex" means no redex anywhere in the tree, not merely at the root. The term
\lambda x.\, (\lambda y.\, y)\ x is not normal — it hides the redex
(\lambda y.\, y)\ x under the outer \lambda x.
Contract it and you reach the genuinely normal \lambda x.\, x.
A reduction graph
Because a term can have several redexes, its reductions form a graph, not a line:
nodes are terms, edges are single \to_\beta steps. Take
(\lambda x.\, x)\big((\lambda y.\, y)\ z\big), which has two redexes — an
outer one and an inner one. Whichever we fire first, the paths reconverge:
Both routes land on the normal form z. This little diamond is not an
accident — it is a shadow of the Church–Rosser property we prove two lessons from now,
which guarantees the paths always reconverge and hence that the normal form is
unique. For now, absorb the picture: reduction branches, but for this term it heals.
Some terms never stop: Ω
Not every term is normalising. Define the self-application
\omega = \lambda x.\, x\ x and apply it to itself:
\Omega \;=\; (\lambda x.\, x\ x)\,(\lambda x.\, x\ x)
\;\longrightarrow_\beta\; (\lambda x.\, x\ x)\,(\lambda x.\, x\ x) \;=\; \Omega .
Substituting x := \omega into the body x\ x gives
\omega\,\omega = \Omega right back. The single redex reproduces itself:
\Omega reduces only to \Omega, forever. It has
no normal form — the lambda-calculus analogue of an infinite loop, and the reason a
general "does this program halt?" question is undecidable here just as on a Turing machine.
There exist terms with no β-normal form; \Omega = (\lambda x.\, x\ x)(\lambda x.\, x\ x)
is one, since its only reduct is \Omega itself. Consequently the property
"M has a normal form" is undecidable in general.
A β-reducer you can run
Below is a normal-order reducer: step finds and contracts the leftmost-outermost redex
(returning null when none remains — i.e. the term is normal), and normalize
iterates step under a fuel budget so a non-terminating term like
\Omega stops instead of hanging. Watch the diamond term collapse to
z, and \Omega exhaust its fuel.
type Term =
| { tag: "var"; name: string }
| { tag: "abs"; param: string; body: Term }
| { tag: "app"; fn: Term; arg: Term };
const v = (name: string): Term => ({ tag: "var", name });
const lam = (param: string, body: Term): Term => ({ tag: "abs", param, body });
const app = (fn: Term, arg: Term): Term => ({ tag: "app", fn, arg });
function freeVars(t: Term): Set<string> {
switch (t.tag) {
case "var": return new Set([t.name]);
case "app": return new Set([...freeVars(t.fn), ...freeVars(t.arg)]);
case "abs": { const s = freeVars(t.body); s.delete(t.param); return s; }
}
}
function fresh(base: string, avoid: Set<string>): string {
let n = base; while (avoid.has(n)) n += "'"; return n;
}
function subst(M: Term, x: string, N: Term): Term {
switch (M.tag) {
case "var": return M.name === x ? N : M;
case "app": return app(subst(M.fn, x, N), subst(M.arg, x, N));
case "abs": {
if (M.param === x) return M;
if (!freeVars(N).has(M.param)) return lam(M.param, subst(M.body, x, N));
const y2 = fresh(M.param, new Set([...freeVars(N), ...freeVars(M.body), x]));
return lam(y2, subst(subst(M.body, M.param, v(y2)), x, N));
}
}
}
// One leftmost-outermost β-step, or null if the term is in normal form.
function step(t: Term): Term | null {
if (t.tag === "app") {
if (t.fn.tag === "abs") return subst(t.fn.body, t.fn.param, t.arg); // top redex
const f = step(t.fn); if (f) return app(f, t.arg); // then operator
const a = step(t.arg); if (a) return app(t.fn, a); // then operand
return null;
}
if (t.tag === "abs") { const b = step(t.body); return b ? lam(t.param, b) : null; }
return null; // a variable is normal
}
function show(t: Term): string {
switch (t.tag) {
case "var": return t.name;
case "abs": return `λ${t.param}. ${show(t.body)}`;
case "app": {
const f = t.fn.tag === "abs" ? `(${show(t.fn)})` : show(t.fn);
const a = t.arg.tag === "var" ? show(t.arg) : `(${show(t.arg)})`;
return `${f} ${a}`;
}
}
}
function normalize(t: Term, fuel = 100): { term: Term; steps: number; normal: boolean } {
let cur = t, steps = 0;
for (; steps < fuel; steps++) {
const nx = step(cur);
if (nx === null) return { term: cur, steps, normal: true };
cur = nx;
}
return { term: cur, steps, normal: false };
}
// Diamond term: (λx. x) ((λy. y) z)
const diamond = app(lam("x", v("x")), app(lam("y", v("y")), v("z")));
const r1 = normalize(diamond);
console.log("diamond →", show(r1.term), `in ${r1.steps} steps, normal=${r1.normal}`);
// Ω = (λx. x x)(λx. x x) — reduces to itself forever.
const omega = lam("x", app(v("x"), v("x")));
const OMEGA = app(omega, omega);
const r2 = normalize(OMEGA, 20);
console.log("Ω after 20 steps →", show(r2.term), `normal=${r2.normal}`);
The diamond reaches z in two steps; \Omega burns all 20 units
of fuel and reports normal=false — our finite stand-in for "diverges." Every real
evaluator carries the same tension: it must reduce as far as needed while accepting that "as far as
needed" is, in general, forever.
Emphatically no — β-reduction can make a term grow, sometimes explosively. The culprit is that
substitution copies the argument once per free occurrence of the parameter. Contract
(\lambda x.\, x\ x\ x)\ N and you get N\ N\ N —
three copies of N. Chain such duplicators and the term size can blow up
super-exponentially before (if ever) it shrinks to a normal form. This is exactly why
\Omega can stay the same size forever while looping, and why terms exist
that do normalise but only after ballooning to astronomical size first. "Reduction" is a
misnomer inherited from arithmetic; think "rewriting," which may enlarge as easily as shrink.
Two traps. First, a term is normal only when it has no redex anywhere, including under
\lambdas. \lambda x.\, (\lambda y.\, y)\, x
looks finished but is not — there is a redex in its body. Real language implementations often
stop earlier, at weak head normal form (no redex at the head, but redexes may
remain under binders), because they never evaluate inside an unapplied function. Do not conflate the
two: "the mathematical normal form" and "what my interpreter prints" can differ.
Second, having a normal form is a property of the term, not of a particular path. A term can
have a terminating path and a non-terminating one — for example
(\lambda x.\, y)\,\Omega, which is y if you
contract the outer redex first, but loops forever if you insist on reducing
\Omega inside. Weakly normalising does not imply strongly normalising. Which
strategy guarantees you find the normal form is the cliff-hanger for the next lesson.