Confluence and the Church–Rosser Theorem
We have seen that a term can branch: several redexes, several next steps, several reduction paths.
The diamond in the beta-reduction lesson closed up neatly, but was that luck? Could two people, reducing
the same program by different valid strategies, ever reach two different answers? If so, the
lambda calculus would be a hopeless model of computation — the result would depend on the whim of the
evaluator. The Church–Rosser theorem is the profound guarantee that this never happens:
no matter how reduction branches, the branches can always be brought back together. It is the theorem
that makes "the value of a program" a well-defined notion.
Confluence, stated precisely
A rewrite relation is confluent (has the Church–Rosser property) when
any two reducts of a term can be rejoined. Writing \twoheadrightarrow for
multi-step reduction:
\text{if } M \twoheadrightarrow M_1 \text{ and } M \twoheadrightarrow M_2,
\text{ then there exists } N \text{ with } M_1 \twoheadrightarrow N \text{ and } M_2 \twoheadrightarrow N.
Picture it as a diamond: two paths diverge from the top and a common vertex at the bottom closes them.
The bottom vertex N is asserted to exist — that is the whole content
of the theorem. Step through the shape:
The solid arrows are the reductions you performed (any number of steps, any strategy). The dashed
arrows are the ones the theorem promises you can perform to reconcile them. Confluence says the
promise is always kept, for every term and every pair of divergent paths — even paths of wildly
different lengths.
The theorem and what it buys
-
Confluence. β-reduction is confluent: if
M \twoheadrightarrow_\beta M_1 and
M \twoheadrightarrow_\beta M_2, there is a term
N with M_1 \twoheadrightarrow_\beta N and
M_2 \twoheadrightarrow_\beta N.
-
Interpolation for equality. If M =_\beta N (the two are
β-equivalent) then there is a common reduct L with
M \twoheadrightarrow_\beta L and
N \twoheadrightarrow_\beta L.
Three corollaries follow immediately, and they are the reason the theorem matters so much.
-
Uniqueness of normal forms. A term has at most one normal form (up to
α-equivalence). For if M \twoheadrightarrow N_1 and
M \twoheadrightarrow N_2 with both normal, confluence gives a common
reduct — but a normal form reduces only to itself, so N_1 =_\alpha N_2.
"The answer" is well-defined.
-
Consistency of the theory. Not all terms are β-equal. If they were,
\text{TRUE} =_\beta \text{FALSE}; but these are distinct normal forms, so
by uniqueness they cannot be equal. The equational theory \lambda\beta is
therefore consistent — it does not collapse into triviality.
-
Strategy independence. Combined with the normalisation theorem, confluence means the
normal form found by normal order is the normal form — any terminating strategy that reaches
a normal form reaches the same one.
Why it is hard: the diamond that isn't
One might hope to prove confluence from a one-step diamond property: whenever
M \to M_1 and M \to M_2 in a single step, close
the square in one step each. But \to_\beta does not have this
property. Contracting a redex can duplicate another redex (recall substitution copies
its argument), so one step on the left may require several steps on the right to catch up. The
naive diamond fails.
The classical repair is the Tait–Martin-Löf method: define a
parallel reduction \Rrightarrow that contracts a whole set of
redexes at once, prove that relation has the diamond property (the duplication is absorbed
because parallel reduction can fire the copies simultaneously), and observe that
\Rrightarrow sits between \to_\beta and
\twoheadrightarrow_\beta so its transitive closure coincides with
\twoheadrightarrow_\beta. Confluence of β then follows. It is a small
masterpiece of proof engineering, and the template for confluence proofs across rewriting theory.
Confluence, checked empirically
We cannot prove Church–Rosser by running code, but we can witness its most useful
corollary: reduce one term by two different strategies and confirm the normal forms coincide. Below,
a term with several redexes is normalised by normal order and by applicative order; both
arrive at the identical result. Press Run.
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 = (p: string, b: Term): Term => ({ tag: "abs", param: p, body: b });
const app = (f: Term, a: Term): Term => ({ tag: "app", fn: f, arg: a });
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(b: string, a: Set<string>): string { let n = b; while (a.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));
}
}
}
function step(t: Term, strat: "normal" | "applicative"): Term | null {
if (t.tag === "abs") { const b = step(t.body, strat); return b ? lam(t.param, b) : null; }
if (t.tag === "app") {
if (strat === "normal" && t.fn.tag === "abs") return subst(t.fn.body, t.fn.param, t.arg);
const f = step(t.fn, strat); if (f) return app(f, t.arg);
const a = step(t.arg, strat); if (a) return app(t.fn, a);
if (strat === "applicative" && t.fn.tag === "abs") return subst(t.fn.body, t.fn.param, t.arg);
return null;
}
return null;
}
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 norm(t: Term, s: "normal" | "applicative", fuel = 200): Term {
let c = t; for (let i = 0; i < fuel; i++) { const n = step(c, s); if (!n) return c; c = n; } return c;
}
// A branchy term: (λf. λx. f (f x)) (λy. (λw.w) y) applied to a.
// Church-2 of the function (λy.(λw.w)y), then fed a — several interleavable redexes.
const two = lam("f", lam("x", app(v("f"), app(v("f"), v("x")))));
const g = lam("y", app(lam("w", v("w")), v("y"))); // ≡ identity, but with an inner redex
const term = app(app(two, g), v("a"));
const nf1 = show(norm(term, "normal"));
const nf2 = show(norm(term, "applicative"));
console.log("normal order →", nf1);
console.log("applicative order →", nf2);
console.log("normal forms agree?", nf1 === nf2); // true — a witness of confluence
Both strategies collapse the term to the same normal form, and the equality check prints
true. Church–Rosser is the theorem guaranteeing this can never come out
false — for any term, any two strategies, forever.
It feels like local confluence — closing every one-step divergence — ought to give global
confluence for free. It does not, in general. The classic counterexample is the
abstract system with b \to a, b \to c,
a \to b, c \to d where a,d
are normal-ish traps: every one-step peak can be closed, yet a and
d are distinct normal forms both reachable from b
— not confluent. Newman's Lemma rescues the intuition but only with an extra
hypothesis: for a terminating (strongly normalising) relation, local confluence
does imply confluence. β-reduction is not terminating (think
\Omega), so Newman's Lemma does not apply to it — which is precisely why
Church and Rosser needed the subtler parallel-reduction argument. Confluence of β is a genuine theorem,
not a triviality.
The single most common misreading: "the calculus is confluent, so every program has a unique answer."
Half right. Confluence guarantees uniqueness — at most one normal form — but says
nothing about existence. \Omega is a perfectly confluent
term with no normal form: its only reduct is itself, so all its (trivial) paths trivially
reconcile, yet it never reaches a value. Confluence and normalisation are independent properties.
β-reduction has the first for all terms and the second only for some.
A second subtlety: confluence is stated for multi-step
\twoheadrightarrow_\beta, not for single steps. β-reduction is confluent but
does not enjoy the one-step diamond property — a single step on one side may need many steps on
the other to catch up, because contracting one redex can copy another. Quoting "the diamond property"
for raw \to_\beta is a real and common error.