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

structure Cslib.LambdaCalculus.LocallyNameless.Stlc.Saturated {Var : Type u} (S : Set (Untyped.Term Var)) : Prop

A set of terms is called saturated if it

1. only contains locally closed terms,
2. only contains strongly normalizing terms,
3. contains all neutral locally closed terms, and
4. is closed under top-level β-reduction of the form (λ M) N P₁ … Pₙ → M ^ N P₁ … Pₙ.

• lc (M : Untyped.Term Var) : M ∈ S → M.LC
• sn (M : Untyped.Term Var) : M ∈ S → Relation.SN Untyped.Term.FullBeta M
• neutal_lc (M : Untyped.Term Var) : M.Neutral → M.LC → M ∈ S
• multiApp (M N : Untyped.Term Var) (P : List (Untyped.Term Var)) : N.LC → Relation.SN Untyped.Term.FullBeta N → (M.open' N).multiApp P ∈ S → (M.abs.app N).multiApp P ∈ S

def Cslib.LambdaCalculus.LocallyNameless.Stlc.semanticMap {Var : Type u} {Base : Type v} : Ty Base → Set (Untyped.Term Var)

The semantic map maps each type to a corresponding saturated set of terms. For the strong normalization proof to work, we must ensure that Γ ⊢ t ∶ τ implies that t is in the set of terms corresponding to τ.

Strong normalization later follows from the fact that terms in saturated sets are strongly normalizing.

Equations

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

theorem Cslib.LambdaCalculus.LocallyNameless.Stlc.semanticMap_saturated {Var : Type u} {Base : Type v} [DecidableEq Var] [HasFresh Var] (τ : Ty Base) : Saturated (semanticMap τ)

The sets constructed by semanticMap are saturated

@[reducible, inline]

abbrev Cslib.LambdaCalculus.LocallyNameless.Stlc.entailsContext {Var : Type u} {Base : Type v} [DecidableEq Var] (E : Untyped.Term.Env Var) (Γ : Context Var (Ty Base)) : Prop

The entailsContext predicate ensures that each variable in the context is mapped to a term in the corresponding semantic map.

Equations

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

theorem Cslib.LambdaCalculus.LocallyNameless.Stlc.entailsContext_empty {Var : Type u} {Base : Type v} [DecidableEq Var] [HasFresh Var] {Γ : Context Var (Ty Base)} : entailsContext [] Γ

The empty context is entailed by any environment.

theorem Cslib.LambdaCalculus.LocallyNameless.Stlc.entailsContext_cons {Var : Type u} {Base : Type v} [DecidableEq Var] (E : Untyped.Term.Env Var) (Γ : Context Var (Ty Base)) (x : Var) (τ : Ty Base) (sub : Untyped.Term Var) (h_fresh : x ∉ Context.dom E ∪ E.fv ∪ Γ.dom) (h_mem : sub ∈ semanticMap τ) : entailsContext E Γ → entailsContext (⟨x, sub⟩ :: E) (⟨x, τ⟩ :: Γ)

The entailsContext predicate is preserved when extending the context with a new variable, provided the new variable is fresh and its substitution is in the corresponding semantic map.

@[reducible, inline]

abbrev Cslib.LambdaCalculus.LocallyNameless.Stlc.entails {Var : Type u} {Base : Type v} [DecidableEq Var] (Γ : Context Var (Ty Base)) (t : Untyped.Term Var) (τ : Ty Base) : Prop

The entails predicate states that a term t is semantically valid with respect to a context Γ and a type τ

Equations

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

theorem Cslib.LambdaCalculus.LocallyNameless.Stlc.soundness {Var : Type u} {Base : Type v} [DecidableEq Var] [HasFresh Var] {t : Untyped.Term Var} {τ : Ty Base} {Γ : Context Var (Ty Base)} (derivation_t : Typing Γ t τ) : entails Γ t τ

The soundness lemma states that if a term t has type τ in context Γ, then t is semantically valid with respect to Γ and τ

theorem Cslib.LambdaCalculus.LocallyNameless.Stlc.strong_norm {Var : Type u} {Base : Type v} [DecidableEq Var] [HasFresh Var] {Γ : Context Var (Ty Base)} {t : Untyped.Term Var} {τ : Ty Base} (der : Typing Γ t τ) : Relation.SN Untyped.Term.FullBeta t

Using soundness and the fact that the empty context is entailed by any environment, we can conclude that a well-typed term is strongly normalizing.