Standard Reduction and the Standardization Theorem #

Reference #

B. Calisto, Formalization in Coq of the Standardization Theorem for λ-calculus

source

inductive Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.Standard {Var : Type u} :

Term Var → Term Var → Prop

The Standard reduction relation.

fvar {Var : Type u} (x : Var) : (Term.fvar x).Standard (Term.fvar x)
Free variables standardly reduce to themselves.
app {Var : Type u} {L L' M M' : Term Var} : L.Standard L' → M.Standard M' → (L.app M).Standard (L'.app M')
Congruence rule for application.
abs {Var : Type u} {m m' : Term Var} (xs : Finset Var) : (∀ x ∉ xs, (m.open' (Term.fvar x)).Standard (m'.open' (Term.fvar x))) → m.abs.Standard m'.abs
Congruence rule for lambda terms.
rdx {Var : Type u} {m n m' p : Term Var} : m.LC → n.LC → Relation.ReflTransGen CBN m m'.abs → (m'.open' n).Standard p → (m.app n).Standard p
Standard reduction of a head redex.

Instances For

source

def Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.«term_⭢ₛ_» :

Lean.TrailingParserDescr

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.«term_↠ₛ_» :

Lean.TrailingParserDescr

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.Standard.lc_l {Var : Type u} {M N : Term Var} (step : M.Standard N) :

M.LC

The left side of a standard reduction is locally closed.

source

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.Standard.lc_refl {Var : Type u} (M : Term Var) (lc : M.LC) :

M.Standard M

Standard reduction is reflexive for locally closed terms.

source

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.Standard.lc_r {Var : Type u} {M N : Term Var} (step : M.Standard N) :

N.LC

The right side of a standard reduction is locally closed.

source

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.Standard.of_cbn_step {Var : Type u} {M N : Term Var} (step : M.CBN N) (lc_N : N.LC) :

M.Standard N

A single Call-by-Name step is a standard reduction.

source

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.Standard.cbn_step_trans {Var : Type u} {M N P : Term Var} (step : M.CBN P) (std : P.Standard N) :

M.Standard N

A Call-by-Name step followed by a standard reduction is a standard reduction.

source

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.Standard.cbn_trans {Var : Type u} {M N P : Term Var} (h1 : Relation.ReflTransGen CBN M P) (h2 : P.Standard N) :

M.Standard N

A Call-by-Name reduction followed by a standard reduction is a standard reduction.

source

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.Standard.of_cbn {Var : Type u} {M N : Term Var} (step : Relation.ReflTransGen CBN M N) (lc_N : N.LC) :

M.Standard N

Call-by-Name reduction is contained in standard reduction.

source

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.Standard.subst {Var : Type u} {M N M' N' : Term Var} [DecidableEq Var] [HasFresh Var] (hM : M.Standard M') (hN : N.Standard N') (x : Var) (lc_N : N.LC) (lc_N' : N'.LC) :

M[x := N].Standard M'[x := N']

Standard reduction is preserved by substitution.

source

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.Standard.of_beta_step {Var : Type u} {M N : Term Var} [DecidableEq Var] [HasFresh Var] (step : M.FullBeta N) (lc_M : M.LC) :

M.Standard N

A single full β-step is a standard reduction.

source

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.Standard.to_redex {Var : Type u} {M N : Term Var} [DecidableEq Var] [HasFresh Var] (step : M.Standard N) :

Relation.ReflTransGen FullBeta M N

Standard reduction is contained in full β-reduction.

source

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.Standard.abs_inv {Var : Type u} {M N : Term Var} [DecidableEq Var] [HasFresh Var] (h : M.Standard N) (M' : Term Var) (eq : N = M'.abs) :

∃ (M'' : Term Var), Relation.ReflTransGen CBN M M''.abs ∧ M''.abs.Standard M'.abs

If a standard reduction reaches an abstraction, then its leading Call-by-Name reduction reaches an abstraction that standardly reduces to the same target.

source

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.Standard.abs_subst {Var : Type u} {M N M' N' : Term Var} [DecidableEq Var] [HasFresh Var] (h_abs : M.abs.Standard M'.abs) (hN : N.Standard N') (lc_N : N.LC) (lc_N' : N'.LC) :

(M.open' N).Standard (M'.open' N')

Standard reduction of abstractions is preserved by opening.

source

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.Standard.trans_step {Var : Type u} {M N P : Term Var} [DecidableEq Var] [HasFresh Var] (h1 : M.Standard P) (h2 : P.FullBeta N) :

M.Standard N

A standard reduction followed by a full β-step is a standard reduction.

source

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.Standard.trans_redex {Var : Type u} {M N P : Term Var} [DecidableEq Var] [HasFresh Var] (h1 : M.Standard P) (h2 : Relation.ReflTransGen FullBeta P N) :

M.Standard N

A standard reduction followed by a full β-reduction is a standard reduction.

source

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.Standard.trans {Var : Type u} {M N P : Term Var} [DecidableEq Var] [HasFresh Var] (h1 : M.Standard P) (h2 : P.Standard N) :

M.Standard N

Standard reduction is transitive.

source

@[implicit_reducible]

instance Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.instTransStandardFullBeta {Var : Type u} [DecidableEq Var] [HasFresh Var] :

Trans (fun (x1 x2 : Term Var) => x1.Standard x2) (fun (x1 x2 : Term Var) => x1.FullBeta x2) fun (x1 x2 : Term Var) => x1.Standard x2

Equations

Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.instTransStandardFullBeta = { trans := ⋯ }

source

@[implicit_reducible]

instance Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.instTransStandardReflTransGenFullBeta {Var : Type u} [DecidableEq Var] [HasFresh Var] :

Trans (fun (x1 x2 : Term Var) => x1.Standard x2) (fun (x1 x2 : Term Var) => Relation.ReflTransGen FullBeta x1 x2) fun (x1 x2 : Term Var) => x1.Standard x2

Equations