Normalization
We have seen that
type safety
keeps a well-typed program from getting stuck — but it leaves one escape hatch open: a safe
program is allowed to run forever. Remarkably, the simply-typed lambda calculus slams even
that hatch shut. In \lambda_{\to}, every well-typed term
terminates. No matter how you reduce it, in whatever order, evaluation halts in a finite
number of steps at a normal form. This is Strong Normalization, and it is the deepest
and most surprising theorem about the pure typed lambda calculus.
It is also a double-edged sword. Termination is a gift for a proof language — via
Curry–Howard
it means the logic is consistent. But it is a cage for a programming language: a calculus in
which every program halts cannot be Turing-complete. You cannot even write a
general loop. This page explains why \lambda_{\to} is so tame, what it costs
to escape (a fixed-point operator), and the beautiful idea — logical relations — needed to
prove termination at all.
Weak vs strong normalization
A term is in normal form when it contains no redex — no
(\lambda x{:}T.\,t)\,v waiting to be reduced. Two grades of termination
matter:
- Weakly normalizing (WN): some reduction sequence reaches a normal form.
There exists a way to finish.
- Strongly normalizing (SN): every reduction sequence reaches a normal form
— there is no infinite reduction path at all, whatever choices you make.
SN is far stronger: it says you cannot loop even by trying to. Combined with the
Church–Rosser (confluence) property — which
\lambda_{\to} also enjoys — SN gives every well-typed term a
unique normal form, reached by every strategy. Evaluation in
\lambda_{\to} is a total, deterministic function.
- If \Gamma \vdash t : T, then t is
strongly normalizing: there is no infinite reduction sequence
t \to t_1 \to t_2 \to \cdots.
- With confluence, t therefore has a unique normal form,
reached in finitely many steps by any reduction order.
Termination and its opposite, pictured
On the left below, a well-typed term with two redexes reduces along either path and both roads
converge to the same normal form — confluence and termination working together. On the right lurks the
term that \lambda_{\to} forbids: the self-application
\Omega, which \beta-reduces to itself
forever. The point of the type system is that \Omega can never be built.
The diamond on the left is strong normalization in miniature: from
(\lambda x.x)\big((\lambda y.y)\,z\big) you may reduce the outer or the inner
redex first, but every route lands on the normal form z in finitely many
steps. The loop on the right is
\Omega = (\lambda x.\,x\,x)(\lambda x.\,x\,x): it steps to itself endlessly.
Its non-termination hinges on the self-application x\,x — which, as we saw,
cannot be typed in \lambda_{\to} (it would need
x to be both T\to U and
T). Strip out untypable terms and every survivor terminates.
Adding a fixed point breaks everything (on purpose)
Real languages must loop, so they add a fixed-point operator
\mathsf{fix} (equivalently, recursive definitions), with the typing rule and
reduction:
\dfrac{\Gamma \vdash t : T \to T}{\Gamma \vdash \mathsf{fix}\;t : T}\;\textsf{(T-Fix)} \qquad\qquad \mathsf{fix}\;(\lambda x{:}T.\,t) \;\to\; [x \mapsto \mathsf{fix}\,(\lambda x{:}T.\,t)]\,t
This one rule is type-safe — Progress and Preservation still hold, so
\mathsf{fix} never gets stuck. But it destroys strong
normalization: \mathsf{fix}\;(\lambda x{:}T.\,x) reduces to itself
forever, giving a well-typed, non-terminating term of every type T.
With \mathsf{fix} the calculus (this is PCF) becomes
Turing-complete — you regain general recursion, and with it the halting problem, at
the price of termination. There is no free lunch: you cannot have all three of type-safety,
Turing-completeness, and guaranteed termination.
No — and this is the sharp edge of Curry–Howard. Since
\mathsf{fix}\;(\lambda x{:}T.\,x) : T for any
T, it in particular inhabits the empty type
\mathbf{0} = \bot. A term of type \bot is a
"proof of falsity" — so the logic corresponding to PCF is inconsistent: it proves
everything. That is exactly why proof assistants like Coq, Agda and Lean forbid unrestricted
\mathsf{fix} and instead demand structurally decreasing
recursion (a termination checker), so that every function provably halts and the logic stays sound.
Termination is not a nicety there — it is the very thing keeping the mathematics honest.
Why the proof is hard: logical relations
You might expect to prove SN by simple structural induction on terms: "each subterm is SN, so the whole
is SN." It fails — and the failure is instructive. The culprit is
\beta-reduction on an application
(\lambda x{:}T.\,t)\,s: it substitutes s
into t, and the result [x\mapsto s]t can be
larger and more complex than either piece. The induction hypothesis about the parts says
nothing strong enough about the whole. Knowing t and
s merely terminate does not tell you their combination does.
Tait's fix (1967), later polished by Girard, is the method of logical relations (also
called reducibility candidates). Instead of proving "SN" directly, define a stronger,
type-indexed predicate \mathcal{R}_T — "reducible at type
T" — by induction on the type, not the term:
- At a base type \iota:
t \in \mathcal{R}_\iota iff t is strongly
normalizing.
- At a function type T_1 \to T_2:
t \in \mathcal{R}_{T_1 \to T_2} iff for every
s \in \mathcal{R}_{T_1}, the application
t\,s \in \mathcal{R}_{T_2}.
The clever part is the arrow clause: reducibility at a function type is defined in terms of
reducibility at smaller types, so the definition is well-founded on the structure of the type.
One then proves two lemmas — (1) every reducible term is SN, and (2) every well-typed term is reducible
(the "fundamental lemma", by induction on the typing derivation, with substitution baked into the
statement so the application case goes through). Together: well-typed ⟹ reducible ⟹ SN. The extra
strength of "reducible" is exactly what survives substitution where "SN" alone could not. This
technique — proving a property by a type-indexed relation rather than head-on — is one of the most
reused tools in all of programming-language theory (parametricity, contextual equivalence, and program
logics all descend from it).
Seeing it terminate — and seeing the cage
Below is a normal-order \beta-reducer for lambda terms. Feed it a term
corresponding to a well-typed \lambda_{\to} program and it reaches a normal
form in a handful of steps. Feed it \Omega — the untypable self-application
— and it runs until we cap it, a stand-in for the non-termination that typing rules out.
type Term =
| { kind: "Var"; name: string }
| { kind: "Lam"; param: string; body: Term }
| { kind: "App"; fn: Term; arg: Term };
const V = (name: string): Term => ({ kind: "Var", name });
const L = (param: string, body: Term): Term => ({ kind: "Lam", param, body });
const A = (fn: Term, arg: Term): Term => ({ kind: "App", fn, arg });
const show = (t: Term): string => {
switch (t.kind) {
case "Var": return t.name;
case "Lam": return `λ${t.param}.${show(t.body)}`;
case "App": return `(${show(t.fn)} ${show(t.arg)})`;
}
};
function freeVars(t: Term): Set<string> {
switch (t.kind) {
case "Var": return new Set([t.name]);
case "Lam": { const s = freeVars(t.body); s.delete(t.param); return s; }
case "App": return new Set([...freeVars(t.fn), ...freeVars(t.arg)]);
}
}
let fresh = 0;
// Capture-avoiding substitution [x ↦ s] t.
function subst(t: Term, x: string, s: Term): Term {
switch (t.kind) {
case "Var": return t.name === x ? s : t;
case "App": return A(subst(t.fn, x, s), subst(t.arg, x, s));
case "Lam": {
if (t.param === x) return t; // x is shadowed
if (freeVars(s).has(t.param)) { // rename to avoid capture
const y = `${t.param}_${fresh++}`;
return L(y, subst(subst(t.body, t.param, V(y)), x, s));
}
return L(t.param, subst(t.body, x, s));
}
}
}
// One leftmost-outermost (normal-order) β-step, or null if in normal form.
function step1(t: Term): Term | null {
if (t.kind === "App") {
if (t.fn.kind === "Lam") return subst(t.fn.body, t.fn.param, t.arg); // β
const f = step1(t.fn); if (f) return A(f, t.arg);
const a = step1(t.arg); if (a) return A(t.fn, a);
return null;
}
if (t.kind === "Lam") { const b = step1(t.body); return b ? L(t.param, b) : null; }
return null;
}
function normalize(t: Term, cap = 100): { nf: Term; steps: number; capped: boolean } {
let cur = t, steps = 0;
while (steps < cap) {
const nx = step1(cur);
if (nx === null) return { nf: cur, steps, capped: false };
cur = nx; steps++;
}
return { nf: cur, steps, capped: true };
}
// K = λx.λy.x , I = λx.x — both well-typed in λ→.
const K = L("x", L("y", V("x")));
const I = L("x", V("x"));
const term = A(A(K, A(I, V("a"))), V("b")); // K (I a) b should normalize to a
const r = normalize(term);
console.log(`well-typed: ${show(term)} →* ${show(r.nf)} (${r.steps} steps, halted=${!r.capped})`);
// Ω = (λx. x x)(λx. x x) — UNTYPABLE in λ→, and non-terminating.
const omega = A(L("x", A(V("x"), V("x"))), L("x", A(V("x"), V("x"))));
const o = normalize(omega, 100);
console.log(`untypable Ω: still reducing after ${o.steps} steps, capped=${o.capped} (λ→ forbids this term)`);
The consequence: not Turing-complete
Strong normalization has a stark corollary. If every \lambda_{\to} program
halts, then \lambda_{\to} cannot express every computable
function — for a Turing-complete language must be able to write a non-terminating program (a
universal interpreter would necessarily loop on some inputs). Concretely, the functions on Church
numerals definable in pure \lambda_{\to} are exactly the
extended polynomials (built from +, \times and conditionals) — a
vanishingly small slice of the computable functions. There is no
\lambda_{\to} term computing, say, an unbounded search or the Ackermann
function.
This is the fundamental tension every language designer navigates. Total languages (Coq's
Gallina, Agda, dependently-typed cores) buy guaranteed termination and logical
consistency at the cost of expressiveness and force you to prove your recursions well-founded.
General-purpose languages take \mathsf{fix}, regain Turing-completeness, and
accept that the halting problem — and the occasional infinite loop — comes with the territory. Strong
normalization is the theorem that makes the trade-off precise.
"Every term halts" is a fact about WELL-TYPED terms, and it does not mean the type-checker
runs the program. Two confusions to avoid. First, strong normalization says nothing about
ill-typed or untyped terms — \Omega is a perfectly good
untyped lambda term that loops forever; it is only excluded because it fails to type. The
untyped lambda calculus is Turing-complete precisely because it admits such terms. Second, termination
of programs is a different question from decidability of type-checking: even in
Turing-complete PCF, type-checking stays decidable and fast — the checker never runs your
loop, it only builds a derivation. Do not conflate "the language always terminates" (false once you add
\mathsf{fix}) with "type-checking always terminates" (true throughout). They
are independent properties.