From d6edb26d79d4c35f7a0a990d027bf0d4eebaac44 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Fri, 24 Jul 2026 18:06:45 +0200 Subject: [PATCH 1/2] fix(LambdaCalculus): prevent capture in alpha-equivalence --- .../LambdaCalculus/Named/Untyped/Basic.lean | 9 ++++++--- CslibTests/LambdaCalculus.lean | 14 +++++++++++++- 2 files changed, 19 insertions(+), 4 deletions(-) diff --git a/Cslib/Languages/LambdaCalculus/Named/Untyped/Basic.lean b/Cslib/Languages/LambdaCalculus/Named/Untyped/Basic.lean index 364b7cf8f..7cbf5bdda 100644 --- a/Cslib/Languages/LambdaCalculus/Named/Untyped/Basic.lean +++ b/Cslib/Languages/LambdaCalculus/Named/Untyped/Basic.lean @@ -61,7 +61,9 @@ inductive Term.Subst [DecidableEq Var] : Term Var → Var → Term Var → Term | absIn : x ≠ y → y ∉ r.fv → m.Subst x r m' → (abs y m).Subst x r (abs y m') | app : m.Subst x r m' → n.Subst x r n' → (app m n).Subst x r (app m' n') -/-- Renaming, or variable substitution. `m.rename x y` renames `x` into `y` in `m`. -/ +/-- Renaming, or variable substitution. `m.rename x y` renames the free occurrences of `x` into +`y` in `m`. This operation is not capture-avoiding, so callers must ensure that `y` is fresh when +capture matters. -/ def Term.rename [DecidableEq Var] (m : Term Var) (x y : Var) : Term Var := match m with | var z => if z = x then (var y) else (var z) @@ -146,9 +148,10 @@ open Term /-- α-equivalence. -/ inductive Term.AlphaEquiv [DecidableEq Var] : Term Var → Term Var → Prop where --- The α-axiom +-- The α-axiom. Freshness for every variable name prevents `rename` from capturing an occurrence +-- beneath an inner abstraction. | ax {m : Term Var} {x y : Var} : - y ∉ m.fv → AlphaEquiv (abs x m) (abs y (m.rename x y)) + y ∉ m.vars → AlphaEquiv (abs x m) (abs y (m.rename x y)) -- Equivalence relation rules | refl : AlphaEquiv m m | symm : AlphaEquiv m n → AlphaEquiv n m diff --git a/CslibTests/LambdaCalculus.lean b/CslibTests/LambdaCalculus.lean index 1a331ea58..96e3f6c97 100644 --- a/CslibTests/LambdaCalculus.lean +++ b/CslibTests/LambdaCalculus.lean @@ -18,7 +18,19 @@ def lambdaId := abs 0 (var 0) example : (abs 0 (var 0)) =α (abs 1 (var 1)) := by constructor - simp [Term.fv] + simp [Term.vars, Term.fv, Term.bv] + +-- The new binder must also be fresh for bound variable names in the body. Otherwise +-- renaming `0` to `1` below the inner abstraction would capture the renamed occurrence. +example : True := by + fail_if_success + exact (AlphaEquiv.ax + (m := abs 1 (var 0)) + (x := 0) + (y := 1) + (by simp [Term.vars, Term.fv, Term.bv]) : + (abs 0 (abs 1 (var 0)) : NatTerm) =α (abs 1 (abs 1 (var 1)))) + trivial example : (abs 1 (var 0)).subst 0 (app (var 1) (var 2)) = (abs 3 (app (var 1) (var 2))) := by simp +instances [subst, fv, bv, vars, rename, instHasFreshNat, HasFresh.ofSucc] From cb4e20460f1a7ef67b08974c75623f12ac49b4bc Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Fri, 24 Jul 2026 18:35:14 +0200 Subject: [PATCH 2/2] fix(LambdaCalculus): use nominal swapping for alpha-equivalence --- .../LambdaCalculus/Named/Untyped/Basic.lean | 20 ++++++++++++--- CslibTests/LambdaCalculus.lean | 25 ++++++++++++++++--- 2 files changed, 38 insertions(+), 7 deletions(-) diff --git a/Cslib/Languages/LambdaCalculus/Named/Untyped/Basic.lean b/Cslib/Languages/LambdaCalculus/Named/Untyped/Basic.lean index 7cbf5bdda..4ae8de843 100644 --- a/Cslib/Languages/LambdaCalculus/Named/Untyped/Basic.lean +++ b/Cslib/Languages/LambdaCalculus/Named/Untyped/Basic.lean @@ -75,6 +75,21 @@ def Term.rename [DecidableEq Var] (m : Term Var) (x y : Var) : Term Var := abs z (m'.rename x y) | app n1 n2 => app (n1.rename x y) (n2.rename x y) +/-- Structurally swap the variable names `x` and `y`, including abstraction binders. Unlike +`Term.rename`, swapping preserves the binding structure even when one of the names already occurs +bound in the term. -/ +def Term.swap [DecidableEq Var] (m : Term Var) (x y : Var) : Term Var := + match m with + | var z => var (Equiv.swap x y z) + | abs z m' => abs (Equiv.swap x y z) (m'.swap x y) + | app n₁ n₂ => app (n₁.swap x y) (n₂.swap x y) + +/-- Swapping the same two variable names twice leaves a term unchanged. -/ +@[simp] +theorem Term.swap_swap [DecidableEq Var] (m : Term Var) (x y : Var) : + (m.swap x y).swap x y = m := by + induction m <;> simp [Term.swap, *] + /-- Renaming preserves size. -/ @[simp] theorem Term.rename.eq_sizeOf {m : Term Var} {x y : Var} [DecidableEq Var] : @@ -148,10 +163,9 @@ open Term /-- α-equivalence. -/ inductive Term.AlphaEquiv [DecidableEq Var] : Term Var → Term Var → Prop where --- The α-axiom. Freshness for every variable name prevents `rename` from capturing an occurrence --- beneath an inner abstraction. +-- The α-axiom, using nominal swapping to preserve binding structure. | ax {m : Term Var} {x y : Var} : - y ∉ m.vars → AlphaEquiv (abs x m) (abs y (m.rename x y)) + y ∉ m.fv → AlphaEquiv (abs x m) (abs y (m.swap x y)) -- Equivalence relation rules | refl : AlphaEquiv m m | symm : AlphaEquiv m n → AlphaEquiv n m diff --git a/CslibTests/LambdaCalculus.lean b/CslibTests/LambdaCalculus.lean index 96e3f6c97..dd3d87d81 100644 --- a/CslibTests/LambdaCalculus.lean +++ b/CslibTests/LambdaCalculus.lean @@ -18,20 +18,37 @@ def lambdaId := abs 0 (var 0) example : (abs 0 (var 0)) =α (abs 1 (var 1)) := by constructor - simp [Term.vars, Term.fv, Term.bv] + simp [Term.fv] --- The new binder must also be fresh for bound variable names in the body. Otherwise --- renaming `0` to `1` below the inner abstraction would capture the renamed occurrence. +-- Swapping also renames the colliding inner binder, preserving which abstraction binds each +-- variable occurrence. +example : + (abs 0 (abs 1 (var 0)) : NatTerm) =α (abs 1 (abs 0 (var 1))) := by + apply AlphaEquiv.ax + simp [Term.fv] + +-- The old one-way renaming axiom instead produced this captured term. example : True := by fail_if_success exact (AlphaEquiv.ax (m := abs 1 (var 0)) (x := 0) (y := 1) - (by simp [Term.vars, Term.fv, Term.bv]) : + (by simp [Term.fv]) : (abs 0 (abs 1 (var 0)) : NatTerm) =α (abs 1 (abs 1 (var 1)))) trivial +-- Unlike requiring freshness for every variable name, nominal swapping permits a new binder name +-- that already occurs bound in the body. +example : + (abs 0 (abs 1 (var 1)) : NatTerm) =α (abs 1 (abs 1 (var 1))) := by + apply AlphaEquiv.trans (m2 := abs 1 (abs 0 (var 0))) + · apply AlphaEquiv.ax + simp [Term.fv] + · apply AlphaEquiv.ctx (c := Context.abs 1 Context.hole) + apply AlphaEquiv.ax + simp [Term.fv] + example : (abs 1 (var 0)).subst 0 (app (var 1) (var 2)) = (abs 3 (app (var 1) (var 2))) := by simp +instances [subst, fv, bv, vars, rename, instHasFreshNat, HasFresh.ofSucc]