Continuation-passing style translation

DefinitionCall-by-name CPS translation of types#✓fully proved

Fix an answer type \(R\) of the simply typed lambda calculus. The call-by-name CPS translation \(A^\ast\) of a simple type \(A\) is defined by recursion on \(A\): a base type is translated to itself, \(b^\ast = b\), and a function type is translated by \((A \to B)^\ast = ((A^\ast \to R) \to R) \to ((B^\ast \to R) \to R)\).

def cbnTy (R : Ty Base) : Ty Base → Ty Base
  | .base b => .base b
  | .arr A B => ((cbnTy R A ⇒ R) ⇒ R) ⇒ ((cbnTy R B ⇒ R) ⇒ R)

Uses 1 · Used by 14

Statement usesSimple types

Used byCall-by-name CPS translation of terms · Computation types of the call-by-name CPS translation · Related computations in the call-by-name CPS translation · Denotational correctness of the call-by-name CPS translation · The call-by-name CPS translation at base types · Running the call-by-name CPS translation with the identity continuation · Call-by-name evaluation is preserved by the CPS translation · Logical relation for the call-by-name CPS translation · The call-by-name CPS translation of a renaming · The call-by-name CPS translation commutes with renaming · Plotkin's simulation theorem for the call-by-name CPS translation · The call-by-name CPS translation commutes with substitution · The translation of a closed term is a value · The translation of an abstraction passes the translated function to its continuation

AbbreviationComputation types of the call-by-name CPS translation#✓fully proved

For an answer type \(R\) and a simple type \(A\), the type of call-by-name computations of type \(A\) is \(C(A) = (A^\ast \to R) \to R\), where \(A^\ast\) is the call-by-name CPS translation of \(A\).

abbrev cbnComp (R : Ty Base) (A : Ty Base) : Ty Base := (cbnTy R A ⇒ R) ⇒ R

Uses 2 · Used by 17

Statement usesCall-by-name CPS translation of types · Simple types

Used byCall-by-name CPS translation of terms · Related computations in the call-by-name CPS translation · Denotational correctness of the call-by-name CPS translation · The call-by-name CPS translation at base types · Running the call-by-name CPS translation with the identity continuation · Related environments for the call-by-name CPS translation · Call-by-name evaluation is preserved by the CPS translation · The call-by-name CPS translation commutes with instantiation · Logical relation for the call-by-name CPS translation · The call-by-name CPS translation of a renaming · The call-by-name CPS translation commutes with renaming · Plotkin's simulation theorem for the call-by-name CPS translation · The call-by-name CPS translation commutes with substitution · The translation of a closed term is a value · Call-by-name CPS translation of variables · The call-by-name CPS translation commutes with weakening · The translation of an abstraction passes the translated function to its continuation

DefinitionCall-by-name CPS translation of variables#✓fully proved

Fix an answer type \(R\) and write \(C(A) = (A^\ast \to R) \to R\), where \(A^\ast\) is the call-by-name CPS translation of a simple type \(A\). A variable of type \(A\) in a context \(A_1, \dots, A_n\) is translated to the variable at the same position in the translated context \(C(A_1), \dots, C(A_n)\), where it has type \(C(A)\).

def cbnVar : {Γ : List (Ty Base)} → {A : Ty Base} →
    Var Γ A → Var (Γ.map (cbnComp R)) (cbnComp R A)
  | _, _, .zero => .zero
  | _, _, .succ x => .succ (cbnVar x)

Uses 3 · Used by 7

Statement usesComputation types of the call-by-name CPS translation · Simple types · Typed de Bruijn variables of the simply typed lambda calculus

Used byCall-by-name CPS translation of terms · Denotational correctness of the call-by-name CPS translation · Related environments for the call-by-name CPS translation · The call-by-name CPS translation commutes with instantiation · The call-by-name CPS translation of a renaming · The call-by-name CPS translation commutes with renaming · The call-by-name CPS translation commutes with substitution

DefinitionCall-by-name CPS translation of terms#✓fully proved

Fix an answer type \(R\) and write \(C(A) = (A^\ast \to R) \to R\), where \(A^\ast\) is the call-by-name CPS translation of a simple type \(A\). A term \(t\) of type \(A\) in a context \(A_1, \dots, A_n\) is translated to a term \(\overline{t}\) of type \(C(A)\) in the context \(C(A_1), \dots, C(A_n)\), by recursion on \(t\): a variable \(x\) is translated to the variable at the same position; an abstraction by \(\overline{\lambda x.\, M} = \lambda k.\, k\,(\lambda x.\, \overline{M})\); and an application by \(\overline{M\,N} = \lambda k.\, \overline{M}\,(\lambda m.\, m\,\overline{N}\,k)\), where \(k\) and \(m\) are fresh variables.

def cbn : {Γ : List (Ty Base)} → {A : Ty Base} →
    Tm Γ A → Tm (Γ.map (cbnComp R)) (cbnComp R A)
  | _, _, .var x => .var (cbnVar R x)
  | _, _, .lam body => .lam (.app (.var .zero) (Tm.weaken (.lam (cbn body))))
  | _, _, .app f a =>
      .lam (.app (Tm.weaken (cbn f))
        (.lam (.app (.app (.var .zero) (Tm.weaken (Tm.weaken (cbn a)))) (.var (.succ .zero)))))

Uses 7 · Used by 11

Statement usesComputation types of the call-by-name CPS translation · Call-by-name CPS translation of types · Call-by-name CPS translation of variables · Intrinsically typed terms of the simply typed lambda calculus · Weakening a simply typed term · Simple types · Typed de Bruijn variables of the simply typed lambda calculus

Used byDenotational correctness of the call-by-name CPS translation · The call-by-name CPS translation at base types · Running the call-by-name CPS translation with the identity continuation · Call-by-name evaluation is preserved by the CPS translation · The call-by-name CPS translation commutes with instantiation · The call-by-name CPS translation commutes with renaming · Plotkin's simulation theorem for the call-by-name CPS translation · The call-by-name CPS translation commutes with substitution · The translation of a closed term is a value · The call-by-name CPS translation commutes with weakening · The translation of an abstraction passes the translated function to its continuation

DefinitionLogical relation for the call-by-name CPS translation#✓fully proved

Fix an answer type \(R\) and an interpretation \(I\) of the base types. Write \(D(A)\) for the set of values of a simple type \(A\) (\(D(b) = I(b)\) for a base type \(b\), and \(D(A \to B)\) is the set of functions from \(D(A)\) to \(D(B)\)), \(A^\ast\) for the call-by-name CPS translation of \(A\), and \(C(A) = (A^\ast \to R) \to R\). The relation \(a \sim_A a'\) between \(a \in D(A)\) and \(a' \in D(A^\ast)\) is defined by recursion on \(A\). At a base type \(b\), \(a \sim_b a'\) holds when \(a = a'\). At a function type, \(f \sim_{A \to B} g\) holds when for every \(a \in D(A)\) and every \(c \in D(C(A))\): if there is \(v\) with \(a \sim_A v\) and \(c\,k = k\,v\) for every \(k \in D(A^\ast \to R)\), then there is \(w\) with \(f\,a \sim_B w\) and \(g\,c\,k = k\,w\) for every \(k \in D(B^\ast \to R)\).

def CbnRel (I : Base → Type v) : (A : Ty Base) → Ty.denote I A → Ty.denote I (cbnTy R A) → Prop
  | .base _, a, a' => a = a'
  | .arr A B, f, g => ∀ a (c : Ty.denote I (cbnComp R A)),
      (∃ v, CbnRel I A a v ∧ ∀ k, c k = k v) →
        ∃ w, CbnRel I B (f a) w ∧ ∀ k, g c k = k w

Uses 4 · Used by 3

Statement usesComputation types of the call-by-name CPS translation · Call-by-name CPS translation of types · Simple types · Denotation of simple types

Used byRelated computations in the call-by-name CPS translation · Denotational correctness of the call-by-name CPS translation · The call-by-name CPS translation at base types

DefinitionRelated computations in the call-by-name CPS translation#✓fully proved

Fix an answer type \(R\) and an interpretation \(I\) of the base types; write \(D(A)\) for the set of values of a simple type \(A\), \(A^\ast\) for its call-by-name CPS translation, \(C(A) = (A^\ast \to R) \to R\), and \(\sim_A\) for the call-by-name logical relation between \(D(A)\) and \(D(A^\ast)\). A computation \(c \in D(C(A))\) is related to a value \(a \in D(A)\) when there is \(v \in D(A^\ast)\) with \(a \sim_A v\) such that \(c\,k = k\,v\) for every continuation \(k \in D(A^\ast \to R)\).

def CbnCompRel (I : Base → Type v) (A : Ty Base) (a : Ty.denote I A)
    (c : Ty.denote I (cbnComp R A)) : Prop :=
  ∃ v, CbnRel R I A a v ∧ ∀ k, c k = k v

Uses 5 · Used by 3

Statement usesLogical relation for the call-by-name CPS translation · Computation types of the call-by-name CPS translation · Call-by-name CPS translation of types · Simple types · Denotation of simple types

Used byDenotational correctness of the call-by-name CPS translation · The call-by-name CPS translation at base types · Related environments for the call-by-name CPS translation

DefinitionRelated environments for the call-by-name CPS translation#✓fully proved

Fix an answer type \(R\) and an interpretation of the base types, and write \(C(A) = (A^\ast \to R) \to R\), where \(A^\ast\) is the call-by-name CPS translation of a simple type \(A\). Let \(\eta\) be an environment for a context \(\Gamma = A_1, \dots, A_n\), assigning to each variable \(x\) of type \(A\) a value \(\eta(x)\) of type \(A\), and let \(\eta'\) be an environment for the translated context \(C(A_1), \dots, C(A_n)\). Then \(\eta\) and \(\eta'\) are related when for every variable \(x\) of \(\Gamma\), of type \(A\) say, the value that \(\eta'\) assigns to the variable at the same position as \(x\) in the translated context is a computation of type \(C(A)\) related to \(\eta(x)\).

def CbnEnvRel {Γ : List (Ty Base)} (η : Env I Γ) (η' : Env I (Γ.map (cbnComp R))) : Prop :=
  ∀ {A} (x : Var Γ A), CbnCompRel R I A (η x) (η' (cbnVar R x))

Uses 6 · Used by 3

Statement usesRelated computations in the call-by-name CPS translation · Computation types of the call-by-name CPS translation · Call-by-name CPS translation of variables · Semantic environments for the denotational semantics of STLC · Simple types · Typed de Bruijn variables of the simply typed lambda calculus

Used byDenotational correctness of the call-by-name CPS translation · The call-by-name CPS translation at base types · Running the call-by-name CPS translation with the identity continuation

TheoremDenotational correctness of the call-by-name CPS translation#✓fully proved

Fix an answer type \(R\) and an interpretation of the base types; write \(D(A)\) for the set of values of a simple type \(A\), \(A^\ast\) for its call-by-name CPS translation, and \(\sim_A\) for the call-by-name logical relation. Let \(t\) be a term of type \(A\) in a context \(\Gamma\), and let \(\eta\) be an environment for \(\Gamma\) and \(\eta'\) an environment for the translated context such that \(\eta\) and \(\eta'\) are related. Let \(a \in D(A)\) be the denotation of \(t\) in \(\eta\), and let \(c\) be the denotation in \(\eta'\) of the call-by-name CPS translation \(\overline{t}\) of \(t\). Then there is \(v \in D(A^\ast)\) with \(a \sim_A v\) such that \(c\,k = k\,v\) for every continuation \(k \in D(A^\ast \to R)\).

theorem cbn_correct {Γ : List (Ty Base)} {A : Ty Base} (t : Tm Γ A) {η : Env I Γ}
    {η' : Env I (Γ.map (cbnComp R))} (hη : CbnEnvRel R η η') :
    CbnCompRel R I A (Tm.denote I t η) (Tm.denote I (cbn R t) η')

Uses 16 · Used by 1

Statement usesRelated computations in the call-by-name CPS translation · Related environments for the call-by-name CPS translation · Call-by-name CPS translation of terms · Computation types of the call-by-name CPS translation · Semantic environments for the denotational semantics of STLC · Intrinsically typed terms of the simply typed lambda calculus · Denotation of an STLC term · Simple types

Proof usesLogical relation for the call-by-name CPS translation · Call-by-name CPS translation of types · Call-by-name CPS translation of variables · Extending a semantic environment in STLC · Weakening preserves STLC denotation · Weakening a simply typed term · Denotation of simple types · Typed de Bruijn variables of the simply typed lambda calculus

Used byThe call-by-name CPS translation at base types

TheoremThe call-by-name CPS translation at base types#✓fully proved

Fix an answer type \(R\) and an interpretation of the base types. Let \(t\) be a term of a base type \(b\) in a context \(\Gamma\), let \(\eta\) be an environment for \(\Gamma\), and let \(\eta'\) be an environment for the translated context related to \(\eta\). Then for every continuation \(k\) from the values of type \(b\) to the values of type \(R\), the denotation in \(\eta'\) of the call-by-name CPS translation \(\overline{t}\) of \(t\), applied to \(k\), equals \(k\) applied to the denotation of \(t\) in \(\eta\).

theorem cbn_denote_base {Γ : List (Ty Base)} {b : Base} (t : Tm Γ (.base b))
    {η : Env I Γ} {η' : Env I (Γ.map (cbnComp R))} (hη : CbnEnvRel R η η')
    (k : Ty.denote I (cbnTy R (.base b) ⇒ R)) :
    Tm.denote I (cbn R t) η' k = k (Tm.denote I t η)

Uses 12 · Used by 1

Statement usesRelated environments for the call-by-name CPS translation · Call-by-name CPS translation of terms · Computation types of the call-by-name CPS translation · Call-by-name CPS translation of types · Semantic environments for the denotational semantics of STLC · Intrinsically typed terms of the simply typed lambda calculus · Denotation of an STLC term · Simple types · Denotation of simple types

Proof usesRelated computations in the call-by-name CPS translation · Logical relation for the call-by-name CPS translation · Denotational correctness of the call-by-name CPS translation

Used byRunning the call-by-name CPS translation with the identity continuation

TheoremRunning the call-by-name CPS translation with the identity continuation#✓fully proved

Fix an interpretation of the base types. Let \(t\) be a term of a base type \(b\) in a context \(\Gamma\), take the answer type to be \(b\), let \(\eta\) be an environment for \(\Gamma\), and let \(\eta'\) be an environment for the translated context related to \(\eta\). Then the denotation in \(\eta'\) of the call-by-name CPS translation \(\overline{t}\) of \(t\), applied to the identity function on the values of type \(b\), equals the denotation of \(t\) in \(\eta\).

theorem cbn_denote_base_id {Γ : List (Ty Base)} {b : Base} (t : Tm Γ (.base b))
    {η : Env I Γ} {η' : Env I (Γ.map (cbnComp (.base b)))} (hη : CbnEnvRel (.base b) η η') :
    Tm.denote I (cbn (.base b) t) η' id = Tm.denote I t η

Uses 10

Statement usesRelated environments for the call-by-name CPS translation · Call-by-name CPS translation of terms · Computation types of the call-by-name CPS translation · Call-by-name CPS translation of types · Semantic environments for the denotational semantics of STLC · Intrinsically typed terms of the simply typed lambda calculus · Denotation of an STLC term · Simple types · Denotation of simple types

Proof usesThe call-by-name CPS translation at base types

DefinitionCall-by-value CPS translation of types#✓fully proved

For a fixed answer type \(R\), the translation \(\overline{A}\) of a simple type \(A\) is defined by recursion on \(A\): \(\overline{b} = b\) for a base type \(b\), and \(\overline{A \to B} = \overline{A} \to ((\overline{B} \to R) \to R)\).

def cpsTy (R : Ty Base) : Ty Base → Ty Base
  | .base b => .base b
  | .arr A B => cpsTy R A ⇒ ((cpsTy R B ⇒ R) ⇒ R)

Uses 1 · Used by 17

Statement usesSimple types

Used byCPS computation type · Call-by-value CPS translation of terms · Denotational correctness of the CPS translation (Meyer–Wand) · CPS translation at a base type · CPS translation at a base type with the identity continuation · The CPS translation commutes with instantiation by a value or variable · Translated renaming · The call-by-value CPS translation commutes with renaming · Plotkin's simulation theorem, big-step form · Simulation for terms evaluating to an abstraction · The CPS translation commutes with substitution of values and variables · CPS translation of variables · The CPS translation commutes with weakening · Related environments · Plotkin's value translation \(\Psi\) · Logical relation for the CPS translation · The value translation preserves values

AbbreviationCPS computation type#✓fully proved

For an answer type \(R\) and a simple type \(A\), the type of CPS computations returning a value of type \(A\) is \((\overline{A} \to R) \to R\), where \(\overline{A}\) is the call-by-value CPS translation of \(A\) for answer type \(R\).

abbrev compTy (R : Ty Base) (A : Ty Base) : Ty Base :=
  (cpsTy R A ⇒ R) ⇒ R

Uses 2 · Used by 9

Statement usesCall-by-value CPS translation of types · Simple types

Used byCall-by-value CPS translation of terms · Denotational correctness of the CPS translation (Meyer–Wand) · CPS translation at a base type · CPS translation at a base type with the identity continuation · The CPS translation commutes with instantiation by a value or variable · The call-by-value CPS translation commutes with renaming · Plotkin's simulation theorem, big-step form · The CPS translation commutes with substitution of values and variables · The CPS translation commutes with weakening

DefinitionCPS translation of variables#✓fully proved

Fix an answer type \(R\) and write \(\overline{A}\) for the call-by-value CPS translation of a type \(A\). A de Bruijn variable of type \(A\) in a context \(A_1, \ldots, A_n\) is sent to the variable at the same position in the translated context \(\overline{A_1}, \ldots, \overline{A_n}\), which has type \(\overline{A}\).

def cpsVar : {Γ : List (Ty Base)} → {A : Ty Base} →
    Var Γ A → Var (Γ.map (cpsTy R)) (cpsTy R A)
  | _, _, .zero => .zero
  | _, _, .succ x => .succ (cpsVar x)

Uses 3 · Used by 11

Statement usesCall-by-value CPS translation of types · Simple types · Typed de Bruijn variables of the simply typed lambda calculus

Used byCall-by-value CPS translation of terms · Denotational correctness of the CPS translation (Meyer–Wand) · The CPS translation commutes with instantiation by a value or variable · Translated renaming · The call-by-value CPS translation commutes with renaming · Plotkin's simulation theorem, big-step form · Simulation for terms evaluating to an abstraction · The CPS translation commutes with substitution of values and variables · Related environments · Plotkin's value translation \(\Psi\) · The value translation preserves values

DefinitionCall-by-value CPS translation of terms#✓fully proved

Fix an answer type \(R\) and write \(\overline{A}\) for the call-by-value CPS translation of a type \(A\) and \(\overline{\Gamma}\) for the context obtained by translating each type of a context \(\Gamma\). A term \(M\) of type \(A\) in context \(\Gamma\) is sent to a term \(\overline{M}\) of type \((\overline{A} \to R) \to R\) in context \(\overline{\Gamma}\), defined by recursion on \(M\) by \(\overline{x} = \lambda k.\,k\,x\), \(\overline{\lambda x.\,M} = \lambda k.\,k\,(\lambda x.\,\overline{M})\) and \(\overline{M\,N} = \lambda k.\,\overline{M}\,(\lambda m.\,\overline{N}\,(\lambda n.\,m\,n\,k))\), where \(k\), \(m\) and \(n\) are fresh variables.

def cps : {Γ : List (Ty Base)} → {A : Ty Base} →
    Tm Γ A → Tm (Γ.map (cpsTy R)) (compTy R A)
  | _, _, .var x => .lam (.app (.var .zero) (.var (.succ (cpsVar R x))))
  | _, _, .lam body => .lam (.app (.var .zero) (Tm.weaken (.lam (cps body))))
  | _, _, .app f a =>
      .lam (.app (Tm.weaken (cps f))
        (.lam (.app (Tm.weaken (Tm.weaken (cps a)))
          (.lam (.app (.app (.var (.succ .zero)) (.var .zero))
            (.var (.succ (.succ .zero))))))))

Uses 7 · Used by 11

Statement usesCPS computation type · Call-by-value CPS translation of types · CPS translation of variables · Intrinsically typed terms of the simply typed lambda calculus · Weakening a simply typed term · Simple types · Typed de Bruijn variables of the simply typed lambda calculus

Used byDenotational correctness of the CPS translation (Meyer–Wand) · CPS translation at a base type · CPS translation at a base type with the identity continuation · The CPS translation commutes with instantiation by a value or variable · The call-by-value CPS translation commutes with renaming · Plotkin's simulation theorem, big-step form · Simulation for terms evaluating to an abstraction · The CPS translation commutes with substitution of values and variables · The CPS translation commutes with weakening · Plotkin's value translation \(\Psi\) · The value translation preserves values

DefinitionLogical relation for the CPS translation#✓fully proved

Fix an answer type \(R\) and an interpretation \(I\) of the base types; write \(D(A)\) for the set interpreting a simple type \(A\) under \(I\) and \(\overline{A}\) for the call-by-value CPS translation of \(A\). The relation \(a \sim_A a'\) between \(a \in D(A)\) and \(a' \in D(\overline{A})\) is defined by recursion on \(A\): at a base type \(b\), \(a \sim_b a'\) means \(a = a'\); at a function type, \(f \sim_{A \to B} f'\) means that for all \(a \sim_A a'\) there is a \(b' \in D(\overline{B})\) with \(f(a) \sim_B b'\) and \(f'(a')(k) = k(b')\) for every continuation \(k \in D(\overline{B} \to R)\).

def Rel (I : Base → Type v) : (A : Ty Base) → Ty.denote I A → Ty.denote I (cpsTy R A) → Prop
  | .base _, a, a' => a = a'
  | .arr A B, f, f' => ∀ a a', Rel I A a a' →
      ∃ b', Rel I B (f a) b' ∧ ∀ k, f' a' k = k b'

Uses 3 · Used by 3

Statement usesCall-by-value CPS translation of types · Simple types · Denotation of simple types

Used byDenotational correctness of the CPS translation (Meyer–Wand) · CPS translation at a base type · Related environments

DefinitionRelated environments#✓fully proved

Fix an answer type \(R\) and an interpretation \(I\) of the base types, and write \(\overline{\Gamma}\) for the context obtained by translating each type of a context \(\Gamma\) by the call-by-value CPS translation. An environment \(\eta\) for \(\Gamma\) and an environment \(\eta'\) for \(\overline{\Gamma}\) are related when, for every variable \(x\) of type \(A\) in \(\Gamma\), the value \(\eta(x)\) is related at type \(A\), by the CPS logical relation, to the value that \(\eta'\) assigns to the variable at the same position in \(\overline{\Gamma}\).

def EnvRel {Γ : List (Ty Base)} (η : Env I Γ) (η' : Env I (Γ.map (cpsTy R))) : Prop :=
  ∀ {A} (x : Var Γ A), Rel R I A (η x) (η' (cpsVar R x))

Uses 6 · Used by 3

Statement usesLogical relation for the CPS translation · Call-by-value CPS translation of types · CPS translation of variables · Semantic environments for the denotational semantics of STLC · Simple types · Typed de Bruijn variables of the simply typed lambda calculus

Used byDenotational correctness of the CPS translation (Meyer–Wand) · CPS translation at a base type · CPS translation at a base type with the identity continuation

TheoremDenotational correctness of the CPS translation (Meyer–Wand)#✓fully proved

Fix an answer type \(R\) and an interpretation \(I\) of the base types; write \(D(A)\) for the set interpreting a type \(A\), \(\overline{A}\), \(\overline{\Gamma}\) and \(\overline{t}\) for the call-by-value CPS translations of types, contexts and terms, and \([t]_\eta\) for the denotation of a term \(t\) in an environment \(\eta\). Let \(t\) be a term of type \(A\) in context \(\Gamma\), and let \(\eta\) and \(\eta'\) be related environments for \(\Gamma\) and \(\overline{\Gamma}\). Then there is a value \(v' \in D(\overline{A})\), related to \([t]_\eta\) by the CPS logical relation at \(A\), such that \([\overline{t}]_{\eta'}(k) = k(v')\) for every continuation \(k \colon D(\overline{A}) \to D(R)\).

theorem cps_correct {Γ : List (Ty Base)} {A : Ty Base} (t : Tm Γ A) {η : Env I Γ}
    {η' : Env I (Γ.map (cpsTy R))} (hη : EnvRel R η η') :
    ∃ v', Rel R I A (Tm.denote I t η) v' ∧
      ∀ k, Tm.denote I (cps R t) η' k = k v'

Uses 15 · Used by 1

Statement usesRelated environments · Logical relation for the CPS translation · CPS computation type · Call-by-value CPS translation of terms · Call-by-value CPS translation of types · Semantic environments for the denotational semantics of STLC · Intrinsically typed terms of the simply typed lambda calculus · Denotation of an STLC term · Simple types · Denotation of simple types

Proof usesCPS translation of variables · Extending a semantic environment in STLC · Weakening preserves STLC denotation · Weakening a simply typed term · Typed de Bruijn variables of the simply typed lambda calculus

Used byCPS translation at a base type

TheoremCPS translation at a base type#✓fully proved

Fix an answer type \(R\) and an interpretation \(I\) of the base types; write \(D(A)\) for the set interpreting a type \(A\), \(\overline{\Gamma}\) and \(\overline{t}\) for the call-by-value CPS translations of contexts and terms, and \([t]_\eta\) for the denotation of a term \(t\) in an environment \(\eta\). Let \(t\) be a term of base type \(b\) in context \(\Gamma\), and let \(\eta\) and \(\eta'\) be related environments for \(\Gamma\) and \(\overline{\Gamma}\). Then \([\overline{t}]_{\eta'}(k) = k([t]_\eta)\) for every continuation \(k \colon I(b) \to D(R)\).

theorem cps_denote_base {Γ : List (Ty Base)} {b : Base} (t : Tm Γ (.base b))
    {η : Env I Γ} {η' : Env I (Γ.map (cpsTy R))} (hη : EnvRel R η η')
    (k : Ty.denote I (cpsTy R (.base b) ⇒ R)) :
    Tm.denote I (cps R t) η' k = k (Tm.denote I t η)

Uses 11 · Used by 1

Statement usesRelated environments · CPS computation type · Call-by-value CPS translation of terms · Call-by-value CPS translation of types · Semantic environments for the denotational semantics of STLC · Intrinsically typed terms of the simply typed lambda calculus · Denotation of an STLC term · Simple types · Denotation of simple types

Proof usesLogical relation for the CPS translation · Denotational correctness of the CPS translation (Meyer–Wand)

Used byCPS translation at a base type with the identity continuation

TheoremCPS translation at a base type with the identity continuation#✓fully proved

Fix an interpretation \(I\) of the base types, let \(t\) be a term of base type \(b\) in context \(\Gamma\), and take the answer type to be \(b\); write \(\overline{\Gamma}\) and \(\overline{t}\) for the call-by-value CPS translations of \(\Gamma\) and \(t\), and \([t]_\eta\) for the denotation of \(t\) in an environment \(\eta\). If \(\eta\) and \(\eta'\) are related environments for \(\Gamma\) and \(\overline{\Gamma}\), then \([\overline{t}]_{\eta'}(\mathrm{id}) = [t]_\eta\), where \(\mathrm{id}\) is the identity on \(I(b)\).

theorem cps_denote_base_id {Γ : List (Ty Base)} {b : Base} (t : Tm Γ (.base b))
    {η : Env I Γ} {η' : Env I (Γ.map (cpsTy (.base b)))} (hη : EnvRel (.base b) η η') :
    Tm.denote I (cps (.base b) t) η' id = Tm.denote I t η

Uses 10

Statement usesRelated environments · CPS computation type · Call-by-value CPS translation of terms · Call-by-value CPS translation of types · Semantic environments for the denotational semantics of STLC · Intrinsically typed terms of the simply typed lambda calculus · Denotation of an STLC term · Simple types · Denotation of simple types

Proof usesCPS translation at a base type

DefinitionTranslated renaming#✓fully proved

Fix an answer type \(R\) and write \(\llbracket \Gamma \rrbracket\) for the context obtained by applying the call-by-value CPS type translation to every entry of \(\Gamma\). A renaming \(\rho\) from \(\Gamma\) to \(\Delta\) induces the renaming from \(\llbracket \Gamma \rrbracket\) to \(\llbracket \Delta \rrbracket\) that sends the translation of each variable \(x\) of \(\Gamma\) (the variable at the same position) to the translation of \(\rho(x)\).

def cpsRen : {Γ Δ : List (Ty Base)} → Ren Γ Δ → Ren (Γ.map (cpsTy R)) (Δ.map (cpsTy R))
  | [], _, _, _, x => nomatch x
  | _ :: _, _, ρ, _, .zero => cpsVar R (ρ .zero)
  | _ :: _, _, ρ, _, .succ y => cpsRen (fun x => ρ (.succ x)) y

Uses 5 · Used by 3

Statement usesCall-by-value CPS translation of types · CPS translation of variables · Renamings of simply typed contexts · Simple types · Typed de Bruijn variables of the simply typed lambda calculus

Used byThe call-by-value CPS translation commutes with renaming · The CPS translation commutes with substitution of values and variables · The CPS translation commutes with weakening

TheoremThe call-by-value CPS translation commutes with renaming#✓fully proved

Fix an answer type \(R\) and write \(\llbracket \cdot \rrbracket\) for the call-by-value CPS translation of types, contexts (entrywise) and terms. For every renaming \(\rho\) from a context \(\Gamma\) to a context \(\Delta\) and every term \(t\) of type \(A\) in \(\Gamma\), the translation of the renamed term \(t[\rho]\) equals the renaming of \(\llbracket t \rrbracket\) along the translated renaming from \(\llbracket \Gamma \rrbracket\) to \(\llbracket \Delta \rrbracket\), which sends the translation of each variable \(x\) of \(\Gamma\) to the translation of \(\rho(x)\).

theorem cps_rename (ρ : Ren Γ Δ) (t : Tm Γ A) :
    cps R (Tm.rename ρ t) = Tm.rename (cpsRen R ρ) (cps R t)

Uses 13 · Used by 2

Statement usesCPS computation type · Call-by-value CPS translation of terms · Translated renaming · Call-by-value CPS translation of types · Renamings of simply typed contexts · Intrinsically typed terms of the simply typed lambda calculus · Renaming a simply typed term · Simple types

Proof usesCPS translation of variables · Renaming commutes with weakening for intrinsically typed STLC terms · Weakening a simply typed term · Typed de Bruijn variables of the simply typed lambda calculus · Lifting a renaming under a binder

Used byThe CPS translation commutes with substitution of values and variables · The CPS translation commutes with weakening

TheoremThe CPS translation commutes with weakening#✓fully proved

Fix an answer type \(R\) and write \(\llbracket \cdot \rrbracket\) for the call-by-value CPS translation of types, contexts (entrywise) and terms. For every term \(t\) of type \(A\) in a context \(\Gamma\) and every type \(B\), the translation of the weakening of \(t\) to the context \(B, \Gamma\) is the weakening of \(\llbracket t \rrbracket\) to the context \(\llbracket B \rrbracket, \llbracket \Gamma \rrbracket\).

theorem cps_weaken (t : Tm Γ A) :
    cps R (Tm.weaken (B := B) t) = Tm.weaken (cps R t)

Uses 13

Statement usesCPS computation type · Call-by-value CPS translation of terms · Call-by-value CPS translation of types · Intrinsically typed terms of the simply typed lambda calculus · Weakening a simply typed term · Simple types

Proof usesTranslated renaming · The call-by-value CPS translation commutes with renaming · Renamings of simply typed contexts · Renaming a simply typed term · Typed de Bruijn variables of the simply typed lambda calculus · Identity renaming of a simply typed context · Lifting a renaming under a binder

InductivePlotkin's value translation \(\Psi\)#✓fully proved

Fix an answer type \(R\), and write \(A^*\) for the call-by-value CPS translation of a type \(A\), \(\Gamma^*\) for the context obtained by translating each type of a context \(\Gamma\), and \(\overline{M}\) for the CPS translation of a term \(M\). The relation \(\Psi\) between terms of type \(A\) in context \(\Gamma\) and terms of type \(A^*\) in context \(\Gamma^*\) holds in exactly two cases: a variable \(x\) of \(\Gamma\) is related to the variable at the same position in \(\Gamma^*\), and an abstraction \(\lambda x.\, N\) is related to \(\lambda x.\, \overline{N}\).

inductive PsiRel : {Γ : List (Ty Base)} → {A : Ty Base} →
    Tm Γ A → Tm (Γ.map (cpsTy R)) (cpsTy R A) → Prop
  | var {Γ : List (Ty Base)} {A : Ty Base} (x : Var Γ A) : PsiRel (.var x) (.var (cpsVar R x))
  | lam {Γ : List (Ty Base)} {A B : Ty Base} (body : Tm (A :: Γ) B) :
      PsiRel (.lam body) (.lam (cps R body))

Uses 6 · Used by 5

Statement usesCall-by-value CPS translation of terms · Call-by-value CPS translation of types · CPS translation of variables · Intrinsically typed terms of the simply typed lambda calculus · Simple types · Typed de Bruijn variables of the simply typed lambda calculus

Used byThe CPS translation commutes with instantiation by a value or variable · Plotkin's simulation theorem, big-step form · Simulation for terms evaluating to an abstraction · The CPS translation commutes with substitution of values and variables · The value translation preserves values

TheoremThe CPS translation commutes with substitution of values and variables#✓fully proved

Fix an answer type \(R\) and write \(\llbracket \cdot \rrbracket\) for the call-by-value CPS translation of types, contexts (entrywise) and terms; for a variable \(x\) of \(\Gamma\), \(\llbracket x \rrbracket\) is the variable of \(\llbracket \Gamma \rrbracket\) at the same position. Let \(\sigma\) be a substitution from \(\Gamma\) to \(\Delta\) and \(\tau\) a substitution from \(\llbracket \Gamma \rrbracket\) to \(\llbracket \Delta \rrbracket\) such that for every variable \(x\) of \(\Gamma\), the term \(\tau(\llbracket x \rrbracket)\) is related to \(\sigma(x)\) by the value translation \(\Psi\) (a variable is related to the corresponding variable, \(\lambda y. N\) to \(\lambda y. \llbracket N \rrbracket\)). Then for every term \(M\) in \(\Gamma\), writing \(M[\sigma]\) for the result of applying \(\sigma\) to \(M\), we have \(\llbracket M[\sigma] \rrbracket = \llbracket M \rrbracket[\tau]\).

theorem cps_subst (t : Tm Γ A) {σ : Sub Γ Δ} {τ : Sub (Γ.map (cpsTy R)) (Δ.map (cpsTy R))}
    (hτ : ∀ {B} (x : Var Γ B), PsiRel (R := R) (σ x) (τ (cpsVar R x))) :
    cps R (Tm.subst σ t) = Tm.subst τ (cps R t)

Uses 19 · Used by 1

Statement usesPlotkin's value translation \(\Psi\) · CPS computation type · Call-by-value CPS translation of terms · Call-by-value CPS translation of types · CPS translation of variables · Simultaneous substitutions of simply typed contexts · Intrinsically typed terms of the simply typed lambda calculus · Simultaneous substitution (simply typed lambda calculus) · Simple types · Typed de Bruijn variables of the simply typed lambda calculus

Proof usesTranslated renaming · The call-by-value CPS translation commutes with renaming · Renamings of simply typed contexts · Lifting a substitution under a binder (simply typed lambda calculus) · Renaming a simply typed term · Lifted substitution commutes with weakening for intrinsically typed STLC terms · Weakening a simply typed term · Identity renaming of a simply typed context · Lifting a renaming under a binder

Used byThe CPS translation commutes with instantiation by a value or variable

TheoremThe CPS translation commutes with instantiation by a value or variable#✓fully proved

Fix an answer type \(R\) and write \(\llbracket \cdot \rrbracket\) for the call-by-value CPS translation of types, contexts (entrywise) and terms. Let \(N\) be a term of type \(B\) in a context \(A, \Gamma\), let \(v\) be a term of type \(A\) in \(\Gamma\), and let \(p\) be a term of type \(\llbracket A \rrbracket\) in \(\llbracket \Gamma \rrbracket\) related to \(v\) by the value translation \(\Psi\) (a variable is related to the corresponding variable, \(\lambda x. M\) to \(\lambda x. \llbracket M \rrbracket\)). Writing \(N[u]\) for \(N\) with its newest free variable replaced by \(u\), we have \(\llbracket N[v] \rrbracket = \llbracket N \rrbracket[p]\).

theorem cps_instantiate (body : Tm (A :: Γ) B) {v : Tm Γ A}
    {p : Tm (Γ.map (cpsTy R)) (cpsTy R A)} (h : PsiRel (R := R) v p) :
    cps R (Tm.instantiate body v) = Tm.instantiate (cps R body) p

Uses 11 · Used by 1

Statement usesPlotkin's value translation \(\Psi\) · CPS computation type · Call-by-value CPS translation of terms · Call-by-value CPS translation of types · Intrinsically typed terms of the simply typed lambda calculus · Instantiating a binder body (simply typed lambda calculus) · Simple types

Proof usesCPS translation of variables · The CPS translation commutes with substitution of values and variables · Single-variable substitution (simply typed lambda calculus) · Typed de Bruijn variables of the simply typed lambda calculus

Used byPlotkin's simulation theorem, big-step form

TheoremThe value translation preserves values#✓fully proved

Fix an answer type \(R\). If a term \(v\) of type \(A\) in context \(\Gamma\) is related by Plotkin's value translation \(\Psi\) to a term \(p\) (of the translated type in the translated context), and \(v\) is a value, that is, a \(\lambda\)-abstraction, then \(p\) is a value.

theorem PsiRel.value {v : Tm Γ A} {p : Tm (Γ.map (cpsTy R)) (cpsTy R A)}
    (h : PsiRel (R := R) v p) (hv : Value v) : Value p

Uses 8 · Used by 1

Statement usesPlotkin's value translation \(\Psi\) · Call-by-value CPS translation of types · Intrinsically typed terms of the simply typed lambda calculus · Simple types · Values of STLC

Proof usesCall-by-value CPS translation of terms · CPS translation of variables · Typed de Bruijn variables of the simply typed lambda calculus

Used byPlotkin's simulation theorem, big-step form

TheoremA β-redex with a value argument evaluates as its contractum#✓fully proved

Let \(N\) be a term of type \(D\) in a context \(C, \Xi\) and let \(v\) be a value of type \(C\) in \(\Xi\). Writing \(N[v]\) for \(N\) with its newest free variable replaced by \(v\), for every term \(w\) of type \(D\) the application \((\lambda x. N)\, v\) evaluates to \(w\) under call-by-value big-step evaluation if and only if \(N[v]\) evaluates to \(w\).

theorem eval_app_lam_iff {body : Tm (C :: Ξ) D} {v : Tm Ξ C} (hv : Value v) {w : Tm Ξ D} :
    Eval (.app (.lam body) v) w ↔ Eval (Tm.instantiate body v) w

Uses 8 · Used by 3

Statement usesBig-step call-by-value evaluation in the simply typed lambda calculus · Intrinsically typed terms of the simply typed lambda calculus · Instantiating a binder body (simply typed lambda calculus) · Simple types · Values of STLC

Proof usesDeterminism of big-step evaluation in the simply typed lambda calculus · Values evaluate to themselves · Typed de Bruijn variables of the simply typed lambda calculus

Used byCall-by-name evaluation is preserved by the CPS translation · Plotkin's simulation theorem, big-step form · The translation of an abstraction passes the translated function to its continuation

TheoremEvaluation of an application depends on the function only through its results#✓fully proved

Let \(F\) and \(F'\) be terms of type \(C \to D\) in a context \(\Xi\) such that, for every term \(u\), \(F\) evaluates to \(u\) under call-by-value big-step evaluation if and only if \(F'\) does. Then for every term \(a\) of type \(C\) and every term \(w\) of type \(D\) in \(\Xi\), the application \(F\, a\) evaluates to \(w\) if and only if \(F'\, a\) evaluates to \(w\).

theorem eval_app_congr_fun {F F' : Tm Ξ (C ⇒ D)} (h : ∀ u, Eval F u ↔ Eval F' u)
    {a : Tm Ξ C} {w : Tm Ξ D} : Eval (.app F a) w ↔ Eval (.app F' a) w

Uses 5 · Used by 2

Statement usesBig-step call-by-value evaluation in the simply typed lambda calculus · Intrinsically typed terms of the simply typed lambda calculus · Simple types

Proof usesInstantiating a binder body (simply typed lambda calculus) · Typed de Bruijn variables of the simply typed lambda calculus

Used byCall-by-name evaluation is preserved by the CPS translation · Plotkin's simulation theorem, big-step form

TheoremInstantiating a return to the continuation#✓fully proved

Let \(V\) be a term of type \(X\) and \(K\) a term of type \(X \to Z\) in a context \(\Xi\). In the context \(X \to Z, \Xi\), let \(k\) be the newest variable (of type \(X \to Z\)) and \(V'\) the weakening of \(V\). Replacing \(k\) by \(K\) in the term \(k\, V'\) gives \(K\, V\).

theorem instantiate_ret (V : Tm Ξ X) (K : Tm Ξ (X ⇒ Z)) :
    Tm.instantiate (.app (.var .zero) (Tm.weaken V)) K = .app K V

Uses 8 · Used by 2

Statement usesIntrinsically typed terms of the simply typed lambda calculus · Instantiating a binder body (simply typed lambda calculus) · Weakening a simply typed term · Simple types · Typed de Bruijn variables of the simply typed lambda calculus

Proof usesSingle-variable substitution (simply typed lambda calculus) · Simultaneous substitution (simply typed lambda calculus) · Single substitution cancels weakening

Used byPlotkin's simulation theorem, big-step form · The translation of an abstraction passes the translated function to its continuation

TheoremPlotkin's simulation theorem, big-step form#✓fully proved

Fix an answer type \(R\) and write \(\llbracket \cdot \rrbracket\) for the call-by-value CPS translation of types, contexts (entrywise) and terms. If a term \(M\) of type \(A\) in a context \(\Gamma\) evaluates to \(V\) under call-by-value big-step evaluation, then there is a term \(p\) related to \(V\) by the value translation \(\Psi\) (a variable is related to the corresponding variable, \(\lambda x. N\) to \(\lambda x. \llbracket N \rrbracket\)) such that for every value \(K\) of type \(\llbracket A \rrbracket \to R\) in \(\llbracket \Gamma \rrbracket\) and every term \(w\), the application \(\llbracket M \rrbracket\, K\) evaluates to \(w\) if and only if \(K\, p\) evaluates to \(w\).

theorem cps_simulation {M V : Tm Γ A} (h : Eval M V) :
    ∃ p, PsiRel (R := R) V p ∧ ∀ (K : Tm (Γ.map (cpsTy R)) (cpsTy R A ⇒ R)), Value K →
      ∀ w, (Eval (.app (cps R M) K) w ↔ Eval (.app K p) w)

Uses 23 · Used by 1

Statement usesPlotkin's value translation \(\Psi\) · Call-by-value CPS translation of terms · Call-by-value CPS translation of types · Big-step call-by-value evaluation in the simply typed lambda calculus · Intrinsically typed terms of the simply typed lambda calculus · Simple types · Values of STLC

Proof usesThe value translation preserves values · CPS computation type · CPS translation of variables · The CPS translation commutes with instantiation by a value or variable · Evaluation of an application depends on the function only through its results · A β-redex with a value argument evaluates as its contractum · Instantiating a return to the continuation · Big-step evaluation produces values · Lifting a substitution under a binder (simply typed lambda calculus) · Single-variable substitution (simply typed lambda calculus) · Instantiating a binder body (simply typed lambda calculus) · Simultaneous substitution (simply typed lambda calculus) · Lifted substitution commutes with weakening for intrinsically typed STLC terms · Single substitution cancels weakening · Weakening a simply typed term · Typed de Bruijn variables of the simply typed lambda calculus

Used bySimulation for terms evaluating to an abstraction

TheoremSimulation for terms evaluating to an abstraction#✓fully proved

Fix an answer type \(R\) and write \(\llbracket \cdot \rrbracket\) for the call-by-value CPS translation of types, contexts (entrywise) and terms. If a term \(M\) of type \(A \to B\) in a context \(\Gamma\) evaluates to \(\lambda x. N\) under call-by-value big-step evaluation, then for every value \(K\) of type \(\llbracket A \to B \rrbracket \to R\) in \(\llbracket \Gamma \rrbracket\) and every term \(w\) of type \(R\), the application \(\llbracket M \rrbracket\, K\) evaluates to \(w\) if and only if \(K\, (\lambda x. \llbracket N \rrbracket)\) evaluates to \(w\).

theorem cps_simulation_lam {M : Tm Γ (A ⇒ B)} {body : Tm (A :: Γ) B} (h : Eval M (.lam body))
    (K : Tm (Γ.map (cpsTy R)) (cpsTy R (A ⇒ B) ⇒ R)) (hK : Value K) (w : Tm _ R) :
    Eval (.app (cps R M) K) w ↔ Eval (.app K (.lam (cps R body))) w

Uses 10

Statement usesCall-by-value CPS translation of terms · Call-by-value CPS translation of types · Big-step call-by-value evaluation in the simply typed lambda calculus · Intrinsically typed terms of the simply typed lambda calculus · Simple types · Values of STLC

Proof usesPlotkin's value translation \(\Psi\) · CPS translation of variables · Plotkin's simulation theorem, big-step form · Typed de Bruijn variables of the simply typed lambda calculus

InductiveCall-by-name big-step evaluation#✓fully proved

Call-by-name big-step evaluation \(M \Downarrow_n V\) of the simply typed \(\lambda\)-calculus relates two terms of the same type in the same context \(\Gamma\). It is the least relation closed under two rules: every abstraction \(\lambda x.\,N\) evaluates to itself, and if \(f \Downarrow_n \lambda x.\,N\) and \(N[a/x] \Downarrow_n v\), then \(f\,a \Downarrow_n v\). The argument \(a\) is substituted for \(x\) without being evaluated.

inductive EvalN {Γ : List (Ty Base)} : {A : Ty Base} → Tm Γ A → Tm Γ A → Prop
  | lam {A B : Ty Base} (body : Tm (A :: Γ) B) : EvalN (.lam body) (.lam body)
  | app {A B : Ty Base} {f : Tm Γ (A ⇒ B)} {a : Tm Γ A} {body : Tm (A :: Γ) B}
      {v : Tm Γ B} (hf : EvalN f (.lam body)) (hb : EvalN (Tm.instantiate body a) v) :
      EvalN (.app f a) v

Uses 3 · Used by 2

Statement usesIntrinsically typed terms of the simply typed lambda calculus · Instantiating a binder body (simply typed lambda calculus) · Simple types

Used byCall-by-name evaluation is preserved by the CPS translation · Plotkin's simulation theorem for the call-by-name CPS translation

DefinitionThe call-by-name CPS translation of a renaming#✓fully proved

Fix an answer type \(R\). The translation of a context \(\Gamma\) replaces each type \(A\) in it by the computation type \((A^* \to R) \to R\), where \(A^*\) is the call-by-name translation of \(A\), and a variable \(x\) of \(\Gamma\) becomes the variable \(\overline{x}\) at the same position of the translated context. A renaming \(\rho\) from \(\Gamma\) to \(\Delta\), a type-preserving map from the variables of \(\Gamma\) to those of \(\Delta\), is transported to the renaming \(\overline{\rho}\) of the translated contexts with \(\overline{\rho}(\overline{x}) = \overline{\rho(x)}\) for every variable \(x\) of \(\Gamma\).

def cbnRen : {Γ Δ : List (Ty Base)} → Ren Γ Δ →
    Ren (Γ.map (cbnComp R)) (Δ.map (cbnComp R))
  | [], _, _, _, x => nomatch x
  | _ :: _, _, ρ, _, .zero => cbnVar R (ρ .zero)
  | _ :: _, _, ρ, _, .succ y => cbnRen (fun x => ρ (.succ x)) y

Uses 6 · Used by 2

Statement usesComputation types of the call-by-name CPS translation · Call-by-name CPS translation of types · Call-by-name CPS translation of variables · Renamings of simply typed contexts · Simple types · Typed de Bruijn variables of the simply typed lambda calculus

Used byThe call-by-name CPS translation commutes with renaming · The call-by-name CPS translation commutes with weakening

TheoremThe call-by-name CPS translation commutes with renaming#✓fully proved

Fix an answer type \(R\) and write \(\overline{t}\) for the call-by-name CPS translation of a term \(t\). For a renaming \(\rho\) from a context \(\Gamma\) to a context \(\Delta\), let \(\overline{\rho}\) be the renaming of the translated contexts that sends the translation of each variable \(x\) of \(\Gamma\) to the translation of \(\rho(x)\). Then for every term \(t\) in context \(\Gamma\), the translation of the renamed term \(t[\rho]\) is the renaming of \(\overline{t}\) by \(\overline{\rho}\): \(\overline{t[\rho]} = \overline{t}[\overline{\rho}]\).

theorem cbn_rename (ρ : Ren Γ Δ) (t : Tm Γ A) :
    cbn R (Tm.rename ρ t) = Tm.rename (cbnRen R ρ) (cbn R t)

Uses 13 · Used by 1

Statement usesCall-by-name CPS translation of terms · Computation types of the call-by-name CPS translation · The call-by-name CPS translation of a renaming · Renamings of simply typed contexts · Intrinsically typed terms of the simply typed lambda calculus · Renaming a simply typed term · Simple types

Proof usesCall-by-name CPS translation of types · Call-by-name CPS translation of variables · Renaming commutes with weakening for intrinsically typed STLC terms · Weakening a simply typed term · Typed de Bruijn variables of the simply typed lambda calculus · Lifting a renaming under a binder

Used byThe call-by-name CPS translation commutes with weakening

TheoremThe call-by-name CPS translation commutes with weakening#✓fully proved

Fix an answer type \(R\) and write \(\overline{t}\) for the call-by-name CPS translation of a term \(t\). For every term \(t\) in a context \(\Gamma\) and every type \(B\), translating the weakening of \(t\) to the context \(B, \Gamma\) (which adds a fresh newest variable of type \(B\)) gives the weakening of \(\overline{t}\) to the translated context, which adds a fresh newest variable of the translated type \((B^* \to R) \to R\), where \(B^*\) is the call-by-name translation of \(B\).

theorem cbn_weaken (t : Tm Γ A) :
    cbn R (Tm.weaken (B := B) t) = Tm.weaken (cbn R t)

Uses 12 · Used by 1

Statement usesCall-by-name CPS translation of terms · Computation types of the call-by-name CPS translation · Intrinsically typed terms of the simply typed lambda calculus · Weakening a simply typed term · Simple types

Proof usesThe call-by-name CPS translation of a renaming · The call-by-name CPS translation commutes with renaming · Renamings of simply typed contexts · Renaming a simply typed term · Typed de Bruijn variables of the simply typed lambda calculus · Identity renaming of a simply typed context · Lifting a renaming under a binder

Used byThe call-by-name CPS translation commutes with substitution

TheoremThe call-by-name CPS translation commutes with substitution#✓fully proved

Fix an answer type \(R\) and write \(\overline{t}\) for the call-by-name CPS translation of a term \(t\) and \(\overline{x}\) for the translation of a variable \(x\), the variable at the same position of the translated context. Let \(\sigma\) be a substitution from a context \(\Gamma\) to a context \(\Delta\) (assigning to each variable of \(\Gamma\) a term of the same type in context \(\Delta\)), and let \(\tau\) be a substitution from the translated context of \(\Gamma\) to that of \(\Delta\) such that \(\tau(\overline{x}) = \overline{\sigma(x)}\) for every variable \(x\) of \(\Gamma\). Then for every term \(t\) in context \(\Gamma\), \(\overline{t[\sigma]} = \overline{t}[\tau]\).

theorem cbn_subst (t : Tm Γ A) {σ : Sub Γ Δ}
    {τ : Sub (Γ.map (cbnComp R)) (Δ.map (cbnComp R))}
    (hτ : ∀ {B} (x : Var Γ B), τ (cbnVar R x) = cbn R (σ x)) :
    cbn R (Tm.subst σ t) = Tm.subst τ (cbn R t)

Uses 13 · Used by 1

Statement usesCall-by-name CPS translation of terms · Computation types of the call-by-name CPS translation · Call-by-name CPS translation of variables · Simultaneous substitutions of simply typed contexts · Intrinsically typed terms of the simply typed lambda calculus · Simultaneous substitution (simply typed lambda calculus) · Simple types · Typed de Bruijn variables of the simply typed lambda calculus

Proof usesCall-by-name CPS translation of types · The call-by-name CPS translation commutes with weakening · Lifting a substitution under a binder (simply typed lambda calculus) · Lifted substitution commutes with weakening for intrinsically typed STLC terms · Weakening a simply typed term

Used byThe call-by-name CPS translation commutes with instantiation

TheoremThe call-by-name CPS translation commutes with instantiation#✓fully proved

Fix an answer type \(R\) and write \(\overline{t}\) for the call-by-name CPS translation of a term \(t\). Let \(N\) be a term of type \(B\) in a context \(A, \Gamma\) whose newest variable \(x\) has type \(A\), and let \(a\) be a term of type \(A\) in context \(\Gamma\). Then translating the instantiation \(N[a/x]\) of \(x\) by \(a\) gives the instantiation of the newest variable of \(\overline{N}\) by \(\overline{a}\): \(\overline{N[a/x]} = \overline{N}[\overline{a}/x]\).

theorem cbn_instantiate (body : Tm (A :: Γ) B) (a : Tm Γ A) :
    cbn R (Tm.instantiate body a) = Tm.instantiate (cbn R body) (cbn R a)

Uses 9 · Used by 1

Statement usesCall-by-name CPS translation of terms · Computation types of the call-by-name CPS translation · Intrinsically typed terms of the simply typed lambda calculus · Instantiating a binder body (simply typed lambda calculus) · Simple types

Proof usesCall-by-name CPS translation of variables · The call-by-name CPS translation commutes with substitution · Single-variable substitution (simply typed lambda calculus) · Typed de Bruijn variables of the simply typed lambda calculus

Used byCall-by-name evaluation is preserved by the CPS translation

TheoremThe translation of a closed term is a value#✓fully proved

Fix an answer type \(R\). For every closed term \(t\), the call-by-name CPS translation of \(t\) is a value, that is, a \(\lambda\)-abstraction.

theorem cbn_value : (t : Tm [] A) → Value (cbn R t)

Uses 8 · Used by 1

Statement usesCall-by-name CPS translation of terms · Computation types of the call-by-name CPS translation · Intrinsically typed terms of the simply typed lambda calculus · Simple types · Values of STLC

Proof usesCall-by-name CPS translation of types · Weakening a simply typed term · Typed de Bruijn variables of the simply typed lambda calculus

Used byCall-by-name evaluation is preserved by the CPS translation

TheoremAdministrative step of the call-by-name translation of an application#✓fully proved

Let \(\Xi\) be a context and \(W\), \(V\), \(Z\) types, and write \(t^{\uparrow}\) for the weakening of a term \(t\) by one new newest variable. Let \(F\) be a term of type \(((W \Rightarrow ((V \Rightarrow Z) \Rightarrow Z)) \Rightarrow Z) \Rightarrow Z\), \(N\) a term of type \(W\) and \(K\) a term of type \(V \Rightarrow Z\), all in context \(\Xi\). In the context \(\Xi\) extended by a newest variable \(k\) of type \(V \Rightarrow Z\), consider the term \(F^{\uparrow}\,(\lambda p.\; p\; N^{\uparrow\uparrow}\; k)\). Here \(p\) is the bound variable, of type \(W \Rightarrow ((V \Rightarrow Z) \Rightarrow Z)\), with de Bruijn index \(0\), and \(k\) has index \(1\) under the binder. Instantiating \(k\) with \(K\) in this term gives \(F\,(\lambda p.\; p\; N^{\uparrow}\; K^{\uparrow})\).

theorem instantiate_cbnApp₁ (F : Tm Ξ (((W ⇒ ((V ⇒ Z) ⇒ Z)) ⇒ Z) ⇒ Z)) (N : Tm Ξ W)
    (K : Tm Ξ (V ⇒ Z)) :
    Tm.instantiate (.app (Tm.weaken F)
        (.lam (.app (.app (.var .zero) (Tm.weaken (Tm.weaken N))) (.var (.succ .zero))))) K =
      .app F (.lam (.app (.app (.var .zero) (Tm.weaken N)) (Tm.weaken K)))

Uses 10 · Used by 1

Statement usesIntrinsically typed terms of the simply typed lambda calculus · Instantiating a binder body (simply typed lambda calculus) · Weakening a simply typed term · Simple types · Typed de Bruijn variables of the simply typed lambda calculus

Proof usesLifting a substitution under a binder (simply typed lambda calculus) · Single-variable substitution (simply typed lambda calculus) · Simultaneous substitution (simply typed lambda calculus) · Lifted substitution commutes with weakening for intrinsically typed STLC terms · Single substitution cancels weakening

Used byCall-by-name evaluation is preserved by the CPS translation

TheoremThe translation of an abstraction passes the translated function to its continuation#✓fully proved

Fix an answer type \(R\), and write \(\overline{t}\) for the call-by-name CPS translation of a term \(t\), \(T^*\) for the translation of a type \(T\), and \(\Gamma^*\) for the context obtained from \(\Gamma\) by replacing each type \(C\) with \((C^* \to R) \to R\). Let \(N\) be a term of type \(B\) in context \(A, \Gamma\), let \(K\) be a value of type \((A \to B)^* \to R\) in context \(\Gamma^*\), and let \(w\) be a term of type \(R\) in context \(\Gamma^*\). Then \(\overline{\lambda x.\,N}\,K\) evaluates to \(w\) under call-by-value big-step evaluation if and only if \(K\,(\lambda x.\,\overline{N})\) does.

theorem eval_cbn_lam_iff (body : Tm (A :: Γ) B)
    {K : Tm (Γ.map (cbnComp R)) (cbnTy R (A ⇒ B) ⇒ R)} (hK : Value K) (w : Tm _ R) :
    Eval (.app (cbn R (.lam body)) K) w ↔ Eval (.app K (.lam (cbn R body))) w

Uses 12 · Used by 2

Statement usesCall-by-name CPS translation of terms · Computation types of the call-by-name CPS translation · Call-by-name CPS translation of types · Big-step call-by-value evaluation in the simply typed lambda calculus · Intrinsically typed terms of the simply typed lambda calculus · Simple types · Values of STLC

Proof usesA β-redex with a value argument evaluates as its contractum · Instantiating a return to the continuation · Instantiating a binder body (simply typed lambda calculus) · Weakening a simply typed term · Typed de Bruijn variables of the simply typed lambda calculus

Used byCall-by-name evaluation is preserved by the CPS translation · Plotkin's simulation theorem for the call-by-name CPS translation

TheoremCall-by-name evaluation is preserved by the CPS translation#✓fully proved

Fix an answer type \(R\), and write \(\overline{M}\) for the call-by-name CPS translation of a term \(M\) and \(T^*\) for the translation of a type \(T\). Let \(M\) and \(V\) be closed terms of type \(T\) such that \(M\) evaluates to \(V\) under call-by-name big-step evaluation. Then for every closed value \(K\) of type \(T^* \to R\) and every closed term \(w\) of type \(R\), the application \(\overline{M}\,K\) evaluates to \(w\) under call-by-value big-step evaluation if and only if \(\overline{V}\,K\) does.

theorem cbn_evalN {T : Ty Base} {M V : Tm [] T} (h : EvalN M V)
    (K : Tm ([].map (cbnComp R)) (cbnTy R T ⇒ R)) (hK : Value K) (w : Tm [] R) :
    Eval (.app (cbn R M) K) w ↔ Eval (.app (cbn R V) K) w

Uses 20 · Used by 1

Statement usesCall-by-name big-step evaluation · Call-by-name CPS translation of terms · Computation types of the call-by-name CPS translation · Call-by-name CPS translation of types · Big-step call-by-value evaluation in the simply typed lambda calculus · Intrinsically typed terms of the simply typed lambda calculus · Simple types · Values of STLC

Proof usesThe call-by-name CPS translation commutes with instantiation · The translation of a closed term is a value · Evaluation of an application depends on the function only through its results · A β-redex with a value argument evaluates as its contractum · The translation of an abstraction passes the translated function to its continuation · Administrative step of the call-by-name translation of an application · Single-variable substitution (simply typed lambda calculus) · Instantiating a binder body (simply typed lambda calculus) · Simultaneous substitution (simply typed lambda calculus) · Single substitution cancels weakening · Weakening a simply typed term · Typed de Bruijn variables of the simply typed lambda calculus

Used byPlotkin's simulation theorem for the call-by-name CPS translation

TheoremPlotkin's simulation theorem for the call-by-name CPS translation#✓fully proved

Fix an answer type \(R\), and write \(\overline{M}\) for the call-by-name CPS translation of a term \(M\) and \(T^*\) for the translation of a type \(T\). Let \(M\) be a closed term of type \(A \to B\) that evaluates to \(\lambda x.\,N\) under call-by-name big-step evaluation. Then for every closed value \(K\) of type \((A \to B)^* \to R\) and every closed term \(w\) of type \(R\), the application \(\overline{M}\,K\) evaluates to \(w\) under call-by-value big-step evaluation if and only if \(K\,(\lambda x.\,\overline{N})\) does.

This is the big-step form of the theorem, for the simply typed calculus.

theorem cbn_simulation {M : Tm [] (A ⇒ B)} {body : Tm [A] B} (h : EvalN M (.lam body))
    (K : Tm ([].map (cbnComp R)) (cbnTy R (A ⇒ B) ⇒ R)) (hK : Value K) (w : Tm [] R) :
    Eval (.app (cbn R M) K) w ↔ Eval (.app K (.lam (cbn R body))) w

Uses 10

Statement usesCall-by-name big-step evaluation · Call-by-name CPS translation of terms · Computation types of the call-by-name CPS translation · Call-by-name CPS translation of types · Big-step call-by-value evaluation in the simply typed lambda calculus · Intrinsically typed terms of the simply typed lambda calculus · Simple types · Values of STLC

Proof usesCall-by-name evaluation is preserved by the CPS translation · The translation of an abstraction passes the translated function to its continuation

42 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.