A partial-function reduction relation is confluent. The TLC evaluator is a partial function. QED.
The Church-Rosser theorem for a confluent reduction relation is usually proved via a one-step diamond, Tait-Martin-Löf parallel reduction, or a Takahashi translation. For any deterministic evaluator these machines are unnecessary. We give a three-line Lean proof of Church-Rosser for the ternary lambda calculus TLC: the one-step relation is a partial function, its reflexive transitive closure is therefore confluent, and Church-Rosser is an immediate corollary. The proof lives in Proof/ChurchRosser.lean with zero sorrys.
Let R ⊆ α × α be a reduction relation. Call R functional (equivalently: deterministic, or a partial function) if
R(a, b) ∧ R(a, c) ⇒ b = c.
Call R confluent if
R*(a, b) ∧ R*(a, c) ⇒ ∃d. R*(b, d) ∧ R*(c, d).
Theorem. If R is functional, then R* is confluent.
Proof. By induction on R^*(a, b). The reflexive case joins at c. The transitive step a →_R a' →* b inherits a second path a →_R a'' →* c. Functionality gives a' = a'', so the induction hypothesis on a' supplies the join.
That is the whole argument. In Lean, with Relation.ReflTransGen:
theorem confluent_of_partial_function
{R : α → α → Prop} (hfun : ∀ a b c, R a b → R a c → b = c) :
Confluent (Relation.ReflTransGen R) := by
intro a b c hab hac
induction hab with
| refl => exact ⟨c, hac, Relation.ReflTransGen.refl⟩
| tail _ hstep ih =>
rcases ih with ⟨d, hd₁, hd₂⟩
exact ⟨d, hd₁, hd₂.tail hstep⟩Four lines of Lean, one line of idea.
The ternary lambda calculus TLC uses a left-biased betaStep evaluator: at every beta-redex the leftmost outermost reduction fires. The evaluator is a total function betaStep : Term → Option Term. Its graph
betaRel(t, t′) : ⇔ betaStep(t) = some t′
is therefore a partial function in the relational sense. This is betaRel_deterministic in ChurchRosser.lean, proved by rfl-style case analysis on betaStep.
Apply §1 to R = betaRel:
theorem betaStar_confluent : Confluent (Relation.ReflTransGen betaRel) :=
confluent_of_partial_function betaRel_deterministic
theorem church_rosser : ChurchRosser (Relation.ReflTransGen betaRel) :=
betaStar_confluentNormal forms are unique. Two successful bounded normaliser runs agree:
theorem nf_result_unique (t t₁ t₂ : Term) (fuel₁ fuel₂ : Nat) :
nf fuel₁ t = some t₁ → nf fuel₂ t = some t₂ → t₁ = t₂Again a direct corollary — functionality of nf follows from functionality of betaStep.
The usual Church-Rosser proof handles non-deterministic relations: untyped lambda calculus with full beta reduction admits (λx. x x) ((λy. y) z) → (λx. x x) z → z z and (λx. x x) ((λy. y) z) → ((λy. y) z) ((λy. y) z) → z z. There the diamond is content.
TLC fixes a left-biased evaluator. There is never a choice of redex. Confluence is trivial — but non-trivially trivial: the fact that the same theorem that costs 200 lines of parallel-reduction machinery in the general setting can be had for ten lines in the deterministic setting is precisely why deterministic evaluators are the right semantic primitive. You pay for non-determinism once, at the boundary where you pick an evaluation strategy, and from there on every metatheoretic fact is a one-liner.
The NilSquare residual calculus (nilsquare_anti_comm, residualElt_mul_comm_zero in the same file) is the algebraic shadow of this fact: two residuals of a common redex multiply to zero in the dual-number ring, and this is the one-line replacement for the Hindley-Rosen commutative square.
Uniqueness of bounded WHNF. whnf_result_unique is the same argument on the weak-head relation.
Monotone fuel. nf_mono and whnf_mono: once bounded normalisation succeeds, every larger fuel returns the same term. The proof is one call to church_rosser.
Replay-purity of the Zig runtime. native/runtime/ steps TLC-compiled event streams. Because the underlying evaluator is a partial function, the stepper is replay-pure by construction — two identical event logs produce identical state. This is the Church-Rosser theorem in production.
Proof/ChurchRosser.lean, 573 lines (most are the TLC term-level betaStep definition; the confluence proof itself is §1 and §3 above, ~30 lines).lake build verifies everything.This paper is shorter than most Church-Rosser proofs. The theorem is shorter than the paper. Both are correct.