Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.StrongNorm

Strong normalization (termination) for full beta-reduction of untyped lambda calculus.

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.sn_step {Var : Type u} {t t' : Term Var} (t_st_t' : t.FullBeta t') (sn_t : Relation.SN FullBeta t) :

Relation.SN FullBeta t'

A single β-reduction step preserves strong normalization.

source

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.sn_steps {Var : Type u} {t t' : Term Var} (t_st_t' : Relation.ReflTransGen FullBeta t t') (sn_t : Relation.SN FullBeta t) :

Relation.SN FullBeta t'

Multiple β-reduction steps also preserve strong normalization.

source

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.sn_fvar {Var : Type u} {x : Var} :

Relation.SN FullBeta (fvar x)

Free variables are strongly normalizing.

source

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.sn_app {Var : Type u} (t s : Term Var) (sn_t : Relation.SN FullBeta t) (sn_s : Relation.SN FullBeta s) (hβ : ∀ {t' s' : Term Var}, Relation.ReflTransGen FullBeta t t'.abs → Relation.ReflTransGen FullBeta s s' → Relation.SN FullBeta (t'.open' s')) :

Relation.SN FullBeta (t.app s)

An application is strongly normalizing if the left and right terms are strongly normalizing, as well as all possible future top level abstraction application beta reductions

source

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.sn_app_left {Var : Type u} (M N : Term Var) (lc_N : N.LC) (sn_MN : Relation.SN FullBeta (M.app N)) :

Relation.SN FullBeta M

The left side of a strongly normalizing application is strongly normalizing.

source

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.sn_app_right {Var : Type u} (M N : Term Var) (lc_M : M.LC) (sn_MN : Relation.SN FullBeta (M.app N)) :

Relation.SN FullBeta N

The right side of a strongly normalizing application is strongly normalizing.

source

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

Term Var → Prop

A neutral term is a term of the form v t₁ … t_n where v is a variable and t₁ … t_n are strongly normalizing terms.

bvar {Var : Type u} (n : ℕ) : (Term.bvar n).Neutral
Just a bound variable is neutral.
fvar {Var : Type u} (x : Var) : (Term.fvar x).Neutral
Just a free variable is neutral.
app {Var : Type u} (t1 t2 : Term Var) : t1.Neutral → Relation.SN FullBeta t2 → (t1.app t2).Neutral
Applying a strongly normalizing term to a neutral term yields a neutral term.

Instances For

source

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.neutral_step {Var : Type u} {t t' : Term Var} (Hneut : t.Neutral) (Hstep : t.FullBeta t') :

t'.Neutral

Neutral terms only reduce to other neutral terms in a single step

source

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.neutral_steps {Var : Type u} {t t' : Term Var} (Hneut : t.Neutral) (Hsteps : Relation.ReflTransGen FullBeta t t') :

t'.Neutral

Neutral terms only reduce to other neutral terms in multiple steps

source

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.sn_neutral {Var : Type u} {t : Term Var} (Hneut : t.Neutral) :

Relation.SN FullBeta t

Neutral terms are strongly normalizing.

source

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.sn_abs {Var : Type u} [DecidableEq Var] [HasFresh Var] {M N : Term Var} (sn_MN : Relation.SN FullBeta (M.open' N)) (lc_N : N.LC) :

Relation.SN FullBeta M.abs

A lambda abstraction is strongly normalizing if its body is strongly normalizing.

source

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.sn_abs_app_multiApp {Var : Type u} [DecidableEq Var] [HasFresh Var] {Ps : List (Term Var)} {M N : Term Var} (sn_N : Relation.SN FullBeta N) (sn_MNPs : Relation.SN FullBeta ((M.open' N).multiApp Ps)) (lc_N : N.LC) (lc_MNPs : ((M.open' N).multiApp Ps).LC) :

Relation.SN FullBeta ((M.abs.app N).multiApp Ps)

A term of the form λ M N P_1 … P_n is strongly normalizing if

N is strongly normalizing,
M ^ N P₁ … Pₙ is strongly normalizing,
N is locally closed,
M ^ N P₁ … Pₙ is locally closed