Normalization by evaluation

DefinitionKripke semantic values#✓fully proved

For a context \(\Gamma\), the semantic values of a simple type in \(\Gamma\) are defined by recursion on the type. At a base type \(b\) they are the neutral terms of type \(b\) in \(\Gamma\) (variables applied to zero or more normal arguments). At an arrow type \(A \Rightarrow B\) a semantic value is a family that, for every context \(\Delta\) and every renaming from \(\Gamma\) to \(\Delta\), maps semantic values of type \(A\) in \(\Delta\) to semantic values of type \(B\) in \(\Delta\).

Because a semantic function acts after every renaming into a later context, reification under a binder needs no untyped weakening operation.

def Sem (Γ : List (Ty Base)) : Ty Base → Type u
  | .base b => Ne Γ (.base b)
  | A ⇒ B => ∀ {Δ}, Ren Γ Δ → Sem Δ A → Sem Δ B

Uses 3 · Used by 16

Statement usesRenamings of simply typed contexts · Simple types · Typed de Bruijn variables of the simply typed lambda calculus

Used byExtending a semantic environment by one variable · The identity environment under a binder · The identity semantic environment · The identity semantic environment realizes every environment · Evaluation into the Kripke semantic domain · Evaluation respects pointwise equal environments · Evaluating a neutral term reflects it · Fundamental lemma for NbE evaluation · Kripke realization relation for NbE · Normalization by evaluation · Normal forms are fixed points of normalization · NbE preserves denotation · Reflection commutes with renaming · Renaming a semantic value · Realization is stable under renaming · Semantic environments for normalization by evaluation

DefinitionRenaming a semantic value#✓fully proved

Given a renaming \(\rho\) from a context \(\Gamma\) to a context \(\Delta\), a simple type \(A\) and a semantic value \(v\) of type \(A\) in \(\Gamma\), the renamed value is the semantic value of type \(A\) in \(\Delta\) defined by cases on \(A\). At a base type it is the neutral term \(v\) with its free variables renamed by \(\rho\). At an arrow type \(A = B \Rightarrow C\) it sends a renaming \(\sigma\) from \(\Delta\) to a context \(\Theta\) and a semantic value \(a\) of type \(B\) in \(\Theta\) to the semantic value of type \(C\) in \(\Theta\) that \(v\) assigns to the composite renaming (\(\rho\) followed by \(\sigma\)) and \(a\).

def rename (ρ : Ren Γ Δ) (A : Ty Base) (v : Sem Γ A) : Sem Δ A :=
  match A with
  | .base _ => Ne.rename ρ v
  | _ ⇒ _ => fun σ a => v (Var.comp ρ σ) a

Uses 6 · Used by 4

Statement usesRenamings of simply typed contexts · Kripke semantic values · Simple types · Typed de Bruijn variables of the simply typed lambda calculus · Composition of renamings of simply typed contexts · Lifting a renaming under a binder

Used byEvaluation respects pointwise equal environments · Reflection commutes with renaming · Renaming a semantic environment · Realization is stable under renaming

AbbreviationSemantic environments for normalization by evaluation#✓fully proved

For contexts \(\Delta\) and \(\Gamma\), a semantic environment for \(\Gamma\) in \(\Delta\) assigns to every variable of \(\Gamma\), of any type \(A\), a Kripke semantic value of type \(A\) in \(\Delta\).

abbrev SemEnv (Δ Γ : List (Ty Base)) := ∀ {A}, Var Γ A → Sem Δ A

Uses 3 · Used by 8

Statement usesKripke semantic values · Simple types · Typed de Bruijn variables of the simply typed lambda calculus

Used byExtending a semantic environment by one variable · The identity environment under a binder · The identity semantic environment · Realization of environments · Evaluation into the Kripke semantic domain · Evaluation respects pointwise equal environments · Fundamental lemma for NbE evaluation · Renaming a semantic environment

DefinitionRenaming a semantic environment#✓fully proved

Given a renaming \(\rho\) from a context \(\Delta\) to a context \(\Theta\) and a semantic environment \(\eta\) for \(\Gamma\) in \(\Delta\), the renamed environment is the semantic environment for \(\Gamma\) in \(\Theta\) that sends each variable \(x\) of type \(A\) to the semantic value \(\eta(x)\) renamed along \(\rho\) at type \(A\).

def rename (ρ : Ren Δ Θ) (η : SemEnv Δ Γ) : SemEnv Θ Γ :=
  fun {A} x => Sem.rename ρ A (η x)

Uses 5 · Used by 6

Statement usesRenamings of simply typed contexts · Renaming a semantic value · Semantic environments for normalization by evaluation · Simple types · Typed de Bruijn variables of the simply typed lambda calculus

Used byThe identity environment under a binder · Evaluation into the Kripke semantic domain · Evaluation respects pointwise equal environments · Evaluating a neutral term reflects it · Fundamental lemma for NbE evaluation · Normal forms are fixed points of normalization

DefinitionExtending a semantic environment by one variable#✓fully proved

Given a semantic value \(a\) of type \(A\) in a context \(\Delta\) and a semantic environment \(\eta\) for \(\Gamma\) in \(\Delta\), the extended environment is the semantic environment for the context \(A :: \Gamma\) (the context \(\Gamma\) with a new innermost variable of type \(A\)) in \(\Delta\) that sends the new innermost variable to \(a\) and sends the successor of each variable \(x\) of \(\Gamma\) to \(\eta(x)\).

def cons (a : Sem Δ A) (η : SemEnv Δ Γ) : SemEnv Δ (A :: Γ)
  | _, .zero => a
  | _, .succ x => η x

Uses 4 · Used by 6

Statement usesKripke semantic values · Semantic environments for normalization by evaluation · Simple types · Typed de Bruijn variables of the simply typed lambda calculus

Used byThe identity environment under a binder · Evaluation into the Kripke semantic domain · Evaluation respects pointwise equal environments · Evaluating a neutral term reflects it · Fundamental lemma for NbE evaluation · Normal forms are fixed points of normalization

DefinitionThe identity semantic environment#✓fully proved

For a context \(\Gamma\), the identity environment is the semantic environment for \(\Gamma\) in \(\Gamma\) that sends each variable \(x\) of type \(A\) to the reflection at type \(A\) of the neutral term \(x\). Reflection turns a neutral term into a semantic value of the same type in the same context.

def identity : SemEnv Γ Γ := fun {A} x => reflect A (.var x)

Uses 6 · Used by 6

Statement usesRenamings of simply typed contexts · Kripke semantic values · Semantic environments for normalization by evaluation · Simple types · Typed de Bruijn variables of the simply typed lambda calculus · Lifting a renaming under a binder

Used byThe identity environment under a binder · The identity semantic environment realizes every environment · Evaluating a neutral term reflects it · Normalization by evaluation · Normal forms are fixed points of normalization · NbE preserves denotation

DefinitionEvaluation into the Kripke semantic domain#✓fully proved

Let \(t\) be a term of type \(T\) in context \(\Gamma\) and let \(\eta\) be a semantic environment interpreting every variable of \(\Gamma\) as a semantic value in context \(\Delta\). The evaluation \(\operatorname{ev}(t, \eta)\) is the semantic value of type \(T\) in context \(\Delta\) defined by recursion on \(t\): a variable \(x\) evaluates to \(\eta(x)\); an application \(f\,a\) evaluates to the semantic function \(\operatorname{ev}(f, \eta)\) applied, along the identity renaming of \(\Delta\), to \(\operatorname{ev}(a, \eta)\); and an abstraction \(\lambda b\) of type \(A \to B\), whose body \(b\) lies in the context \(\Gamma\) extended by \(A\), evaluates to the semantic function that sends a renaming \(\rho\) from \(\Delta\) to a context \(\Theta\) and a semantic value \(a\) of type \(A\) in \(\Theta\) to \(\operatorname{ev}(b, \eta')\), where \(\eta'\) sends the new variable to \(a\) and each variable \(x\) of \(\Gamma\) to \(\eta(x)\) renamed along \(\rho\).

def nbeEval : {Γ Δ : List (Ty Base)} → {A : Ty Base} →
    Tm Γ A → SemEnv Δ Γ → Sem Δ A
  | _, _, _, .var x, η => η x
  | _, _, _, .app f a, η => nbeEval f η Var.id (nbeEval a η)
  | _, _, _, .lam body, η => fun ρ a =>
      nbeEval body (SemEnv.cons a (SemEnv.rename ρ η))

Uses 9 · Used by 6

Statement usesRenamings of simply typed contexts · Kripke semantic values · Semantic environments for normalization by evaluation · Extending a semantic environment by one variable · Renaming a semantic environment · Intrinsically typed terms of the simply typed lambda calculus · Simple types · Typed de Bruijn variables of the simply typed lambda calculus · Identity renaming of a simply typed context

Used byEvaluation respects pointwise equal environments · Evaluating a neutral term reflects it · Fundamental lemma for NbE evaluation · Normalization by evaluation · Normal forms are fixed points of normalization · NbE preserves denotation

DefinitionNormalization by evaluation#✓fully proved

For a term \(t\) of type \(A\) in context \(\Gamma\), its normal form is the beta-normal, eta-long term of type \(A\) in context \(\Gamma\) obtained by reifying, at type \(A\), the evaluation of \(t\) in the identity semantic environment of \(\Gamma\), which interprets each variable as the reflection of that variable.

def normalizeNf (t : Tm Γ A) : Nf Γ A := quote A (nbeEval t SemEnv.identity)

Uses 8 · Used by 12

Statement usesRenamings of simply typed contexts · Kripke semantic values · The identity semantic environment · Intrinsically typed terms of the simply typed lambda calculus · Simple types · Typed de Bruijn variables of the simply typed lambda calculus · Lifting a renaming under a binder · Evaluation into the Kripke semantic domain

Used byCanonical terms are the fixed points of normalization · Evaluating a neutral term reflects it · Normal forms are fixed points of normalization · Normalization of terms · Renormalizing a computed normal form · Normalization fixes the terms of normal forms · The normal form of a canonical term · Erasing normal forms is injective · Raw normalization of an erased term · Raw normalization produces well-typed terms · Raw normalization is idempotent · Raw normalization reports the inferred type

DefinitionNormalization of terms#✓fully proved

For a term \(t\) of type \(A\) in context \(\Gamma\), its normalized term is the term of type \(A\) in context \(\Gamma\) underlying the beta-normal, eta-long normal form of \(t\) computed by normalization by evaluation.

def normalizeTm (t : Tm Γ A) : Tm Γ A := (normalizeNf t).toTm

Uses 4 · Used by 17

Statement usesIntrinsically typed terms of the simply typed lambda calculus · Simple types · Typed de Bruijn variables of the simply typed lambda calculus · Normalization by evaluation

Used byCertified canonical terms · Canonical terms are the fixed points of normalization · Normalized terms are canonical · Equal NbE normal forms imply model equality · NbE preserves denotation · Normalization by evaluation is idempotent · Every term is model-equal to its NbE normal form · Renormalizing a computed normal form · Every term is semantically equal to its NbE normal form in each model · Normalization fixes the terms of normal forms · Normal forms as canonical terms · The normal form of a canonical term · Normalization of raw terms · Raw normalization of an erased term · Raw normalization produces well-typed terms · Raw normalization is idempotent · Raw normalization reports the inferred type

TheoremReflection commutes with renaming#✓fully proved

For every type \(A\), every renaming \(\rho\) from a context \(\Gamma\) to a context \(\Delta\), and every neutral term \(n\) of type \(A\) in context \(\Gamma\), transporting the semantic value obtained by reflecting \(n\) at type \(A\) along \(\rho\) gives the reflection at type \(A\) of the neutral term \(n\) renamed by \(\rho\).

theorem reflect_rename (A : Ty Base) (ρ : Ren Γ Δ) (n : Ne Γ A) :
    Sem.rename ρ A (reflect A n) = reflect A (n.rename ρ)

Uses 7 · Used by 1

Statement usesRenamings of simply typed contexts · Kripke semantic values · Renaming a semantic value · Simple types · Typed de Bruijn variables of the simply typed lambda calculus · Lifting a renaming under a binder

Proof usesComposition of renamings of simply typed contexts

Used byThe identity environment under a binder

TheoremThe identity environment under a binder#✓fully proved

Let \(\Gamma\) be a context, \(A\) a type, and \(\Gamma, A\) the context \(\Gamma\) extended by a newest variable of type \(A\). Transport the identity semantic environment of \(\Gamma\) (which reflects each variable as a neutral value) along the weakening renaming from \(\Gamma\) to \(\Gamma, A\) that sends each variable to its successor, and extend the result by the reflection at type \(A\) of the newest variable of \(\Gamma, A\). The resulting semantic environment equals the identity semantic environment of \(\Gamma, A\).

theorem SemEnv.cons_reflect_rename_identity :
    @SemEnv.cons Base A Γ (A :: Γ) (reflect A (.var .zero))
        (SemEnv.rename (.succ : Ren Γ (A :: Γ)) SemEnv.identity) =
      @SemEnv.identity Base (A :: Γ)

Uses 10 · Used by 2

Statement usesRenamings of simply typed contexts · Kripke semantic values · Semantic environments for normalization by evaluation · Extending a semantic environment by one variable · The identity semantic environment · Renaming a semantic environment · Simple types · Typed de Bruijn variables of the simply typed lambda calculus · Lifting a renaming under a binder

Proof usesReflection commutes with renaming

Used byEvaluating a neutral term reflects it · Normal forms are fixed points of normalization

TheoremEvaluation respects pointwise equal environments#✓fully proved

Let \(t\) be a term of type \(A\) in context \(\Gamma\), and let \(\xi\) and \(\zeta\) be semantic environments interpreting the variables of \(\Gamma\) in a context \(\Delta\). If \(\xi(x) = \zeta(x)\) for every variable \(x\) of \(\Gamma\), of any type, then evaluating \(t\) in \(\xi\) and evaluating \(t\) in \(\zeta\) give the same semantic value.

theorem nbeEval_congr (t : Tm Γ A) {ξ ζ : SemEnv Δ Γ}
    (h : ∀ {B} (x : Var Γ B), ξ x = ζ x) : nbeEval t ξ = nbeEval t ζ

Uses 11 · Used by 2

Statement usesKripke semantic values · Semantic environments for normalization by evaluation · Intrinsically typed terms of the simply typed lambda calculus · Simple types · Typed de Bruijn variables of the simply typed lambda calculus · Evaluation into the Kripke semantic domain

Proof usesRenamings of simply typed contexts · Renaming a semantic value · Extending a semantic environment by one variable · Renaming a semantic environment · Identity renaming of a simply typed context

Used byEvaluating a neutral term reflects it · Normal forms are fixed points of normalization

TheoremEvaluating a neutral term reflects it#✓fully proved

For every neutral term \(n\) of type \(A\) in context \(\Gamma\), evaluating the underlying term of \(n\) in the identity semantic environment of \(\Gamma\) gives the reflection of \(n\) at type \(A\).

theorem nbeEval_ne_toTm (n : Ne Γ A) :
    nbeEval n.toTm SemEnv.identity = reflect A n

Uses 14

Statement usesRenamings of simply typed contexts · Kripke semantic values · The identity semantic environment · Intrinsically typed terms of the simply typed lambda calculus · Simple types · Typed de Bruijn variables of the simply typed lambda calculus · Lifting a renaming under a binder · Evaluation into the Kripke semantic domain

Proof usesExtending a semantic environment by one variable · The identity environment under a binder · Renaming a semantic environment · Identity renaming of a simply typed context · Evaluation respects pointwise equal environments · Normalization by evaluation

TheoremNormal forms are fixed points of normalization#✓fully proved

For every beta-normal, eta-long normal form \(n\) of type \(A\) in context \(\Gamma\), normalizing the underlying term of \(n\) by evaluation returns the normal form \(n\) itself.

@[simp] theorem normalizeNf_toTm (n : Nf Γ A) : normalizeNf n.toTm = n

Uses 14 · Used by 4

Statement usesIntrinsically typed terms of the simply typed lambda calculus · Simple types · Typed de Bruijn variables of the simply typed lambda calculus · Normalization by evaluation

Proof usesRenamings of simply typed contexts · Kripke semantic values · Extending a semantic environment by one variable · The identity environment under a binder · The identity semantic environment · Renaming a semantic environment · Identity renaming of a simply typed context · Lifting a renaming under a binder · Evaluation into the Kripke semantic domain · Evaluation respects pointwise equal environments

Used byRenormalizing a computed normal form · Normalization fixes the terms of normal forms · Erasing normal forms is injective · Raw normalization is idempotent

TheoremRenormalizing a computed normal form#✓fully proved

For every term \(t\) of type \(A\) in context \(\Gamma\), normalizing the underlying term of the normal form that normalization by evaluation computes from \(t\) gives the same term as normalizing \(t\).

@[simp] theorem normalizeTm_normalizeNf (t : Tm Γ A) :
    normalizeTm (normalizeNf t).toTm = normalizeTm t

Uses 6 · Used by 1

Statement usesIntrinsically typed terms of the simply typed lambda calculus · Simple types · Typed de Bruijn variables of the simply typed lambda calculus · Normalization by evaluation · Normalization of terms

Proof usesNormal forms are fixed points of normalization

Used byNormalization by evaluation is idempotent

TheoremNormalization by evaluation is idempotent#✓fully proved

For every term \(t\) of type \(A\) in context \(\Gamma\), normalizing the normalized term of \(t\) by evaluation gives the normalized term of \(t\) again.

@[simp] theorem normalizeTm_idem (t : Tm Γ A) :
    normalizeTm (normalizeTm t) = normalizeTm t

Uses 4 · Used by 1

Statement usesIntrinsically typed terms of the simply typed lambda calculus · Simple types · Normalization of terms

Proof usesRenormalizing a computed normal form

Used byNormalized terms are canonical

TheoremNormalization fixes the terms of normal forms#✓fully proved

For every eta-long normal form \(n\) of type \(A\) in context \(\Gamma\), normalizing the underlying term of \(n\) returns that term unchanged.

@[simp] theorem normalizeTm_toTm (n : Nf Γ A) : normalizeTm n.toTm = n.toTm

Uses 6 · Used by 2

Statement usesIntrinsically typed terms of the simply typed lambda calculus · Simple types · Typed de Bruijn variables of the simply typed lambda calculus · Normalization of terms

Proof usesNormalization by evaluation · Normal forms are fixed points of normalization

Used byCanonical terms are the fixed points of normalization · Normal forms as canonical terms

TheoremErasing normal forms is injective#✓fully proved

For every context \(\Gamma\) and type \(A\), two eta-long normal forms of type \(A\) in context \(\Gamma\) with the same underlying term are equal.

NbE gives an explicit left inverse, so no separate syntactic injectivity argument is needed.

theorem Nf.toTm_injective : Function.Injective (@Nf.toTm Base Γ A)

Uses 5 · Used by 1

Statement usesIntrinsically typed terms of the simply typed lambda calculus · Simple types · Typed de Bruijn variables of the simply typed lambda calculus

Proof usesNormalization by evaluation · Normal forms are fixed points of normalization

Used byCanonical terms have a unique normal form

DefinitionCanonical terms#✓fully proved

A term \(t\) of type \(A\) in context \(\Gamma\) is canonical when it is the underlying term of some beta-normal, eta-long normal form of type \(A\) in context \(\Gamma\).

def IsCanonical (t : Tm Γ A) : Prop := ∃ n : Nf Γ A, n.toTm = t

Uses 3 · Used by 4

Statement usesIntrinsically typed terms of the simply typed lambda calculus · Simple types · Typed de Bruijn variables of the simply typed lambda calculus

Used byCanonical terms have a unique normal form · Canonical terms are the fixed points of normalization · Normalized terms are canonical · Renaming preserves canonical terms

TheoremCanonical terms are the fixed points of normalization#✓fully proved

A term \(t\) of type \(A\) in context \(\Gamma\) is canonical if and only if normalization by evaluation maps \(t\) to itself, that is, the term underlying the normal form computed for \(t\) is \(t\).

theorem isCanonical_iff_normalizeTm_eq (t : Tm Γ A) :
    IsCanonical t ↔ normalizeTm t = t

Uses 7 · Used by 1

Statement usesCanonical terms · Intrinsically typed terms of the simply typed lambda calculus · Simple types · Normalization of terms

Proof usesTyped de Bruijn variables of the simply typed lambda calculus · Normalization by evaluation · Normalization fixes the terms of normal forms

Used byNormalized terms are canonical

TheoremNormalized terms are canonical#✓fully proved

For every term \(t\) of type \(A\) in context \(\Gamma\), the term obtained by normalizing \(t\) by evaluation is canonical.

theorem isCanonical_normalizeTm (t : Tm Γ A) : IsCanonical (normalizeTm t)

Uses 6

Statement usesCanonical terms · Intrinsically typed terms of the simply typed lambda calculus · Simple types · Normalization of terms

Proof usesCanonical terms are the fixed points of normalization · Normalization by evaluation is idempotent

TheoremRenaming preserves canonical terms#✓fully proved

If a term \(t\) of type \(A\) in context \(\Gamma\) is canonical, then for every renaming \(\rho\) from \(\Gamma\) to a context \(\Delta\), the term obtained by renaming \(t\) along \(\rho\) is canonical.

theorem IsCanonical.rename {t : Tm Γ A} (h : IsCanonical t) (ρ : Ren Γ Δ) :
    IsCanonical (Tm.rename ρ t)

Uses 7

Statement usesCanonical terms · Renamings of simply typed contexts · Intrinsically typed terms of the simply typed lambda calculus · Renaming a simply typed term · Simple types

Proof usesTyped de Bruijn variables of the simply typed lambda calculus · Lifting a renaming under a binder

AbbreviationCertified canonical terms#✓fully proved

For a context \(\Gamma\) and a type \(A\), a certified canonical term of type \(A\) in context \(\Gamma\) is a term \(t\) of type \(A\) in context \(\Gamma\) together with a proof that \(t\) is a fixed point of normalization by evaluation: the term underlying the normal form computed for \(t\) is \(t\) itself.

abbrev CanonicalTm (Γ : List (Ty Base)) (A : Ty Base) :=
  {t : Tm Γ A // normalizeTm t = t}

Uses 3 · Used by 2

Statement usesIntrinsically typed terms of the simply typed lambda calculus · Simple types · Normalization of terms

Used byNormal forms as canonical terms · The normal form of a canonical term

DefinitionNormal forms as canonical terms#✓fully proved

The canonical term of an eta-long normal form \(n\) of type \(A\) in context \(\Gamma\) is the underlying term of \(n\), certified to be a fixed point of normalization.

def Nf.toCanonicalTm (n : Nf Γ A) : CanonicalTm Γ A :=
  ⟨n.toTm, normalizeTm_toTm n⟩

Uses 6

Statement usesCertified canonical terms · Intrinsically typed terms of the simply typed lambda calculus · Simple types · Typed de Bruijn variables of the simply typed lambda calculus · Normalization of terms · Normalization fixes the terms of normal forms

DefinitionThe normal form of a canonical term#✓fully proved

For a canonical term \(t\) of type \(A\) in context \(\Gamma\), that is, a term that normalization returns unchanged, its normal form is the eta-long normal form that normalization by evaluation computes from \(t\).

def CanonicalTm.toNf (t : CanonicalTm Γ A) : Nf Γ A := normalizeNf t.1

Uses 5

Statement usesCertified canonical terms · Intrinsically typed terms of the simply typed lambda calculus · Simple types · Normalization by evaluation · Normalization of terms

TheoremCanonical terms have a unique normal form#✓fully proved

Let \(t\) be a term of type \(A\) in context \(\Gamma\). If \(t\) is canonical, then there is exactly one beta-normal, eta-long normal form of type \(A\) in context \(\Gamma\) whose underlying term is \(t\).

theorem isCanonical_existsUniqueNf {t : Tm Γ A} (h : IsCanonical t) :
    ∃ n : Nf Γ A, n.toTm = t ∧ ∀ m : Nf Γ A, m.toTm = t → m = n

Uses 5

Statement usesCanonical terms · Intrinsically typed terms of the simply typed lambda calculus · Simple types · Typed de Bruijn variables of the simply typed lambda calculus

Proof usesErasing normal forms is injective

DefinitionKripke realization relation for NbE#✓fully proved

Fix an interpretation \(I\) of the base types. For a context \(\Gamma\), an environment \(\eta\) for \(\Gamma\) in \(I\), a type \(A\), a Kripke semantic value \(v\) of type \(A\) in \(\Gamma\) and an element \(d\) of the denotation of \(A\) under \(I\), the relation "\(v\) realizes \(d\) at \(\eta\)" is defined by recursion on \(A\). At a base type, \(v\) is a neutral term, and \(v\) realizes \(d\) when the denotation of \(v\), read as a term, in \(\eta\) equals \(d\). At a function type \(A \Rightarrow B\), \(v\) realizes \(d\) when for every context \(\Delta\), every renaming \(\rho : \Gamma \to \Delta\), every environment \(\theta\) for \(\Delta\) with \(\theta \circ \rho = \eta\), every semantic value \(a\) of type \(A\) in \(\Delta\) and every element \(e\) of the denotation of \(A\) such that \(a\) realizes \(e\) at \(\theta\), the semantic value \(v(\rho, a)\) realizes \(d(e)\) at \(\theta\).

def NbeRelated (I : Base → Type v) : {Γ : List (Ty Base)} →
    Env I Γ → (A : Ty Base) → Sem Γ A → Ty.denote I A → Prop
  | _, η, .base _, n, d => Tm.denote I n.toTm (@η) = d
  | Γ, η, A ⇒ B, f, d => ∀ {Δ} (ρ : Ren Γ Δ) (θ : Env I Δ),
      @Env.rename Base Γ Δ I ρ θ = @η → ∀ (a : Sem Δ A) (da : Ty.denote I A),
      NbeRelated I (@θ) A a da → NbeRelated I (@θ) B (f ρ a) (d da)

Uses 9 · Used by 5

Statement usesSemantic environments for the denotational semantics of STLC · Renaming an environment · Renamings of simply typed contexts · Kripke semantic values · Intrinsically typed terms of the simply typed lambda calculus · Denotation of an STLC term · Simple types · Denotation of simple types · Typed de Bruijn variables of the simply typed lambda calculus

Used byThe identity semantic environment realizes every environment · Realization of environments · Fundamental lemma for NbE evaluation · NbE preserves denotation · Realization is stable under renaming

TheoremRealization is stable under renaming#✓fully proved

Fix an interpretation \(I\) of the base types. Let \(v\) be a Kripke semantic value of type \(A\) in context \(\Gamma\) that realizes an element \(d\) of the denotation of \(A\) at an environment \(\eta\) for \(\Gamma\). If \(\rho : \Gamma \to \Delta\) is a renaming and \(\theta\) is an environment for \(\Delta\) with \(\theta \circ \rho = \eta\), then the transport of \(v\) along \(\rho\) realizes \(d\) at \(\theta\).

theorem NbeRelated.rename (h : NbeRelated I (@η) A v d) (ρ : Ren Γ Δ)
    (θ : Env I Δ) (hθ : @Env.rename Base Γ Δ I ρ θ = @η) :
    NbeRelated I (@θ) A (Sem.rename ρ A v) d

Uses 15 · Used by 1

Statement usesSemantic environments for the denotational semantics of STLC · Renaming an environment · Kripke realization relation for NbE · Renamings of simply typed contexts · Kripke semantic values · Renaming a semantic value · Simple types · Denotation of simple types

Proof usesIntrinsically typed terms of the simply typed lambda calculus · Denotation of an STLC term · Renaming lemma for STLC denotation · Renaming a simply typed term · Typed de Bruijn variables of the simply typed lambda calculus · Composition of renamings of simply typed contexts · Lifting a renaming under a binder

Used byFundamental lemma for NbE evaluation

DefinitionRealization of environments#✓fully proved

Fix an interpretation \(I\) of the base types, contexts \(\Delta\) and \(\Gamma\), an environment \(\theta\) for \(\Delta\) in \(I\), a Kripke semantic environment \(\xi\) assigning to each variable of \(\Gamma\) a semantic value in \(\Delta\), and an environment \(\eta\) for \(\Gamma\) in \(I\). Then \(\xi\) realizes \(\eta\) at \(\theta\) when for every type \(A\) and every variable \(x\) of type \(A\) in \(\Gamma\), the semantic value \(\xi(x)\) realizes \(\eta(x)\) at \(\theta\).

def NbeEnvRelated (I : Base → Type v) (θ : Env I Δ)
    (ξ : SemEnv Δ Γ) (η : Env I Γ) : Prop :=
  ∀ {A} (x : Var Γ A), NbeRelated I (@θ) A (ξ x) (η x)

Uses 5 · Used by 2

Statement usesSemantic environments for the denotational semantics of STLC · Kripke realization relation for NbE · Semantic environments for normalization by evaluation · Simple types · Typed de Bruijn variables of the simply typed lambda calculus

Used byThe identity semantic environment realizes every environment · Fundamental lemma for NbE evaluation

TheoremFundamental lemma for NbE evaluation#✓fully proved

Fix an interpretation \(I\) of the base types. Let \(t\) be a term of type \(A\) in context \(\Gamma\), let \(\xi\) be a Kripke semantic environment assigning to each variable of \(\Gamma\) a semantic value in context \(\Delta\), and let \(\eta\) and \(\theta\) be environments in \(I\) for \(\Gamma\) and \(\Delta\). If \(\xi\) realizes \(\eta\) at \(\theta\), then the NbE evaluation of \(t\) in \(\xi\) realizes the denotation of \(t\) in \(\eta\) at \(\theta\).

theorem nbeEval_related (t : Tm Γ A) (ξ : SemEnv Δ Γ)
    (η : Env I Γ) (θ : Env I Δ) (hξ : NbeEnvRelated I θ ξ η) :
    NbeRelated I (@θ) A (nbeEval t ξ) (Tm.denote I t (@η))

Uses 18 · Used by 1

Statement usesSemantic environments for the denotational semantics of STLC · Realization of environments · Kripke realization relation for NbE · Semantic environments for normalization by evaluation · Intrinsically typed terms of the simply typed lambda calculus · Denotation of an STLC term · Simple types · Evaluation into the Kripke semantic domain

Proof usesExtending a semantic environment in STLC · Renaming an environment · Realization is stable under renaming · Renamings of simply typed contexts · Kripke semantic values · Extending a semantic environment by one variable · Renaming a semantic environment · Denotation of simple types · Typed de Bruijn variables of the simply typed lambda calculus · Identity renaming of a simply typed context

Used byNbE preserves denotation

TheoremThe identity semantic environment realizes every environment#✓fully proved

Fix an interpretation \(I\) of the base types and an environment \(\eta\) for a context \(\Gamma\) in \(I\). Then the identity Kripke semantic environment on \(\Gamma\), which reflects each variable as a neutral value, realizes \(\eta\) at \(\eta\).

theorem identity_related (η : Env I Γ) :
    NbeEnvRelated I η SemEnv.identity η

Uses 16 · Used by 1

Statement usesSemantic environments for the denotational semantics of STLC · Realization of environments · The identity semantic environment · Simple types

Proof usesExtending a semantic environment in STLC · Renaming an environment · Kripke realization relation for NbE · Renamings of simply typed contexts · Kripke semantic values · Intrinsically typed terms of the simply typed lambda calculus · Denotation of an STLC term · Renaming lemma for STLC denotation · Renaming a simply typed term · Denotation of simple types · Typed de Bruijn variables of the simply typed lambda calculus · Lifting a renaming under a binder

Used byNbE preserves denotation

TheoremNbE preserves denotation#✓fully proved

For every interpretation \(I\) of the base types, every term \(t\) of type \(A\) in context \(\Gamma\) and every environment \(\eta\) for \(\Gamma\) in \(I\), the NbE normal form of \(t\) has the same denotation in \(\eta\) as \(t\).

theorem normalizeTm_denote (I : Base → Type v) (t : Tm Γ A) (η : Env I Γ) :
    Tm.denote I (normalizeTm t) η = Tm.denote I t η

Uses 19 · Used by 1

Statement usesSemantic environments for the denotational semantics of STLC · Intrinsically typed terms of the simply typed lambda calculus · Denotation of an STLC term · Simple types · Denotation of simple types · Normalization of terms

Proof usesExtending a semantic environment in STLC · Renaming an environment · Kripke realization relation for NbE · Renamings of simply typed contexts · Kripke semantic values · The identity semantic environment · Renaming lemma for STLC denotation · Renaming a simply typed term · Typed de Bruijn variables of the simply typed lambda calculus · Lifting a renaming under a binder · The identity semantic environment realizes every environment · Evaluation into the Kripke semantic domain · Fundamental lemma for NbE evaluation

Used byEvery term is semantically equal to its NbE normal form in each model

TheoremEvery term is semantically equal to its NbE normal form in each model#✓fully proved

For every interpretation \(I\) of the base types and every term \(t\) of type \(A\) in context \(\Gamma\), \(t\) and its NbE normal form are semantically equal in \(I\): they have the same denotation in every environment for \(\Gamma\) in \(I\).

theorem normalizeTm_semEq (I : Base → Type v) (t : Tm Γ A) :
    SemEq I t (normalizeTm t)

Uses 8 · Used by 1

Statement usesSemantic equality of terms in a model · Intrinsically typed terms of the simply typed lambda calculus · Simple types · Normalization of terms

Proof usesSemantic environments for the denotational semantics of STLC · Denotation of an STLC term · Denotation of simple types · NbE preserves denotation

Used byEvery term is model-equal to its NbE normal form

TheoremEvery term is model-equal to its NbE normal form#✓fully proved

Every term \(t\) of type \(A\) in context \(\Gamma\) is model-equal to its NbE normal form.

theorem normalizeTm_modelEq (t : Tm Γ A) : ModelEq t (normalizeTm t)

Uses 5 · Used by 1

Statement usesModel equality of STLC terms · Intrinsically typed terms of the simply typed lambda calculus · Simple types · Normalization of terms

Proof usesEvery term is semantically equal to its NbE normal form in each model

Used byEqual NbE normal forms imply model equality

TheoremEqual NbE normal forms imply model equality#✓fully proved

If two terms \(t\) and \(u\) of type \(A\) in context \(\Gamma\) have the same NbE normal form, then \(t\) and \(u\) are model-equal.

Equality of computed normal forms is thus a sound test for model equality; no converse is claimed.

theorem modelEq_of_normalizeTm_eq {t u : Tm Γ A}
    (h : normalizeTm t = normalizeTm u) : ModelEq t u

Uses 8

Statement usesModel equality of STLC terms · Intrinsically typed terms of the simply typed lambda calculus · Simple types · Normalization of terms

Proof usesSemantic equality is reflexive · Symmetry of semantic equality of terms · Transitivity of semantic equality of terms · Every term is model-equal to its NbE normal form

35 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.