Skip to content

feat(untyped): standardization theorem for the lambda calculus #679

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
m-ow wants to merge 2 commits into
base: main
Choose a base branch
from
Open

feat(untyped): standardization theorem for the lambda calculus #679

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
fc9e067
add basic properties
m-ow Jun 23, 2026
7f7a6cd
add standardization theorem
m-ow Jun 24, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
32 changes: 29 additions & 3 deletions Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/CallByName.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -31,18 +31,44 @@ inductive CBN : Term Var → Term Var → Prop
/-- Evaluates the leftmost term. -/
| app : LC Z → CBN M N → CBN (app M Z) (app N Z)

variable {M N : Term Var}
variable {M M' N N' : Term Var}

/-- The left side of a CBN reduction step is locally closed. -/
/-- The left side of a Call-by-Name step is locally closed. -/
lemma CBN.lc_l (step : M ⭢ₙ N) : LC M := by
induction step with grind

/-- A single Call-by-Name step is a full β-reduction. -/
lemma CBN.step_to_redex (step : M ⭢ₙ N) : M ↠βᶠ N := by
induction step <;> grind [FullBeta.redex_app_l_cong, Relation.ReflTransGen.single]

/-- Call-by-Name reduction is contained in full β-reduction. -/
lemma CBN.to_redex (step : M ↠ₙ N) : M ↠βᶠ N := by
induction step <;> grind [CBN.step_to_redex, Relation.ReflTransGen.trans]

/-- Left congruence rule for application in Call-by-Name reduction. -/
lemma CBN.steps_app_l_cong (step : M ↠ₙ M') (lc_N : LC N) : Term.app M N ↠ₙ Term.app M' N := by
induction step <;> grind [CBN.app]

variable [HasFresh Var] [DecidableEq Var]

/-- The right side of a CBN reduction step is locally closed. -/
/-- The right side of a Call-by-Name step is locally closed. -/
lemma CBN.lc_r (step : M ⭢ₙ N) : LC N := by
induction step with grind

/-- The right side of a Call-by-Name reduction is locally closed. -/
lemma CBN.steps_lc_r (lc_M : LC M) (step : M ↠ₙ N) : LC N := by
induction step <;> grind [CBN.lc_r]

/-- Substitution preserves a single Call-by-Name step. -/
lemma CBN.step_subst (x : Var) (h : M ⭢ₙ M') (lc_N : LC N) :
M[x := N] ⭢ₙ M'[x := N] := by
induction h <;> grind [Term.subst_open, Term.subst_lc, CBN.base, CBN.app]

/-- Substitution preserves Call-by-Name reduction. -/
lemma CBN.steps_subst (x : Var) (step : M ↠ₙ M') (lc_N : LC N) :
M[x := N] ↠ₙ M'[x := N] := by
induction step <;> grind [CBN.step_subst]

end LambdaCalculus.LocallyNameless.Untyped.Term

end Cslib
171 changes: 169 additions & 2 deletions Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ module

public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.CallByName

/-! # Standard Reduction
/-! # Standard Reduction and the Standardization Theorem

## Reference

Expand All @@ -18,6 +18,8 @@ public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.CallByName

@[expose] public section

set_option linter.unusedDecidableInType false

namespace Cslib

universe u
Expand All @@ -39,7 +41,7 @@ inductive Standard : Term Var → Term Var → Prop
/-- Standard reduction of a head redex. -/
| rdx : LC m → LC n → m ↠ₙ (abs m') → Standard (m' ^ n) p → Standard (app m n) p

variable {M N : Term Var}
variable {M N P M' N' : Term Var}

/-- The left side of a standard reduction is locally closed. -/
lemma Standard.lc_l (step : M ⭢ₛ N) : LC M := by
Expand All @@ -58,6 +60,171 @@ lemma Standard.lc_r (step : M ⭢ₛ N) : LC N := by
case abs xs _ ih => exact LC.abs xs _ ih
all_goals grind

/-- A single Call-by-Name step is a standard reduction. -/
lemma Standard.of_cbn_step (step : M ⭢ₙ N) (lc_N : LC N) : M ⭢ₛ N := by
induction step
case base h_beta =>
cases h_beta
exact rdx (by assumption) (by assumption) .refl (lc_refl _ lc_N)
case app L _ _ lc_L _ ih =>
exact app (ih (by cases lc_N; assumption)) (lc_refl L lc_L)

/-- A Call-by-Name step followed by a standard reduction is a standard reduction. -/
lemma Standard.cbn_step_trans (step : M ⭢ₙ P) (std : P ⭢ₛ N) : M ⭢ₛ N := by
induction step generalizing N
case base h_beta =>
cases h_beta
exact rdx (by assumption) (by assumption) .refl std
case app step_M ih =>
cases std with
| app std_L' std_M => exact app (ih std_L') std_M
| rdx _ lc_Z cbn_m std_body =>
exact rdx (CBN.lc_l step_M) lc_Z (.head step_M cbn_m) std_body

/-- A Call-by-Name reduction followed by a standard reduction is a standard reduction. -/
lemma Standard.cbn_trans (h1 : M ↠ₙ P) (h2 : P ⭢ₛ N) : M ⭢ₛ N := by
induction h1 with
| refl => exact h2
| tail _ h_step ih => exact ih (cbn_step_trans h_step h2)

/-- Call-by-Name reduction is contained in standard reduction. -/
lemma Standard.of_cbn (step : M ↠ₙ N) (lc_N : LC N) : M ⭢ₛ N :=
cbn_trans step (lc_refl N lc_N)

variable [DecidableEq Var] [HasFresh Var]

/-- Standard reduction is preserved by substitution. -/
lemma Standard.subst (hM : M ⭢ₛ M') (hN : N ⭢ₛ N') (x : Var) (lc_N : LC N) (lc_N' : LC N') :
(M [ x := N ]) ⭢ₛ (M' [ x := N' ]) := by
induction hM generalizing N N'
case fvar =>
simp only [Term.subst_fvar]
split
· exact hN
· exact fvar _
case app ihL ihM =>
rw [Term.subst_app]
exact app (ihL hN lc_N lc_N') (ihM hN lc_N lc_N')
case abs m m' _ _ ih =>
simp only [Term.subst_abs]
apply abs <| free_union [fv] Var
intro y hy
have h_neq : x ≠ y := by aesop
rw [← Term.subst_open_var y x N m h_neq lc_N, ← Term.subst_open_var y x N' m' h_neq lc_N']
exact ih y (by aesop) hN lc_N lc_N'
case rdx n m' _ lc_m lc_n cbn_m std_p ih =>
rw [Term.subst_app]
have std_p_subst := ih hN lc_N lc_N'
rw [Term.subst_open x N n m' lc_N] at std_p_subst
exact rdx (Term.subst_lc (x := x) lc_m lc_N) (Term.subst_lc (x := x) lc_n lc_N)
(CBN.steps_subst x cbn_m lc_N) std_p_subst

/-- A single full β-step is a standard reduction. -/
lemma Standard.of_beta_step (step : M ⭢βᶠ N) (lc_M : LC M) : M ⭢ₛ N := by
induction step
case base h_beta =>
cases h_beta
exact rdx (by assumption) (by assumption) .refl
(lc_refl _ (Term.beta_lc (by assumption) (by assumption)))
case appL A B _ _ _ =>
have : LC A := by cases lc_M; assumption
apply Standard.app <;> grind [lc_refl]
case appR A _ _ _ _ =>
have : LC A := by cases lc_M; assumption
apply Standard.app <;> grind [lc_refl]
case abs ih =>
apply Standard.abs <| free_union [fv] Var
intro x hx
exact ih x (by aesop) (Term.beta_lc lc_M (by constructor))

/-- Standard reduction is contained in full β-reduction. -/
lemma Standard.to_redex (step : M ⭢ₛ N) : M ↠βᶠ N := by
induction step
case fvar => rfl
case app step_L step_M ih_L ih_M =>
exact .trans (FullBeta.redex_app_l_cong ih_L (Standard.lc_l step_M))
(FullBeta.redex_app_r_cong ih_M (Standard.lc_r step_L))
case abs xs _ ih => exact FullBeta.redex_abs_cong xs ih
case rdx n m' _ lc_m lc_n cbn_m std_p ih =>
have step1 := FullBeta.redex_app_l_cong (CBN.to_redex cbn_m) lc_n
have step2 : Term.app (Term.abs m') n ↠βᶠ (m' ^ n) :=
.single (Xi.base (Beta.beta (CBN.steps_lc_r lc_m cbn_m) lc_n))
exact .trans step1 (.trans step2 ih)

/-- If a standard reduction reaches an abstraction, then its leading Call-by-Name
reduction reaches an abstraction that standardly reduces to the same target. -/
lemma Standard.abs_inv (h : M ⭢ₛ N) (M' : Term Var) (eq : N = Term.abs M') :
∃ M'', M ↠ₙ Term.abs M'' ∧ Term.abs M'' ⭢ₛ Term.abs M' := by
induction h generalizing M'
case fvar => trivial
case app => trivial
case abs m_body m_target xs h_body ih =>
cases eq
exact ⟨m_body, .refl, Standard.abs xs h_body⟩
case rdx m1 n1 m1' p1 lc_m1 lc_n1 cbn_m1 _ ih =>
have ⟨p'', cbn_body, std_p''⟩ := ih M' eq
have step1 : Term.app m1 n1 ↠ₙ Term.app (Term.abs m1') n1 := CBN.steps_app_l_cong cbn_m1 lc_n1
have step2 : Term.app (Term.abs m1') n1 ⭢ₙ (m1' ^ n1) :=
CBN.base (Beta.beta (CBN.steps_lc_r lc_m1 cbn_m1) lc_n1)
exact ⟨p'', .trans step1 (.head step2 cbn_body), std_p''⟩

/-- Standard reduction of abstractions is preserved by opening. -/
lemma Standard.abs_subst
(h_abs : Term.abs M ⭢ₛ Term.abs M') (hN : N ⭢ₛ N') (lc_N : LC N) (lc_N' : LC N') :
(M ^ N) ⭢ₛ (M' ^ N') := by
cases h_abs
case abs h_body =>
have ⟨y, _⟩ := fresh_exists <| free_union [fv] Var
have h_subst := Standard.subst (h_body y (by aesop)) hN y lc_N lc_N'
rw [← Term.subst_intro y N M (by aesop), ← Term.subst_intro y N' M' (by aesop)] at h_subst
exact h_subst

/-- A standard reduction followed by a full β-step is a standard reduction. -/
lemma Standard.trans_step (h1 : M ⭢ₛ P) (h2 : P ⭢βᶠ N) : M ⭢ₛ N := by
induction h1 generalizing N
case fvar => contradiction
case rdx lc_L lc_M cbn _ ih => exact Standard.rdx lc_L lc_M cbn (ih h2)
case abs p_body ih =>
cases h2
case abs ih_beta =>
apply Standard.abs <| free_union [fv] Var
intro y hy
exact ih y (by aesop) (ih_beta y (by aesop))
· grind
case app L1 _ M1 _ std_L std_M ih_L ih_M =>
cases h2
case appL step_M => exact Standard.app std_L (ih_M step_M)
case appR step_L _ => exact Standard.app (ih_L step_L) std_M
case base h_beta =>
cases h_beta
have ⟨L1', cbn_L1, std_abs⟩ := Standard.abs_inv std_L _ rfl
have std_subst := Standard.abs_subst std_abs std_M (Standard.lc_l std_M) (Standard.lc_r std_M)
have step1 : Term.app L1 M1 ↠ₙ Term.app (Term.abs L1') M1 :=
CBN.steps_app_l_cong cbn_L1 (Standard.lc_l std_M)
have step2 : Term.app (Term.abs L1') M1 ⭢ₙ (L1' ^ M1) :=
CBN.base (Beta.beta (CBN.steps_lc_r (Standard.lc_l std_L) cbn_L1) (Standard.lc_l std_M))
exact Standard.cbn_trans (.trans step1 (.single step2)) std_subst

/-- A standard reduction followed by a full β-reduction is a standard reduction. -/
lemma Standard.trans_redex (h1 : M ⭢ₛ P) (h2 : P ↠βᶠ N) : M ⭢ₛ N := by
induction h2 with
| refl => exact h1
| tail _ step ih => exact Standard.trans_step ih step

/-- Standard reduction is transitive. -/
lemma Standard.trans (h1 : M ⭢ₛ P) (h2 : P ⭢ₛ N) : M ⭢ₛ N :=
trans_redex h1 (to_redex h2)

/-- The standardization theorem: every full β-reduction is a standard reduction. -/
theorem Standard.standardization (lc_M : LC M) (step : M ↠βᶠ N) : M ⭢ₛ N := by
induction step with
| refl => exact Standard.lc_refl M lc_M
| tail _ h_step ih => exact ih.trans (Standard.of_beta_step h_step (FullBeta.step_lc_l h_step))

/-- Standard reduction coincides with full β-reduction on locally closed terms. -/
theorem Standard.iff_redex (lc_M : LC M) : M ⭢ₛ N ↔ M ↠βᶠ N :=
⟨to_redex, standardization lc_M⟩

end LambdaCalculus.LocallyNameless.Untyped.Term

end Cslib
Loading