Lambda calculus with references

InductiveTypes of the simply typed lambda calculus with references#✓fully proved

Fix a type \(B\) of base types. The types over \(B\) are generated by the grammar \(T ::= b \mid \mathsf{Unit} \mid T_1 \to T_2 \mid \mathsf{Ref}\,T\) with \(b \in B\): base types, the unit type, function types, and types \(\mathsf{Ref}\,T\) of reference cells holding values of type \(T\).

inductive Ty (Base : Type u) where
  /-- An uninterpreted base type. -/
  | base : Base → Ty Base
  /-- The unit type. -/
  | unit : Ty Base
  /-- Function types. -/
  | arr : Ty Base → Ty Base → Ty Base
  /-- Reference cells holding values of the given type. -/
  | ref : Ty Base → Ty Base
  deriving DecidableEq, Repr
Used by 50
Used byAllocation preserves store typing · The recursive function of Landin's knot, with the cell free · The stored recursive function of Landin's knot · The knot after allocation · Determinism of evaluation with references · Well-typed stores hold a typed value at every location · Store-typing weakening · Retyping a well-typed store under an extended store typing · Typing judgment for the lambda calculus with references · The identity on Unit · Substitution lemma for the lambda calculus with references · Landin's knot · The cycle of Landin's knot · Landin's knot never evaluates to a value · Landin's knot is well typed · The first four steps of Landin's knot · Landin's knot never gets stuck · Canonical forms for function types · Canonical forms for reference types · Values do not step · No value has a base type · Embedding of raw STLC terms into the calculus with references · Typing is preserved by the embedding of raw STLC terms · Embedding of simple types into the calculus with references · Typing of embedded intrinsically typed STLC terms · Preservation for the lambda calculus with references · Preservation for multi-step evaluation · Progress · Configurations on the evaluation path of Landin's knot · Renaming preserves typing · Renaming the variables of a term · Renaming respects pointwise equality · Renaming by the identity · Composition of renamings · Substituting then renaming · Assignment preserves store typing · One-step evaluation with references · Well-typed stores · Parallel substitution preserves typing · Parallel substitution in a term · Substitution respects pointwise equality · Substitution by variables is the identity · Renaming then substituting · Composition of substitutions in the lambda calculus with references · Terms of the simply typed lambda calculus with references · Type safety · Type safety from the empty store · Canonical forms for the unit type · Values of the simply typed lambda calculus with references · Weakening of typing

InductiveTerms of the simply typed lambda calculus with references#✓fully proved

Fix a type \(B\) of base types. The terms are generated by: variables, given as de Bruijn indices \(x \in \mathbb{N}\); abstractions \(\lambda{:}T.\,t\), where \(T\) is a type over \(B\) and \(t\) is a term in which index \(0\) refers to the abstraction's parameter; applications \(t_1\,t_2\); the unit value \(\mathsf{unit}\); store locations \(l \in \mathbb{N}\); allocations \(\mathsf{ref}\,t\); dereferences \(!t\); and assignments \(t_1 := t_2\).

Store locations arise during evaluation, not in source programs.

Cslib.Languages.LambdaCalculus.References.Term · 19 lines 
inductive Term (Base : Type u) where
  /-- A de Bruijn variable. -/
  | var : Nat → Term Base
  /-- A lambda abstraction annotated with its parameter type. -/
  | lam : Ty Base → Term Base → Term Base
  /-- Application. -/
  | app : Term Base → Term Base → Term Base
  /-- The unit value. -/
  | unit : Term Base
  /-- A store location. Locations arise during evaluation, not in source
  programs. -/
  | loc : Nat → Term Base
  /-- Allocation of a fresh reference cell, `ref t`. -/
  | ref : Term Base → Term Base
  /-- Dereferencing, `!t`. -/
  | deref : Term Base → Term Base
  /-- Assignment, `t₁ := t₂`. -/
  | assign : Term Base → Term Base → Term Base
  deriving DecidableEq, Repr
Uses 1 · Used by 54
Statement usesTypes of the simply typed lambda calculus with references
Used byAllocation preserves store typing · The recursive function of Landin's knot, with the cell free · The stored recursive function of Landin's knot · The knot after allocation · Determinism of evaluation with references · Well-typed stores hold a typed value at every location · Store-typing weakening · Retyping a well-typed store under an extended store typing · Typing judgment for the lambda calculus with references · The identity on Unit · Substitution lemma for the lambda calculus with references · Substitution of a term for variable zero · Instantiating a shifted term · Landin's knot · The cycle of Landin's knot · Landin's knot never evaluates to a value · Landin's knot is well typed · The first four steps of Landin's knot · Landin's knot never gets stuck · Canonical forms for function types · Lifting a substitution under a binder · Canonical forms for reference types · Cycle term of Landin's knot · Values do not step · No value has a base type · Embedding of raw STLC terms into the calculus with references · Typing is preserved by the embedding of raw STLC terms · Preservation for the lambda calculus with references · Preservation for multi-step evaluation · Progress · Configurations on the evaluation path of Landin's knot · Renaming preserves typing · Renaming the variables of a term · Renaming respects pointwise equality · Renaming by the identity · Composition of renamings · Substituting then renaming · Assignment preserves store typing · Single-variable substitution at index zero · One-step evaluation with references · Multi-step evaluation with references · Store · Well-typed stores · Parallel substitution preserves typing · Parallel substitution in a term · Substitution respects pointwise equality · Substitution by variables is the identity · Renaming then substituting · Composition of substitutions in the lambda calculus with references · Type safety · Type safety from the empty store · Canonical forms for the unit type · Values of the simply typed lambda calculus with references · Weakening of typing

InductiveValues of the simply typed lambda calculus with references#✓fully proved

A term is a value if and only if it is an abstraction \(\lambda{:}T.\,t\), the unit value \(\mathsf{unit}\), or a store location \(l\).

inductive Value : Term Base → Prop
  | lam (T : Ty Base) (body : Term Base) : Value (.lam T body)
  | unit : Value .unit
  | loc (l : Nat) : Value (.loc l)
Uses 2 · Used by 20
Statement usesTerms of the simply typed lambda calculus with references · Types of the simply typed lambda calculus with references
Used byAllocation preserves store typing · Determinism of evaluation with references · Well-typed stores hold a typed value at every location · Retyping a well-typed store under an extended store typing · The cycle of Landin's knot · Landin's knot never evaluates to a value · The first four steps of Landin's knot · Landin's knot never gets stuck · Canonical forms for function types · Canonical forms for reference types · Values do not step · No value has a base type · Preservation for the lambda calculus with references · Progress · Assignment preserves store typing · One-step evaluation with references · Well-typed stores · Type safety · Type safety from the empty store · Canonical forms for the unit type

DefinitionLifting a renaming under a binder in the lambda calculus with references#✓fully proved

Given a renaming \(\rho : \mathbb{N} \to \mathbb{N}\) of de Bruijn indices, its lift is the renaming that sends \(0\) to \(0\) and each \(x + 1\) to \(\rho(x) + 1\).

def liftRen (ρ : Nat → Nat) : Nat → Nat
  | 0 => 0
  | x + 1 => ρ x + 1
Used by 7
Used byRenaming preserves typing · Renaming the variables of a term · Renaming respects pointwise equality · Renaming by the identity · Composition of renamings · Substituting then renaming · Renaming then substituting

DefinitionRenaming the variables of a term#✓fully proved

Given a renaming \(\rho : \mathbb{N} \to \mathbb{N}\) of de Bruijn indices, renaming a term by \(\rho\) replaces each variable \(x\) by \(\rho(x)\); renames the body of an abstraction \(\lambda{:}T.\,t\) by the lift of \(\rho\) (which sends \(0\) to \(0\) and each \(x + 1\) to \(\rho(x) + 1\)), keeping the type annotation \(T\); leaves the unit value and store locations unchanged; and acts componentwise on applications, allocations, dereferences and assignments.

def rename : (Nat → Nat) → Term Base → Term Base
  | ρ, .var x => .var (ρ x)
  | ρ, .lam T body => .lam T (rename (liftRen ρ) body)
  | ρ, .app f a => .app (rename ρ f) (rename ρ a)
  | _, .unit => .unit
  | _, .loc l => .loc l
  | ρ, .ref t => .ref (rename ρ t)
  | ρ, .deref t => .deref (rename ρ t)
  | ρ, .assign t₁ t₂ => .assign (rename ρ t₁) (rename ρ t₂)
Uses 3 · Used by 11
Statement usesTerms of the simply typed lambda calculus with references · Lifting a renaming under a binder in the lambda calculus with references · Types of the simply typed lambda calculus with references
Used byInstantiating a shifted term · Lifting a substitution under a binder · Renaming preserves typing · Renaming respects pointwise equality · Renaming by the identity · Composition of renamings · Substituting then renaming · Substitution respects pointwise equality · Renaming then substituting · Composition of substitutions in the lambda calculus with references · Weakening of typing

DefinitionLifting a substitution under a binder#✓fully proved

Given a substitution \(\sigma\) assigning a term to each de Bruijn index, its lift is the substitution that sends \(0\) to the variable \(0\) and each \(x + 1\) to the term \(\sigma(x)\) renamed by \(n \mapsto n + 1\), that is, with every free variable raised by one.

def liftSub (σ : Nat → Term Base) : Nat → Term Base
  | 0 => .var 0
  | x + 1 => rename Nat.succ (σ x)
Uses 2 · Used by 7
Statement usesTerms of the simply typed lambda calculus with references · Renaming the variables of a term
Used bySubstituting then renaming · Parallel substitution preserves typing · Parallel substitution in a term · Substitution respects pointwise equality · Substitution by variables is the identity · Renaming then substituting · Composition of substitutions in the lambda calculus with references

DefinitionParallel substitution in a term#✓fully proved

Given a substitution \(\sigma\) assigning a term to each de Bruijn index, substituting \(\sigma\) into a term replaces each variable \(x\) by \(\sigma(x)\); substitutes into the body of an abstraction \(\lambda{:}T.\,t\) the lift of \(\sigma\) (which sends \(0\) to the variable \(0\) and each \(x + 1\) to \(\sigma(x)\) with every free variable raised by one), keeping the type annotation \(T\); leaves the unit value and store locations unchanged; and acts componentwise on applications, allocations, dereferences and assignments.

def subst : (Nat → Term Base) → Term Base → Term Base
  | σ, .var x => σ x
  | σ, .lam T body => .lam T (subst (liftSub σ) body)
  | σ, .app f a => .app (subst σ f) (subst σ a)
  | _, .unit => .unit
  | _, .loc l => .loc l
  | σ, .ref t => .ref (subst σ t)
  | σ, .deref t => .deref (subst σ t)
  | σ, .assign t₁ t₂ => .assign (subst σ t₁) (subst σ t₂)
Uses 3 · Used by 8
Statement usesTerms of the simply typed lambda calculus with references · Lifting a substitution under a binder · Types of the simply typed lambda calculus with references
Used bySubstitution of a term for variable zero · Instantiating a shifted term · Substituting then renaming · Parallel substitution preserves typing · Substitution respects pointwise equality · Substitution by variables is the identity · Renaming then substituting · Composition of substitutions in the lambda calculus with references

DefinitionSingle-variable substitution at index zero#✓fully proved

For a term \(s\), the single-variable substitution for \(s\) sends the de Bruijn index \(0\) to \(s\) and each index \(x + 1\) to the variable \(x\).

def singleSub (s : Term Base) : Nat → Term Base
  | 0 => s
  | x + 1 => .var x
Uses 1 · Used by 3
Statement usesTerms of the simply typed lambda calculus with references
Used bySubstitution lemma for the lambda calculus with references · Substitution of a term for variable zero · Instantiating a shifted term

DefinitionSubstitution of a term for variable zero#✓fully proved

For terms \(t\) and \(s\), the instantiation of \(t\) by \(s\) applies to \(t\) the parallel substitution that sends the de Bruijn index \(0\) to \(s\) and each index \(x + 1\) to the variable \(x\). Thus the free occurrences of variable \(0\) in \(t\) are replaced by \(s\), with the free variables of \(s\) raised by the number of binders crossed, and every other free variable of \(t\) is lowered by one.

This is the substitution of β-reduction, written \(\uparrow^{-1}([0 \mapsto \uparrow^1 s]\,t)\) in TAPL Section 6.3; TAPL's \([0 \mapsto s]\,t\) alone does not lower the other free variables.

def instantiate (t s : Term Base) : Term Base :=
  subst (singleSub s) t
Uses 3 · Used by 11
Statement usesTerms of the simply typed lambda calculus with references · Single-variable substitution at index zero · Parallel substitution in a term
Used byDeterminism of evaluation with references · Substitution lemma for the lambda calculus with references · Instantiating a shifted term · The cycle of Landin's knot · Landin's knot never evaluates to a value · The first four steps of Landin's knot · Landin's knot never gets stuck · Values do not step · Preservation for the lambda calculus with references · Progress · One-step evaluation with references

AbbreviationStore#✓fully proved

A store \(\mu\) is a finite list of terms; each location \(l\) less than the length of \(\mu\) holds the term \(\mu[l]\), the entry of \(\mu\) at index \(l\).

abbrev Store (Base : Type u) := List (Term Base)
Uses 1 · Used by 17
Statement usesTerms of the simply typed lambda calculus with references
Used byAllocation preserves store typing · Determinism of evaluation with references · Retyping a well-typed store under an extended store typing · The cycle of Landin's knot · Landin's knot never evaluates to a value · The first four steps of Landin's knot · Landin's knot never gets stuck · Values do not step · Preservation for the lambda calculus with references · Preservation for multi-step evaluation · Progress · Configurations on the evaluation path of Landin's knot · Assignment preserves store typing · One-step evaluation with references · Multi-step evaluation with references · Type safety · Type safety from the empty store

InductiveOne-step evaluation with references#✓fully proved

One step of call-by-value evaluation \(t \mid \mu \to t' \mid \mu'\), from a term \(t\) with a store \(\mu\) to a term \(t'\) with a store \(\mu'\), is the least relation closed under the following rules, in which \(v\), \(v_1\) and \(v_2\) are values. If \(t \mid \mu \to t' \mid \mu'\), then \(t\,t_2 \mid \mu \to t'\,t_2 \mid \mu'\), \(v_1\,t \mid \mu \to v_1\,t' \mid \mu'\), \(\mathsf{ref}\,t \mid \mu \to \mathsf{ref}\,t' \mid \mu'\), \(!t \mid \mu \to {!t'} \mid \mu'\), \(t := t_2 \mid \mu \to t' := t_2 \mid \mu'\) and \(v_1 := t \mid \mu \to v_1 := t' \mid \mu'\). The application \((\lambda{:}T.\,s)\,v_2\) with store \(\mu\) steps, with \(\mu\) unchanged, to the result of substituting \(v_2\) for variable \(0\) in \(s\). The allocation \(\mathsf{ref}\,v\) with store \(\mu\) steps to the location \(n\), where \(n\) is the length of \(\mu\), and the store becomes \(\mu\) with \(v\) appended at the end. If \(\mu\) has an entry \(u\) at location \(l\), then \(!l \mid \mu \to u \mid \mu\). If \(l\) is less than the length of \(\mu\), then \(l := v \mid \mu \to \mathsf{unit} \mid \mu'\), where \(\mu'\) is \(\mu\) with its entry at \(l\) replaced by \(v\).

Cslib.Languages.LambdaCalculus.References.Step · 33 lines 
inductive Step : Term Base → Store Base → Term Base → Store Base → Prop
  /-- E-App1. -/
  | appLeft {t₁ t₁' t₂ : Term Base} {μ μ' : Store Base}
      (h : Step t₁ μ t₁' μ') : Step (.app t₁ t₂) μ (.app t₁' t₂) μ'
  /-- E-App2. -/
  | appRight {v₁ t₂ t₂' : Term Base} {μ μ' : Store Base}
      (hv₁ : v₁.Value) (h : Step t₂ μ t₂' μ') : Step (.app v₁ t₂) μ (.app v₁ t₂') μ'
  /-- E-AppAbs. -/
  | appAbs {T : Ty Base} {body v₂ : Term Base} {μ : Store Base}
      (hv₂ : v₂.Value) : Step (.app (.lam T body) v₂) μ (body.instantiate v₂) μ
  /-- E-Ref. -/
  | ref {t t' : Term Base} {μ μ' : Store Base}
      (h : Step t μ t' μ') : Step (.ref t) μ (.ref t') μ'
  /-- E-RefV, allocating the fresh location `μ.length` at the end of the
  store. -/
  | refValue {v : Term Base} {μ : Store Base}
      (hv : v.Value) : Step (.ref v) μ (.loc μ.length) (μ ++ [v])
  /-- E-Deref. -/
  | deref {t t' : Term Base} {μ μ' : Store Base}
      (h : Step t μ t' μ') : Step (.deref t) μ (.deref t') μ'
  /-- E-DerefLoc. -/
  | derefLoc {l : Nat} {v : Term Base} {μ : Store Base}
      (hl : μ[l]? = some v) : Step (.deref (.loc l)) μ v μ
  /-- E-Assign1. -/
  | assignLeft {t₁ t₁' t₂ : Term Base} {μ μ' : Store Base}
      (h : Step t₁ μ t₁' μ') : Step (.assign t₁ t₂) μ (.assign t₁' t₂) μ'
  /-- E-Assign2. -/
  | assignRight {v₁ t₂ t₂' : Term Base} {μ μ' : Store Base}
      (hv₁ : v₁.Value) (h : Step t₂ μ t₂' μ') :
      Step (.assign v₁ t₂) μ (.assign v₁ t₂') μ'
  /-- E-Assign: overwrite an allocated location. -/
  | assignLoc {l : Nat} {v : Term Base} {μ : Store Base}
      (hv : v.Value) (hl : l < μ.length) : Step (.assign (.loc l) v) μ .unit (μ.set l v)
Sources
  • TAPL Figure 13-1, with each fresh location allocated at the end of the store.
Uses 5 · Used by 12
Statement usesStore · Terms of the simply typed lambda calculus with references · Values of the simply typed lambda calculus with references · Substitution of a term for variable zero · Types of the simply typed lambda calculus with references
Used byDeterminism of evaluation with references · The cycle of Landin's knot · Landin's knot never evaluates to a value · The first four steps of Landin's knot · Landin's knot never gets stuck · Values do not step · Preservation for the lambda calculus with references · Preservation for multi-step evaluation · Progress · Multi-step evaluation with references · Type safety · Type safety from the empty store

DefinitionMulti-step evaluation with references#✓fully proved

The relation \(t \mid \mu \to^* t' \mid \mu'\) holds when the configuration \((t, \mu)\) reaches \((t', \mu')\) in zero or more evaluation steps; that is, it is the reflexive-transitive closure of one-step evaluation on pairs of a term and a store.

def Steps (t : Term Base) (μ : Store Base) (t' : Term Base) (μ' : Store Base) : Prop :=
  Relation.ReflTransGen (fun (c c' : Term Base × Store Base) => Step c.1 c.2 c'.1 c'.2)
    (t, μ) (t', μ')
Uses 3 · Used by 5
Statement usesOne-step evaluation with references · Store · Terms of the simply typed lambda calculus with references
Used byLandin's knot never evaluates to a value · Landin's knot never gets stuck · Preservation for multi-step evaluation · Type safety · Type safety from the empty store

TheoremValues do not step#✓fully proved

If \(v\) is a value, then there are no stores \(\mu\), \(\mu'\) and term \(t'\) such that the configuration \((v, \mu)\) steps to \((t', \mu')\): values are normal forms.

theorem not_of_value {v t' : Term Base} {μ μ' : Store Base} (hv : v.Value) :
    ¬ Step v μ t' μ'
Uses 6 · Used by 1
Statement usesOne-step evaluation with references · Store · Terms of the simply typed lambda calculus with references · Values of the simply typed lambda calculus with references
Proof usesSubstitution of a term for variable zero · Types of the simply typed lambda calculus with references
Used byDeterminism of evaluation with references

TheoremDeterminism of evaluation with references#✓fully proved

If a configuration \((t, \mu)\) steps to \((t_1, \mu_1)\) and also to \((t_2, \mu_2)\), then \(t_1 = t_2\) and \(\mu_1 = \mu_2\).

This relies on allocating each fresh location at the end of the store, at the index equal to the length of \(\mu\); with TAPL's arbitrary choice of fresh location only the result up to renaming of locations is unique.

theorem deterministic {t t₁ t₂ : Term Base} {μ μ₁ μ₂ : Store Base}
    (h₁ : Step t μ t₁ μ₁) (h₂ : Step t μ t₂ μ₂) : t₁ = t₂ ∧ μ₁ = μ₂
Uses 7 · Used by 2
Statement usesOne-step evaluation with references · Store · Terms of the simply typed lambda calculus with references
Proof usesValues do not step · Values of the simply typed lambda calculus with references · Substitution of a term for variable zero · Types of the simply typed lambda calculus with references
Used byLandin's knot never evaluates to a value · Landin's knot never gets stuck

TheoremRenaming respects pointwise equality#✓fully proved

Let \(\rho, \rho' : \mathbb{N} \to \mathbb{N}\) be renamings of de Bruijn variables with \(\rho(x) = \rho'(x)\) for every \(x \in \mathbb{N}\). Then for every term \(t\) of the simply typed lambda calculus with references, renaming \(t\) by \(\rho\) gives the same term as renaming \(t\) by \(\rho'\).

theorem rename_congr {ρ ρ' : Nat → Nat} (h : ∀ x, ρ x = ρ' x) (t : Term Base) :
    rename ρ t = rename ρ' t
Uses 4 · Used by 3
Statement usesTerms of the simply typed lambda calculus with references · Renaming the variables of a term
Proof usesLifting a renaming under a binder in the lambda calculus with references · Types of the simply typed lambda calculus with references
Used byRenaming by the identity · Composition of renamings · Substituting then renaming

TheoremRenaming by the identity#✓fully proved

For every term \(t\) of the simply typed lambda calculus with references, renaming the de Bruijn variables of \(t\) by the identity map of \(\mathbb{N}\) gives back \(t\).

@[simp] theorem rename_id (t : Term Base) : rename id t = t
Uses 5
Statement usesTerms of the simply typed lambda calculus with references · Renaming the variables of a term
Proof usesLifting a renaming under a binder in the lambda calculus with references · Renaming respects pointwise equality · Types of the simply typed lambda calculus with references

TheoremComposition of renamings#✓fully proved

For all renamings \(\rho, \rho' : \mathbb{N} \to \mathbb{N}\) of de Bruijn variables and every term \(t\) of the simply typed lambda calculus with references, renaming \(t\) by \(\rho\) and then renaming the result by \(\rho'\) gives the same term as renaming \(t\) by the composite \(\rho' \circ \rho\).

theorem rename_rename (ρ ρ' : Nat → Nat) (t : Term Base) :
    rename ρ' (rename ρ t) = rename (ρ' ∘ ρ) t
Uses 5 · Used by 1
Statement usesTerms of the simply typed lambda calculus with references · Renaming the variables of a term
Proof usesLifting a renaming under a binder in the lambda calculus with references · Renaming respects pointwise equality · Types of the simply typed lambda calculus with references
Used bySubstituting then renaming

TheoremSubstitution respects pointwise equality#✓fully proved

Let \(\sigma, \sigma'\) be parallel substitutions, each sending every de Bruijn index to a term of the simply typed lambda calculus with references, with \(\sigma(x) = \sigma'(x)\) for every \(x \in \mathbb{N}\). Then for every term \(t\), applying \(\sigma\) to \(t\) gives the same term as applying \(\sigma'\) to \(t\).

theorem subst_congr {σ σ' : Nat → Term Base} (h : ∀ x, σ x = σ' x) (t : Term Base) :
    subst σ t = subst σ' t
Uses 5 · Used by 5
Statement usesTerms of the simply typed lambda calculus with references · Parallel substitution in a term
Proof usesLifting a substitution under a binder · Renaming the variables of a term · Types of the simply typed lambda calculus with references
Used byInstantiating a shifted term · Substituting then renaming · Substitution by variables is the identity · Renaming then substituting · Composition of substitutions in the lambda calculus with references

TheoremSubstitution by variables is the identity#✓fully proved

For every term \(t\) of the simply typed lambda calculus with references, applying the parallel substitution that sends each de Bruijn index \(x\) to the variable term \(x\) gives back \(t\).

@[simp] theorem subst_id (t : Term Base) : subst .var t = t
Uses 5 · Used by 1
Statement usesTerms of the simply typed lambda calculus with references · Parallel substitution in a term
Proof usesLifting a substitution under a binder · Substitution respects pointwise equality · Types of the simply typed lambda calculus with references
Used byInstantiating a shifted term

TheoremRenaming then substituting#✓fully proved

Let \(\rho : \mathbb{N} \to \mathbb{N}\) be a renaming of de Bruijn variables, \(\sigma\) a parallel substitution sending each index to a term of the simply typed lambda calculus with references, and \(t\) a term. Renaming \(t\) by \(\rho\) and then applying \(\sigma\) gives the same term as applying the substitution \(\sigma \circ \rho\) to \(t\).

theorem subst_rename (ρ : Nat → Nat) (σ : Nat → Term Base) (t : Term Base) :
    subst σ (rename ρ t) = subst (σ ∘ ρ) t
Uses 7 · Used by 2
Statement usesTerms of the simply typed lambda calculus with references · Renaming the variables of a term · Parallel substitution in a term
Proof usesLifting a renaming under a binder in the lambda calculus with references · Lifting a substitution under a binder · Substitution respects pointwise equality · Types of the simply typed lambda calculus with references
Used byInstantiating a shifted term · Composition of substitutions in the lambda calculus with references

TheoremSubstituting then renaming#✓fully proved

Let \(\rho : \mathbb{N} \to \mathbb{N}\) be a renaming of de Bruijn variables, \(\sigma\) a parallel substitution sending each index to a term of the simply typed lambda calculus with references, and \(t\) a term. Applying \(\sigma\) to \(t\) and then renaming the result by \(\rho\) gives the same term as applying to \(t\) the substitution that sends each index \(x\) to the renaming of \(\sigma(x)\) by \(\rho\).

theorem rename_subst (ρ : Nat → Nat) (σ : Nat → Term Base) (t : Term Base) :
    rename ρ (subst σ t) = subst (rename ρ ∘ σ) t
Uses 9 · Used by 1
Statement usesTerms of the simply typed lambda calculus with references · Renaming the variables of a term · Parallel substitution in a term
Proof usesLifting a renaming under a binder in the lambda calculus with references · Lifting a substitution under a binder · Renaming respects pointwise equality · Composition of renamings · Substitution respects pointwise equality · Types of the simply typed lambda calculus with references
Used byComposition of substitutions in the lambda calculus with references

TheoremComposition of substitutions in the lambda calculus with references#✓fully proved

For all parallel substitutions \(\sigma, \tau\), each sending every de Bruijn index to a term of the simply typed lambda calculus with references, and every term \(t\), applying \(\sigma\) to \(t\) and then \(\tau\) to the result gives the same term as applying to \(t\) the substitution that sends each index \(x\) to the result of applying \(\tau\) to \(\sigma(x)\).

theorem subst_subst (σ τ : Nat → Term Base) (t : Term Base) :
    subst τ (subst σ t) = subst (fun x => subst τ (σ x)) t
Uses 8
Statement usesTerms of the simply typed lambda calculus with references · Parallel substitution in a term
Proof usesLifting a substitution under a binder · Renaming the variables of a term · Substituting then renaming · Substitution respects pointwise equality · Renaming then substituting · Types of the simply typed lambda calculus with references

TheoremInstantiating a shifted term#✓fully proved

For all terms \(t\) and \(s\) of the simply typed lambda calculus with references, shift every free de Bruijn variable of \(t\) up by one (rename by \(x \mapsto x + 1\)), then instantiate the result with \(s\), replacing variable \(0\) by \(s\) and lowering every other variable \(x + 1\) to \(x\). The outcome is \(t\).

@[simp] theorem instantiate_rename_succ (t s : Term Base) :
    (rename Nat.succ t).instantiate s = t
Uses 8
Statement usesTerms of the simply typed lambda calculus with references · Substitution of a term for variable zero · Renaming the variables of a term
Proof usesSingle-variable substitution at index zero · Parallel substitution in a term · Substitution respects pointwise equality · Substitution by variables is the identity · Renaming then substituting

InductiveTyping judgment for the lambda calculus with references#✓fully proved

The judgment \(\Gamma \mid S \vdash t : T\) (TAPL Figure 13-1), where the context \(\Gamma\) lists the types of the free de Bruijn variables (index \(0\) first) and the store typing \(S\) lists the types of the locations \(0, 1, \ldots\), is the least relation closed under the following rules, in which \(t : T\) abbreviates \(\Gamma \mid S \vdash t : T\). A variable \(x\) has type \(T\) if \(\Gamma\) assigns \(T\) to index \(x\). If \(t\) has type \(T_2\) in the context \(\Gamma\) extended by \(T_1\) at index \(0\) (with the same \(S\)), then \(\lambda{:}T_1.\, t : T_1 \to T_2\). If \(t_1 : T_1 \to T_2\) and \(t_2 : T_1\), then \(t_1\, t_2 : T_2\). The term \(\mathtt{unit}\) has type \(\mathrm{Unit}\). A location \(l\) has type \(\mathrm{Ref}\, T\) if \(S\) assigns \(T\) to \(l\). If \(t : T\), then \(\mathrm{ref}\, t : \mathrm{Ref}\, T\). If \(t : \mathrm{Ref}\, T\), then \(!t : T\). If \(t_1 : \mathrm{Ref}\, T\) and \(t_2 : T\), then \(t_1 := t_2\) has type \(\mathrm{Unit}\).

Cslib.Languages.LambdaCalculus.References.HasType · 21 lines 
inductive HasType : List (Ty Base) → List (Ty Base) → Term Base → Ty Base → Prop
  | var {Γ S : List (Ty Base)} {x : Nat} {T : Ty Base} (hx : Γ[x]? = some T) :
      HasType Γ S (.var x) T
  | lam {Γ S : List (Ty Base)} {T₁ T₂ : Ty Base} {body : Term Base}
      (hbody : HasType (T₁ :: Γ) S body T₂) :
      HasType Γ S (.lam T₁ body) (.arr T₁ T₂)
  | app {Γ S : List (Ty Base)} {T₁ T₂ : Ty Base} {f a : Term Base}
      (hf : HasType Γ S f (.arr T₁ T₂)) (ha : HasType Γ S a T₁) :
      HasType Γ S (.app f a) T₂
  | unit {Γ S : List (Ty Base)} : HasType Γ S .unit .unit
  | loc {Γ S : List (Ty Base)} {l : Nat} {T : Ty Base} (hl : S[l]? = some T) :
      HasType Γ S (.loc l) (.ref T)
  | ref {Γ S : List (Ty Base)} {t : Term Base} {T : Ty Base}
      (ht : HasType Γ S t T) :
      HasType Γ S (.ref t) (.ref T)
  | deref {Γ S : List (Ty Base)} {t : Term Base} {T : Ty Base}
      (ht : HasType Γ S t (.ref T)) :
      HasType Γ S (.deref t) T
  | assign {Γ S : List (Ty Base)} {t₁ t₂ : Term Base} {T : Ty Base}
      (ht₁ : HasType Γ S t₁ (.ref T)) (ht₂ : HasType Γ S t₂ T) :
      HasType Γ S (.assign t₁ t₂) .unit
Uses 2 · Used by 22
Statement usesTerms of the simply typed lambda calculus with references · Types of the simply typed lambda calculus with references
Used byAllocation preserves store typing · Well-typed stores hold a typed value at every location · Store-typing weakening · Retyping a well-typed store under an extended store typing · Substitution lemma for the lambda calculus with references · Landin's knot is well typed · Canonical forms for function types · Canonical forms for reference types · No value has a base type · Typing is preserved by the embedding of raw STLC terms · Typing of embedded intrinsically typed STLC terms · Preservation for the lambda calculus with references · Preservation for multi-step evaluation · Progress · Renaming preserves typing · Assignment preserves store typing · Well-typed stores · Parallel substitution preserves typing · Type safety · Type safety from the empty store · Canonical forms for the unit type · Weakening of typing

DefinitionWell-typed stores#✓fully proved

Let \(\Gamma\) be a variable context and \(S\) a store typing. A store \(\mu\), a list of terms whose entry at index \(l\) is the contents of location \(l\), is well typed under \(\Gamma\) and \(S\), written \(\Gamma \mid S \vdash \mu\), when \(\mu\) and \(S\) have the same length and, for every location \(l\) less than this length, the entry of \(\mu\) at \(l\) is a value that has, under \(\Gamma\) and \(S\), the type that \(S\) assigns to \(l\).

Stores here are lists of terms rather than of values, so each entry is required to be a value.

def StoreTyped (Γ S : List (Ty Base)) (μ : List (Term Base)) : Prop :=
  List.Forall₂ (fun v T => v.Value ∧ HasType Γ S v T) μ S
Sources
  • TAPL Definition 13.5.1.
Uses 4 · Used by 8
Statement usesTyping judgment for the lambda calculus with references · Terms of the simply typed lambda calculus with references · Values of the simply typed lambda calculus with references · Types of the simply typed lambda calculus with references
Used byAllocation preserves store typing · Well-typed stores hold a typed value at every location · Retyping a well-typed store under an extended store typing · Preservation for the lambda calculus with references · Preservation for multi-step evaluation · Progress · Assignment preserves store typing · Type safety

TheoremWell-typed stores hold a typed value at every location#✓fully proved

Let \(\Gamma\) be a typing context, \(S\) a store typing, and \(\mu\) a store (a list of terms, whose entry at index \(l\) is the contents of location \(l\)) that is well typed, \(\Gamma \mid S \vdash \mu\). If \(S\) assigns type \(T\) to location \(l\), then \(\mu\) has an entry \(v\) at location \(l\), \(v\) is a value, and \(\Gamma \mid S \vdash v : T\).

theorem exists_of_getElem? {l : Nat} {T : Ty Base} (h : StoreTyped Γ S μ)
    (hl : S[l]? = some T) : ∃ v, μ[l]? = some v ∧ v.Value ∧ HasType Γ S v T
Uses 5 · Used by 2
Statement usesTyping judgment for the lambda calculus with references · Well-typed stores · Terms of the simply typed lambda calculus with references · Values of the simply typed lambda calculus with references · Types of the simply typed lambda calculus with references
Used byPreservation for the lambda calculus with references · Progress

TheoremCanonical forms for function types#✓fully proved

For every context \(\Gamma\) and store typing \(S\), if \(v\) is a value and \(\Gamma \mid S \vdash v : T_1 \to T_2\), then \(v\) is an abstraction \(\lambda{:}T_1.\, t\) with parameter type \(T_1\), for some body \(t\).

theorem lam_of_value {T₁ T₂ : Ty Base} (hv : v.Value) (h : HasType Γ S v (.arr T₁ T₂)) :
    ∃ body, v = .lam T₁ body
Uses 4 · Used by 1
Statement usesTyping judgment for the lambda calculus with references · Terms of the simply typed lambda calculus with references · Values of the simply typed lambda calculus with references · Types of the simply typed lambda calculus with references
Used byProgress

TheoremCanonical forms for reference types#✓fully proved

For every context \(\Gamma\) and store typing \(S\), if \(v\) is a value and \(\Gamma \mid S \vdash v : \mathrm{Ref}\, T\), then \(v\) is a location \(l\) to which \(S\) assigns type \(T\).

theorem loc_of_value {T : Ty Base} (hv : v.Value) (h : HasType Γ S v (.ref T)) :
    ∃ l, v = .loc l ∧ S[l]? = some T
Uses 4 · Used by 1
Statement usesTyping judgment for the lambda calculus with references · Terms of the simply typed lambda calculus with references · Values of the simply typed lambda calculus with references · Types of the simply typed lambda calculus with references
Used byProgress

TheoremCanonical forms for the unit type#✓fully proved

For every context \(\Gamma\) and store typing \(S\), if \(v\) is a value and \(\Gamma \mid S \vdash v : \mathrm{Unit}\), then \(v = \mathtt{unit}\).

theorem unit_of_value (hv : v.Value) (h : HasType Γ S v .unit) : v = .unit
Uses 4
Statement usesTyping judgment for the lambda calculus with references · Terms of the simply typed lambda calculus with references · Values of the simply typed lambda calculus with references · Types of the simply typed lambda calculus with references

TheoremNo value has a base type#✓fully proved

For every context \(\Gamma\), store typing \(S\) and base type \(b\), there is no value \(v\) with \(\Gamma \mid S \vdash v : b\).

theorem not_value_base {b : Base} (hv : v.Value) (h : HasType Γ S v (.base b)) : False
Uses 4
Statement usesTyping judgment for the lambda calculus with references · Terms of the simply typed lambda calculus with references · Values of the simply typed lambda calculus with references · Types of the simply typed lambda calculus with references

DefinitionThe identity on Unit#✓fully proved

The identity function \(\lambda x{:}\mathrm{Unit}.\ x\) on the unit type.

def idU : Term Base := .lam .unit (.var 0)
Uses 2 · Used by 6
Statement usesTerms of the simply typed lambda calculus with references · Types of the simply typed lambda calculus with references
Used byLandin's knot · Landin's knot never evaluates to a value · Landin's knot is well typed · The first four steps of Landin's knot · Landin's knot never gets stuck · Configurations on the evaluation path of Landin's knot

DefinitionThe recursive function of Landin's knot, with the cell free#✓fully proved

The term \(\lambda x{:}\mathrm{Unit}.\ (!r)\,x\), which applies the contents of the reference \(r\) to its argument. Here \(r\) is a free variable, de Bruijn index \(1\) under the binder \(\lambda x\); in Landin's knot it is bound by the outer \(\lambda r\).

def body : Term Base := .lam .unit (.app (.deref (.var 1)) (.var 0))
Uses 2 · Used by 6
Statement usesTerms of the simply typed lambda calculus with references · Types of the simply typed lambda calculus with references
Used byThe knot after allocation · Landin's knot · Landin's knot never evaluates to a value · Landin's knot is well typed · The first four steps of Landin's knot · Landin's knot never gets stuck

DefinitionLandin's knot#✓fully proved

The term

\[ (\lambda r{:}\mathrm{Ref}\,(\mathrm{Unit}\to\mathrm{Unit}).\ (\lambda y{:}\mathrm{Unit}.\ (!r)\, \mathrm{unit})\ (r := \lambda x{:}\mathrm{Unit}.\ (!r)\,x)) \ (\mathrm{ref}\,(\lambda x{:}\mathrm{Unit}.\ x)) \]

of the simply typed lambda calculus with references.

It allocates a cell \(r\) holding the identity on \(\mathrm{Unit}\), overwrites it with a function that calls whatever \(r\) holds, and then calls the contents of \(r\) on \(\mathrm{unit}\): a recursive knot tied through the store.

def knot : Term Base :=
  .app (.lam (.ref (.arr .unit .unit))
      (.app (.lam .unit (.app (.deref (.var 1)) .unit)) (.assign (.var 0) body)))
    (.ref idU)
Uses 4 · Used by 5
Statement usesThe recursive function of Landin's knot, with the cell free · The identity on Unit · Terms of the simply typed lambda calculus with references · Types of the simply typed lambda calculus with references
Used byLandin's knot never evaluates to a value · Landin's knot is well typed · The first four steps of Landin's knot · Landin's knot never gets stuck · Configurations on the evaluation path of Landin's knot

DefinitionThe stored recursive function of Landin's knot#✓fully proved

The term \(b_0 = \lambda x{:}\mathrm{Unit}.\ (!\ell_0)\,x\), which applies the contents of store location \(\ell_0 = 0\) to its argument.

It is the function Landin's knot writes into location \(0\).

def body₀ : Term Base := .lam .unit (.app (.deref (.loc 0)) (.var 0))
Uses 2 · Used by 5
Statement usesTerms of the simply typed lambda calculus with references · Types of the simply typed lambda calculus with references
Used byThe cycle of Landin's knot · Landin's knot never evaluates to a value · The first four steps of Landin's knot · Landin's knot never gets stuck · Configurations on the evaluation path of Landin's knot

DefinitionCycle term of Landin's knot#✓fully proved

The term \((!\ell_0)\ \mathrm{unit}\): the dereference of the store location \(\ell_0\) (location \(0\)), applied to the unit value.

When \(\ell_0\) holds \(b_0 = \lambda x{:}\mathrm{Unit}.\,(!\ell_0)\,x\), this term steps to \(b_0\ \mathrm{unit}\), which steps back to it; these are the two configurations of the cycle.

def loopA : Term Base := .app (.deref (.loc 0)) .unit
Uses 1 · Used by 5
Statement usesTerms of the simply typed lambda calculus with references
Used byThe cycle of Landin's knot · Landin's knot never evaluates to a value · The first four steps of Landin's knot · Landin's knot never gets stuck · Configurations on the evaluation path of Landin's knot

DefinitionThe knot after allocation#✓fully proved

The term \((\lambda r{:}\mathrm{Ref}\,(\mathrm{Unit}\to\mathrm{Unit}).\ (\lambda y{:}\mathrm{Unit}.\ (!r)\, \mathrm{unit})\ (r := \lambda x{:}\mathrm{Unit}.\ (!r)\,x))\ \ell_0\), where \(\ell_0\) is store location \(0\): Landin's knot with its allocation \(\mathrm{ref}\,(\lambda x{:}\mathrm{Unit}.\ x)\) replaced by \(\ell_0\).

def c₁ : Term Base :=
  .app (.lam (.ref (.arr .unit .unit))
      (.app (.lam .unit (.app (.deref (.var 1)) .unit)) (.assign (.var 0) body)))
    (.loc 0)
Uses 3 · Used by 4
Statement usesThe recursive function of Landin's knot, with the cell free · Terms of the simply typed lambda calculus with references · Types of the simply typed lambda calculus with references
Used byLandin's knot never evaluates to a value · The first four steps of Landin's knot · Landin's knot never gets stuck · Configurations on the evaluation path of Landin's knot

TheoremThe first four steps of Landin's knot#✓fully proved

Write \(\ell_0\) for store location \(0\) and \([t]\) for the store whose only entry, at \(\ell_0\), is \(t\), and let \(\mathrm{id} = \lambda x{:}\mathrm{Unit}.\ x\) and \(b_0 = \lambda x{:}\mathrm{Unit}.\ (!\ell_0)\,x\). Each of the following is one call-by-value step: Landin's knot with the empty store steps to \((\lambda r{:}\mathrm{Ref}\,(\mathrm{Unit}\to\mathrm{Unit}).\ (\lambda y{:}\mathrm{Unit}.\ (!r)\, \mathrm{unit})\ (r := \lambda x{:}\mathrm{Unit}.\ (!r)\,x))\ \ell_0\) with store \([\mathrm{id}]\); that term with store \([\mathrm{id}]\) steps to \((\lambda y{:}\mathrm{Unit}.\ (!\ell_0)\,\mathrm{unit})\ (\ell_0 := b_0)\) with store \([\mathrm{id}]\); that term with store \([\mathrm{id}]\) steps to \((\lambda y{:}\mathrm{Unit}.\ (!\ell_0)\,\mathrm{unit})\ \mathrm{unit}\) with store \([b_0]\); and that term with store \([b_0]\) steps to \((!\ell_0)\,\mathrm{unit}\) with store \([b_0]\).

theorem knot_prefix :
    Step (knot : Term Base) [] c₁ [idU] ∧ Step (c₁ : Term Base) [idU] c₂ [idU] ∧
      Step (c₂ : Term Base) [idU] c₃ [body₀] ∧ Step (c₃ : Term Base) [body₀] loopA [body₀]
Uses 12
Statement usesThe stored recursive function of Landin's knot · The knot after allocation · The identity on Unit · Landin's knot · Cycle term of Landin's knot · One-step evaluation with references · Terms of the simply typed lambda calculus with references · Types of the simply typed lambda calculus with references
Proof usesThe recursive function of Landin's knot, with the cell free · Store · Values of the simply typed lambda calculus with references · Substitution of a term for variable zero

TheoremThe cycle of Landin's knot#✓fully proved

Write \(\ell_0\) for store location \(0\), let \(b_0 = \lambda x{:}\mathrm{Unit}.\ (!\ell_0)\,x\), and let \([b_0]\) be the store whose only entry, at \(\ell_0\), is \(b_0\). In one call-by-value step, \((!\ell_0)\,\mathrm{unit}\) with store \([b_0]\) steps to \(b_0\,\mathrm{unit}\) with store \([b_0]\), and in one further step \(b_0\,\mathrm{unit}\) with store \([b_0]\) steps back to \((!\ell_0)\,\mathrm{unit}\) with store \([b_0]\).

theorem knot_cycle :
    Step (loopA : Term Base) [body₀] loopB [body₀] ∧
      Step (loopB : Term Base) [body₀] loopA [body₀]
Uses 8
Statement usesThe stored recursive function of Landin's knot · Cycle term of Landin's knot · One-step evaluation with references · Terms of the simply typed lambda calculus with references
Proof usesStore · Values of the simply typed lambda calculus with references · Substitution of a term for variable zero · Types of the simply typed lambda calculus with references

DefinitionConfigurations on the evaluation path of Landin's knot#✓fully proved

Let \(K\) be Landin's knot, \(\iota = \lambda x{:}\mathrm{Unit}.\,x\), \(b_0 = \lambda x{:}\mathrm{Unit}.\,(!\ell_0)\,x\) with \(\ell_0\) the store location \(0\), \(a = (!\ell_0)\ \mathrm{unit}\), \(b = b_0\ \mathrm{unit}\), \(c_1\) the term \(K\) with its argument \(\mathrm{ref}\ \iota\) replaced by \(\ell_0\), \(c_2 = (\lambda y{:}\mathrm{Unit}.\,a)\,(\ell_0 := b_0)\) and \(c_3 = (\lambda y{:}\mathrm{Unit}.\,a)\ \mathrm{unit}\); write \([\,]\) for the empty store and \([t]\) for the store whose only location \(\ell_0\) holds \(t\). This is the list of the six configurations (term, store) \((K, [\,])\), \((c_1, [\iota])\), \((c_2, [\iota])\), \((c_3, [b_0])\), \((a, [b_0])\), \((b, [b_0])\).

Each configuration steps to the next and \((b, [b_0])\) steps back to \((a, [b_0])\); every configuration reachable from \((K, [\,])\) lies in this list.

def reachable : List (Term Base × Store Base) :=
  [(knot, []), (c₁, [idU]), (c₂, [idU]), (c₃, [body₀]), (loopA, [body₀]), (loopB, [body₀])]
Uses 8 · Used by 2
Statement usesThe stored recursive function of Landin's knot · The knot after allocation · The identity on Unit · Landin's knot · Cycle term of Landin's knot · Store · Terms of the simply typed lambda calculus with references · Types of the simply typed lambda calculus with references
Used byLandin's knot never evaluates to a value · Landin's knot never gets stuck

TheoremLandin's knot is well typed#✓fully proved

Landin's knot is closed and has type \(\mathrm{Unit}\) in the empty typing context under the empty store typing.

theorem knot_hasType : HasType ([] : List (Ty Base)) [] (knot : Term Base) .unit
Uses 6
Statement usesTyping judgment for the lambda calculus with references · Landin's knot · Types of the simply typed lambda calculus with references
Proof usesThe recursive function of Landin's knot, with the cell free · The identity on Unit · Terms of the simply typed lambda calculus with references

TheoremLandin's knot never evaluates to a value#✓fully proved

Starting from Landin's knot with the empty store, no sequence of zero or more call-by-value evaluation steps reaches a configuration \((v, \mu)\) in which the term \(v\) is a value, whatever the store \(\mu\).

theorem knot_diverges :
    ¬ ∃ (v : Term Base) (μ : Store Base), Steps (knot : Term Base) [] v μ ∧ v.Value
Uses 15
Statement usesLandin's knot · Multi-step evaluation with references · Store · Terms of the simply typed lambda calculus with references · Values of the simply typed lambda calculus with references
Proof usesThe recursive function of Landin's knot, with the cell free · The stored recursive function of Landin's knot · The knot after allocation · The identity on Unit · Cycle term of Landin's knot · Configurations on the evaluation path of Landin's knot · One-step evaluation with references · Determinism of evaluation with references · Substitution of a term for variable zero · Types of the simply typed lambda calculus with references

TheoremLandin's knot never gets stuck#✓fully proved

If Landin's knot with the empty store evaluates in zero or more call-by-value steps to a term \(t\) with store \(\mu\), then \(t\) with store \(\mu\) takes a further step to some term \(t'\) with some store \(\mu'\). So the evaluation of the knot runs forever.

theorem knot_runs_forever {t : Term Base} {μ : Store Base}
    (h : Steps (knot : Term Base) [] t μ) : ∃ t' μ', Step t μ t' μ'
Uses 15
Statement usesLandin's knot · One-step evaluation with references · Multi-step evaluation with references · Store · Terms of the simply typed lambda calculus with references
Proof usesThe recursive function of Landin's knot, with the cell free · The stored recursive function of Landin's knot · The knot after allocation · The identity on Unit · Cycle term of Landin's knot · Configurations on the evaluation path of Landin's knot · Determinism of evaluation with references · Values of the simply typed lambda calculus with references · Substitution of a term for variable zero · Types of the simply typed lambda calculus with references

DefinitionEmbedding of simple types into the calculus with references#✓fully proved

Fix a type \(B\) of base types. The embedding \(\iota\) sends a simple type over \(B\) to a type of the calculus with references over \(B\), by recursion: \(\iota(b) = b\) for a base type \(b \in B\), and \(\iota(A_1 \to A_2) = \iota(A_1) \to \iota(A_2)\).

def Ty.ofStlc : Stlc.Ty Base → Ty Base
  | .base b => .base b
  | .arr A B => .arr (ofStlc A) (ofStlc B)
Uses 2 · Used by 3
Statement usesTypes of the simply typed lambda calculus with references · Simple types
Used byEmbedding of raw STLC terms into the calculus with references · Typing is preserved by the embedding of raw STLC terms · Typing of embedded intrinsically typed STLC terms

DefinitionEmbedding of raw STLC terms into the calculus with references#✓fully proved

Fix a type \(B\) of base types. The embedding \(\iota\) sends a raw (extrinsically typed, binder-annotated) term of the simply typed lambda calculus over \(B\) to a term of the calculus with references over \(B\), by recursion: a de Bruijn variable \(n\) goes to the variable \(n\), an application \(f\,a\) goes to \(\iota(f)\,\iota(a)\), and an abstraction \(\lambda{:}A.\,t\) goes to \(\lambda{:}\iota(A).\,\iota(t)\), where \(\iota(A)\) is the embedding of the simple type \(A\).

The image is reference-free: it contains no unit value, locations, allocations, dereferences or assignments.

def Term.ofRaw : Stlc.RawTm Base → Term Base
  | .var n => .var n
  | .app f a => .app (ofRaw f) (ofRaw a)
  | .lam A body => .lam (Ty.ofStlc A) (ofRaw body)
Uses 5 · Used by 2
Statement usesTerms of the simply typed lambda calculus with references · Types of the simply typed lambda calculus with references · Embedding of simple types into the calculus with references · Raw lambda terms · Simple types
Used byTyping is preserved by the embedding of raw STLC terms · Typing of embedded intrinsically typed STLC terms

TheoremTyping is preserved by the embedding of raw STLC terms#✓fully proved

Fix a type \(B\) of base types, and write \(\iota\) for the embeddings of simple types and of raw terms of the simply typed lambda calculus over \(B\) into types and terms of the calculus with references over \(B\). Let \(\Gamma\) be a context of simple types, \(t\) a raw term and \(A\) a simple type such that \(t\) has type \(A\) in \(\Gamma\). Then for every store typing \(S\) we have \(\iota(\Gamma) \mid S \vdash \iota(t) : \iota(A)\), where \(\iota(\Gamma)\) is the context obtained by applying \(\iota\) to each entry of \(\Gamma\).

theorem HasType.ofRaw {Γ : List (Stlc.Ty Base)} {raw : Stlc.RawTm Base}
    {A : Stlc.Ty Base} (h : Stlc.HasType Γ raw A) (S : List (Ty Base)) :
    HasType (Γ.map Ty.ofStlc) S (Term.ofRaw raw) (Ty.ofStlc A)
Uses 12 · Used by 1
Statement usesTyping judgment for the lambda calculus with references · Embedding of raw STLC terms into the calculus with references · Types of the simply typed lambda calculus with references · Embedding of simple types into the calculus with references · Declarative typing of raw terms · Raw lambda terms · Simple types
Proof usesTerms of the simply typed lambda calculus with references · Typed de Bruijn variables of the simply typed lambda calculus · Index of a typed variable · Variable lookup · Lookup returns a variable with the queried index
Used byTyping of embedded intrinsically typed STLC terms

TheoremTyping of embedded intrinsically typed STLC terms#✓fully proved

Fix a type \(B\) of base types, and write \(\iota\) for the embeddings of simple types and of raw terms of the simply typed lambda calculus over \(B\) into types and terms of the calculus with references over \(B\). Let \(\Gamma\) be a context of simple types, \(A\) a simple type and \(t\) an intrinsically typed term of type \(A\) in \(\Gamma\), and let \(\mathrm{erase}(t)\) be the raw term obtained from \(t\) by erasing its typing information while keeping binder annotations. Then for every store typing \(S\) we have \(\iota(\Gamma) \mid S \vdash \iota(\mathrm{erase}(t)) : \iota(A)\), where \(\iota(\Gamma)\) is the context obtained by applying \(\iota\) to each entry of \(\Gamma\).

theorem HasType.ofStlc {Γ : List (Stlc.Ty Base)} {A : Stlc.Ty Base}
    (t : Stlc.Tm Γ A) (S : List (Ty Base)) :
    HasType (Γ.map Ty.ofStlc) S (Term.ofRaw t.erase) (Ty.ofStlc A)
Uses 9
Statement usesTyping judgment for the lambda calculus with references · Embedding of raw STLC terms into the calculus with references · Types of the simply typed lambda calculus with references · Embedding of simple types into the calculus with references · Intrinsically typed terms of the simply typed lambda calculus · Erasure of intrinsically typed terms · Simple types
Proof usesTyping is preserved by the embedding of raw STLC terms · Erasure preserves typing

TheoremProgress#✓fully proved

Let \(S\) be a store typing, \(t\) a term of some type \(T\) in the empty variable context under \(S\), and \(\mu\) a store that is well typed under \(S\) in the empty context. Then \(t\) is a value, or the configuration \((t, \mu)\) takes an evaluation step to some \((t', \mu')\).

theorem progress {S : List (Ty Base)} {μ : Store Base} {t : Term Base} {T : Ty Base}
    (ht : HasType [] S t T) (hμ : StoreTyped [] S μ) :
    t.Value ∨ ∃ t' μ', Step t μ t' μ'
Sources
  • TAPL Theorem 13.5.7.
Uses 11 · Used by 1
Statement usesTyping judgment for the lambda calculus with references · One-step evaluation with references · Store · Well-typed stores · Terms of the simply typed lambda calculus with references · Values of the simply typed lambda calculus with references · Types of the simply typed lambda calculus with references
Proof usesCanonical forms for function types · Canonical forms for reference types · Well-typed stores hold a typed value at every location · Substitution of a term for variable zero
Used byType safety

TheoremRenaming preserves typing#✓fully proved

Let \(\Gamma\) and \(\Delta\) be variable contexts, \(S\) a store typing, and \(\rho : \mathbb{N} \to \mathbb{N}\) a renaming of variable indices such that whenever \(\Gamma\) assigns type \(A\) to variable \(x\), \(\Delta\) assigns type \(A\) to variable \(\rho(x)\). If a term \(t\) has type \(T\) under \(\Gamma\) and \(S\), then the term obtained from \(t\) by renaming its variables by \(\rho\) has type \(T\) under \(\Delta\) and \(S\).

theorem rename {Γ Δ S : List (Ty Base)} {t : Term Base} {T : Ty Base}
    (h : HasType Γ S t T) {ρ : Nat → Nat}
    (hρ : ∀ x A, Γ[x]? = some A → Δ[ρ x]? = some A) :
    HasType Δ S (t.rename ρ) T
Uses 5 · Used by 1
Statement usesTyping judgment for the lambda calculus with references · Terms of the simply typed lambda calculus with references · Renaming the variables of a term · Types of the simply typed lambda calculus with references
Proof usesLifting a renaming under a binder in the lambda calculus with references
Used byWeakening of typing

TheoremWeakening of typing#✓fully proved

If a term \(t\) has type \(T\) in a variable context \(\Gamma\) under a store typing \(S\), then for every type \(A\), the term obtained from \(t\) by shifting each free de Bruijn variable up by one has type \(T\) under \(S\) in the context obtained from \(\Gamma\) by adding \(A\) in front as variable \(0\).

theorem weaken {Γ S : List (Ty Base)} {t : Term Base} {T : Ty Base} (A : Ty Base)
    (h : HasType Γ S t T) : HasType (A :: Γ) S (t.rename Nat.succ) T
Uses 5 · Used by 1
Statement usesTyping judgment for the lambda calculus with references · Terms of the simply typed lambda calculus with references · Renaming the variables of a term · Types of the simply typed lambda calculus with references
Proof usesRenaming preserves typing
Used byParallel substitution preserves typing

TheoremParallel substitution preserves typing#✓fully proved

Let \(\Gamma\) and \(\Delta\) be variable contexts, \(S\) a store typing, and \(\sigma\) a substitution sending each variable index to a term, such that whenever \(\Gamma\) assigns type \(A\) to variable \(x\), the term \(\sigma(x)\) has type \(A\) under \(\Delta\) and \(S\). If a term \(t\) has type \(T\) under \(\Gamma\) and \(S\), then the term obtained from \(t\) by applying \(\sigma\) has type \(T\) under \(\Delta\) and \(S\).

theorem subst {Γ Δ S : List (Ty Base)} {t : Term Base} {T : Ty Base}
    (h : HasType Γ S t T) {σ : Nat → Term Base}
    (hσ : ∀ x A, Γ[x]? = some A → HasType Δ S (σ x) A) :
    HasType Δ S (t.subst σ) T
Uses 6 · Used by 1
Statement usesTyping judgment for the lambda calculus with references · Terms of the simply typed lambda calculus with references · Parallel substitution in a term · Types of the simply typed lambda calculus with references
Proof usesWeakening of typing · Lifting a substitution under a binder
Used bySubstitution lemma for the lambda calculus with references

TheoremSubstitution lemma for the lambda calculus with references#✓fully proved

Let \(\Gamma\) be a variable context and \(S\) a store typing. If a term \(t\) has type \(T\) under \(S\) and the context that extends \(\Gamma\) by a new innermost variable (index \(0\)) of type \(A\), and a term \(s\) has type \(A\) under \(\Gamma\) and \(S\), then substituting \(s\) for variable \(0\) in \(t\) (and lowering every other variable by one) gives a term of type \(T\) under \(\Gamma\) and \(S\).

This is TAPL Lemma 13.5.4 in de Bruijn form.

theorem instantiate {Γ S : List (Ty Base)} {body s : Term Base} {A T : Ty Base}
    (hbody : HasType (A :: Γ) S body T) (hs : HasType Γ S s A) :
    HasType Γ S (body.instantiate s) T
Uses 6 · Used by 1
Statement usesTyping judgment for the lambda calculus with references · Terms of the simply typed lambda calculus with references · Substitution of a term for variable zero · Types of the simply typed lambda calculus with references
Proof usesParallel substitution preserves typing · Single-variable substitution at index zero
Used byPreservation for the lambda calculus with references

TheoremStore-typing weakening#✓fully proved

Let \(\Gamma\) be a variable context and let \(S\) and \(S'\) be store typings such that \(S\) is a prefix of \(S'\). If a term \(t\) has type \(T\) under \(\Gamma\) and \(S\), then \(t\) has type \(T\) under \(\Gamma\) and \(S'\).

This is TAPL Lemma 13.5.6, with the extension of store typings taken as the prefix order on lists.

theorem extendStore {Γ S S' : List (Ty Base)} {t : Term Base} {T : Ty Base}
    (h : HasType Γ S t T) (hS : S <+: S') : HasType Γ S' t T
Uses 3 · Used by 3
Statement usesTyping judgment for the lambda calculus with references · Terms of the simply typed lambda calculus with references · Types of the simply typed lambda calculus with references
Used byAllocation preserves store typing · Retyping a well-typed store under an extended store typing · Preservation for the lambda calculus with references

TheoremRetyping a well-typed store under an extended store typing#✓fully proved

Let \(\Gamma\) be a variable context, let \(S\) and \(S'\) be store typings such that \(S\) is a prefix of \(S'\), and let \(\mu\) be a store that is well typed under \(\Gamma\) and \(S\). Then \(\mu\) and \(S\) have the same length, and for every location \(l\) less than this length, the entry of \(\mu\) at \(l\) is a value that has, under \(\Gamma\) and \(S'\), the type that \(S\) assigns to \(l\).

theorem extendStore {S' : List (Ty Base)} (h : StoreTyped Γ S μ) (hS : S <+: S') :
    List.Forall₂ (fun v T => v.Value ∧ HasType Γ S' v T) μ S
Uses 7 · Used by 1
Statement usesTyping judgment for the lambda calculus with references · Store · Well-typed stores · Terms of the simply typed lambda calculus with references · Values of the simply typed lambda calculus with references · Types of the simply typed lambda calculus with references
Proof usesStore-typing weakening
Used byAllocation preserves store typing

TheoremAllocation preserves store typing#✓fully proved

Let \(\Gamma\) be a variable context, \(S\) a store typing and \(\mu\) a store that is well typed under \(\Gamma\) and \(S\). If \(v\) is a value of type \(T\) under \(\Gamma\) and \(S\), then the store obtained by appending \(v\) at the end of \(\mu\) is well typed under \(\Gamma\) and the store typing obtained by appending \(T\) at the end of \(S\).

theorem append {v : Term Base} {T : Ty Base} (h : StoreTyped Γ S μ) (hval : v.Value)
    (hv : HasType Γ S v T) : StoreTyped Γ (S ++ [T]) (μ ++ [v])
Uses 8 · Used by 1
Statement usesTyping judgment for the lambda calculus with references · Store · Well-typed stores · Terms of the simply typed lambda calculus with references · Values of the simply typed lambda calculus with references · Types of the simply typed lambda calculus with references
Proof usesStore-typing weakening · Retyping a well-typed store under an extended store typing
Used byPreservation for the lambda calculus with references

TheoremAssignment preserves store typing#✓fully proved

Let the store \(\mu\) be well typed under the variable context \(\Gamma\) and the store typing \(S\), and let \(l\) be a location to which \(S\) assigns the type \(T\). If \(v\) is a value of type \(T\) under \(\Gamma\) and \(S\), then the store obtained from \(\mu\) by overwriting the entry at \(l\) with \(v\) is well typed under \(\Gamma\) and \(S\).

This is TAPL Lemma 13.5.5.

theorem set {l : Nat} {v : Term Base} {T : Ty Base} (h : StoreTyped Γ S μ)
    (hl : S[l]? = some T) (hval : v.Value) (hv : HasType Γ S v T) :
    StoreTyped Γ S (μ.set l v)
Uses 6 · Used by 1
Statement usesTyping judgment for the lambda calculus with references · Store · Well-typed stores · Terms of the simply typed lambda calculus with references · Values of the simply typed lambda calculus with references · Types of the simply typed lambda calculus with references
Used byPreservation for the lambda calculus with references

TheoremPreservation for the lambda calculus with references#✓fully proved

Let \(\Gamma\) be a variable context and \(S\) a store typing. If a term \(t\) has type \(T\) under \(\Gamma\) and \(S\), the store \(\mu\) is well typed under \(\Gamma\) and \(S\), and \(t\) with store \(\mu\) takes one evaluation step to \(t'\) with store \(\mu'\), then there is a store typing \(S'\) having \(S\) as a prefix such that \(t'\) has type \(T\) under \(\Gamma\) and \(S'\) and \(\mu'\) is well typed under \(\Gamma\) and \(S'\).

This is TAPL Theorem 13.5.3, with the extension of store typings taken as the prefix order on lists.

theorem preservation {Γ S : List (Ty Base)} {t t' : Term Base} {μ μ' : Store Base}
    {T : Ty Base} (ht : HasType Γ S t T) (hμ : StoreTyped Γ S μ) (hstep : Step t μ t' μ') :
    ∃ S', S <+: S' ∧ HasType Γ S' t' T ∧ StoreTyped Γ S' μ'
Uses 13 · Used by 1
Statement usesTyping judgment for the lambda calculus with references · One-step evaluation with references · Store · Well-typed stores · Terms of the simply typed lambda calculus with references · Types of the simply typed lambda calculus with references
Proof usesStore-typing weakening · Substitution lemma for the lambda calculus with references · Allocation preserves store typing · Well-typed stores hold a typed value at every location · Assignment preserves store typing · Values of the simply typed lambda calculus with references · Substitution of a term for variable zero
Used byPreservation for multi-step evaluation

TheoremPreservation for multi-step evaluation#✓fully proved

Let \(\Gamma\) be a variable context and \(S\) a store typing. If a term \(t\) has type \(T\) under \(\Gamma\) and \(S\), the store \(\mu\) is well typed under \(\Gamma\) and \(S\), and \(t\) with store \(\mu\) evaluates in zero or more steps to \(t'\) with store \(\mu'\), then there is a store typing \(S'\) having \(S\) as a prefix such that \(t'\) has type \(T\) under \(\Gamma\) and \(S'\) and \(\mu'\) is well typed under \(\Gamma\) and \(S'\).

theorem Steps.preservation {Γ S : List (Ty Base)} {t t' : Term Base}
    {μ μ' : Store Base} {T : Ty Base} (h : Steps t μ t' μ')
    (ht : HasType Γ S t T) (hμ : StoreTyped Γ S μ) :
    ∃ S', S <+: S' ∧ HasType Γ S' t' T ∧ StoreTyped Γ S' μ'
Uses 8 · Used by 1
Statement usesTyping judgment for the lambda calculus with references · Multi-step evaluation with references · Store · Well-typed stores · Terms of the simply typed lambda calculus with references · Types of the simply typed lambda calculus with references
Proof usesOne-step evaluation with references · Preservation for the lambda calculus with references
Used byType safety

TheoremType safety#✓fully proved

Let \(S\) be a store typing, \(T\) a type, \(t\) a term of type \(T\) in the empty variable context under \(S\), and \(\mu\) a store that is well typed under \(S\) in the empty context. If the configuration \((t, \mu)\) evaluates in zero or more steps to \((t', \mu')\), then \(t'\) is a value or \((t', \mu')\) takes a step to some configuration \((t'', \mu'')\). So a closed term that is well typed in a well-typed store never reaches a stuck configuration.

theorem typeSafety {S : List (Ty Base)} {t t' : Term Base} {μ μ' : Store Base}
    {T : Ty Base} (ht : HasType [] S t T) (hμ : StoreTyped [] S μ)
    (h : Steps t μ t' μ') : t'.Value ∨ ∃ t'' μ'', Step t' μ' t'' μ''
Uses 10 · Used by 1
Statement usesTyping judgment for the lambda calculus with references · One-step evaluation with references · Multi-step evaluation with references · Store · Well-typed stores · Terms of the simply typed lambda calculus with references · Values of the simply typed lambda calculus with references · Types of the simply typed lambda calculus with references
Proof usesPreservation for multi-step evaluation · Progress
Used byType safety from the empty store

TheoremType safety from the empty store#✓fully proved

A closed term typed under the empty store typing, run from the empty store, never gets stuck: every term it reaches in zero or more steps, together with the store reached alongside it, is a value or can take a further step.

theorem typeSafety_empty {t t' : Term Base} {μ' : Store Base} {T : Ty Base}
    (ht : HasType [] [] t T) (h : Steps t [] t' μ') :
    t'.Value ∨ ∃ t'' μ'', Step t' μ' t'' μ''
Uses 8
Statement usesTyping judgment for the lambda calculus with references · One-step evaluation with references · Multi-step evaluation with references · Store · Terms of the simply typed lambda calculus with references · Values of the simply typed lambda calculus with references · Types of the simply typed lambda calculus with references
Proof usesType safety
59 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.