Denotational semantics of the simply typed lambda calculus

DefinitionDenotation of simple types#✓fully proved

Given an interpretation \(I\) assigning a type \(I(b)\) to each base type \(b\), the denotation \([\![A]\!]_I\) of a simple type \(A\) is defined by recursion on \(A\): a base type \(b\) denotes \(I(b)\), and a function type \(A \Rightarrow B\) denotes the type of all functions from \([\![A]\!]_I\) to \([\![B]\!]_I\).

def denote (I : Base → Type v) : Ty Base → Type v
  | .base b => I b
  | .arr A B => denote I A → denote I B

Uses 1 · Used by 40

Statement usesSimple types

Used byRelated computations in the call-by-name CPS translation · Denotational correctness of the call-by-name CPS translation · The call-by-name CPS translation at base types · Running the call-by-name CPS translation with the identity continuation · Logical relation for the call-by-name CPS translation · Denotational correctness of the CPS translation (Meyer–Wand) · CPS translation at a base type · CPS translation at a base type with the identity continuation · Logical relation for the CPS translation · Semantic equality is a congruence for application · Beta is sound for the denotational semantics · Extending a semantic environment in STLC · Denotation of an STLC term · One reduction step preserves STLC denotation · Multi-step reduction preserves STLC denotation · Big-step evaluation preserves STLC denotation · Denotation of an instantiated STLC body · Renaming lemma for STLC denotation · Substitution lemma for STLC denotation · Weakening preserves STLC denotation · Semantic environments for the denotational semantics of STLC · Eta is sound for the denotational semantics · Semantic equality is a congruence for lambda abstraction · Semantic equality is reflexive · Pointwise semantic equality of substitutions is reflexive · Renaming preserves semantic equality · Semantic equality of terms in a model · Pointwise semantic equality of substitutions · Substitution preserves semantic equality · Semantically equal substitutions give semantically equal results · Symmetry of semantic equality of terms · Symmetry of pointwise semantic equality of substitutions · Transitivity of semantic equality of terms · Transitivity of pointwise semantic equality of substitutions · The identity semantic environment realizes every environment · Fundamental lemma for NbE evaluation · Kripke realization relation for NbE · NbE preserves denotation · Every term is semantically equal to its NbE normal form in each model · Realization is stable under renaming

AbbreviationSemantic environments for the denotational semantics of STLC#✓fully proved

Given an interpretation \(I\) assigning a type to each base type and a typing context \(\Gamma\) (a list of simple types), an environment for \(\Gamma\) assigns to every variable \(x\) of \(\Gamma\), of any simple type \(A\), an element of the denotation \([\![A]\!]_I\).

abbrev Env (I : Base → Type v) (Γ : List (Ty Base)) :=
  ∀ {A}, Var Γ A → Ty.denote I A

Uses 3 · Used by 43

Statement usesSimple types · Denotation of simple types · Typed de Bruijn variables of the simply typed lambda calculus

Used byDenotational correctness of the call-by-name CPS translation · The call-by-name CPS translation at base types · Running the call-by-name CPS translation with the identity continuation · Related environments for the call-by-name CPS translation · Denotational correctness of the CPS translation (Meyer–Wand) · CPS translation at a base type · CPS translation at a base type with the identity continuation · Related environments · Semantic equality is a congruence for application · Beta is sound for the denotational semantics · Extending a semantic environment in STLC · Denotation of an STLC term · One reduction step preserves STLC denotation · Multi-step reduction preserves STLC denotation · Big-step evaluation preserves STLC denotation · Denotation of an instantiated STLC body · Renaming lemma for STLC denotation · Denotation of an STLC substitution · Substitution lemma for STLC denotation · Weakening preserves STLC denotation · Eta is sound for the denotational semantics · Semantic equality is a congruence for lambda abstraction · Single-step evaluation is a semantic equation · Multi-step evaluation is a semantic equation · Semantic equality is reflexive · Pointwise semantic equality of substitutions is reflexive · Renaming an environment · Renaming preserves semantic equality · Semantic equality of terms in a model · Pointwise semantic equality of substitutions · Substitution preserves semantic equality · Semantically equal substitutions give semantically equal results · Symmetry of semantic equality of terms · Symmetry of pointwise semantic equality of substitutions · Transitivity of semantic equality of terms · Transitivity of pointwise semantic equality of substitutions · The identity semantic environment realizes every environment · Realization of environments · Fundamental lemma for NbE evaluation · Kripke realization relation for NbE · NbE preserves denotation · Every term is semantically equal to its NbE normal form in each model · Realization is stable under renaming

DefinitionExtending a semantic environment in STLC#✓fully proved

Given an interpretation \(I\) of the base types, a value \(a\) in the denotation of a type \(A\) and an environment \(\eta\) for a context \(\Gamma\), the extended environment for the context \(A :: \Gamma\) sends the newest variable to \(a\) and the successor \(\mathrm{succ}\,x\) of each variable \(x\) of \(\Gamma\) to \(\eta(x)\).

def cons (a : Ty.denote I A) (η : Env I Γ) : Env I (A :: Γ)
  | _, .zero => a
  | _, .succ x => η x

Uses 4 · Used by 14

Statement usesSemantic environments for the denotational semantics of STLC · Simple types · Denotation of simple types · Typed de Bruijn variables of the simply typed lambda calculus

Used byDenotational correctness of the call-by-name CPS translation · Denotational correctness of the CPS translation (Meyer–Wand) · Beta is sound for the denotational semantics · Denotation of an STLC term · One reduction step preserves STLC denotation · Denotation of an instantiated STLC body · Renaming lemma for STLC denotation · Substitution lemma for STLC denotation · Weakening preserves STLC denotation · Eta is sound for the denotational semantics · Semantic equality is a congruence for lambda abstraction · The identity semantic environment realizes every environment · Fundamental lemma for NbE evaluation · NbE preserves denotation

DefinitionRenaming an environment#✓fully proved

Given a renaming \(\rho\) from context \(\Gamma\) to context \(\Delta\) (a type-preserving map from the variables of \(\Gamma\) to those of \(\Delta\)) and an environment \(\eta\) for \(\Delta\), the renamed environment for \(\Gamma\) sends each variable \(x\) of \(\Gamma\) to \(\eta(\rho(x))\); that is, it is the composite \(\eta \circ \rho\).

def rename (ρ : Ren Γ Δ) (η : Env I Δ) : Env I Γ := fun x ↦ η (ρ x)

Uses 4 · Used by 8

Statement usesSemantic environments for the denotational semantics of STLC · Renamings of simply typed contexts · Simple types · Typed de Bruijn variables of the simply typed lambda calculus

Used byRenaming lemma for STLC denotation · Weakening preserves STLC denotation · Renaming preserves semantic equality · The identity semantic environment realizes every environment · Fundamental lemma for NbE evaluation · Kripke realization relation for NbE · NbE preserves denotation · Realization is stable under renaming

DefinitionDenotation of an STLC term#✓fully proved

Given an interpretation \(I\) of the base types, the denotation of a well-typed term \(t\) of type \(A\) in context \(\Gamma\) in an environment \(\eta\) for \(\Gamma\) is the element of the denotation of \(A\) defined by recursion on \(t\): a variable \(x\) denotes \(\eta(x)\), an application \(f\,a\) denotes the denotation of \(f\) applied to the denotation of \(a\) (both in \(\eta\)), and an abstraction \(\lambda.\,b\) denotes the function sending each value \(a\) of its argument type to the denotation of the body \(b\) in \(\eta\) extended by \(a\) for the newest variable.

def denote (I : Base → Type v) : {Γ : List (Ty Base)} → {A : Ty Base} →
    Tm Γ A → Env I Γ → Ty.denote I A
  | _, _, .var x, η => η x
  | _, _, .app f a, η => denote I f η (denote I a η)
  | _, _, .lam body, η => fun a ↦ denote I body (Env.cons a η)

Uses 6 · Used by 35

Statement usesSemantic environments for the denotational semantics of STLC · Extending a semantic environment in STLC · Intrinsically typed terms of the simply typed lambda calculus · Simple types · Denotation of simple types · Typed de Bruijn variables of the simply typed lambda calculus

Used byDenotational correctness of the call-by-name CPS translation · The call-by-name CPS translation at base types · Running the call-by-name CPS translation with the identity continuation · Denotational correctness of the CPS translation (Meyer–Wand) · CPS translation at a base type · CPS translation at a base type with the identity continuation · Semantic equality is a congruence for application · Beta is sound for the denotational semantics · One reduction step preserves STLC denotation · Multi-step reduction preserves STLC denotation · Big-step evaluation preserves STLC denotation · Denotation of an instantiated STLC body · Renaming lemma for STLC denotation · Denotation of an STLC substitution · Substitution lemma for STLC denotation · Weakening preserves STLC denotation · Eta is sound for the denotational semantics · Semantic equality is a congruence for lambda abstraction · Semantic equality is reflexive · Pointwise semantic equality of substitutions is reflexive · Renaming preserves semantic equality · Semantic equality of terms in a model · Pointwise semantic equality of substitutions · Substitution preserves semantic equality · Semantically equal substitutions give semantically equal results · Symmetry of semantic equality of terms · Symmetry of pointwise semantic equality of substitutions · Transitivity of semantic equality of terms · Transitivity of pointwise semantic equality of substitutions · The identity semantic environment realizes every environment · Fundamental lemma for NbE evaluation · Kripke realization relation for NbE · NbE preserves denotation · Every term is semantically equal to its NbE normal form in each model · Realization is stable under renaming

TheoremRenaming lemma for STLC denotation#✓fully proved

For every interpretation \(I\) of the base types, every type-preserving renaming \(\rho\) from context \(\Gamma\) to context \(\Delta\), every term \(t\) in context \(\Gamma\) and every environment \(\eta\) for \(\Delta\), the denotation in \(\eta\) of the term obtained by renaming the variables of \(t\) along \(\rho\) equals the denotation of \(t\) in the environment that sends each variable \(x\) of \(\Gamma\) to \(\eta(\rho(x))\).

theorem denote_rename (I : Base → Type v) (ρ : Ren Γ Δ) (t : Tm Γ A) (η : Env I Δ) :
    denote I (rename ρ t) η = denote I t (Env.rename ρ η)

Uses 11 · Used by 5

Statement usesSemantic environments for the denotational semantics of STLC · Renaming an environment · Renamings of simply typed contexts · Intrinsically typed terms of the simply typed lambda calculus · Denotation of an STLC term · Renaming a simply typed term · Simple types · Denotation of simple types

Proof usesExtending a semantic environment in STLC · Typed de Bruijn variables of the simply typed lambda calculus · Lifting a renaming under a binder

Used byWeakening preserves STLC denotation · Renaming preserves semantic equality · The identity semantic environment realizes every environment · NbE preserves denotation · Realization is stable under renaming

TheoremWeakening preserves STLC denotation#✓fully proved

For every interpretation \(I\) of the base types, every term \(t\) of type \(A\) in context \(\Gamma\), every type \(B\), every value \(a\) in the denotation of \(B\) and every environment \(\eta\) for \(\Gamma\), the weakening of \(t\) to the context \(B :: \Gamma\) has, in the environment that extends \(\eta\) by \(a\) for the newest variable, the same denotation as \(t\) in \(\eta\).

theorem denote_weaken (I : Base → Type v) (t : Tm Γ A) (a : Ty.denote I B) (η : Env I Γ) :
    denote I (weaken (B := B) t) (Env.cons a η) = denote I t η

Uses 11 · Used by 4

Statement usesSemantic environments for the denotational semantics of STLC · Extending a semantic environment in STLC · Intrinsically typed terms of the simply typed lambda calculus · Denotation of an STLC term · Weakening a simply typed term · Simple types · Denotation of simple types

Proof usesRenaming an environment · Renaming lemma for STLC denotation · Renaming a simply typed term · Typed de Bruijn variables of the simply typed lambda calculus

Used byDenotational correctness of the call-by-name CPS translation · Denotational correctness of the CPS translation (Meyer–Wand) · Substitution lemma for STLC denotation · Eta is sound for the denotational semantics

DefinitionDenotation of an STLC substitution#✓fully proved

Given an interpretation \(I\) of the base types, a type-preserving substitution \(\sigma\) mapping each variable of a context \(\Gamma\) to a term in a context \(\Delta\), and an environment \(\eta\) for \(\Delta\), this is the environment for \(\Gamma\) that sends each variable \(x\) to the denotation of \(\sigma(x)\) in \(\eta\).

def denoteSub (I : Base → Type v) (σ : Sub Γ Δ) (η : Env I Δ) : Env I Γ :=
  fun x ↦ denote I (σ x) η

Uses 5 · Used by 4

Statement usesSemantic environments for the denotational semantics of STLC · Simultaneous substitutions of simply typed contexts · Denotation of an STLC term · Simple types · Typed de Bruijn variables of the simply typed lambda calculus

Used byDenotation of an instantiated STLC body · Substitution lemma for STLC denotation · Substitution preserves semantic equality · Semantically equal substitutions give semantically equal results

TheoremSubstitution lemma for STLC denotation#✓fully proved

For every interpretation \(I\) of the base types, every type-preserving substitution \(\sigma\) mapping each variable of a context \(\Gamma\) to a term in a context \(\Delta\), every term \(t\) in context \(\Gamma\) and every environment \(\eta\) for \(\Delta\), the denotation in \(\eta\) of \(t\) with \(\sigma\) applied simultaneously to its variables equals the denotation of \(t\) in the environment that sends each variable \(x\) of \(\Gamma\) to the denotation of \(\sigma(x)\) in \(\eta\).

theorem denote_subst (I : Base → Type v) (σ : Sub Γ Δ) (t : Tm Γ A) (η : Env I Δ) :
    denote I (subst σ t) η = denote I t (denoteSub I σ η)

Uses 12 · Used by 3

Statement usesSemantic environments for the denotational semantics of STLC · Simultaneous substitutions of simply typed contexts · Intrinsically typed terms of the simply typed lambda calculus · Denotation of an STLC term · Denotation of an STLC substitution · Simultaneous substitution (simply typed lambda calculus) · Simple types · Denotation of simple types

Proof usesExtending a semantic environment in STLC · Lifting a substitution under a binder (simply typed lambda calculus) · Weakening preserves STLC denotation · Typed de Bruijn variables of the simply typed lambda calculus

Used byDenotation of an instantiated STLC body · Substitution preserves semantic equality · Semantically equal substitutions give semantically equal results

TheoremDenotation of an instantiated STLC body#✓fully proved

For every interpretation \(I\) of the base types, every term \(b\) of type \(B\) in context \(A :: \Gamma\), every term \(a\) of type \(A\) in context \(\Gamma\) and every environment \(\eta\) for \(\Gamma\), the denotation in \(\eta\) of \(b\) with its newest variable replaced by \(a\) equals the denotation of \(b\) in the environment that extends \(\eta\) by the denotation of \(a\) in \(\eta\) for the newest variable.

theorem denote_instantiate (I : Base → Type v) (body : Tm (A :: Γ) B) (a : Tm Γ A)
    (η : Env I Γ) :
    denote I (instantiate body a) η = denote I body (Env.cons (denote I a η) η)

Uses 12 · Used by 2

Statement usesSemantic environments for the denotational semantics of STLC · Extending a semantic environment in STLC · Intrinsically typed terms of the simply typed lambda calculus · Denotation of an STLC term · Instantiating a binder body (simply typed lambda calculus) · Simple types · Denotation of simple types

Proof usesSingle-variable substitution (simply typed lambda calculus) · Denotation of an STLC substitution · Substitution lemma for STLC denotation · Simultaneous substitution (simply typed lambda calculus) · Typed de Bruijn variables of the simply typed lambda calculus

Used byBeta is sound for the denotational semantics · One reduction step preserves STLC denotation

TheoremOne reduction step preserves STLC denotation#✓fully proved

For every interpretation \(I\) of the base types, if a term \(t\) reduces to \(t'\) in one step of call-by-value reduction, then \(t\) and \(t'\) have the same denotation in every environment \(\eta\) for their context.

theorem denote_eq (I : Base → Type v) {t t' : Tm Γ A} (h : Step t t') (η : Env I Γ) :
    Tm.denote I t η = Tm.denote I t' η

Uses 10 · Used by 2

Statement usesSemantic environments for the denotational semantics of STLC · Small-step call-by-value reduction in STLC · Intrinsically typed terms of the simply typed lambda calculus · Denotation of an STLC term · Simple types · Denotation of simple types

Proof usesExtending a semantic environment in STLC · Denotation of an instantiated STLC body · Instantiating a binder body (simply typed lambda calculus) · Values of STLC

Used byMulti-step reduction preserves STLC denotation · Single-step evaluation is a semantic equation

TheoremMulti-step reduction preserves STLC denotation#✓fully proved

For every interpretation \(I\) of the base types, if a term \(t\) reduces to \(t'\) in zero or more steps of call-by-value reduction, then \(t\) and \(t'\) have the same denotation in every environment \(\eta\) for their context.

theorem denote_eq (I : Base → Type v) {t t' : Tm Γ A} (h : Steps t t') (η : Env I Γ) :
    Tm.denote I t η = Tm.denote I t' η

Uses 8 · Used by 2

Statement usesSemantic environments for the denotational semantics of STLC · Multi-step call-by-value reduction in STLC · Intrinsically typed terms of the simply typed lambda calculus · Denotation of an STLC term · Simple types · Denotation of simple types

Proof usesSmall-step call-by-value reduction in STLC · One reduction step preserves STLC denotation

Used byBig-step evaluation preserves STLC denotation · Multi-step evaluation is a semantic equation

TheoremBig-step evaluation preserves STLC denotation#✓fully proved

For every interpretation \(I\) of the base types, if a term \(t\) evaluates to \(v\) under call-by-value big-step evaluation, then \(t\) and \(v\) have the same denotation in every environment \(\eta\) for their context.

theorem denote_eq (I : Base → Type v) {t value : Tm Γ A} (h : Eval t value)
    (η : Env I Γ) : Tm.denote I t η = Tm.denote I value η

Uses 8

Statement usesSemantic environments for the denotational semantics of STLC · Big-step call-by-value evaluation in the simply typed lambda calculus · Intrinsically typed terms of the simply typed lambda calculus · Denotation of an STLC term · Simple types · Denotation of simple types

Proof usesBig-step evaluation implies small-step evaluation · Multi-step reduction preserves STLC denotation

DefinitionSemantic equality of terms in a model#✓fully proved

Fix an interpretation \(I\) of the base types as types. Two terms \(t\) and \(u\) of the same type \(A\) in the same context \(\Gamma\) are semantically equal in \(I\) when, for every semantic environment \(\eta\) for \(\Gamma\), the denotation of \(t\) in \(I\) at \(\eta\) equals the denotation of \(u\) in \(I\) at \(\eta\).

def SemEq (I : Base → Type v) (t u : Tm Γ A) : Prop :=
  ∀ η : Env I Γ, Tm.denote I t η = Tm.denote I u η

Uses 5 · Used by 16

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

Used bySemantic equality is a congruence for application · Beta is sound for the denotational semantics · Semantic equality is an equivalence relation · Eta is sound for the denotational semantics · Semantic equality is a congruence for lambda abstraction · Model equality of STLC terms · Single-step evaluation is a semantic equation · Multi-step evaluation is a semantic equation · Semantic equality is reflexive · Renaming preserves semantic equality · Semantic equality is a congruence for typed contexts · Substitution preserves semantic equality · Semantically equal substitutions give semantically equal results · Symmetry of semantic equality of terms · Transitivity of semantic equality of terms · Every term is semantically equal to its NbE normal form in each model

TheoremSemantic equality is reflexive#✓fully proved

For every interpretation \(I\) of the base types, every term \(t\) is semantically equal to itself in \(I\): it has the same denotation as itself in every environment.

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

Uses 6 · Used by 3

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

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

Used bySemantic equality is an equivalence relation · Semantic equality is a congruence for typed contexts · Equal NbE normal forms imply model equality

TheoremSymmetry of semantic equality of terms#✓fully proved

For every interpretation \(I\) of the base types and all terms \(t\) and \(u\) of the same type in the same context, if \(t\) and \(u\) are semantically equal in \(I\), then \(u\) and \(t\) are semantically equal in \(I\).

theorem symm {t u : Tm Γ A} (h : SemEq I t u) : SemEq I u t

Uses 6 · Used by 2

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

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

Used bySemantic equality is an equivalence relation · Equal NbE normal forms imply model equality

TheoremTransitivity of semantic equality of terms#✓fully proved

For every interpretation \(I\) of the base types and all terms \(t\), \(u\) and \(w\) of the same type in the same context, if \(t\) and \(u\) are semantically equal in \(I\) and \(u\) and \(w\) are semantically equal in \(I\), then \(t\) and \(w\) are semantically equal in \(I\).

theorem trans {t u w : Tm Γ A} (htu : SemEq I t u) (huw : SemEq I u w) :
    SemEq I t w

Uses 6 · Used by 2

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

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

Used bySemantic equality is an equivalence relation · Equal NbE normal forms imply model equality

TheoremSemantic equality is a congruence for application#✓fully proved

Fix an interpretation \(I\) of the base types. If terms \(f\) and \(g\) of type \(A \Rightarrow B\) in a context \(\Gamma\) are semantically equal in \(I\) (they have the same denotation in every environment), and terms \(a\) and \(b\) of type \(A\) in \(\Gamma\) are semantically equal in \(I\), then the applications \(f\,a\) and \(g\,b\) are semantically equal in \(I\).

theorem app {f g : Tm Γ (A ⇒ B)} {a b : Tm Γ A}
    (hfg : SemEq I f g) (hab : SemEq I a b) : SemEq I (.app f a) (.app g b)

Uses 6 · Used by 1

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

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

Used bySemantic equality is a congruence for typed contexts

TheoremSemantic equality is a congruence for lambda abstraction#✓fully proved

Fix an interpretation \(I\) of the base types. If two terms of type \(B\) in the context \(\Gamma\) extended by a newest variable of type \(A\) are semantically equal in \(I\) (they have the same denotation in every environment), then their lambda abstractions, terms of type \(A \Rightarrow B\) in \(\Gamma\), are semantically equal in \(I\).

theorem lam {body body' : Tm (A :: Γ) B} (h : SemEq I body body') :
    SemEq I (.lam body) (.lam body')

Uses 7 · Used by 1

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

Proof usesSemantic environments for the denotational semantics of STLC · Extending a semantic environment in STLC · Denotation of an STLC term · Denotation of simple types

Used bySemantic equality is a congruence for typed contexts

TheoremRenaming preserves semantic equality#✓fully proved

Fix an interpretation \(I\) of the base types. If terms \(t\) and \(u\) of type \(A\) in a context \(\Gamma\) are semantically equal in \(I\) (they have the same denotation in every environment), then for every type-preserving renaming \(\rho\) of the variables of \(\Gamma\) into a context \(\Delta\), the renamed terms \(\rho(t)\) and \(\rho(u)\) are semantically equal in \(I\).

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

Uses 10

Statement usesRenamings of simply typed contexts · Semantic equality of terms in a model · Intrinsically typed terms of the simply typed lambda calculus · Renaming a simply typed term · Simple types

Proof usesSemantic environments for the denotational semantics of STLC · Renaming an environment · Denotation of an STLC term · Renaming lemma for STLC denotation · Denotation of simple types

TheoremSubstitution preserves semantic equality#✓fully proved

For every interpretation \(I\) of the base types, if two terms \(t\) and \(u\) of the same type \(A\) in a context \(\Gamma\) are semantically equal in \(I\), then for every simultaneous substitution \(\sigma\) from \(\Gamma\) to a context \(\Delta\), the result of applying \(\sigma\) to \(t\) and the result of applying \(\sigma\) to \(u\) are semantically equal in \(I\).

theorem subst {t u : Tm Γ A} (h : SemEq I t u) (σ : Sub Γ Δ) :
    SemEq I (Tm.subst σ t) (Tm.subst σ u)

Uses 10

Statement usesSemantic equality of terms in a model · Simultaneous substitutions of simply typed contexts · Intrinsically typed terms of the simply typed lambda calculus · Simultaneous substitution (simply typed lambda calculus) · Simple types

Proof usesSemantic environments for the denotational semantics of STLC · Denotation of an STLC term · Denotation of an STLC substitution · Substitution lemma for STLC denotation · Denotation of simple types

TheoremSingle-step evaluation is a semantic equation#✓fully proved

For every interpretation \(I\) of the base types, if a term \(t\) reduces to a term \(u\) in one call-by-value evaluation step, then \(t\) and \(u\) are semantically equal in \(I\): they have the same denotation in every environment.

theorem of_step {t u : Tm Γ A} (h : Step t u) : SemEq I t u

Uses 6

Statement usesSemantic equality of terms in a model · Small-step call-by-value reduction in STLC · Intrinsically typed terms of the simply typed lambda calculus · Simple types

Proof usesSemantic environments for the denotational semantics of STLC · One reduction step preserves STLC denotation

TheoremMulti-step evaluation is a semantic equation#✓fully proved

For every interpretation \(I\) of the base types, if a term \(t\) reduces to a term \(u\) in zero or more call-by-value evaluation steps, then \(t\) and \(u\) are semantically equal in \(I\): they have the same denotation in every environment.

theorem of_steps {t u : Tm Γ A} (h : Steps t u) : SemEq I t u

Uses 6

Statement usesSemantic equality of terms in a model · Multi-step call-by-value reduction in STLC · Intrinsically typed terms of the simply typed lambda calculus · Simple types

Proof usesSemantic environments for the denotational semantics of STLC · Multi-step reduction preserves STLC denotation

TheoremBeta is sound for the denotational semantics#✓fully proved

For every interpretation \(I\) of the base types, every term \(t\) of type \(B\) in the context \(\Gamma\) extended by a newest variable of type \(A\), and every term \(a\) of type \(A\) in \(\Gamma\), the redex \((\lambda.\,t)\,a\) is semantically equal in \(I\) (has the same denotation in every environment) to the instantiation \(t[a]\), which replaces the newest free variable of \(t\) by \(a\).

The argument \(a\) need not be a value.

theorem beta (I : Base → Type v) (body : Tm (A :: Γ) B) (a : Tm Γ A) :
    SemEq I (.app (.lam body) a) (Tm.instantiate body a)

Uses 9 · Used by 1

Statement usesSemantic equality of terms in a model · Intrinsically typed terms of the simply typed lambda calculus · Instantiating a binder body (simply typed lambda calculus) · Simple types

Proof usesSemantic environments for the denotational semantics of STLC · Extending a semantic environment in STLC · Denotation of an STLC term · Denotation of an instantiated STLC body · Denotation of simple types

Used byModel-independent beta equality

TheoremEta is sound for the denotational semantics#✓fully proved

For every interpretation \(I\) of the base types and every term \(f\) of type \(A \Rightarrow B\) in a context \(\Gamma\), let \(f'\) be the weakening of \(f\) to the context \(\Gamma\) extended by a newest variable \(x\) of type \(A\). Then the term \(\lambda x.\, f'\,x\), which binds \(x\), is semantically equal to \(f\) in \(I\) (has the same denotation in every environment).

theorem eta (I : Base → Type v) (f : Tm Γ (A ⇒ B)) :
    SemEq I (.lam (.app (Tm.weaken f) (.var .zero))) f

Uses 10 · Used by 1

Statement usesSemantic equality of terms in a model · Intrinsically typed terms of the simply typed lambda calculus · Weakening a simply typed term · Simple types · Typed de Bruijn variables of the simply typed lambda calculus

Proof usesSemantic environments for the denotational semantics of STLC · Extending a semantic environment in STLC · Denotation of an STLC term · Weakening preserves STLC denotation · Denotation of simple types

Used byModel-independent eta equality

DefinitionPointwise semantic equality of substitutions#✓fully proved

Fix an interpretation \(I\) of the base types as types. Two simultaneous substitutions \(\sigma\) and \(\tau\) from a context \(\Gamma\) to a context \(\Delta\) are pointwise semantically equal in \(I\) when, for every variable \(x\) of \(\Gamma\) (of any type) and every semantic environment \(\eta\) for \(\Delta\), the denotation of the term \(\sigma(x)\) in \(I\) at \(\eta\) equals the denotation of the term \(\tau(x)\) in \(I\) at \(\eta\).

def SubSemEq (I : Base → Type v) (σ τ : Sub Γ Δ) : Prop :=
  ∀ {A} (x : Var Γ A) (η : Env I Δ), Tm.denote I (σ x) η = Tm.denote I (τ x) η

Uses 6 · Used by 4

Statement usesSemantic environments for the denotational semantics of STLC · Simultaneous substitutions of simply typed contexts · Denotation of an STLC term · Simple types · Denotation of simple types · Typed de Bruijn variables of the simply typed lambda calculus

Used byPointwise semantic equality of substitutions is reflexive · Semantically equal substitutions give semantically equal results · Symmetry of pointwise semantic equality of substitutions · Transitivity of pointwise semantic equality of substitutions

TheoremPointwise semantic equality of substitutions is reflexive#✓fully proved

For every interpretation \(I\) of the base types and every simultaneous substitution \(\sigma\) that replaces each variable of a context \(\Gamma\) by a term of the same type in a context \(\Delta\), \(\sigma\) is pointwise semantically equal to itself in \(I\): for every variable \(x\) of \(\Gamma\), the term \(\sigma(x)\) has the same denotation as itself in every environment for \(\Delta\).

theorem refl (I : Base → Type v) (σ : Sub Γ Δ) : SubSemEq I σ σ

Uses 7

Statement usesSimultaneous substitutions of simply typed contexts · Pointwise semantic equality of substitutions · Simple types

Proof usesSemantic environments for the denotational semantics of STLC · Denotation of an STLC term · Denotation of simple types · Typed de Bruijn variables of the simply typed lambda calculus

TheoremSymmetry of pointwise semantic equality of substitutions#✓fully proved

For every interpretation \(I\) of the base types and all simultaneous substitutions \(\sigma\) and \(\tau\) from a context \(\Gamma\) to a context \(\Delta\), if \(\sigma\) and \(\tau\) are pointwise semantically equal in \(I\), then \(\tau\) and \(\sigma\) are pointwise semantically equal in \(I\).

theorem symm {σ τ : Sub Γ Δ} (h : SubSemEq I σ τ) : SubSemEq I τ σ

Uses 7

Statement usesSimultaneous substitutions of simply typed contexts · Pointwise semantic equality of substitutions · Simple types

Proof usesSemantic environments for the denotational semantics of STLC · Denotation of an STLC term · Denotation of simple types · Typed de Bruijn variables of the simply typed lambda calculus

TheoremTransitivity of pointwise semantic equality of substitutions#✓fully proved

For every interpretation \(I\) of the base types and all simultaneous substitutions \(\sigma\), \(\tau\) and \(\upsilon\) from a context \(\Gamma\) to a context \(\Delta\), if \(\sigma\) and \(\tau\) are pointwise semantically equal in \(I\) and \(\tau\) and \(\upsilon\) are pointwise semantically equal in \(I\), then \(\sigma\) and \(\upsilon\) are pointwise semantically equal in \(I\).

theorem trans {σ τ υ : Sub Γ Δ} (hστ : SubSemEq I σ τ) (hτυ : SubSemEq I τ υ) :
    SubSemEq I σ υ

Uses 7

Statement usesSimultaneous substitutions of simply typed contexts · Pointwise semantic equality of substitutions · Simple types

Proof usesSemantic environments for the denotational semantics of STLC · Denotation of an STLC term · Denotation of simple types · Typed de Bruijn variables of the simply typed lambda calculus

TheoremSemantically equal substitutions give semantically equal results#✓fully proved

For every interpretation \(I\) of the base types, every term \(t\) of type \(A\) in a context \(\Gamma\), and all simultaneous substitutions \(\sigma\) and \(\tau\) from \(\Gamma\) to a context \(\Delta\) that are pointwise semantically equal in \(I\), the result of applying \(\sigma\) to \(t\) and the result of applying \(\tau\) to \(t\) are semantically equal in \(I\).

theorem subst_congr (t : Tm Γ A) {σ τ : Sub Γ Δ} (hστ : SubSemEq I σ τ) :
    SemEq I (Tm.subst σ t) (Tm.subst τ t)

Uses 12

Statement usesSemantic equality of terms in a model · Simultaneous substitutions of simply typed contexts · Pointwise semantic equality of substitutions · Intrinsically typed terms of the simply typed lambda calculus · Simultaneous substitution (simply typed lambda calculus) · Simple types

Proof usesSemantic environments for the denotational semantics of STLC · Denotation of an STLC term · Denotation of an STLC substitution · Substitution lemma for STLC denotation · Denotation of simple types · Typed de Bruijn variables of the simply typed lambda calculus

TheoremSemantic equality is an equivalence relation#✓fully proved

For every interpretation \(I\) of the base types, every context \(\Gamma\) and every type \(A\), semantic equality in \(I\) of terms of type \(A\) in \(\Gamma\) (having the same denotation in every environment) is reflexive, symmetric and transitive.

theorem equivalence (I : Base → Type v) : Equivalence (@SemEq Base A Γ I)

Uses 6

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

Proof usesSemantic equality is reflexive · Symmetry of semantic equality of terms · Transitivity of semantic equality of terms

InductiveTyped one-hole contexts#✓fully proved

Fix simple types over a type of base types. A one-hole context whose hole has type \(A\) in variable context \(\Gamma\), and which produces a term of type \(B\) in variable context \(\Delta\), is built by four rules. The hole itself is such a context, with \(\Delta = \Gamma\) and \(B = A\). If \(C\) produces type \(S \Rightarrow T\) in \(\Delta\) and \(a\) is a term of type \(S\) in \(\Delta\), then the application \(C\,a\) produces type \(T\) in \(\Delta\). If \(f\) is a term of type \(S \Rightarrow T\) in \(\Delta\) and \(C\) produces type \(S\) in \(\Delta\), then the application \(f\,C\) produces type \(T\) in \(\Delta\). If \(C\) produces type \(T\) in the context \(S :: \Delta\) obtained from \(\Delta\) by adding a new leading variable of type \(S\), then the abstraction \(\lambda C\) produces type \(S \Rightarrow T\) in \(\Delta\). In every rule the hole keeps type \(A\) in context \(\Gamma\).

inductive TmCtx {Base : Type u} (Γ : List (Ty Base)) (A : Ty Base) :
    (Δ : List (Ty Base)) → (B : Ty Base) → Type u where
  | hole : TmCtx Γ A Γ A
  | appFun {Δ : List (Ty Base)} {B C : Ty Base}
      (ctx : TmCtx Γ A Δ (B ⇒ C)) (a : Tm Δ B) : TmCtx Γ A Δ C
  | appArg {Δ : List (Ty Base)} {B C : Ty Base}
      (f : Tm Δ (B ⇒ C)) (ctx : TmCtx Γ A Δ B) : TmCtx Γ A Δ C
  | lam {Δ : List (Ty Base)} {B C : Ty Base}
      (ctx : TmCtx Γ A (B :: Δ) C) : TmCtx Γ A Δ (B ⇒ C)

Uses 2 · Used by 8

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

Used byComposition of STLC contexts · Associativity of composition of STLC contexts · Model equality is a congruence for STLC contexts · Beta equality inside an STLC context · Eta equality inside an STLC context · Plugging a term into an STLC context · Plugging into a composite STLC context · Semantic equality is a congruence for typed contexts

DefinitionPlugging a term into an STLC context#✓fully proved

Let \(E\) be a typed one-hole context whose hole has type \(A\) in variable context \(\Gamma\) and which produces a term of type \(B\) in variable context \(\Delta\). For a term \(t\) of type \(A\) in \(\Gamma\), the plugged term \(E[t]\) of type \(B\) in \(\Delta\) is defined by recursion on \(E\): \([\,][t] = t\), \((E\,a)[t] = E[t]\,a\), \((f\,E)[t] = f\,E[t]\) and \((\lambda.\,E)[t] = \lambda.\,E[t]\), where \([\,]\) is the bare hole, \(E\,a\) applies \(E\) to a term \(a\), \(f\,E\) applies a term \(f\) to \(E\), and \(\lambda.\,E\) puts \(E\) under a lambda. No renaming is applied, so a lambda above the hole may bind free variables of \(t\).

def plug {Δ : List (Ty Base)} {B : Ty Base} : TmCtx Γ A Δ B → Tm Γ A → Tm Δ B
  | .hole, t => t
  | .appFun C a, t => .app (plug C t) a
  | .appArg f C, t => .app f (plug C t)
  | .lam C, t => .lam (plug C t)

Uses 3 · Used by 5

Statement usesIntrinsically typed terms of the simply typed lambda calculus · Typed one-hole contexts · Simple types

Used byModel equality is a congruence for STLC contexts · Beta equality inside an STLC context · Eta equality inside an STLC context · Plugging into a composite STLC context · Semantic equality is a congruence for typed contexts

DefinitionComposition of STLC contexts#✓fully proved

Let \(E_2\) be a typed one-hole context whose hole has type \(B\) in variable context \(\Delta\) and which produces a term of type \(C\) in context \(\Theta\), and let \(E_1\) be one whose hole has type \(A\) in context \(\Gamma\) and which produces a term of type \(B\) in \(\Delta\). The composite \(E_2 \circ E_1\), with hole of type \(A\) in \(\Gamma\) and result of type \(C\) in \(\Theta\), replaces the hole of \(E_2\) by \(E_1\); by recursion on \(E_2\): \([\,] \circ E_1 = E_1\), \((E_2\,a) \circ E_1 = (E_2 \circ E_1)\,a\), \((f\,E_2) \circ E_1 = f\,(E_2 \circ E_1)\) and \((\lambda.\,E_2) \circ E_1 = \lambda.\,(E_2 \circ E_1)\), where \([\,]\) is the bare hole and \(E\,a\), \(f\,E\), \(\lambda.\,E\) apply a context \(E\) to a term \(a\), apply a term \(f\) to \(E\), and put \(E\) under a lambda.

def comp {Δ Θ : List (Ty Base)} {B C : Ty Base} :
    TmCtx Δ B Θ C → TmCtx Γ A Δ B → TmCtx Γ A Θ C
  | .hole, inner => inner
  | .appFun outer a, inner => .appFun (comp outer inner) a
  | .appArg f outer, inner => .appArg f (comp outer inner)
  | .lam outer, inner => .lam (comp outer inner)

Uses 3 · Used by 2

Statement usesIntrinsically typed terms of the simply typed lambda calculus · Typed one-hole contexts · Simple types

Used byAssociativity of composition of STLC contexts · Plugging into a composite STLC context

TheoremPlugging into a composite STLC context#✓fully proved

Let \(E_2\) be a typed one-hole context whose hole has type \(B\) in variable context \(\Delta\) and which produces a term of type \(C\) in context \(\Theta\), and let \(E_1\) be one whose hole has type \(A\) in context \(\Gamma\) and which produces a term of type \(B\) in \(\Delta\). Then for every term \(t\) of type \(A\) in \(\Gamma\), \((E_2 \circ E_1)[t] = E_2[E_1[t]]\).

theorem plug_comp (outer : TmCtx Δ B Θ C) (inner : TmCtx Γ A Δ B) (t : Tm Γ A) :
    plug (comp outer inner) t = plug outer (plug inner t)

Uses 5

Statement usesIntrinsically typed terms of the simply typed lambda calculus · Typed one-hole contexts · Composition of STLC contexts · Plugging a term into an STLC context · Simple types

TheoremAssociativity of composition of STLC contexts#✓fully proved

Let \(E_1\) be a typed one-hole context whose hole has type \(A\) in variable context \(\Gamma\) and which produces a term of type \(B\) in context \(\Delta\), \(E_2\) one with hole of type \(B\) in \(\Delta\) producing type \(C\) in \(\Theta\), and \(E_3\) one with hole of type \(C\) in \(\Theta\) producing type \(D\) in \(\Xi\). Then \((E_3 \circ E_2) \circ E_1 = E_3 \circ (E_2 \circ E_1)\).

theorem comp_assoc (outer : TmCtx Θ C Ξ D) (middle : TmCtx Δ B Θ C)
    (inner : TmCtx Γ A Δ B) :
    comp (comp outer middle) inner = comp outer (comp middle inner)

Uses 4

Statement usesTyped one-hole contexts · Composition of STLC contexts · Simple types

Proof usesIntrinsically typed terms of the simply typed lambda calculus

TheoremSemantic equality is a congruence for typed contexts#✓fully proved

Fix an interpretation \(I\) of the base types. Let \(t\) and \(u\) be terms of type \(A\) in variable context \(\Gamma\) that denote the same value in \(I\) under every semantic environment. Then for every typed one-hole context \(C\) whose hole has type \(A\) in context \(\Gamma\) and which produces a term of type \(B\) in context \(\Delta\), the terms \(C[t]\) and \(C[u]\) obtained by plugging \(t\) and \(u\) into the hole also denote the same value in \(I\) under every semantic environment.

theorem semEq {I : Base → Type v} (C : TmCtx Γ A Δ B) {t u : Tm Γ A}
    (h : SemEq I t u) : SemEq I (plug C t) (plug C u)

Uses 8 · Used by 1

Statement usesSemantic equality of terms in a model · Intrinsically typed terms of the simply typed lambda calculus · Typed one-hole contexts · Plugging a term into an STLC context · Simple types

Proof usesSemantic equality is a congruence for application · Semantic equality is a congruence for lambda abstraction · Semantic equality is reflexive

Used byModel equality is a congruence for STLC contexts

DefinitionModel equality of STLC terms#✓fully proved

Two terms \(t\) and \(u\) of type \(A\) in variable context \(\Gamma\) are model-equal when, for every interpretation \(I\) of the base types by types in the same universe as the type of base types, they are semantically equal in \(I\): with function types interpreted as full function spaces, the denotations of \(t\) and \(u\) agree at every semantic environment for \(\Gamma\).

Unlike semantic equality in a fixed interpretation, this relation does not choose a particular model.

def ModelEq (t u : Tm Γ A) : Prop :=
  ∀ I : Base → Type u, SemEq I t u

Uses 3 · Used by 7

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

Used byModel-independent beta equality · Model equality is a congruence for STLC contexts · Beta equality inside an STLC context · Eta equality inside an STLC context · Model-independent eta equality · Equal NbE normal forms imply model equality · Every term is model-equal to its NbE normal form

TheoremModel equality is a congruence for STLC contexts#✓fully proved

Let \(E\) be a typed one-hole context whose hole has type \(A\) in variable context \(\Gamma\) and which produces a term of type \(B\) in context \(\Delta\). If two terms \(t\) and \(u\) of type \(A\) in \(\Gamma\) are model-equal, then \(E[t]\) and \(E[u]\) are model-equal.

theorem context (C : TmCtx Γ A Δ B) {t u : Tm Γ A} (h : ModelEq t u) :
    ModelEq (C.plug t) (C.plug u)

Uses 6 · Used by 2

Statement usesModel equality of STLC terms · Intrinsically typed terms of the simply typed lambda calculus · Typed one-hole contexts · Plugging a term into an STLC context · Simple types

Proof usesSemantic equality is a congruence for typed contexts

Used byBeta equality inside an STLC context · Eta equality inside an STLC context

TheoremModel-independent beta equality#✓fully proved

For every term \(b\) of type \(B\) in the variable context \(\Gamma\) extended by a newest variable of type \(A\), and every term \(a\) of type \(A\) in \(\Gamma\), the application \((\lambda.\,b)\,a\) is model-equal to \(b[a]\), the result of substituting \(a\) for the newest variable of \(b\).

theorem beta (body : Tm (A :: Γ) B) (a : Tm Γ A) :
    ModelEq (.app (.lam body) a) (Tm.instantiate body a)

Uses 5 · Used by 1

Statement usesModel equality of STLC terms · Intrinsically typed terms of the simply typed lambda calculus · Instantiating a binder body (simply typed lambda calculus) · Simple types

Proof usesBeta is sound for the denotational semantics

Used byBeta equality inside an STLC context

TheoremModel-independent eta equality#✓fully proved

For every term \(f\) of type \(A \Rightarrow B\) in variable context \(\Gamma\), the term \(\lambda.\,(f^{\uparrow}\,x_0)\) is model-equal to \(f\), where \(f^{\uparrow}\) is \(f\) weakened by a newest variable of type \(A\) and \(x_0\) is that variable.

theorem eta (f : Tm Γ (A ⇒ B)) :
    ModelEq (.lam (.app (Tm.weaken f) (.var .zero))) f

Uses 6 · Used by 1

Statement usesModel equality of STLC terms · Intrinsically typed terms of the simply typed lambda calculus · Weakening a simply typed term · Simple types · Typed de Bruijn variables of the simply typed lambda calculus

Proof usesEta is sound for the denotational semantics

Used byEta equality inside an STLC context

TheoremBeta equality inside an STLC context#✓fully proved

Let \(E\) be a typed one-hole context whose hole has type \(B\) in variable context \(\Gamma\) and which produces a term of type \(C\) in context \(\Delta\). For every term \(b\) of type \(B\) in \(\Gamma\) extended by a newest variable of type \(A\), and every term \(a\) of type \(A\) in \(\Gamma\), the term \(E[(\lambda.\,b)\,a]\) is model-equal to \(E[b[a]]\), where \(b[a]\) is the result of substituting \(a\) for the newest variable of \(b\).

theorem context_beta (C : TmCtx Γ B Δ C) (body : Tm (A :: Γ) B) (a : Tm Γ A) :
    ModelEq (C.plug (.app (.lam body) a)) (C.plug (Tm.instantiate body a))

Uses 8

Statement usesModel equality of STLC terms · Intrinsically typed terms of the simply typed lambda calculus · Instantiating a binder body (simply typed lambda calculus) · Typed one-hole contexts · Plugging a term into an STLC context · Simple types

Proof usesModel-independent beta equality · Model equality is a congruence for STLC contexts

TheoremEta equality inside an STLC context#✓fully proved

Let \(E\) be a typed one-hole context whose hole has type \(A \Rightarrow B\) in variable context \(\Gamma\) and which produces a term of type \(C\) in context \(\Delta\). For every term \(f\) of type \(A \Rightarrow B\) in \(\Gamma\), the term \(E[\lambda.\,(f^{\uparrow}\,x_0)]\) is model-equal to \(E[f]\), where \(f^{\uparrow}\) is \(f\) weakened by a newest variable of type \(A\) and \(x_0\) is that variable.

theorem context_eta (C : TmCtx Γ (A ⇒ B) Δ C) (f : Tm Γ (A ⇒ B)) :
    ModelEq (C.plug (.lam (.app (Tm.weaken f) (.var .zero))) ) (C.plug f)

Uses 9

Statement usesModel equality of STLC terms · Intrinsically typed terms of the simply typed lambda calculus · Weakening a simply typed term · Typed one-hole contexts · Plugging a term into an STLC context · Simple types · Typed de Bruijn variables of the simply typed lambda calculus

Proof usesModel equality is a congruence for STLC contexts · Model-independent eta equality

43 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.