Skip to content

Commit a915db9

Browse files
m-owchenson2018
andauthored
feat: prove strong confluence of eta-reduction (#425)
This PR formalizes the strong confluence of full η-reduction (`stronglyConfluent_eta`) for the locally nameless untyped λ-calculus. --------- Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com> Co-authored-by: Chris Henson <chrishenson.net@gmail.com>
1 parent 9a159ac commit a915db9

5 files changed

Lines changed: 124 additions & 2 deletions

File tree

Cslib.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -93,6 +93,7 @@ public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Basic
9393
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBeta
9494
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBetaConfluence
9595
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullEta
96+
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullEtaConfluence
9697
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.LcAt
9798
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.MultiApp
9899
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.MultiSubst

Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullEta.lean

Lines changed: 31 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -37,14 +37,23 @@ namespace FullEta
3737

3838
attribute [scoped grind .] appL appR
3939

40-
variable {M M' : Term Var}
40+
variable {M M' N N' : Term Var}
4141

4242
/-- The right side of an η-reduction is locally closed. -/
43+
@[scoped grind →]
4344
lemma step_lc_r (step : M ⭢ηᶠ M') : LC M' := by
4445
induction step
4546
case abs => constructor; assumption
4647
all_goals grind
4748

49+
/- Single reduction `app M (fvar x) ⭢ηᶠ N` implies `N = app M' (fvar x)` for some M' -/
50+
@[scoped grind →]
51+
lemma invert_step_app_fvar (step : (app M (fvar x)) ⭢ηᶠ N) :
52+
∃ M', N = app M' (fvar x) ∧ M ⭢ηᶠ M' := by
53+
cases step with
54+
| appR _ step_M => exact ⟨_, rfl, step_M⟩
55+
| appL _ step_x => cases step_x
56+
4857
variable [HasFresh Var] [DecidableEq Var]
4958

5059
/-- An η-reduction step does not introduce new free variables. -/
@@ -56,6 +65,27 @@ lemma step_not_fv (step : M ⭢ηᶠ M') (hw : w ∉ M.fv) : w ∉ M'.fv := by
5665
grind [close_preserve_not_fvar, open_fresh_preserve_not_fvar]
5766
| _ => grind
5867

68+
/-- Substitution of a fresh variable preserves an η-reduction step. -/
69+
@[scoped grind ←]
70+
lemma eta_subst_fvar {x y : Var} (step : M ⭢ηᶠ M') : M [ x := fvar y ] ⭢ηᶠ M' [ x := fvar y ] := by
71+
have lc_fy : LC (fvar y) := by constructor
72+
induction step with
73+
| eta lc_M => exact eta (subst_lc lc_M lc_fy)
74+
| appL lc_Z _ ih => exact appL (subst_lc lc_Z lc_fy) ih
75+
| appR lc_Z _ ih => exact appR (subst_lc lc_Z lc_fy) ih
76+
| abs xs _ ih =>
77+
apply abs (xs ∪ {x, y})
78+
grind
79+
80+
/- Closing a sequence of η-reduction steps over a fresh variable preserves the steps. -/
81+
open Relation in
82+
lemma close_eta_steps (hx_M : x ∉ M.fv) (st_M : ReflGen FullEta (M ^ fvar x) N) :
83+
ReflGen FullEta M.abs (N ^* x).abs := by
84+
cases st_M with
85+
| refl => rw [←open_close_var x M hx_M]
86+
| single st =>
87+
exact .single (.abs {x} fun _ _ => by grind)
88+
5989
end LambdaCalculus.LocallyNameless.Untyped.Term.FullEta
6090

6191
end Cslib
Lines changed: 71 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,71 @@
1+
/-
2+
Copyright (c) 2026 Maximiliano Onofre Martínez. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Maximiliano Onofre Martínez
5+
-/
6+
7+
module
8+
9+
public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullEta
10+
11+
@[expose] public section
12+
13+
set_option linter.unusedDecidableInType false
14+
15+
/-! # η-confluence for the λ-calculus
16+
17+
## Reference
18+
19+
* [T. Nipkow, *More Church-Rosser Proofs (in Isabelle/HOL)*][Nipkow2001]
20+
21+
-/
22+
23+
namespace Cslib
24+
25+
universe u
26+
27+
variable {Var : Type u}
28+
29+
namespace LambdaCalculus.LocallyNameless.Untyped.Term
30+
31+
open Relation
32+
33+
variable [HasFresh Var] [DecidableEq Var]
34+
35+
open FullEta in
36+
lemma stronglyConfluent_eta : StronglyConfluent (@FullEta Var) := by
37+
intro _ y z h₁ h₂
38+
suffices ∃ w, ReflGen FullEta y w ∧ ReflGen FullEta z w by grind
39+
induction h₁ generalizing z
40+
case appL Z _ N _ _ ih =>
41+
cases h₂
42+
case appL _ _ st => use (disch := grind) app Z (ih st).choose
43+
case appR z_red _ _ => use (disch := grind) app z_red N
44+
case appR M _ Z _ _ ih =>
45+
cases h₂
46+
case appR _ st _ => use (disch := grind) app (ih st).choose M
47+
case appL z_red _ _ => use (disch := grind) app Z z_red
48+
case eta M lc_M =>
49+
cases h₂
50+
case eta => use M
51+
case abs N L st_body =>
52+
have ⟨w, _⟩ := fresh_exists <| free_union [fv] Var
53+
have ⟨M', _⟩ := invert_step_app_fvar <| st_body w <| by grind
54+
use M'
55+
grind [→ eta, step_not_fv, open_eq_app]
56+
case abs M N L ih₁ ih₂ =>
57+
cases h₂
58+
case eta z _ =>
59+
have ⟨w, _⟩ := fresh_exists <| free_union [fv] Var
60+
have ⟨z', _⟩ := invert_step_app_fvar <| ih₁ w <| by grind
61+
use z'
62+
grind [→ eta, step_not_fv, open_eq_app]
63+
case abs N2 L2 st_M_N2 =>
64+
have ⟨x, _⟩ := fresh_exists <| free_union [fv] Var
65+
have ⟨w, _⟩ := ih₂ (z := N2 ^ fvar x) x (by grind) (by grind)
66+
use abs (w ^* x)
67+
grind [close_eta_steps]
68+
69+
end LambdaCalculus.LocallyNameless.Untyped.Term
70+
71+
end Cslib

Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Properties.lean

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -40,6 +40,10 @@ theorem subst_fresh (x : Var) (t sub : Term Var) (nmem : x ∉ t.fv) : t [x := s
4040
lemma open_close (x : Var) (t : Term Var) (k : ℕ) (nmem : x ∉ t.fv) : t = t⟦k ↝ fvar x⟧⟦k ↜ x⟧ := by
4141
induction t generalizing k <;> grind
4242

43+
/-- Specializes `open_close` to the first closing. -/
44+
lemma open_close_var (x : Var) (t : Term Var) (nmem : x ∉ t.fv) : t = (t ^ fvar x) ^* x :=
45+
open_close x t 0 nmem
46+
4347
/-- Opening is injective. -/
4448
lemma open_injective (x : Var) (M M') (free_M : x ∉ M.fv) (free_M' : x ∉ M'.fv)
4549
(eq : M ^ fvar x = M' ^ fvar x) : M = M' := by
@@ -82,6 +86,12 @@ lemma open_lc (k t) (e : Term Var) (e_lc : e.LC) : e = e⟦k ↝ t⟧ := by
8286
| abs xs e _ _ => grind [open_lc_aux e 0 (fvar (fresh xs)) (k+1) t]
8387
| _ => grind
8488

89+
/- If opening yields `app m x`, the original term was `app m (bvar 0)`. -/
90+
lemma open_eq_app {x : Var} {m n : Term Var} (hw_n : x ∉ n.fv) (hw_m : x ∉ m.fv) (lc_m : LC m)
91+
(h : n ^ fvar x = app m (fvar x)) : n = app m (bvar 0) := by
92+
apply open_injective x n _ hw_n (by grind)
93+
grind [open_lc 0 (fvar x) m lc_m]
94+
8595
/-- Substitution of a locally closed term distributes with opening. -/
8696
@[scoped grind =]
8797
lemma subst_openRec (x : Var) (t : Term Var) (k : ℕ) (u e : Term Var) (lc : LC t) :

references.bib

Lines changed: 11 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -45,7 +45,7 @@ @inproceedings{Danielsson2008
4545
location = {San Francisco, California, USA},
4646
series = {POPL '08}
4747
}
48-
48+
4949

5050
@article{ Barendregt1984,
5151
title={Introduction to Lambda Calculus},
@@ -192,6 +192,16 @@ @Book{ Montesi2023
192192
keywords = {choreographic-programming,choreographic-language,choreography,concurrency-theory}
193193
}
194194

195+
@article{ Nipkow2001,
196+
title = {More {Church-Rosser} Proofs (in {Isabelle/HOL})},
197+
author = {Nipkow, Tobias},
198+
journal = {Journal of Automated Reasoning},
199+
volume = {26},
200+
pages = {51--66},
201+
year = {2001},
202+
publisher = {Kluwer Academic Publishers}
203+
}
204+
195205
@Book{ Sangiorgi2011,
196206
location = {Cambridge},
197207
title = {Introduction to Bisimulation and Coinduction},

0 commit comments

Comments
 (0)