A partial-function reduction relation is confluent. The TLC evaluator is a partial function. QED. The usual Church-Rosser proof requires 200 lines of parallel-reduction machinery. The deterministic case needs four lines of Lean and one line of idea.
Let R ⊆ α × α be a reduction relation. Call R functional (deterministic, a partial function) if:
Call R confluent if:
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.
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&sub1;, hd&sub2;⟩
exact ⟨d, hd&sub1;, hd&sub2;.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 a partial function in the relational sense. This is betaRel_deterministic in ChurchRosser.lean, proved by rfl-style case analysis on betaStep.
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&sub1; t&sub2; : Term) (fuel&sub1; fuel&sub2; : Nat) :
nf fuel&sub1; t = some t&sub1; → nf fuel&sub2; t = some t&sub2; → t&sub1; = t&sub2;The usual Church-Rosser proof handles non-deterministic relations: untyped lambda calculus with full beta reduction admits two distinct reduction paths from (λx. x x) ((λy. y) z) that must be shown to rejoin. There the diamond lemma has 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 costs 200 lines in the general setting and ten lines in the deterministic setting is precisely why deterministic evaluators are the right semantic primitive.
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. This is the one-line replacement for the Hindley-Rosen commutative square.
| Consequence | Statement |
|---|---|
| Uniqueness of bounded WHNF | whnf_result_unique: the same argument on the weak-head relation |
| Monotone fuel | nf_mono: once bounded normalisation succeeds, every larger fuel returns the same term |
| Replay-purity of the Zig runtime | The Zig runtime steps TLC-compiled event streams; because the evaluator is a partial function, the stepper is replay-pure by construction — two identical event logs produce identical state |
| Metric | Value |
|---|---|
| File | ChurchRosser.lean |
| Total lines | 571 (most is betaStep definition; confluence proof is ~30 lines) |
| Sorrys | 0 |
| Verification | lake build |