PCF and computational adequacy

AbbreviationPCF types#✓fully proved

PCF types are the simple types over a single ground type, the type of natural numbers.

abbrev Ty := Stlc.Ty Unit

Uses 1 · Used by 71

Statement usesSimple types

Used byComputational adequacy for PCF · Formal approximation relation · The least element approximates every term · Fundamental lemma of formal approximation · Formal approximation is closed under head expansion · Formal approximation is closed under suprema of chains · Composition of PCF contexts · Associativity of PCF context composition · Contextual equivalence in PCF is a congruence · Extending a PCF substitution by a term · One-hole contexts of PCF · Contextual approximation in PCF · Denotational approximation implies contextual approximation in PCF · Contextual equivalence in PCF · Contextual equivalence is mutual contextual approximation in PCF · Equal denotations imply contextual equivalence in PCF · Denotation of PCF terms · Soundness of the PCF denotational semantics · Fixed-point equation for the PCF denotation of fix · PCF denotation of instantiation · Closed PCF terms that evaluate to a numeral denote its value · Equal denotations are preserved by plugging into PCF contexts · Plugging into a PCF context is monotone in the denotation · PCF denotation of a renamed term · PCF denotation of a substituted term · Weakening preserves the PCF denotation · Determinism of PCF big-step evaluation · Determinism of PCF call-by-name reduction · Domain of a PCF type · Semantic environments for PCF · Closed values of ground type are numerals · Big-step call-by-name evaluation of PCF · Backward reduction preserves evaluation in PCF · Reduction to a value implies big-step evaluation in PCF · Big-step evaluation agrees with small-step reduction in PCF · Evaluation to a numeral agrees with the denotation · Identity PCF substitution · Instantiating the newest variable of a PCF term · Instantiation after substitution under a binder · Lifting a PCF substitution under a binder · Variable lookup in a PCF environment · Natural number type of PCF · PCF values are normal forms · Numerals evaluate to themselves · PCF numerals · Injectivity of PCF numerals · PCF numerals are normal forms · Environment from a family of values · PCF values evaluate to themselves · Least elements of PCF domains · Plugging a term into a PCF context · Plugging into a composite PCF context · Contextual equivalence in PCF is reflexive · Contextual approximation in PCF is reflexive · PCF renamings · Renaming of PCF terms · Renaming a PCF term by the identity · Renaming after substitution in PCF · Single-variable substitution in PCF · Call-by-name reduction step of PCF · Multi-step call-by-name reduction of PCF · Big-step evaluation implies reduction in PCF · Parallel substitutions for PCF · Substitution in PCF terms · Substitution after renaming in PCF · Composition of PCF substitutions · Termination agrees with definedness of the denotation · PCF terms · Values of PCF · PCF evaluation results are values · Weakening of PCF terms

AbbreviationNatural number type of PCF#✓fully proved

The ground type \(\mathsf{nat}\) of natural numbers is the unique base type of PCF, whose types are the simple types over a single base type.

abbrev Ty.nat : Ty := .base ()

Uses 2 · Used by 48

Statement usesPCF types · Simple types

Used byComputational adequacy for PCF · Fundamental lemma of formal approximation · Formal approximation is closed under head expansion · Composition of PCF contexts · Associativity of PCF context composition · Contextual equivalence in PCF is a congruence · One-hole contexts of PCF · Contextual approximation in PCF · Denotational approximation implies contextual approximation in PCF · Contextual equivalence in PCF · Contextual equivalence is mutual contextual approximation in PCF · Equal denotations imply contextual equivalence in PCF · Denotation of PCF terms · Soundness of the PCF denotational semantics · Closed PCF terms that evaluate to a numeral denote its value · Equal denotations are preserved by plugging into PCF contexts · Plugging into a PCF context is monotone in the denotation · PCF denotation of a renamed term · PCF denotation of a substituted term · Determinism of PCF big-step evaluation · Determinism of PCF call-by-name reduction · Closed values of ground type are numerals · Big-step call-by-name evaluation of PCF · Backward reduction preserves evaluation in PCF · Evaluation to a numeral agrees with the denotation · Instantiation after substitution under a binder · PCF values are normal forms · Numerals evaluate to themselves · PCF numerals · Injectivity of PCF numerals · PCF numerals are normal forms · PCF values evaluate to themselves · Plugging a term into a PCF context · Plugging into a composite PCF context · Contextual equivalence in PCF is reflexive · Contextual approximation in PCF is reflexive · Renaming of PCF terms · Renaming a PCF term by the identity · Renaming after substitution in PCF · Call-by-name reduction step of PCF · Big-step evaluation implies reduction in PCF · Substitution in PCF terms · Substitution after renaming in PCF · Composition of PCF substitutions · Termination agrees with definedness of the denotation · PCF terms · Values of PCF · PCF evaluation results are values

AbbreviationPCF variables#✓fully proved

PCF uses the typed de Bruijn variables of the simply typed \(\lambda\)-calculus over a single base type: a variable of type \(A\) in a context \(\Gamma\) is a position in the list \(\Gamma\) at which \(A\) occurs.

abbrev Var := @Stlc.Var Unit

Uses 2 · Used by 31

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

Used byComputational adequacy for PCF · Fundamental lemma of formal approximation · Formal approximation is closed under head expansion · Extending a PCF substitution by a term · Denotation of PCF terms · PCF denotation of instantiation · Equal denotations are preserved by plugging into PCF contexts · Plugging into a PCF context is monotone in the denotation · PCF denotation of a renamed term · PCF denotation of a substituted term · Weakening preserves the PCF denotation · Determinism of PCF big-step evaluation · Determinism of PCF call-by-name reduction · Backward reduction preserves evaluation in PCF · Identity PCF substitution · Instantiation after substitution under a binder · Lifting a PCF substitution under a binder · Variable lookup in a PCF environment · PCF values are normal forms · Injectivity of PCF numerals · PCF numerals are normal forms · Environment from a family of values · Renaming of PCF terms · Renaming a PCF term by the identity · Renaming after substitution in PCF · Single-variable substitution in PCF · Parallel substitutions for PCF · Substitution in PCF terms · Substitution after renaming in PCF · Composition of PCF substitutions · PCF terms

InductivePCF terms#✓fully proved

Write \(\mathsf{nat}\) for the ground type of natural numbers and \(A \Rightarrow B\) for the type of functions from \(A\) to \(B\). The intrinsically typed PCF terms of type \(A\) in a context \(\Gamma\) (a list of PCF types) are generated by the following rules: every variable of type \(A\) in \(\Gamma\) is a term of type \(A\); if \(t\) has type \(B\) in the context \(\Gamma\) extended by a newest variable of type \(A\), then \(\lambda t\) has type \(A \Rightarrow B\); if \(f\) has type \(A \Rightarrow B\) and \(a\) has type \(A\), then \(f\,a\) has type \(B\); \(\mathsf{zero}\) has type \(\mathsf{nat}\); if \(t\) has type \(\mathsf{nat}\), so do \(\mathsf{succ}\,t\) and \(\mathsf{pred}\,t\); if \(t\), \(s_1\) and \(s_2\) have type \(\mathsf{nat}\), so does the zero test \(\mathsf{ifz}\,t\,s_1\,s_2\); and if \(t\) has type \(A \Rightarrow A\), then the fixed point \(\mathsf{fix}\,t\) has type \(A\).

inductive Tm : List Ty → Ty → Type where
  | var {Γ : List Ty} {A : Ty} : Var Γ A → Tm Γ A
  | lam {Γ : List Ty} {A B : Ty} : Tm (A :: Γ) B → Tm Γ (A ⇒ B)
  | app {Γ : List Ty} {A B : Ty} : Tm Γ (A ⇒ B) → Tm Γ A → Tm Γ B
  | zero {Γ : List Ty} : Tm Γ .nat
  | succ {Γ : List Ty} : Tm Γ .nat → Tm Γ .nat
  | pred {Γ : List Ty} : Tm Γ .nat → Tm Γ .nat
  /-- `ifz t s₁ s₂` is `s₁` when `t` is zero and `s₂` when `t` is a successor. -/
  | ifz {Γ : List Ty} : Tm Γ .nat → Tm Γ .nat → Tm Γ .nat → Tm Γ .nat
  /-- The fixed-point combinator: `fix t` unfolds to `t (fix t)`. -/
  | fix {Γ : List Ty} {A : Ty} : Tm Γ (A ⇒ A) → Tm Γ A

Uses 4 · Used by 63

Statement usesPCF types · Natural number type of PCF · PCF variables · Simple types

Used byComputational adequacy for PCF · Formal approximation relation · The least element approximates every term · Fundamental lemma of formal approximation · Formal approximation is closed under head expansion · Formal approximation is closed under suprema of chains · Composition of PCF contexts · Associativity of PCF context composition · Contextual equivalence in PCF is a congruence · Extending a PCF substitution by a term · One-hole contexts of PCF · Contextual approximation in PCF · Denotational approximation implies contextual approximation in PCF · Contextual equivalence in PCF · Contextual equivalence is mutual contextual approximation in PCF · Equal denotations imply contextual equivalence in PCF · Denotation of PCF terms · Soundness of the PCF denotational semantics · Fixed-point equation for the PCF denotation of fix · PCF denotation of instantiation · Closed PCF terms that evaluate to a numeral denote its value · Equal denotations are preserved by plugging into PCF contexts · Plugging into a PCF context is monotone in the denotation · PCF denotation of a renamed term · PCF denotation of a substituted term · Weakening preserves the PCF denotation · Determinism of PCF big-step evaluation · Determinism of PCF call-by-name reduction · Closed values of ground type are numerals · Big-step call-by-name evaluation of PCF · Backward reduction preserves evaluation in PCF · Reduction to a value implies big-step evaluation in PCF · Big-step evaluation agrees with small-step reduction in PCF · Evaluation to a numeral agrees with the denotation · Identity PCF substitution · Instantiating the newest variable of a PCF term · Instantiation after substitution under a binder · Lifting a PCF substitution under a binder · PCF values are normal forms · Numerals evaluate to themselves · PCF numerals · Injectivity of PCF numerals · PCF numerals are normal forms · PCF values evaluate to themselves · Plugging a term into a PCF context · Plugging into a composite PCF context · Contextual equivalence in PCF is reflexive · Contextual approximation in PCF is reflexive · Renaming of PCF terms · Renaming a PCF term by the identity · Renaming after substitution in PCF · Single-variable substitution in PCF · Call-by-name reduction step of PCF · Multi-step call-by-name reduction of PCF · Big-step evaluation implies reduction in PCF · Parallel substitutions for PCF · Substitution in PCF terms · Substitution after renaming in PCF · Composition of PCF substitutions · Termination agrees with definedness of the denotation · Values of PCF · PCF evaluation results are values · Weakening of PCF terms

AbbreviationPCF renamings#✓fully proved

For contexts \(\Gamma\) and \(\Delta\) (lists of PCF types), a renaming from \(\Gamma\) to \(\Delta\) is a map sending each variable of \(\Gamma\) of type \(A\), for every type \(A\), to a variable of \(\Delta\) of the same type \(A\); it is the STLC notion of renaming at PCF types.

abbrev Ren (Γ Δ : List Ty) := Stlc.Ren Γ Δ

Uses 2 · Used by 12

Statement usesPCF types · Renamings of simply typed contexts

Used byComposition of PCF contexts · Associativity of PCF context composition · One-hole contexts of PCF · Equal denotations are preserved by plugging into PCF contexts · Plugging into a PCF context is monotone in the denotation · PCF denotation of a renamed term · Plugging a term into a PCF context · Plugging into a composite PCF context · Renaming of PCF terms · Renaming a PCF term by the identity · Renaming after substitution in PCF · Substitution after renaming in PCF

AbbreviationParallel substitutions for PCF#✓fully proved

A substitution from a context \(\Gamma\) to a context \(\Delta\) (lists of PCF types) assigns to every variable of \(\Gamma\), of any type \(A\), a PCF term of type \(A\) in context \(\Delta\).

abbrev Sub (Γ Δ : List Ty) := ∀ {A}, Var Γ A → Tm Δ A

Uses 4 · Used by 12

Statement usesPCF terms · PCF types · PCF variables · Simple types

Used byComputational adequacy for PCF · Fundamental lemma of formal approximation · Extending a PCF substitution by a term · PCF denotation of a substituted term · Identity PCF substitution · Instantiation after substitution under a binder · Lifting a PCF substitution under a binder · Renaming after substitution in PCF · Single-variable substitution in PCF · Substitution in PCF terms · Substitution after renaming in PCF · Composition of PCF substitutions

DefinitionPCF numerals#✓fully proved

For every context \(\Gamma\) and natural number \(n\), the numeral of \(n\) is the term \(\mathsf{succ}^n(\mathsf{zero})\) of type \(\mathsf{nat}\) in \(\Gamma\): the numeral of \(0\) is \(\mathsf{zero}\), and the numeral of \(n + 1\) is \(\mathsf{succ}\) applied to the numeral of \(n\).

def numeral {Γ : List Ty} : Nat → Tm Γ .nat
  | 0 => .zero
  | n + 1 => .succ (numeral n)

Uses 3 · Used by 32

Statement usesPCF terms · PCF types · Natural number type of PCF

Used byComputational adequacy for PCF · Formal approximation relation · The least element approximates every term · Fundamental lemma of formal approximation · Formal approximation is closed under head expansion · Formal approximation is closed under suprema of chains · Contextual equivalence in PCF is a congruence · Contextual approximation in PCF · Denotational approximation implies contextual approximation in PCF · Contextual equivalence in PCF · Contextual equivalence is mutual contextual approximation in PCF · Equal denotations imply contextual equivalence in PCF · Soundness of the PCF denotational semantics · Closed PCF terms that evaluate to a numeral denote its value · Determinism of PCF big-step evaluation · Determinism of PCF call-by-name reduction · Closed values of ground type are numerals · Big-step call-by-name evaluation of PCF · Backward reduction preserves evaluation in PCF · Evaluation to a numeral agrees with the denotation · PCF values are normal forms · Numerals evaluate to themselves · Injectivity of PCF numerals · PCF numerals are normal forms · PCF values evaluate to themselves · Contextual equivalence in PCF is reflexive · Contextual approximation in PCF is reflexive · Call-by-name reduction step of PCF · Big-step evaluation implies reduction in PCF · Termination agrees with definedness of the denotation · Values of PCF · PCF evaluation results are values

TheoremInjectivity of PCF numerals#✓fully proved

In every context, the map sending a natural number \(n\) to the numeral \(\mathsf{succ}^n(\mathsf{zero})\) of type \(\mathsf{nat}\) is injective: distinct natural numbers give distinct numerals.

theorem numeral_injective : Function.Injective (numeral : Nat → Tm Γ .nat)

Uses 6 · Used by 2

Statement usesPCF terms · PCF numerals · PCF types · Natural number type of PCF

Proof usesPCF variables · Simple types

Used byDeterminism of PCF big-step evaluation · Determinism of PCF call-by-name reduction

DefinitionRenaming of PCF terms#✓fully proved

Given a renaming \(\rho\) from a context \(\Gamma\) to a context \(\Delta\), the renaming along \(\rho\) of a PCF term of type \(A\) in context \(\Gamma\) is the term of type \(A\) in context \(\Delta\) obtained by replacing each variable \(x\) by \(\rho(x)\). Under a \(\lambda\)-binder, \(\rho\) is replaced by its lift, which sends the bound variable to itself and the successor of each variable \(x\) of \(\Gamma\) to the successor of \(\rho(x)\). Renaming leaves zero unchanged and commutes with application, successor, predecessor, the zero test and the fixed-point combinator.

def rename : {Γ Δ : List Ty} → Ren Γ Δ → {A : Ty} → Tm Γ A → Tm Δ A
  | _, _, ρ, _, .var x => .var (ρ x)
  | _, _, ρ, _, .lam body => .lam (rename (Stlc.Var.lift ρ) body)
  | _, _, ρ, _, .app f a => .app (rename ρ f) (rename ρ a)
  | _, _, _, _, .zero => .zero
  | _, _, ρ, _, .succ t => .succ (rename ρ t)
  | _, _, ρ, _, .pred t => .pred (rename ρ t)
  | _, _, ρ, _, .ifz t s₁ s₂ => .ifz (rename ρ t) (rename ρ s₁) (rename ρ s₂)
  | _, _, ρ, _, .fix t => .fix (rename ρ t)

Uses 7 · Used by 11

Statement usesPCF renamings · PCF terms · PCF types · Natural number type of PCF · PCF variables · Simple types · Lifting a renaming under a binder

Used byEqual denotations are preserved by plugging into PCF contexts · Plugging into a PCF context is monotone in the denotation · PCF denotation of a renamed term · Weakening preserves the PCF denotation · Plugging a term into a PCF context · Plugging into a composite PCF context · Renaming a PCF term by the identity · Renaming after substitution in PCF · Substitution after renaming in PCF · Composition of PCF substitutions · Weakening of PCF terms

DefinitionWeakening of PCF terms#✓fully proved

Let \(\Gamma\) be a context and \(A\), \(B\) types. Weakening sends a PCF term \(t\) of type \(A\) in context \(\Gamma\) to the term of type \(A\) in the context obtained by prepending a new variable of type \(B\) to \(\Gamma\), by renaming every free variable of \(t\) to its successor, that is, by shifting each de Bruijn index up by one.

def weaken (t : Tm Γ A) : Tm (B :: Γ) A := rename .succ t

Uses 5 · Used by 7

Statement usesPCF terms · Renaming of PCF terms · PCF types · Simple types · Typed de Bruijn variables of the simply typed lambda calculus

Used byComputational adequacy for PCF · Weakening preserves the PCF denotation · Instantiation after substitution under a binder · Lifting a PCF substitution under a binder · Renaming after substitution in PCF · Substitution after renaming in PCF · Composition of PCF substitutions

TheoremRenaming a PCF term by the identity#✓fully proved

For every context \(\Gamma\), type \(A\) and term \(t\) of type \(A\) in \(\Gamma\), renaming \(t\) along the identity renaming of \(\Gamma\) gives \(t\).

@[simp] theorem rename_id (t : Tm Γ A) : rename (Stlc.Var.id : Ren Γ Γ) t = t

Uses 10

Statement usesPCF terms · Renaming of PCF terms · PCF types · Simple types · Identity renaming of a simply typed context

Proof usesPCF renamings · Natural number type of PCF · PCF variables · Typed de Bruijn variables of the simply typed lambda calculus · Lifting a renaming under a binder

DefinitionIdentity PCF substitution#✓fully proved

For every context \(\Gamma\), the identity substitution from \(\Gamma\) to \(\Gamma\) sends each variable \(x\) of \(\Gamma\) to the term consisting of \(x\) alone.

def id : Sub Γ Γ := fun x => .var x

Uses 5 · Used by 2

Statement usesParallel substitutions for PCF · PCF terms · PCF types · PCF variables · Simple types

Used byComputational adequacy for PCF · Instantiation after substitution under a binder

DefinitionLifting a PCF substitution under a binder#✓fully proved

Given a substitution \(\sigma\) from a context \(\Gamma\) to a context \(\Delta\) and a type \(A\), the lift of \(\sigma\) is the substitution from \(\Gamma\) extended by a newest variable of type \(A\) to \(\Delta\) extended by a newest variable of type \(A\) that sends the newest variable to the newest variable and every older variable \(x\) to the weakening of \(\sigma(x)\) by one variable.

def lift (σ : Sub Γ Δ) : Sub (A :: Γ) (A :: Δ)
  | _, .zero => .var .zero
  | _, .succ x => Tm.weaken (σ x)

Uses 7 · Used by 8

Statement usesParallel substitutions for PCF · PCF terms · Weakening of PCF terms · PCF types · PCF variables · Simple types · Typed de Bruijn variables of the simply typed lambda calculus

Used byComputational adequacy for PCF · Fundamental lemma of formal approximation · PCF denotation of a substituted term · Instantiation after substitution under a binder · Renaming after substitution in PCF · Substitution in PCF terms · Substitution after renaming in PCF · Composition of PCF substitutions

DefinitionSingle-variable substitution in PCF#✓fully proved

For a PCF term \(a\) of type \(A\) in a context \(\Gamma\), this is the substitution from the context \(\Gamma\) extended by a newest variable of type \(A\) to \(\Gamma\) that sends the newest variable to \(a\) and each older variable \(x\) to the variable \(x\) of \(\Gamma\).

def single (a : Tm Γ A) : Sub (A :: Γ) Γ
  | _, .zero => a
  | _, .succ x => .var x

Uses 6 · Used by 3

Statement usesParallel substitutions for PCF · PCF terms · PCF types · PCF variables · Simple types · Typed de Bruijn variables of the simply typed lambda calculus

Used byPCF denotation of instantiation · Instantiating the newest variable of a PCF term · Instantiation after substitution under a binder

DefinitionExtending a PCF substitution by a term#✓fully proved

Given a substitution \(\sigma\) from a context \(\Gamma\) to a context \(\Delta\) and a term \(a\) of type \(A\) in \(\Delta\), the extended substitution goes from \(\Gamma\) extended by a newest variable of type \(A\) to \(\Delta\): it sends the newest variable to \(a\) and every older variable \(x\) of \(\Gamma\) to \(\sigma(x)\).

def cons (a : Tm Δ A) (σ : Sub Γ Δ) : Sub (A :: Γ) Δ
  | _, .zero => a
  | _, .succ x => σ x

Uses 6 · Used by 2

Statement usesParallel substitutions for PCF · PCF terms · PCF types · PCF variables · Simple types · Typed de Bruijn variables of the simply typed lambda calculus

Used byFundamental lemma of formal approximation · Instantiation after substitution under a binder

DefinitionSubstitution in PCF terms#✓fully proved

Given a substitution \(\sigma\) from a context \(\Gamma\) to a context \(\Delta\), applying \(\sigma\) to a PCF term of type \(A\) in context \(\Gamma\) gives the term of type \(A\) in context \(\Delta\) obtained by replacing each variable \(x\) by \(\sigma(x)\). Under a \(\lambda\)-binder, \(\sigma\) is replaced by its lift, which sends the bound variable to itself and the successor of each variable \(x\) of \(\Gamma\) to the weakening of \(\sigma(x)\). Substitution leaves zero unchanged and commutes with application, successor, predecessor, the zero test and the fixed-point combinator.

All variables are replaced simultaneously, and since variables are de Bruijn indices the substitution is capture-avoiding.

def subst : {Γ Δ : List Ty} → Sub Γ Δ → {A : Ty} → Tm Γ A → Tm Δ A
  | _, _, σ, _, .var x => σ x
  | _, _, σ, _, .lam body => .lam (subst (Sub.lift σ) body)
  | _, _, σ, _, .app f a => .app (subst σ f) (subst σ a)
  | _, _, _, _, .zero => .zero
  | _, _, σ, _, .succ t => .succ (subst σ t)
  | _, _, σ, _, .pred t => .pred (subst σ t)
  | _, _, σ, _, .ifz t s₁ s₂ => .ifz (subst σ t) (subst σ s₁) (subst σ s₂)
  | _, _, σ, _, .fix t => .fix (subst σ t)

Uses 7 · Used by 9

Statement usesParallel substitutions for PCF · Lifting a PCF substitution under a binder · PCF terms · PCF types · Natural number type of PCF · PCF variables · Simple types

Used byComputational adequacy for PCF · Fundamental lemma of formal approximation · PCF denotation of instantiation · PCF denotation of a substituted term · Instantiating the newest variable of a PCF term · Instantiation after substitution under a binder · Renaming after substitution in PCF · Substitution after renaming in PCF · Composition of PCF substitutions

DefinitionInstantiating the newest variable of a PCF term#✓fully proved

Given a term \(b\) of type \(B\) in a context \(\Gamma\) extended by a newest variable of type \(A\), and a term \(a\) of type \(A\) in \(\Gamma\), the instantiation of \(b\) with \(a\) is the term of type \(B\) in \(\Gamma\) obtained by applying to \(b\) the substitution that sends the newest variable to \(a\) and every older variable to itself.

def instantiate (body : Tm (A :: Γ) B) (a : Tm Γ A) : Tm Γ B :=
  subst (Sub.single a) body

Uses 5 · Used by 14

Statement usesSingle-variable substitution in PCF · PCF terms · Substitution in PCF terms · PCF types · Simple types

Used byFundamental lemma of formal approximation · Formal approximation is closed under head expansion · Soundness of the PCF denotational semantics · PCF denotation of instantiation · Determinism of PCF big-step evaluation · Determinism of PCF call-by-name reduction · Big-step call-by-name evaluation of PCF · Backward reduction preserves evaluation in PCF · Instantiation after substitution under a binder · PCF values are normal forms · PCF numerals are normal forms · Call-by-name reduction step of PCF · Big-step evaluation implies reduction in PCF · PCF evaluation results are values

TheoremSubstitution after renaming in PCF#✓fully proved

Let \(\rho\) be a renaming from a context \(\Gamma\) to a context \(\Delta\) and \(\sigma\) a substitution from \(\Delta\) to a context \(\Xi\). For every PCF term \(t\) of type \(A\) in context \(\Gamma\), applying \(\sigma\) to the renaming of \(t\) along \(\rho\) gives the result of applying to \(t\) the substitution from \(\Gamma\) to \(\Xi\) that sends each variable \(x\) of \(\Gamma\) to \(\sigma(\rho(x))\).

theorem subst_rename (ρ : Ren Γ Δ) (σ : Sub Δ Ξ) (t : Tm Γ A) :
    subst σ (rename ρ t) = subst (fun x => σ (ρ x)) t

Uses 13 · Used by 2

Statement usesPCF renamings · Parallel substitutions for PCF · PCF terms · Renaming of PCF terms · Substitution in PCF terms · PCF types · PCF variables · Simple types

Proof usesLifting a PCF substitution under a binder · Weakening of PCF terms · Natural number type of PCF · Typed de Bruijn variables of the simply typed lambda calculus · Lifting a renaming under a binder

Used byInstantiation after substitution under a binder · Composition of PCF substitutions

TheoremRenaming after substitution in PCF#✓fully proved

Let \(\sigma\) be a substitution from a context \(\Gamma\) to a context \(\Delta\) and \(\rho\) a renaming from \(\Delta\) to a context \(\Xi\). For every PCF term \(t\) of type \(A\) in context \(\Gamma\), renaming along \(\rho\) the result of applying \(\sigma\) to \(t\) gives the result of applying to \(t\) the substitution from \(\Gamma\) to \(\Xi\) that sends each variable \(x\) of \(\Gamma\) to the renaming of \(\sigma(x)\) along \(\rho\).

theorem rename_subst (σ : Sub Γ Δ) (ρ : Ren Δ Ξ) (t : Tm Γ A) :
    rename ρ (subst σ t) = subst (fun x => rename ρ (σ x)) t

Uses 13 · Used by 1

Statement usesPCF renamings · Parallel substitutions for PCF · PCF terms · Renaming of PCF terms · Substitution in PCF terms · PCF types · PCF variables · Simple types

Proof usesLifting a PCF substitution under a binder · Weakening of PCF terms · Natural number type of PCF · Typed de Bruijn variables of the simply typed lambda calculus · Lifting a renaming under a binder

Used byComposition of PCF substitutions

TheoremComposition of PCF substitutions#✓fully proved

Write \(t[\sigma]\) for the result of applying a substitution \(\sigma\) to a PCF term \(t\). Let \(\sigma\) be a substitution from a context \(\Gamma\) to a context \(\Delta\) and \(\tau\) a substitution from \(\Delta\) to a context \(\Xi\). For every PCF term \(t\) of type \(A\) in context \(\Gamma\), \(t[\sigma][\tau] = t[\sigma']\), where \(\sigma'\) is the substitution from \(\Gamma\) to \(\Xi\) that sends each variable \(x\) of \(\Gamma\) to \(\sigma(x)[\tau]\).

theorem subst_subst (σ : Sub Γ Δ) (τ : Sub Δ Ξ) (t : Tm Γ A) :
    subst τ (subst σ t) = subst (fun x => subst τ (σ x)) t

Uses 13 · Used by 1

Statement usesParallel substitutions for PCF · PCF terms · Substitution in PCF terms · PCF types · PCF variables · Simple types

Proof usesLifting a PCF substitution under a binder · Renaming of PCF terms · Renaming after substitution in PCF · Substitution after renaming in PCF · Weakening of PCF terms · Natural number type of PCF · Typed de Bruijn variables of the simply typed lambda calculus

Used byInstantiation after substitution under a binder

TheoremInstantiation after substitution under a binder#✓fully proved

Let \(\sigma\) be a substitution from a context \(\Gamma\) to a context \(\Delta\), let \(b\) be a term of type \(B\) in \(\Gamma\) extended by a newest variable of type \(A\), and let \(a\) be a term of type \(A\) in \(\Delta\). Applying the lift of \(\sigma\) to \(b\) and then instantiating the newest variable with \(a\) gives the same term as applying to \(b\) the extension of \(\sigma\) by \(a\), which sends the newest variable to \(a\) and every older variable \(x\) to \(\sigma(x)\).

theorem instantiate_subst_lift (σ : Sub Γ Δ) (body : Tm (A :: Γ) B) (a : Tm Δ A) :
    (subst (Sub.lift σ) body).instantiate a = subst (Sub.cons a σ) body

Uses 16 · Used by 1

Statement usesParallel substitutions for PCF · Extending a PCF substitution by a term · Lifting a PCF substitution under a binder · PCF terms · Instantiating the newest variable of a PCF term · Substitution in PCF terms · PCF types · Simple types

Proof usesIdentity PCF substitution · Single-variable substitution in PCF · Substitution after renaming in PCF · Composition of PCF substitutions · Weakening of PCF terms · Natural number type of PCF · PCF variables · Typed de Bruijn variables of the simply typed lambda calculus

Used byFundamental lemma of formal approximation

InductiveValues of PCF#✓fully proved

A closed PCF term is a value when it is a \(\lambda\)-abstraction or the numeral \(\mathsf{succ}^n\,\mathsf{zero}\) for some natural number \(n\).

inductive Value : {A : Ty} → Tm [] A → Prop
  | lam {A B : Ty} (body : Tm [A] B) : Value (.lam body)
  | numeral (n : Nat) : Value (numeral n)

Uses 5 · Used by 7

Statement usesPCF terms · PCF numerals · PCF types · Natural number type of PCF · Simple types

Used byDeterminism of PCF call-by-name reduction · Closed values of ground type are numerals · Reduction to a value implies big-step evaluation in PCF · Big-step evaluation agrees with small-step reduction in PCF · PCF values are normal forms · PCF values evaluate to themselves · PCF evaluation results are values

TheoremClosed values of ground type are numerals#✓fully proved

If a closed PCF term \(v\) of the ground type of natural numbers is a value, then \(v\) is the numeral \(\mathsf{succ}^n\,\mathsf{zero}\) for some natural number \(n\).

theorem Value.eq_numeral {v : Tm [] .nat} (hv : v.Value) : ∃ n, v = Tm.numeral n

Uses 6 · Used by 1

Statement usesPCF terms · Values of PCF · PCF numerals · PCF types · Natural number type of PCF

Proof usesSimple types

Used byTermination agrees with definedness of the denotation

InductiveBig-step call-by-name evaluation of PCF#✓fully proved

Write \(\underline{n}\) for the numeral \(\mathsf{succ}^n\,\mathsf{zero}\). For closed PCF terms \(t\) and \(v\) of the same type, \(t \Downarrow v\) (\(t\) evaluates to \(v\)) is the least relation closed under the following rules, where all terms are closed and \(n\) ranges over natural numbers. Every \(\lambda\)-abstraction evaluates to itself, and \(\mathsf{zero} \Downarrow \mathsf{zero}\). If \(t \Downarrow \underline{n}\), then \(\mathsf{succ}\,t \Downarrow \underline{n+1}\). If \(t \Downarrow \mathsf{zero}\), then \(\mathsf{pred}\,t \Downarrow \mathsf{zero}\); if \(t \Downarrow \underline{n+1}\), then \(\mathsf{pred}\,t \Downarrow \underline{n}\). For the zero test, if \(t \Downarrow \mathsf{zero}\) and \(s_1 \Downarrow v\), then \(\mathsf{ifz}\,t\,s_1\,s_2 \Downarrow v\); if \(t \Downarrow \underline{n+1}\) and \(s_2 \Downarrow v\), then \(\mathsf{ifz}\,t\,s_1\,s_2 \Downarrow v\). If \(f \Downarrow \lambda x.\,b\) and \(b[a/x] \Downarrow v\), then \(f\,a \Downarrow v\), where \(b[a/x]\) substitutes the unevaluated argument \(a\) for \(x\) in \(b\). If \(t\,(\mathsf{fix}\,t) \Downarrow v\), then \(\mathsf{fix}\,t \Downarrow v\).

Cslib.Languages.LambdaCalculus.PCF.Tm.Eval · 16 lines

inductive Eval : {A : Ty} → Tm [] A → Tm [] A → Prop
  | lam {A B : Ty} {body : Tm [A] B} : Eval (.lam body) (.lam body)
  | zero : Eval .zero .zero
  | succ {t : Tm [] .nat} {n : Nat} (h : Eval t (numeral n)) :
      Eval (.succ t) (numeral (n + 1))
  | predZero {t : Tm [] .nat} (h : Eval t .zero) : Eval (.pred t) .zero
  | predSucc {t : Tm [] .nat} {n : Nat} (h : Eval t (numeral (n + 1))) :
      Eval (.pred t) (numeral n)
  | ifzZero {t s₁ s₂ v : Tm [] .nat} (ht : Eval t .zero) (hs : Eval s₁ v) :
      Eval (.ifz t s₁ s₂) v
  | ifzSucc {t s₁ s₂ v : Tm [] .nat} {n : Nat} (ht : Eval t (numeral (n + 1)))
      (hs : Eval s₂ v) : Eval (.ifz t s₁ s₂) v
  | app {A B : Ty} {f : Tm [] (A ⇒ B)} {a : Tm [] A} {body : Tm [A] B} {v : Tm [] B}
      (hf : Eval f (.lam body)) (hb : Eval (body.instantiate a) v) : Eval (.app f a) v
  | fix {A : Ty} {t : Tm [] (A ⇒ A)} {v : Tm [] A}
      (h : Eval (.app t (.fix t)) v) : Eval (.fix t) v

Uses 6 · Used by 26

Statement usesPCF terms · Instantiating the newest variable of a PCF term · PCF numerals · PCF types · Natural number type of PCF · Simple types

Used byComputational adequacy for PCF · Formal approximation relation · The least element approximates every term · Fundamental lemma of formal approximation · Formal approximation is closed under head expansion · Formal approximation is closed under suprema of chains · Contextual equivalence in PCF is a congruence · Contextual approximation in PCF · Denotational approximation implies contextual approximation in PCF · Contextual equivalence in PCF · Contextual equivalence is mutual contextual approximation in PCF · Equal denotations imply contextual equivalence in PCF · Soundness of the PCF denotational semantics · Closed PCF terms that evaluate to a numeral denote its value · Determinism of PCF big-step evaluation · Backward reduction preserves evaluation in PCF · Reduction to a value implies big-step evaluation in PCF · Big-step evaluation agrees with small-step reduction in PCF · Evaluation to a numeral agrees with the denotation · Numerals evaluate to themselves · PCF values evaluate to themselves · Contextual equivalence in PCF is reflexive · Contextual approximation in PCF is reflexive · Big-step evaluation implies reduction in PCF · Termination agrees with definedness of the denotation · PCF evaluation results are values

TheoremNumerals evaluate to themselves#✓fully proved

For every natural number \(n\), the closed PCF numeral \(\underline{n} = \mathsf{succ}^n\,\mathsf{zero}\) evaluates to itself under big-step call-by-name evaluation: \(\underline{n} \Downarrow \underline{n}\).

theorem numeral (n : Nat) : Eval (Tm.numeral n) (Tm.numeral n)

Uses 5 · Used by 2

Statement usesBig-step call-by-name evaluation of PCF · PCF numerals · PCF types · Natural number type of PCF

Proof usesPCF terms

Used byBackward reduction preserves evaluation in PCF · PCF values evaluate to themselves

TheoremPCF values evaluate to themselves#✓fully proved

For every type \(A\) and every closed PCF term \(v\) of type \(A\) that is a value, \(v \Downarrow v\) under big-step call-by-name evaluation.

theorem of_value {A : Ty} {v : Tm [] A} (hv : v.Value) : Eval v v

Uses 8 · Used by 1

Statement usesPCF terms · Big-step call-by-name evaluation of PCF · Values of PCF · PCF types

Proof usesNumerals evaluate to themselves · PCF numerals · Natural number type of PCF · Simple types

Used byReduction to a value implies big-step evaluation in PCF

TheoremPCF evaluation results are values#✓fully proved

For closed PCF terms \(t\) and \(v\) of the same type, if \(t \Downarrow v\) under big-step call-by-name evaluation, then \(v\) is a value.

theorem value {A : Ty} {t v : Tm [] A} (h : Eval t v) : v.Value

Uses 8 · Used by 2

Statement usesPCF terms · Big-step call-by-name evaluation of PCF · Values of PCF · PCF types

Proof usesInstantiating the newest variable of a PCF term · PCF numerals · Natural number type of PCF · Simple types

Used byBig-step evaluation agrees with small-step reduction in PCF · Termination agrees with definedness of the denotation

TheoremDeterminism of PCF big-step evaluation#✓fully proved

For closed PCF terms \(t\), \(v\), \(w\) of the same type, if \(t \Downarrow v\) and \(t \Downarrow w\) under big-step call-by-name evaluation, then \(v = w\).

theorem deterministic {A : Ty} {t v w : Tm [] A} (hv : Eval t v) (hw : Eval t w) : v = w

Uses 9 · Used by 1

Statement usesPCF terms · Big-step call-by-name evaluation of PCF · PCF types

Proof usesInstantiating the newest variable of a PCF term · PCF numerals · Injectivity of PCF numerals · Natural number type of PCF · PCF variables · Simple types

Used byBackward reduction preserves evaluation in PCF

DefinitionDomain of a PCF type#✓fully proved

The ω-complete partial order denoted by a PCF type is defined by recursion on the type: the ground type denotes the flat domain of partial natural numbers, and a function type \(A \to B\) denotes the ω-complete partial order of Scott-continuous maps from the domain of \(A\) to the domain of \(B\).

@[reducible] noncomputable def Ty.dom : Ty → ωCPO.{0}
  | .base _ => ωCPO.of (Part ℕ)
  | .arr A B => ωCPO.of (Ty.dom A →𝒄 Ty.dom B)

Uses 2 · Used by 24

Statement usesPCF types · Simple types

Used byComputational adequacy for PCF · Formal approximation relation · The least element approximates every term · Fundamental lemma of formal approximation · Formal approximation is closed under head expansion · Formal approximation is closed under suprema of chains · Denotational approximation implies contextual approximation in PCF · Equal denotations imply contextual equivalence in PCF · Denotation of PCF terms · Soundness of the PCF denotational semantics · Fixed-point equation for the PCF denotation of fix · PCF denotation of instantiation · Closed PCF terms that evaluate to a numeral denote its value · Equal denotations are preserved by plugging into PCF contexts · Plugging into a PCF context is monotone in the denotation · PCF denotation of a renamed term · PCF denotation of a substituted term · Weakening preserves the PCF denotation · Semantic environments for PCF · Evaluation to a numeral agrees with the denotation · Variable lookup in a PCF environment · Environment from a family of values · Least elements of PCF domains · Termination agrees with definedness of the denotation

DefinitionLeast elements of PCF domains#✓fully proved

For every PCF type \(A\), the domain denoted by \(A\) has a least element, defined by recursion on \(A\): at the ground type it is the undefined element of the flat domain of partial natural numbers, and at a function type \(B \to C\) it is the continuous map that sends every argument to the least element of the domain denoted by \(C\).

@[instance_reducible] noncomputable def Ty.orderBot : (A : Ty) → OrderBot (Ty.dom A)
  | .base _ => inferInstanceAs (OrderBot (Part ℕ))
  | .arr A B => @ContinuousHom.instOrderBot (Ty.dom A) (Ty.dom B) _ _ (Ty.orderBot B)

Uses 3 · Used by 8

Statement usesPCF types · Domain of a PCF type · Simple types

Used byThe least element approximates every term · Fundamental lemma of formal approximation · Denotation of PCF terms · Fixed-point equation for the PCF denotation of fix · Equal denotations are preserved by plugging into PCF contexts · Plugging into a PCF context is monotone in the denotation · PCF denotation of a renamed term · PCF denotation of a substituted term

DefinitionSemantic environments for PCF#✓fully proved

The ω-complete partial order of environments for a context \(\Gamma\) (a list of PCF types) is defined by recursion on \(\Gamma\): the empty context has the one-point order, and the environments for \(\Gamma\) extended by a newest variable of type \(A\) are the pairs \((\eta, a)\) of an environment \(\eta\) for \(\Gamma\) and an element \(a\) of the domain of \(A\), ordered componentwise.

@[reducible] noncomputable def Env : List Ty → ωCPO.{0}
  | [] => ωCPO.of PUnit
  | A :: Γ => ωCPO.of (Env Γ × Ty.dom A)

Uses 2 · Used by 18

Statement usesPCF types · Domain of a PCF type

Used byComputational adequacy for PCF · Fundamental lemma of formal approximation · Denotational approximation implies contextual approximation in PCF · Equal denotations imply contextual equivalence in PCF · Denotation of PCF terms · Soundness of the PCF denotational semantics · Fixed-point equation for the PCF denotation of fix · PCF denotation of instantiation · Closed PCF terms that evaluate to a numeral denote its value · Equal denotations are preserved by plugging into PCF contexts · Plugging into a PCF context is monotone in the denotation · PCF denotation of a renamed term · PCF denotation of a substituted term · Weakening preserves the PCF denotation · Evaluation to a numeral agrees with the denotation · Variable lookup in a PCF environment · Environment from a family of values · Termination agrees with definedness of the denotation

DefinitionVariable lookup in a PCF environment#✓fully proved

For a variable \(x\) of type \(A\) in a context \(\Gamma\), the lookup of \(x\) is the Scott-continuous map from environments for \(\Gamma\) to the domain of \(A\) defined by recursion on \(x\): if \(x\) is the newest variable, it sends an environment \((\eta, a)\) to \(a\); if \(x\) is the shift of a variable \(y\) of the older context, it sends \((\eta, a)\) to the lookup of \(y\) at \(\eta\).

noncomputable def Env.lookup : {Γ : List Ty} → {A : Ty} → Var Γ A → (Env Γ →𝒄 Ty.dom A)
  | _ :: _, _, .zero => ContinuousHom.ofFun Prod.snd
  | _ :: _, _, .succ x => (Env.lookup x).comp (ContinuousHom.ofFun Prod.fst)

Uses 6 · Used by 9

Statement usesSemantic environments for PCF · PCF types · Domain of a PCF type · PCF variables · Simple types · Typed de Bruijn variables of the simply typed lambda calculus

Used byComputational adequacy for PCF · Fundamental lemma of formal approximation · Denotation of PCF terms · PCF denotation of instantiation · Equal denotations are preserved by plugging into PCF contexts · Plugging into a PCF context is monotone in the denotation · PCF denotation of a renamed term · PCF denotation of a substituted term · Weakening preserves the PCF denotation

DefinitionEnvironment from a family of values#✓fully proved

Let \(\Gamma\) be a context, that is, a list of PCF types, and suppose that for every type \(A\) and every variable \(x\) of type \(A\) in \(\Gamma\) we are given a value \(f(x)\) in the domain denoted by \(A\). The environment built from \(f\) is the environment for \(\Gamma\) defined by recursion on \(\Gamma\): for the empty context it is the unique element of the one-point domain, and for the context obtained from \(\Gamma'\) by adding a newest variable of type \(B\) it is the pair of the environment built from \(f\) on the older variables of \(\Gamma'\) and the value of \(f\) at the newest variable. So its entry at every variable \(x\) is \(f(x)\).

noncomputable def Env.ofFun : {Γ : List Ty} → (∀ {A}, Var Γ A → Ty.dom A) → Env Γ
  | [], _ => PUnit.unit
  | _ :: _, f => (Env.ofFun fun x => f (.succ x), f .zero)

Uses 6 · Used by 6

Statement usesSemantic environments for PCF · PCF types · Domain of a PCF type · PCF variables · Simple types · Typed de Bruijn variables of the simply typed lambda calculus

Used byPCF denotation of instantiation · Equal denotations are preserved by plugging into PCF contexts · Plugging into a PCF context is monotone in the denotation · PCF denotation of a renamed term · PCF denotation of a substituted term · Weakening preserves the PCF denotation

DefinitionStrict zero test as a continuous map#✓fully proved

Let \(\alpha\) be an ω-complete partial order and let \(t\), \(s_1\), \(s_2\) be Scott-continuous maps from \(\alpha\) to the flat domain of partial natural numbers. Their strict zero test is the Scott-continuous map sending \(x \in \alpha\) to \(s_1(x)\) if \(t(x)\) is defined and equal to \(0\), to \(s_2(x)\) if \(t(x)\) is defined and nonzero, and to the undefined value if \(t(x)\) is undefined.

noncomputable def ifzHom {α : Type*} [OmegaCompletePartialOrder α] (t s₁ s₂ : α →𝒄 Part ℕ) :
    α →𝒄 Part ℕ :=
  ContinuousHom.ofFun (fun x => (t x).bind fun n => if n = 0 then s₁ x else s₂ x)
    (ContinuousHom.ωScottContinuous.bind t.ωScottContinuous (by
      refine ωScottContinuous.of_apply₂ fun n => ?_
      by_cases hn : n = 0
      · simpa [hn] using s₁.ωScottContinuous
      · simpa [hn] using s₂.ωScottContinuous))

Used by 1

Used byDenotation of PCF terms

DefinitionDenotation of PCF terms#✓fully proved

The denotation of a PCF term \(t\) of type \(A\) in a context \(\Gamma\) is the Scott-continuous map \([\![t]\!]\) from environments for \(\Gamma\) to the domain of \(A\), defined by recursion on \(t\): a variable denotes its lookup map; \([\![\lambda t]\!]\) is the currying of \([\![t]\!]\); \([\![f\,a]\!]\eta = [\![f]\!]\eta\,([\![a]\!]\eta)\); \([\![\mathsf{zero}]\!]\) is constantly the defined value \(0\); \([\![\mathsf{succ}\,t]\!]\eta\) and \([\![\mathsf{pred}\,t]\!]\eta\) apply \(n \mapsto n + 1\) and the predecessor map (with \(0 \mapsto 0\)) to the partial natural number \([\![t]\!]\eta\), and are undefined where it is undefined; \([\![\mathsf{ifz}\,t\,s_1\,s_2]\!]\) is the strict zero test of \([\![t]\!]\), \([\![s_1]\!]\), \([\![s_2]\!]\); and \([\![\mathsf{fix}\,t]\!]\eta\) is the least fixed point of the continuous map \([\![t]\!]\eta\).

noncomputable def denote : {Γ : List Ty} → {A : Ty} → Tm Γ A → (Env Γ →𝒄 Ty.dom A)
  | _, _, .var x => Env.lookup x
  | _, _, .lam body => ContinuousHom.curry (denote body)
  | _, _, .app f a => ContinuousHom.ofFun (fun η => denote f η (denote a η))
      (ContinuousHom.ωScottContinuous_apply (denote f).ωScottContinuous
        (denote a).ωScottContinuous)
  | _, _, .zero => ContinuousHom.const (Part.some 0)
  | _, _, .succ t => ContinuousHom.map Nat.succ (denote t)
  | _, _, .pred t => ContinuousHom.map Nat.pred (denote t)
  | _, _, .ifz t s₁ s₂ => ifzHom (denote t) (denote s₁) (denote s₂)
  | _, _, .fix t => ContinuousHom.lfpHom.comp (denote t)

Uses 12 · Used by 15

Statement usesSemantic environments for PCF · Variable lookup in a PCF environment · PCF terms · PCF types · Domain of a PCF type · Natural number type of PCF · Least elements of PCF domains · PCF variables · Strict zero test as a continuous map · Simple types · Currying of Scott-continuous maps · The least-fixed-point operator as a Scott-continuous map

Used byComputational adequacy for PCF · Fundamental lemma of formal approximation · Denotational approximation implies contextual approximation in PCF · Equal denotations imply contextual equivalence in PCF · Soundness of the PCF denotational semantics · Fixed-point equation for the PCF denotation of fix · PCF denotation of instantiation · Closed PCF terms that evaluate to a numeral denote its value · Equal denotations are preserved by plugging into PCF contexts · Plugging into a PCF context is monotone in the denotation · PCF denotation of a renamed term · PCF denotation of a substituted term · Weakening preserves the PCF denotation · Evaluation to a numeral agrees with the denotation · Termination agrees with definedness of the denotation

TheoremFixed-point equation for the PCF denotation of fix#✓fully proved

For every PCF term \(t\) of type \(A \to A\) in a context \(\Gamma\) and every environment \(\eta\) for \(\Gamma\), the denotation of \(\mathsf{fix}\,t\) at \(\eta\) equals the denotation of the application \(t\,(\mathsf{fix}\,t)\) at \(\eta\).

theorem denote_fix_unfold (t : Tm Γ (A ⇒ A)) :
    denote (.fix t) η = denote (.app t (.fix t)) η

Uses 9 · Used by 1

Statement usesSemantic environments for PCF · PCF terms · Denotation of PCF terms · PCF types · Domain of a PCF type · Simple types

Proof usesLeast elements of PCF domains · Least fixed point of a Scott-continuous map · The least fixed point is a fixed point

Used bySoundness of the PCF denotational semantics

TheoremPCF denotation of a renamed term#✓fully proved

Let \(\rho\) be a type-preserving renaming of the variables of a context \(\Gamma\) into a context \(\Delta\), let \(t\) be a PCF term of type \(A\) in context \(\Gamma\), and let \(\eta\) be an environment for \(\Delta\). Then the denotation at \(\eta\) of the renaming of \(t\) along \(\rho\) equals the denotation of \(t\) at the environment for \(\Gamma\) that gives each variable \(x\) of \(\Gamma\) the value of the variable \(\rho(x)\) in \(\eta\).

theorem denote_rename (ρ : Ren Γ Δ) (t : Tm Γ A) (η : Env Δ) :
    denote (rename ρ t) η = denote t (Env.ofFun fun x => Env.lookup (ρ x) η)

Uses 16 · Used by 3

Statement usesSemantic environments for PCF · Variable lookup in a PCF environment · Environment from a family of values · PCF renamings · PCF terms · Denotation of PCF terms · Renaming of PCF terms · PCF types · Domain of a PCF type · PCF variables · Simple types

Proof usesNatural number type of PCF · Least elements of PCF domains · Typed de Bruijn variables of the simply typed lambda calculus · Lifting a renaming under a binder · Least fixed point of a Scott-continuous map

Used byEqual denotations are preserved by plugging into PCF contexts · Plugging into a PCF context is monotone in the denotation · Weakening preserves the PCF denotation

TheoremWeakening preserves the PCF denotation#✓fully proved

Let \(t\) be a PCF term of type \(A\) in a context \(\Gamma\), let \(\eta\) be an environment for \(\Gamma\), and let \(b\) be an element of the domain of a type \(B\). The denotation of the weakening of \(t\) (the same term in the context \(\Gamma\) extended by a newest variable of type \(B\)) at the extended environment \((\eta, b)\) equals the denotation of \(t\) at \(\eta\).

theorem denote_weaken (t : Tm Γ A) (η : Env Γ) (b : Ty.dom B) :
    denote (weaken (B := B) t) ((η, b) : Env (B :: Γ)) = denote t η

Uses 13 · Used by 1

Statement usesSemantic environments for PCF · PCF terms · Denotation of PCF terms · Weakening of PCF terms · PCF types · Domain of a PCF type

Proof usesVariable lookup in a PCF environment · Environment from a family of values · PCF denotation of a renamed term · Renaming of PCF terms · PCF variables · Simple types · Typed de Bruijn variables of the simply typed lambda calculus

Used byPCF denotation of a substituted term

TheoremPCF denotation of a substituted term#✓fully proved

Let \(\sigma\) be a type-preserving substitution assigning to each variable of a context \(\Gamma\) a PCF term in a context \(\Delta\), let \(t\) be a term of type \(A\) in context \(\Gamma\), and let \(\eta\) be an environment for \(\Delta\). Then the denotation at \(\eta\) of the term obtained by applying \(\sigma\) to \(t\) equals the denotation of \(t\) at the environment for \(\Gamma\) that gives each variable \(x\) of \(\Gamma\) the value at \(\eta\) of the denotation of \(\sigma(x)\).

theorem denote_subst (σ : Sub Γ Δ) (t : Tm Γ A) (η : Env Δ) :
    denote (subst σ t) η = denote t (Env.ofFun fun x => denote (σ x) η)

Uses 17 · Used by 1

Statement usesSemantic environments for PCF · Environment from a family of values · Parallel substitutions for PCF · PCF terms · Denotation of PCF terms · Substitution in PCF terms · PCF types · Domain of a PCF type · PCF variables · Simple types

Proof usesVariable lookup in a PCF environment · Lifting a PCF substitution under a binder · Weakening preserves the PCF denotation · Natural number type of PCF · Least elements of PCF domains · Typed de Bruijn variables of the simply typed lambda calculus · Least fixed point of a Scott-continuous map

Used byPCF denotation of instantiation

TheoremPCF denotation of instantiation#✓fully proved

Let \(t\) be a PCF term of type \(B\) in the context \(\Gamma\) extended by a newest variable of type \(A\), let \(a\) be a term of type \(A\) in context \(\Gamma\), and let \(\eta\) be an environment for \(\Gamma\). Writing \([\![s]\!]\eta\) for the denotation of a term \(s\) at \(\eta\), the denotation at \(\eta\) of the term obtained from \(t\) by substituting \(a\) for the newest variable equals \([\![t]\!](\eta, [\![a]\!]\eta)\), the denotation of \(t\) at the extension of \(\eta\) that gives the newest variable the value \([\![a]\!]\eta\).

theorem denote_instantiate (body : Tm (A :: Γ) B) (a : Tm Γ A) (η : Env Γ) :
    denote (body.instantiate a) η = denote body ((η, denote a η) : Env (A :: Γ))

Uses 14 · Used by 1

Statement usesSemantic environments for PCF · PCF terms · Denotation of PCF terms · Instantiating the newest variable of a PCF term · PCF types · Domain of a PCF type

Proof usesVariable lookup in a PCF environment · Environment from a family of values · Single-variable substitution in PCF · PCF denotation of a substituted term · Substitution in PCF terms · PCF variables · Simple types · Typed de Bruijn variables of the simply typed lambda calculus

Used bySoundness of the PCF denotational semantics

InductiveCall-by-name reduction step of PCF#✓fully proved

Write \(\underline{n}\) for the numeral \(\mathrm{succ}^n\,\mathrm{zero}\), and \(b[a]\) for the result of substituting the closed term \(a\) for the bound variable of an abstraction body \(b\). One-step call-by-name reduction \(t \to t'\) between closed PCF terms of the same type is the least relation closed under these rules: \(f\,a \to f'\,a\) whenever \(f \to f'\); \((\lambda b)\,a \to b[a]\), without evaluating \(a\); \(\mathrm{succ}\,t \to \mathrm{succ}\,t'\), \(\mathrm{pred}\,t \to \mathrm{pred}\,t'\) and \(\mathrm{ifz}\,t\,s_1\,s_2 \to \mathrm{ifz}\,t'\,s_1\,s_2\) whenever \(t \to t'\); \(\mathrm{pred}\,\mathrm{zero} \to \mathrm{zero}\) and \(\mathrm{pred}\,\underline{n+1} \to \underline{n}\) for every natural number \(n\); \(\mathrm{ifz}\,\mathrm{zero}\,s_1\,s_2 \to s_1\) and \(\mathrm{ifz}\,\underline{n+1}\,s_1\,s_2 \to s_2\) for every natural number \(n\); and \(\mathrm{fix}\,t \to t\,(\mathrm{fix}\,t)\).

inductive Step : {A : Ty} → Tm [] A → Tm [] A → Prop
  | appLeft {A B : Ty} {f f' : Tm [] (A ⇒ B)} {a : Tm [] A} (h : Step f f') :
      Step (.app f a) (.app f' a)
  | beta {A B : Ty} {body : Tm [A] B} {a : Tm [] A} :
      Step (.app (.lam body) a) (body.instantiate a)
  | succ {t t' : Tm [] .nat} (h : Step t t') : Step (.succ t) (.succ t')
  | pred {t t' : Tm [] .nat} (h : Step t t') : Step (.pred t) (.pred t')
  | predZero : Step (.pred .zero) .zero
  | predSucc (n : Nat) : Step (.pred (numeral (n + 1))) (numeral n)
  | ifz {t t' s₁ s₂ : Tm [] .nat} (h : Step t t') : Step (.ifz t s₁ s₂) (.ifz t' s₁ s₂)
  | ifzZero {s₁ s₂ : Tm [] .nat} : Step (.ifz .zero s₁ s₂) s₁
  | ifzSucc (n : Nat) {s₁ s₂ : Tm [] .nat} : Step (.ifz (numeral (n + 1)) s₁ s₂) s₂
  | fix {A : Ty} {t : Tm [] (A ⇒ A)} : Step (.fix t) (.app t (.fix t))

Uses 6 · Used by 7

Statement usesPCF terms · Instantiating the newest variable of a PCF term · PCF numerals · PCF types · Natural number type of PCF · Simple types

Used byDeterminism of PCF call-by-name reduction · Backward reduction preserves evaluation in PCF · Reduction to a value implies big-step evaluation in PCF · PCF values are normal forms · PCF numerals are normal forms · Multi-step call-by-name reduction of PCF · Big-step evaluation implies reduction in PCF

AbbreviationMulti-step call-by-name reduction of PCF#✓fully proved

For closed PCF terms \(t\) and \(t'\) of the same type, \(t \to^* t'\) holds when \(t\) reduces to \(t'\) in finitely many, possibly zero, one-step call-by-name reductions; that is, \(\to^*\) is the reflexive transitive closure of one-step reduction.

abbrev Steps {A : Ty} : Tm [] A → Tm [] A → Prop := Relation.ReflTransGen Step

Uses 3 · Used by 3

Statement usesPCF terms · Call-by-name reduction step of PCF · PCF types

Used byReduction to a value implies big-step evaluation in PCF · Big-step evaluation agrees with small-step reduction in PCF · Big-step evaluation implies reduction in PCF

TheoremPCF numerals are normal forms#✓fully proved

For every natural number \(n\), the closed numeral \(\mathrm{succ}^n\,\mathrm{zero}\) of type nat does not reduce: there is no closed term \(t'\) such that \(\mathrm{succ}^n\,\mathrm{zero}\) reduces to \(t'\) in one call-by-name step.

theorem numeral_not_step (n : Nat) {t' : Tm [] .nat} : ¬ Step (numeral n) t'

Uses 8 · Used by 2

Statement usesPCF terms · Call-by-name reduction step of PCF · PCF numerals · PCF types · Natural number type of PCF

Proof usesInstantiating the newest variable of a PCF term · PCF variables · Simple types

Used byDeterminism of PCF call-by-name reduction · PCF values are normal forms

TheoremPCF values are normal forms#✓fully proved

If \(v\) is a closed PCF value of type \(A\) (an abstraction or a numeral), then there is no closed term \(t'\) such that \(v\) reduces to \(t'\) in one call-by-name step.

theorem Value.not_step {A : Ty} {v t' : Tm [] A} (hv : v.Value) : ¬ Step v t'

Uses 10 · Used by 1

Statement usesPCF terms · Call-by-name reduction step of PCF · Values of PCF · PCF types

Proof usesInstantiating the newest variable of a PCF term · PCF numerals · PCF numerals are normal forms · Natural number type of PCF · PCF variables · Simple types

Used byDeterminism of PCF call-by-name reduction

TheoremDeterminism of PCF call-by-name reduction#✓fully proved

One-step call-by-name reduction of closed PCF terms is deterministic: if a closed term \(t\) of type \(A\) reduces in one step to \(t_1\) and also reduces in one step to \(t_2\), then \(t_1 = t_2\).

theorem Step.deterministic {A : Ty} {t t₁ t₂ : Tm [] A} (h₁ : Step t t₁) (h₂ : Step t t₂) :
    t₁ = t₂

Uses 12

Statement usesPCF terms · Call-by-name reduction step of PCF · PCF types

Proof usesValues of PCF · PCF values are normal forms · Instantiating the newest variable of a PCF term · PCF numerals · Injectivity of PCF numerals · PCF numerals are normal forms · Natural number type of PCF · PCF variables · Simple types

TheoremBig-step evaluation implies reduction in PCF#✓fully proved

Let \(t\) and \(v\) be closed PCF terms of type \(A\). If \(t\) evaluates to \(v\) in the big-step call-by-name semantics, then \(t\) reduces to \(v\) in finitely many (possibly zero) call-by-name steps.

theorem Eval.steps {A : Ty} {t v : Tm [] A} (h : Eval t v) : Steps t v

Uses 9 · Used by 1

Statement usesPCF terms · Big-step call-by-name evaluation of PCF · Multi-step call-by-name reduction of PCF · PCF types

Proof usesCall-by-name reduction step of PCF · Instantiating the newest variable of a PCF term · PCF numerals · Natural number type of PCF · Simple types

Used byBig-step evaluation agrees with small-step reduction in PCF

TheoremBackward reduction preserves evaluation in PCF#✓fully proved

Let \(t\), \(t'\) and \(v\) be closed PCF terms of type \(A\). If \(t\) reduces to \(t'\) in one call-by-name step and \(t'\) evaluates to \(v\) in the big-step call-by-name semantics, then \(t\) evaluates to \(v\).

theorem Step.eval {A : Ty} {t t' v : Tm [] A} (hstep : Step t t') (heval : Eval t' v) :
    Eval t v

Uses 11 · Used by 1

Statement usesPCF terms · Big-step call-by-name evaluation of PCF · Call-by-name reduction step of PCF · PCF types

Proof usesDeterminism of PCF big-step evaluation · Numerals evaluate to themselves · Instantiating the newest variable of a PCF term · PCF numerals · Natural number type of PCF · PCF variables · Simple types

Used byReduction to a value implies big-step evaluation in PCF

TheoremReduction to a value implies big-step evaluation in PCF#✓fully proved

Let \(t\) and \(v\) be closed PCF terms of type \(A\). If \(t\) reduces to \(v\) in finitely many (possibly zero) call-by-name steps and \(v\) is a value, then \(t\) evaluates to \(v\) in the big-step call-by-name semantics.

theorem Steps.eval {A : Ty} {t v : Tm [] A} (h : Steps t v) (hv : v.Value) : Eval t v

Uses 8 · Used by 1

Statement usesPCF terms · Big-step call-by-name evaluation of PCF · Multi-step call-by-name reduction of PCF · Values of PCF · PCF types

Proof usesPCF values evaluate to themselves · Call-by-name reduction step of PCF · Backward reduction preserves evaluation in PCF

Used byBig-step evaluation agrees with small-step reduction in PCF

TheoremBig-step evaluation agrees with small-step reduction in PCF#✓fully proved

For closed PCF terms \(t\) and \(v\) of type \(A\), \(t\) evaluates to \(v\) in the big-step call-by-name semantics if and only if \(t\) reduces to \(v\) in finitely many (possibly zero) call-by-name steps and \(v\) is a value.

theorem eval_iff_steps {A : Ty} {t v : Tm [] A} : Eval t v ↔ Steps t v ∧ v.Value

Uses 8

Statement usesPCF terms · Big-step call-by-name evaluation of PCF · Multi-step call-by-name reduction of PCF · Values of PCF · PCF types

Proof usesBig-step evaluation implies reduction in PCF · PCF evaluation results are values · Reduction to a value implies big-step evaluation in PCF

TheoremSoundness of the PCF denotational semantics#✓fully proved

Let \(A\) be a PCF type and let \(t\) and \(v\) be closed terms of type \(A\). If \(t\) evaluates to \(v\) under big-step call-by-name evaluation, then for every environment \(\eta\) of the empty context, the denotations of \(t\) and \(v\) at \(\eta\) are equal.

theorem Eval.denote_eq {A : Ty} {t v : Tm [] A} (h : Eval t v) (η : Env []) :
    denote t η = denote v η

Uses 12 · Used by 1

Statement usesSemantic environments for PCF · PCF terms · Big-step call-by-name evaluation of PCF · Denotation of PCF terms · PCF types · Domain of a PCF type

Proof usesFixed-point equation for the PCF denotation of fix · PCF denotation of instantiation · Instantiating the newest variable of a PCF term · PCF numerals · Natural number type of PCF · Simple types

Used byClosed PCF terms that evaluate to a numeral denote its value

TheoremClosed PCF terms that evaluate to a numeral denote its value#✓fully proved

Let \(t\) be a closed PCF term of the ground type of natural numbers and let \(n\) be a natural number. If \(t\) evaluates to the numeral for \(n\), then for every environment \(\eta\) of the empty context, the denotation of \(t\) at \(\eta\) is the defined element \(n\) of the flat domain of partial natural numbers.

theorem Eval.denote_numeral {t : Tm [] .nat} {n : Nat} (h : Eval t (Tm.numeral n)) (η : Env []) :
    denote t η = Part.some n

Uses 9 · Used by 3

Statement usesSemantic environments for PCF · PCF terms · Big-step call-by-name evaluation of PCF · Denotation of PCF terms · PCF numerals · PCF types · Domain of a PCF type · Natural number type of PCF

Proof usesSoundness of the PCF denotational semantics

Used byDenotational approximation implies contextual approximation in PCF · Evaluation to a numeral agrees with the denotation · Termination agrees with definedness of the denotation

DefinitionFormal approximation relation#✓fully proved

For each PCF type \(A\), the relation "\(d\) formally approximates \(t\)" between an element \(d\) of the domain of \(A\) and a closed term \(t\) of type \(A\) is defined by recursion on \(A\). At the ground type, whose domain is the flat domain of partial natural numbers, \(d\) formally approximates \(t\) when, for every natural number \(n\) such that \(d\) is defined with value \(n\), the term \(t\) evaluates to the numeral \(n\). At a function type \(A \to B\), \(f\) formally approximates \(t\) when, for every element \(d\) of the domain of \(A\) and every closed term \(s\) of type \(A\) such that \(d\) formally approximates \(s\), the element \(f(d)\) formally approximates the application \(t\,s\) at type \(B\).

def Approx : (A : Ty) → Ty.dom A → Tm [] A → Prop
  | .base _, d, t => ∀ n : ℕ, n ∈ (d : Part ℕ) → Eval t (numeral n)
  | .arr A B, f, t => ∀ d s, Approx A d s → Approx B (f d) (.app t s)

Uses 6 · Used by 5

Statement usesPCF terms · Big-step call-by-name evaluation of PCF · PCF numerals · PCF types · Domain of a PCF type · Simple types

Used byComputational adequacy for PCF · The least element approximates every term · Fundamental lemma of formal approximation · Formal approximation is closed under head expansion · Formal approximation is closed under suprema of chains

TheoremThe least element approximates every term#✓fully proved

For every PCF type \(A\) and every closed term \(t\) of type \(A\), the least element \(\bot\) of the domain of \(A\) formally approximates \(t\).

theorem approx_bot : ∀ (A : Ty) (t : Tm [] A), Approx A ⊥ t

Uses 8 · Used by 1

Statement usesPCF terms · Formal approximation relation · PCF types · Domain of a PCF type · Least elements of PCF domains

Proof usesBig-step call-by-name evaluation of PCF · PCF numerals · Simple types

Used byFundamental lemma of formal approximation

TheoremFormal approximation is closed under suprema of chains#✓fully proved

Let \(A\) be a PCF type, \(t\) a closed term of type \(A\) and \((c_i)_{i \in \mathbb{N}}\) a chain in the domain of \(A\). If every \(c_i\) formally approximates \(t\), then the supremum \(\bigsqcup_i c_i\) formally approximates \(t\).

theorem approx_ωSup : ∀ (A : Ty) (t : Tm [] A) (c : Chain (Ty.dom A)),
    (∀ i, Approx A (c i) t) → Approx A (ωSup c) t

Uses 7 · Used by 1

Statement usesPCF terms · Formal approximation relation · PCF types · Domain of a PCF type

Proof usesBig-step call-by-name evaluation of PCF · PCF numerals · Simple types

Used byFundamental lemma of formal approximation

TheoremFormal approximation is closed under head expansion#✓fully proved

Let \(A\) be a PCF type, let \(t\) and \(t'\) be closed terms of type \(A\), and let \(d\) be an element of the domain of \(A\). If \(t\) evaluates to every closed term \(v\) to which \(t'\) evaluates, and \(d\) formally approximates \(t'\), then \(d\) formally approximates \(t\).

theorem approx_expand : ∀ (A : Ty) {t t' : Tm [] A} {d : Ty.dom A},
    (∀ v, Eval t' v → Eval t v) → Approx A d t' → Approx A d t

Uses 10 · Used by 1

Statement usesPCF terms · Formal approximation relation · Big-step call-by-name evaluation of PCF · PCF types · Domain of a PCF type

Proof usesInstantiating the newest variable of a PCF term · PCF numerals · Natural number type of PCF · PCF variables · Simple types

Used byFundamental lemma of formal approximation

TheoremFundamental lemma of formal approximation#✓fully proved

Let \(t\) be a PCF term of type \(A\) in a context \(\Gamma\), let \(\eta\) be a semantic environment for \(\Gamma\), and let \(\sigma\) assign to each variable of \(\Gamma\) a closed term of the same type. Suppose that for every variable \(x\) of \(\Gamma\), of type \(B\) say, the value of \(x\) in \(\eta\) formally approximates the closed term \(\sigma(x)\) at type \(B\). Then the denotation of \(t\) in \(\eta\) formally approximates, at type \(A\), the closed term \(\sigma(t)\) obtained by simultaneously substituting \(\sigma(x)\) for each variable \(x\) in \(t\).

theorem approx_denote {Γ : List Ty} {A : Ty} (t : Tm Γ A) (η : Env Γ) (σ : Sub Γ [])
    (hσ : ∀ {B} (x : Var Γ B), Approx B (Env.lookup x η) (σ x)) :
    Approx A (denote t η) (subst σ t)

Uses 24 · Used by 1

Statement usesSemantic environments for PCF · Variable lookup in a PCF environment · Parallel substitutions for PCF · PCF terms · Formal approximation relation · Denotation of PCF terms · Substitution in PCF terms · PCF types · Domain of a PCF type · PCF variables · Simple types

Proof usesExtending a PCF substitution by a term · Lifting a PCF substitution under a binder · Big-step call-by-name evaluation of PCF · The least element approximates every term · Formal approximation is closed under head expansion · Formal approximation is closed under suprema of chains · Instantiating the newest variable of a PCF term · Instantiation after substitution under a binder · PCF numerals · Natural number type of PCF · Least elements of PCF domains · Typed de Bruijn variables of the simply typed lambda calculus · Least fixed point of a Scott-continuous map

Used byComputational adequacy for PCF

TheoremComputational adequacy for PCF#✓fully proved

Let \(t\) be a closed PCF term of ground type \(\mathsf{nat}\) and let \(n\) be a natural number. If the denotation of \(t\) in the empty environment is defined with value \(n\), then \(t\) evaluates to the numeral \(\mathsf{succ}^n(\mathsf{zero})\).

theorem adequacy {t : Tm [] .nat} {n : ℕ} (h : n ∈ (denote t PUnit.unit : Part ℕ)) :
    Eval t (numeral n)

Uses 19 · Used by 3

Statement usesSemantic environments for PCF · PCF terms · Big-step call-by-name evaluation of PCF · Denotation of PCF terms · PCF numerals · PCF types · Domain of a PCF type · Natural number type of PCF

Proof usesVariable lookup in a PCF environment · Parallel substitutions for PCF · Identity PCF substitution · Lifting a PCF substitution under a binder · Formal approximation relation · Fundamental lemma of formal approximation · Substitution in PCF terms · Weakening of PCF terms · PCF variables · Simple types · Typed de Bruijn variables of the simply typed lambda calculus

Used byDenotational approximation implies contextual approximation in PCF · Evaluation to a numeral agrees with the denotation · Termination agrees with definedness of the denotation

TheoremEvaluation to a numeral agrees with the denotation#✓fully proved

For every natural number \(n\), a closed PCF term \(t\) of ground type evaluates to the numeral \(n\) if and only if the denotation of \(t\) is the defined value \(n\).

theorem eval_numeral_iff {t : Tm [] .nat} {n : ℕ} :
    Eval t (numeral n) ↔ denote t PUnit.unit = Part.some n

Uses 10 · Used by 1

Statement usesSemantic environments for PCF · PCF terms · Big-step call-by-name evaluation of PCF · Denotation of PCF terms · PCF numerals · PCF types · Domain of a PCF type · Natural number type of PCF

Proof usesClosed PCF terms that evaluate to a numeral denote its value · Computational adequacy for PCF

Used byEqual denotations imply contextual equivalence in PCF

TheoremTermination agrees with definedness of the denotation#✓fully proved

A closed PCF term \(t\) of ground type evaluates to some term if and only if its denotation, an element of the flat domain of partial natural numbers, is defined.

theorem terminates_iff_dom {t : Tm [] .nat} :
    (∃ v, Eval t v) ↔ (denote t PUnit.unit : Part ℕ).Dom

Uses 12

Statement usesSemantic environments for PCF · PCF terms · Big-step call-by-name evaluation of PCF · Denotation of PCF terms · PCF types · Domain of a PCF type · Natural number type of PCF

Proof usesClosed PCF terms that evaluate to a numeral denote its value · PCF evaluation results are values · Closed values of ground type are numerals · Computational adequacy for PCF · PCF numerals

InductiveOne-hole contexts of PCF#✓fully proved

Fix a typing context \(\Gamma\) and a type \(A\). A one-hole context to \((\Delta, B)\) has a hole that takes a term of type \(A\) in typing context \(\Gamma\) and turns it into a term of type \(B\) in typing context \(\Delta\). These contexts are generated by the following rules, for typing contexts \(\Delta\), \(\Delta'\) and types \(B\), \(C\), with \(\mathbb{N}\) the ground type of natural numbers. The hole itself is a context to \((\Gamma, A)\). If \(\Delta \cdot B\) extends \(\Delta\) by a new innermost variable of type \(B\), a context to \((\Delta \cdot B, C)\) gives by \(\lambda\)-abstraction a context to \((\Delta, B \to C)\). A context to \((\Delta, B \to C)\) applied to a term of type \(B\) in \(\Delta\), and a term of type \(B \to C\) in \(\Delta\) applied to a context to \((\Delta, B)\), are contexts to \((\Delta, C)\). Successor and predecessor of a context to \((\Delta, \mathbb{N})\) are contexts to \((\Delta, \mathbb{N})\), and so is the zero test with a context to \((\Delta, \mathbb{N})\) in any one of its three argument positions and terms of type \(\mathbb{N}\) in \(\Delta\) in the other two. The fixed-point operator applied to a context to \((\Delta, B \to B)\) is a context to \((\Delta, B)\). Finally, a type-preserving renaming of variables from \(\Delta\) to \(\Delta'\) applied to a context to \((\Delta, B)\) is a context to \((\Delta', B)\), which renames the term the inner context builds.

inductive Ctx (Γ : List Ty) (A : Ty) : List Ty → Ty → Type where
  | hole : Ctx Γ A Γ A
  | lam {Δ : List Ty} {B C : Ty} : Ctx Γ A (B :: Δ) C → Ctx Γ A Δ (B ⇒ C)
  | appL {Δ : List Ty} {B C : Ty} : Ctx Γ A Δ (B ⇒ C) → Tm Δ B → Ctx Γ A Δ C
  | appR {Δ : List Ty} {B C : Ty} : Tm Δ (B ⇒ C) → Ctx Γ A Δ B → Ctx Γ A Δ C
  | succ {Δ : List Ty} : Ctx Γ A Δ .nat → Ctx Γ A Δ .nat
  | pred {Δ : List Ty} : Ctx Γ A Δ .nat → Ctx Γ A Δ .nat
  | ifzTest {Δ : List Ty} : Ctx Γ A Δ .nat → Tm Δ .nat → Tm Δ .nat → Ctx Γ A Δ .nat
  | ifzThen {Δ : List Ty} : Tm Δ .nat → Ctx Γ A Δ .nat → Tm Δ .nat → Ctx Γ A Δ .nat
  | ifzElse {Δ : List Ty} : Tm Δ .nat → Tm Δ .nat → Ctx Γ A Δ .nat → Ctx Γ A Δ .nat
  | fix {Δ : List Ty} {B : Ty} : Ctx Γ A Δ (B ⇒ B) → Ctx Γ A Δ B
  | rename {Δ Δ' : List Ty} {B : Ty} : Ren Δ Δ' → Ctx Γ A Δ B → Ctx Γ A Δ' B

Uses 5 · Used by 14

Statement usesPCF renamings · PCF terms · PCF types · Natural number type of PCF · Simple types

Used byComposition of PCF contexts · Associativity of PCF context composition · Contextual equivalence in PCF is a congruence · Contextual approximation in PCF · Denotational approximation implies contextual approximation in PCF · Contextual equivalence in PCF · Contextual equivalence is mutual contextual approximation in PCF · Equal denotations imply contextual equivalence in PCF · Equal denotations are preserved by plugging into PCF contexts · Plugging into a PCF context is monotone in the denotation · Plugging a term into a PCF context · Plugging into a composite PCF context · Contextual equivalence in PCF is reflexive · Contextual approximation in PCF is reflexive

DefinitionPlugging a term into a PCF context#✓fully proved

Let \(C\) be a one-hole context that turns terms of type \(A\) in context \(\Gamma\) into terms of type \(B\) in context \(\Delta\), and \(t\) a term of type \(A\) in context \(\Gamma\). The term \(C[t]\) of type \(B\) in context \(\Delta\) is defined by recursion on \(C\): if \(C\) is the hole, \(C[t] = t\); if \(C\) applies a term former (abstraction, application on either side, successor, predecessor, the zero test at any of its three arguments, or the fixed point) to a subcontext \(C'\) and fixed terms, \(C[t]\) applies the same former to \(C'[t]\) and the same terms; and if \(C\) is a subcontext \(C'\) carried along a renaming \(\rho\), then \(C[t]\) is \(C'[t]\) renamed by \(\rho\).

def plug : {Δ : List Ty} → {B : Ty} → Ctx Γ A Δ B → Tm Γ A → Tm Δ B
  | _, _, .hole, t => t
  | _, _, .lam c, t => .lam (c.plug t)
  | _, _, .appL c a, t => .app (c.plug t) a
  | _, _, .appR f c, t => .app f (c.plug t)
  | _, _, .succ c, t => .succ (c.plug t)
  | _, _, .pred c, t => .pred (c.plug t)
  | _, _, .ifzTest c s₁ s₂, t => .ifz (c.plug t) s₁ s₂
  | _, _, .ifzThen r c s₂, t => .ifz r (c.plug t) s₂
  | _, _, .ifzElse r s₁ c, t => .ifz r s₁ (c.plug t)
  | _, _, .fix c, t => .fix (c.plug t)
  | _, _, .rename ρ c, t => Tm.rename ρ (c.plug t)

Uses 7 · Used by 11

Statement usesOne-hole contexts of PCF · PCF renamings · PCF terms · Renaming of PCF terms · PCF types · Natural number type of PCF · Simple types

Used byContextual equivalence in PCF is a congruence · Contextual approximation in PCF · Denotational approximation implies contextual approximation in PCF · Contextual equivalence in PCF · Contextual equivalence is mutual contextual approximation in PCF · Equal denotations imply contextual equivalence in PCF · Equal denotations are preserved by plugging into PCF contexts · Plugging into a PCF context is monotone in the denotation · Plugging into a composite PCF context · Contextual equivalence in PCF is reflexive · Contextual approximation in PCF is reflexive

DefinitionComposition of PCF contexts#✓fully proved

Let \(C\) be a one-hole context whose hole takes terms of type \(B\) in typing context \(\Delta\) and which produces terms of type \(B'\) in typing context \(\Theta\), and let \(D\) be a one-hole context whose hole takes terms of type \(A\) in typing context \(\Gamma\) and which produces terms of type \(B\) in typing context \(\Delta\). The composite \(C \circ D\) is the context obtained from \(C\) by replacing its hole by \(D\); its hole takes terms of type \(A\) in typing context \(\Gamma\), and it produces terms of type \(B'\) in typing context \(\Theta\).

def comp {Δ Θ : List Ty} {B C : Ty} : Ctx Δ B Θ C → Ctx Γ A Δ B → Ctx Γ A Θ C
  | .hole, inner => inner
  | .lam outer, inner => .lam (comp outer inner)
  | .appL outer a, inner => .appL (comp outer inner) a
  | .appR f outer, inner => .appR f (comp outer inner)
  | .succ outer, inner => .succ (comp outer inner)
  | .pred outer, inner => .pred (comp outer inner)
  | .ifzTest outer s₁ s₂, inner => .ifzTest (comp outer inner) s₁ s₂
  | .ifzThen r outer s₂, inner => .ifzThen r (comp outer inner) s₂
  | .ifzElse r s₁ outer, inner => .ifzElse r s₁ (comp outer inner)
  | .fix outer, inner => .fix (comp outer inner)
  | .rename ρ outer, inner => .rename ρ (comp outer inner)

Uses 6 · Used by 3

Statement usesOne-hole contexts of PCF · PCF renamings · PCF terms · PCF types · Natural number type of PCF · Simple types

Used byAssociativity of PCF context composition · Contextual equivalence in PCF is a congruence · Plugging into a composite PCF context

TheoremPlugging into a composite PCF context#✓fully proved

Let \(D\) be a one-hole context that turns terms of type \(B\) in context \(\Delta\) into terms of type \(C\) in context \(\Theta\), and let \(E\) be one that turns terms of type \(A\) in context \(\Gamma\) into terms of type \(B\) in context \(\Delta\). Write \(K[t]\) for the term obtained by plugging a term \(t\) into the hole of a context \(K\), and \(D \circ E\) for the context obtained by replacing the hole of \(D\) by \(E\). Then \((D \circ E)[t] = D[E[t]]\) for every term \(t\) of type \(A\) in context \(\Gamma\).

theorem plug_comp {Θ : List Ty} (outer : Ctx Δ B Θ C) (inner : Ctx Γ A Δ B) (t : Tm Γ A) :
    (comp outer inner).plug t = outer.plug (inner.plug t)

Uses 9 · Used by 1

Statement usesOne-hole contexts of PCF · Composition of PCF contexts · Plugging a term into a PCF context · PCF terms · PCF types

Proof usesPCF renamings · Renaming of PCF terms · Natural number type of PCF · Simple types

Used byContextual equivalence in PCF is a congruence

TheoremAssociativity of PCF context composition#✓fully proved

For one-hole contexts \(C\) and \(D\) such that the hole of \(C\) takes terms of the type and typing context that \(D\) produces, write \(C \circ D\) for the context obtained from \(C\) by replacing its hole by \(D\). For PCF one-hole contexts \(C_1\), \(C_2\) and \(C_3\) such that the hole of \(C_1\) takes terms of the type and typing context that \(C_2\) produces, and the hole of \(C_2\) takes terms of the type and typing context that \(C_3\) produces, composition is associative: \((C_1 \circ C_2) \circ C_3 = C_1 \circ (C_2 \circ C_3)\).

theorem comp_assoc {Θ Ξ : List Ty} {D : Ty} (outer : Ctx Θ C Ξ D) (middle : Ctx Δ B Θ C)
    (inner : Ctx Γ A Δ B) : comp (comp outer middle) inner = comp outer (comp middle inner)

Uses 7

Statement usesOne-hole contexts of PCF · Composition of PCF contexts · PCF types

Proof usesPCF renamings · PCF terms · Natural number type of PCF · Simple types

DefinitionContextual equivalence in PCF#✓fully proved

Write \(C[s]\) for the term obtained by plugging \(s\) into the hole of a one-hole context \(C\). PCF terms \(t\) and \(u\) of type \(A\) in typing context \(\Gamma\) are contextually equivalent when, for every one-hole context \(C\) whose hole takes terms of type \(A\) in typing context \(\Gamma\) and which produces closed terms of the ground type of natural numbers, and for every natural number \(n\), \(C[t]\) evaluates to the numeral \(n\) if and only if \(C[u]\) evaluates to the numeral \(n\). Evaluation is big-step call-by-name evaluation.

def CtxEquiv {Γ : List Ty} {A : Ty} (t u : Tm Γ A) : Prop :=
  ∀ (C : Ctx Γ A [] .nat) (n : ℕ), Eval (C.plug t) (numeral n) ↔ Eval (C.plug u) (numeral n)

Uses 7 · Used by 4

Statement usesOne-hole contexts of PCF · Plugging a term into a PCF context · PCF terms · Big-step call-by-name evaluation of PCF · PCF numerals · PCF types · Natural number type of PCF

Used byContextual equivalence in PCF is a congruence · Contextual equivalence is mutual contextual approximation in PCF · Equal denotations imply contextual equivalence in PCF · Contextual equivalence in PCF is reflexive

TheoremEqual denotations are preserved by plugging into PCF contexts#✓fully proved

Let \(t\) and \(u\) be PCF terms of type \(A\) in typing context \(\Gamma\) with the same denotation, and let \(C\) be a one-hole context whose hole takes terms of type \(A\) in typing context \(\Gamma\). Then the terms \(C[t]\) and \(C[u]\) obtained by plugging \(t\) and \(u\) into the hole of \(C\) have the same denotation.

theorem denote_plug_congr {Γ Δ : List Ty} {A B : Ty} (C : Ctx Γ A Δ B) {t u : Tm Γ A}
    (h : denote t = denote u) : denote (C.plug t) = denote (C.plug u)

Uses 17 · Used by 1

Statement usesOne-hole contexts of PCF · Plugging a term into a PCF context · Semantic environments for PCF · PCF terms · Denotation of PCF terms · PCF types · Domain of a PCF type

Proof usesVariable lookup in a PCF environment · Environment from a family of values · PCF renamings · PCF denotation of a renamed term · Renaming of PCF terms · Natural number type of PCF · Least elements of PCF domains · PCF variables · Simple types · Least fixed point of a Scott-continuous map

Used byEqual denotations imply contextual equivalence in PCF

TheoremEqual denotations imply contextual equivalence in PCF#✓fully proved

If two PCF terms \(t\) and \(u\) of the same type in the same typing context have the same denotation, as continuous maps from environments to the domain of their type, then \(t\) and \(u\) are contextually equivalent.

theorem ctxEquiv_of_denote_eq {Γ : List Ty} {A : Ty} {t u : Tm Γ A}
    (h : denote t = denote u) : CtxEquiv t u

Uses 13

Statement usesSemantic environments for PCF · PCF terms · Contextual equivalence in PCF · Denotation of PCF terms · PCF types · Domain of a PCF type

Proof usesOne-hole contexts of PCF · Plugging a term into a PCF context · Big-step call-by-name evaluation of PCF · Equal denotations are preserved by plugging into PCF contexts · Evaluation to a numeral agrees with the denotation · PCF numerals · Natural number type of PCF

DefinitionContextual approximation in PCF#✓fully proved

Write \(C[s]\) for the term obtained by plugging \(s\) into the hole of a one-hole context \(C\). For PCF terms \(t\) and \(u\) of type \(A\) in typing context \(\Gamma\), \(t\) contextually approximates \(u\) when, for every one-hole context \(C\) whose hole takes terms of type \(A\) in typing context \(\Gamma\) and which produces closed terms of the ground type of natural numbers, and for every natural number \(n\): if \(C[t]\) evaluates to the numeral \(n\), then \(C[u]\) evaluates to the numeral \(n\). Evaluation is big-step call-by-name evaluation.

def CtxApprox {Γ : List Ty} {A : Ty} (t u : Tm Γ A) : Prop :=
  ∀ (C : Ctx Γ A [] .nat) (n : ℕ), Eval (C.plug t) (numeral n) → Eval (C.plug u) (numeral n)

Uses 7 · Used by 3

Statement usesOne-hole contexts of PCF · Plugging a term into a PCF context · PCF terms · Big-step call-by-name evaluation of PCF · PCF numerals · PCF types · Natural number type of PCF

Used byDenotational approximation implies contextual approximation in PCF · Contextual equivalence is mutual contextual approximation in PCF · Contextual approximation in PCF is reflexive

TheoremPlugging into a PCF context is monotone in the denotation#✓fully proved

Let \(C\) be a one-hole context that turns terms of type \(A\) in context \(\Gamma\) into terms of type \(B\) in context \(\Delta\), and let \(t\) and \(u\) be terms of type \(A\) in context \(\Gamma\). Write \(C[s]\) for the term obtained by plugging a term \(s\) into the hole of \(C\), and \([\![ s ]\!]\,\eta\) for the denotation of a term \(s\) in an environment \(\eta\), ordered in the domain of its type. If \([\![ t ]\!]\,\eta \le [\![ u ]\!]\,\eta\) for every environment \(\eta\) for \(\Gamma\), then \([\![ C[t] ]\!]\,\eta \le [\![ C[u] ]\!]\,\eta\) for every environment \(\eta\) for \(\Delta\).

theorem denote_plug_mono {Γ Δ : List Ty} {A B : Ty} (C : Ctx Γ A Δ B) {t u : Tm Γ A}
    (h : ∀ η, denote t η ≤ denote u η) : ∀ η, denote (C.plug t) η ≤ denote (C.plug u) η

Uses 19 · Used by 1

Statement usesOne-hole contexts of PCF · Plugging a term into a PCF context · Semantic environments for PCF · PCF terms · Denotation of PCF terms · PCF types · Domain of a PCF type

Proof usesVariable lookup in a PCF environment · Environment from a family of values · PCF renamings · PCF denotation of a renamed term · Renaming of PCF terms · Natural number type of PCF · Least elements of PCF domains · PCF variables · Simple types · Least fixed point of a Scott-continuous map · The least fixed point is a fixed point · The least fixed point lies below every prefixed point

Used byDenotational approximation implies contextual approximation in PCF

TheoremDenotational approximation implies contextual approximation in PCF#✓fully proved

Let \(t\) and \(u\) be PCF terms of type \(A\) in typing context \(\Gamma\), and write \([\![s]\!]\) for the denotation of a term \(s\). If \([\![t]\!]\eta \le [\![u]\!]\eta\) in the domain denoted by \(A\) for every environment \(\eta\) for \(\Gamma\), then \(t\) contextually approximates \(u\).

theorem ctxApprox_of_denote_le {Γ : List Ty} {A : Ty} {t u : Tm Γ A}
    (h : ∀ η, denote t η ≤ denote u η) : CtxApprox t u

Uses 14

Statement usesSemantic environments for PCF · PCF terms · Contextual approximation in PCF · Denotation of PCF terms · PCF types · Domain of a PCF type

Proof usesOne-hole contexts of PCF · Plugging a term into a PCF context · Big-step call-by-name evaluation of PCF · Closed PCF terms that evaluate to a numeral denote its value · Computational adequacy for PCF · Plugging into a PCF context is monotone in the denotation · PCF numerals · Natural number type of PCF

TheoremContextual equivalence in PCF is reflexive#✓fully proved

Every term \(t\) of type \(A\) in context \(\Gamma\) is contextually equivalent to itself.

theorem CtxEquiv.refl {Γ : List Ty} {A : Ty} (t : Tm Γ A) : CtxEquiv t t

Uses 8

Statement usesPCF terms · Contextual equivalence in PCF · PCF types

Proof usesOne-hole contexts of PCF · Plugging a term into a PCF context · Big-step call-by-name evaluation of PCF · PCF numerals · Natural number type of PCF

TheoremContextual equivalence in PCF is a congruence#✓fully proved

Let \(t\) and \(u\) be PCF terms of type \(A\) in typing context \(\Gamma\). If \(t\) and \(u\) are contextually equivalent, then for every one-hole context \(D\) whose hole takes terms of type \(A\) in typing context \(\Gamma\), the terms \(D[t]\) and \(D[u]\) obtained by plugging \(t\) and \(u\) into the hole of \(D\) are contextually equivalent.

theorem CtxEquiv.congr {Γ Δ : List Ty} {A B : Ty} {t u : Tm Γ A} (h : CtxEquiv t u)
    (D : Ctx Γ A Δ B) : CtxEquiv (D.plug t) (D.plug u)

Uses 10

Statement usesOne-hole contexts of PCF · Plugging a term into a PCF context · PCF terms · Contextual equivalence in PCF · PCF types

Proof usesComposition of PCF contexts · Plugging into a composite PCF context · Big-step call-by-name evaluation of PCF · PCF numerals · Natural number type of PCF

TheoremContextual approximation in PCF is reflexive#✓fully proved

Every term \(t\) of type \(A\) in context \(\Gamma\) contextually approximates itself.

theorem CtxApprox.refl {Γ : List Ty} {A : Ty} (t : Tm Γ A) : CtxApprox t t

Uses 8

Statement usesPCF terms · Contextual approximation in PCF · PCF types

Proof usesOne-hole contexts of PCF · Plugging a term into a PCF context · Big-step call-by-name evaluation of PCF · PCF numerals · Natural number type of PCF

TheoremContextual equivalence is mutual contextual approximation in PCF#✓fully proved

PCF terms \(t\) and \(u\) of the same type in the same typing context are contextually equivalent if and only if \(t\) contextually approximates \(u\) and \(u\) contextually approximates \(t\).

theorem ctxEquiv_iff_ctxApprox {Γ : List Ty} {A : Ty} {t u : Tm Γ A} :
    CtxEquiv t u ↔ CtxApprox t u ∧ CtxApprox u t

Uses 9

Statement usesPCF terms · Contextual approximation in PCF · Contextual equivalence in PCF · PCF types

Proof usesOne-hole contexts of PCF · Plugging a term into a PCF context · Big-step call-by-name evaluation of PCF · PCF numerals · Natural number type of PCF

74 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.