Operational semantics of the simply typed lambda calculus

InductiveValues of STLC#✓fully proved

A term of type \(A\) in a context \(\Gamma\) is a value exactly when it is a lambda abstraction.

inductive Value {Base : Type u} : {Γ : List (Ty Base)} → {A : Ty Base} → Tm Γ A → Prop where
  | lam {A B : Ty Base} {Γ : List (Ty Base)} (body : Tm (A :: Γ) B) : Value (.lam body)

Uses 2 · Used by 42

Statement usesIntrinsically typed terms of the 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 · The translation of a closed term is a value · Plotkin's simulation theorem, big-step form · Simulation for terms evaluating to an abstraction · A β-redex with a value argument evaluates as its contractum · The translation of an abstraction passes the translated function to its continuation · The value translation preserves values · One reduction step preserves STLC denotation · Termination is closed under backward evaluation · Application preserves having the same result · Evaluating the argument of a value function is a multi-step congruence · Closed functions evaluate to lambda abstractions · Values reduce only to themselves · Termination is closed under forward evaluation · Fundamental theorem of the reducibility relation · Normalization and termination coincide · No closed terms of base type · Uniqueness of normal forms · Evaluation preserves the result of a closed term · Values terminate · Reflexivity of having the same result · Closed terms with the same result · Evaluation to a value passes through every reduct · Symmetry of having the same result · Termination of closed terms · Transitivity of having the same result · Uniqueness of the value reached by evaluation · Big-step evaluation is closed under backward reduction steps · Canonical forms for closed function values · Closed normal forms are exactly the values · Small-step call-by-value reduction in STLC is deterministic · Closed simply typed terms have a big-step evaluation · Big-step evaluation is small-step evaluation to a value · Small-step evaluation to a value implies big-step evaluation · Progress for closed STLC terms · Small-step call-by-value reduction in STLC · Termination in terms of big-step evaluation · Big-step evaluation implies small-step evaluation · Big-step evaluation produces values · Values are irreducible · Values evaluate to themselves

InductiveSmall-step call-by-value reduction in STLC#✓fully proved

One-step reduction on terms of type \(A\) in a context \(\Gamma\) is the least relation closed under three left-to-right call-by-value rules: if \(f\) reduces to \(f'\), then the application \(f\,a\) reduces to \(f'\,a\); if \(f\) is a value and \(a\) reduces to \(a'\), then \(f\,a\) reduces to \(f\,a'\); and if \(a\) is a value, then the application of the abstraction of \(b\) to \(a\) reduces to \(b[a]\), the result of substituting \(a\) for the newest free variable of \(b\).

inductive Step {Base : Type u} : {Γ : List (Ty Base)} → {A : Ty Base} →
    Tm Γ A → Tm Γ A → Prop where
  | appFun {A B : Ty Base} {Γ : List (Ty Base)} {f f' : Tm Γ (A ⇒ B)} {a : Tm Γ A} :
      Step f f' → Step (.app f a) (.app f' a)
  | appArg {A B : Ty Base} {Γ : List (Ty Base)} {f : Tm Γ (A ⇒ B)} {a a' : Tm Γ A} :
      Value f → Step a a' → Step (.app f a) (.app f a')
  | beta {A B : Ty Base} {Γ : List (Ty Base)} {body : Tm (A :: Γ) B} {a : Tm Γ A} :
      Value a → Step (.app (.lam body) a) (Tm.instantiate body a)

Uses 4 · Used by 21

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

Used byOne reduction step preserves STLC denotation · Multi-step reduction preserves STLC denotation · Single-step evaluation is a semantic equation · Termination is closed under backward evaluation · Application preserves having the same result · Evaluating the argument of a value function is a multi-step congruence · Multi-step evaluation is a congruence in function position · Values reduce only to themselves · Fundamental theorem of the reducibility relation · Evaluation preserves the result of a closed term · Values terminate · Evaluation to a value passes through every reduct · Big-step evaluation is closed under backward reduction steps · Big-step evaluation is closed under backward multi-step reduction · Closed normal forms are exactly the values · Small-step call-by-value reduction in STLC is deterministic · Normal forms for call-by-value reduction in STLC · Progress for closed STLC terms · Multi-step call-by-value reduction in STLC · Big-step evaluation implies small-step evaluation · Values are irreducible

TheoremValues are irreducible#✓fully proved

If a term \(t\) of type \(A\) in a context \(\Gamma\) is a value, then there is no term \(t'\) to which \(t\) reduces in one call-by-value step.

theorem value_irreducible {t t' : Tm Γ A} (hv : Value t) : ¬ t ⟶ₛ t'

Uses 6 · Used by 4

Statement usesSmall-step call-by-value reduction in STLC · Intrinsically typed terms of the simply typed lambda calculus · Simple types · Values of STLC

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

Used byValues reduce only to themselves · Evaluation to a value passes through every reduct · Closed normal forms are exactly the values · Small-step call-by-value reduction in STLC is deterministic

TheoremCanonical forms for closed function values#✓fully proved

If a term \(f\) of function type \(A \Rightarrow B\) in the empty context is a value, then \(f\) is a lambda abstraction: there is a term \(b\) of type \(B\) in the one-variable context \([A]\) such that \(f\) is the abstraction of \(b\).

theorem closed_function_value_is_lam {f : Tm [] (A ⇒ B)} (hv : Value f) :
    ∃ body : Tm [A] B, f = .lam body

Uses 3 · Used by 3

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

Used byApplication preserves having the same result · Closed functions evaluate to lambda abstractions · Progress for closed STLC terms

TheoremProgress for closed STLC terms#✓fully proved

Every term \(t\) of type \(A\) in the empty context is either a value or reduces in one call-by-value step to some term \(t'\).

theorem progress : {A : Ty Base} → (t : Tm [] A) → Value t ∨ ∃ t', t ⟶ₛ t'

Uses 7 · Used by 1

Statement usesSmall-step call-by-value reduction in STLC · Intrinsically typed terms of the simply typed lambda calculus · Simple types · Values of STLC

Proof usesCanonical forms for closed function values · Instantiating a binder body (simply typed lambda calculus) · Typed de Bruijn variables of the simply typed lambda calculus

Used byClosed normal forms are exactly the values

TheoremSmall-step call-by-value reduction in STLC is deterministic#✓fully proved

For terms \(t\), \(t_1\), \(t_2\) of type \(A\) in a context \(\Gamma\), if \(t\) reduces in one call-by-value step both to \(t_1\) and to \(t_2\), then \(t_1 = t_2\).

theorem deterministic {t t₁ t₂ : Tm Γ A} (h₁ : t ⟶ₛ t₁) (h₂ : t ⟶ₛ t₂) : t₁ = t₂

Uses 7 · Used by 1

Statement usesSmall-step call-by-value reduction in STLC · Intrinsically typed terms of the simply typed lambda calculus · Simple types

Proof usesValues are irreducible · Instantiating a binder body (simply typed lambda calculus) · Values of STLC · Typed de Bruijn variables of the simply typed lambda calculus

Used byEvaluation to a value passes through every reduct

DefinitionNormal forms for call-by-value reduction in STLC#✓fully proved

A term \(t\) of type \(A\) in a context \(\Gamma\) is in normal form when there is no term \(t'\) such that \(t\) reduces to \(t'\) in one call-by-value step.

def NormalForm (t : Tm Γ A) : Prop := ∀ t', ¬t ⟶ₛ t'

Uses 3 · Used by 4

Statement usesSmall-step call-by-value reduction in STLC · Intrinsically typed terms of the simply typed lambda calculus · Simple types

Used byNormalization and termination coincide · Uniqueness of normal forms · Normalizing closed terms · Closed normal forms are exactly the values

TheoremClosed normal forms are exactly the values#✓fully proved

A term \(t\) of type \(A\) in the empty context is in normal form, that is, has no call-by-value reduction step, if and only if it is a value.

theorem closed_normalForm_iff_value (t : Tm [] A) : NormalForm t ↔ Value t

Uses 7 · Used by 2

Statement usesNormal forms for call-by-value reduction in STLC · Intrinsically typed terms of the simply typed lambda calculus · Simple types · Values of STLC

Proof usesSmall-step call-by-value reduction in STLC · Progress for closed STLC terms · Values are irreducible

Used byNormalization and termination coincide · Uniqueness of normal forms

AbbreviationMulti-step call-by-value reduction in STLC#✓fully proved

For terms of type \(A\) in a context \(\Gamma\), multi-step reduction is the reflexive transitive closure of one-step call-by-value reduction.

abbrev Steps {Base : Type u} {Γ : List (Ty Base)} {A : Ty Base} :=
  Relation.ReflTransGen (@Step Base Γ A)

Uses 3 · Used by 34

Statement usesSmall-step call-by-value reduction in STLC · Intrinsically typed terms of the simply typed lambda calculus · Simple types

Used byMulti-step reduction preserves STLC denotation · Multi-step evaluation is a semantic equation · Termination is closed under backward evaluation · Reducibility is closed under backward evaluation · Left expansion preserves having the same result · Right expansion preserves having the same result · Application preserves having the same result · Evaluating the argument of a value function is a multi-step congruence · Multi-step evaluation is a congruence in function position · Closed functions evaluate to lambda abstractions · Values reduce only to themselves · Termination is closed under forward evaluation · Reducibility is closed under forward evaluation · Fundamental theorem of the reducibility relation · Reducibility is invariant under evaluation · Normalization and termination coincide · No closed terms of base type · Uniqueness of normal forms · Normalizing closed terms · Evaluation preserves the result of a closed term · Values terminate · Reflexivity of having the same result · Closed terms with the same result · Evaluation to a value passes through every reduct · Symmetry of having the same result · Termination of closed terms · Transitivity of having the same result · Uniqueness of the value reached by evaluation · Big-step evaluation is closed under backward multi-step reduction · Closed simply typed terms have a big-step evaluation · Big-step evaluation is small-step evaluation to a value · Small-step evaluation to a value implies big-step evaluation · Termination in terms of big-step evaluation · Big-step evaluation implies small-step evaluation

InductiveBig-step call-by-value evaluation in the simply typed lambda calculus#✓fully proved

Fix a typing context \(\Gamma\). For terms \(t\) and \(v\) of the same type in context \(\Gamma\), the big-step evaluation relation \(t \Downarrow v\) is the least relation such that every lambda abstraction \(\lambda.\,b\) evaluates to itself, and an application \(f\,a\) evaluates to \(v\) whenever \(f \Downarrow \lambda.\,b\), \(a \Downarrow u\) and \(b[u] \Downarrow v\), where \(b[u]\) is the body \(b\) with its newest free variable replaced by \(u\).

The application rule fixes a left-to-right order: first the function, then the argument, then the instantiated body.

inductive Eval : {A : Ty Base} → Tm Γ A → Tm Γ A → Prop where
  | lam {A B : Ty Base} (body : Tm (A :: Γ) B) : Eval (.lam body) (.lam body)
  | app {A B : Ty Base} {f : Tm Γ (A ⇒ B)} {a : Tm Γ A}
      {body : Tm (A :: Γ) B} {va : Tm Γ A} {v : Tm Γ B} :
      Eval f (.lam body) →
      Eval a va →
      Eval (Tm.instantiate body va) v →
      Eval (.app f a) v

Uses 3 · Used by 18

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 · Plotkin's simulation theorem, big-step form · Simulation for terms evaluating to an abstraction · 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 · Big-step evaluation preserves STLC denotation · Big-step evaluation is closed under backward reduction steps · Big-step evaluation is closed under backward multi-step reduction · Determinism of big-step evaluation in the simply typed lambda calculus · Closed simply typed terms have a big-step evaluation · Big-step evaluation is small-step evaluation to a value · Small-step evaluation to a value implies big-step evaluation · Termination in terms of big-step evaluation · Big-step evaluation implies small-step evaluation · Big-step evaluation produces values · Values evaluate to themselves

TheoremBig-step evaluation produces values#✓fully proved

In the call-by-value simply typed lambda calculus, if a term \(t\) of type \(A\) in context \(\Gamma\) evaluates by big-step evaluation to a term \(v\), written \(t \Downarrow v\), then \(v\) is a value, that is, a lambda abstraction.

theorem value {t v : Tm Γ A} (h : t ⇓ v) : Value v

Uses 5 · Used by 5

Statement usesBig-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 usesInstantiating a binder body (simply typed lambda calculus)

Used byPlotkin's simulation theorem, big-step form · Determinism of big-step evaluation in the simply typed lambda calculus · Big-step evaluation is small-step evaluation to a value · Termination in terms of big-step evaluation · Big-step evaluation implies small-step evaluation

TheoremValues evaluate to themselves#✓fully proved

Every value \(v\), that is, every lambda abstraction, of any type in any typing context evaluates to itself in the big-step semantics: \(v \Downarrow v\).

theorem value_self {v : Tm Γ A} (hv : Value v) : v ⇓ v

Uses 4 · 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 · Simple types · Values of STLC

Used byA β-redex with a value argument evaluates as its contractum · Big-step evaluation is closed under backward reduction steps · Small-step evaluation to a value implies big-step evaluation

TheoremBig-step evaluation implies small-step evaluation#✓fully proved

Let \(t\) and \(v\) be terms of the same type in the same typing context. If \(t\) evaluates to \(v\) in the big-step semantics, written \(t \Downarrow v\), then \(t\) reduces to \(v\) in finitely many (possibly zero) left-to-right call-by-value steps.

theorem to_steps {t v : Tm Γ A} (h : t ⇓ v) : Steps t v

Uses 10 · Used by 4

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

Proof usesBig-step evaluation produces values · Small-step call-by-value reduction in STLC · Evaluating the argument of a value function is a multi-step congruence · Multi-step evaluation is a congruence in function position · Instantiating a binder body (simply typed lambda calculus) · Values of STLC

Used byBig-step evaluation preserves STLC denotation · Determinism of big-step evaluation in the simply typed lambda calculus · Big-step evaluation is small-step evaluation to a value · Termination in terms of big-step evaluation

TheoremBig-step evaluation is closed under backward reduction steps#✓fully proved

Let \(t\), \(t'\) and \(v\) be terms of the same type \(A\) in the same typing context \(\Gamma\). If \(t\) reduces to \(t'\) in one left-to-right call-by-value step and \(t'\) evaluates to \(v\) in the big-step semantics, written \(t' \Downarrow v\), then \(t \Downarrow v\).

theorem anti_step {t t' v : Tm Γ A} (hstep : Step t t') (heval : t' ⇓ v) : t ⇓ v

Uses 8 · Used by 1

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

Proof usesValues evaluate to themselves · Instantiating a binder body (simply typed lambda calculus) · Values of STLC · Typed de Bruijn variables of the simply typed lambda calculus

Used byBig-step evaluation is closed under backward multi-step reduction

TheoremBig-step evaluation is closed under backward multi-step reduction#✓fully proved

Let \(t\), \(t'\) and \(v\) be terms of the same type \(A\) in the same typing context \(\Gamma\). If \(t\) reduces to \(t'\) in finitely many (possibly zero) left-to-right call-by-value steps and \(t'\) evaluates to \(v\) in the big-step semantics, written \(t' \Downarrow v\), then \(t \Downarrow v\).

theorem anti_steps {t t' v : Tm Γ A} (hsteps : Steps t t') (heval : t' ⇓ v) : t ⇓ v

Uses 6 · Used by 1

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

Proof usesBig-step evaluation is closed under backward reduction steps · Small-step call-by-value reduction in STLC

Used bySmall-step evaluation to a value implies big-step evaluation

TheoremSmall-step evaluation to a value implies big-step evaluation#✓fully proved

Let \(t\) and \(v\) be terms of the same type in the same typing context. If \(t\) reduces to \(v\) in finitely many (possibly zero) left-to-right call-by-value steps and \(v\) is a value, then \(t\) evaluates to \(v\) in the big-step semantics, written \(t \Downarrow v\).

theorem of_steps {t v : Tm Γ A} (hsteps : Steps t v) (hv : Value v) : t ⇓ v

Uses 7 · Used by 3

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

Proof usesBig-step evaluation is closed under backward multi-step reduction · Values evaluate to themselves

Used byClosed simply typed terms have a big-step evaluation · Big-step evaluation is small-step evaluation to a value · Termination in terms of big-step evaluation

TheoremBig-step evaluation is small-step evaluation to a value#✓fully proved

For terms \(t\) and \(v\) of the same type in the same typing context, \(t\) evaluates to \(v\) in the big-step semantics, written \(t \Downarrow v\), if and only if \(t\) reduces to \(v\) in finitely many (possibly zero) left-to-right call-by-value steps and \(v\) is a value, that is, a lambda abstraction.

theorem iff_steps_value {t v : Tm Γ A} : t ⇓ v ↔ Steps t v ∧ Value v

Uses 8

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

Proof usesSmall-step evaluation to a value implies big-step evaluation · Big-step evaluation implies small-step evaluation · Big-step evaluation produces values

TheoremDeterminism of big-step evaluation in the simply typed lambda calculus#✓fully proved

For every typing context \(\Gamma\) and type \(A\), if a term \(t\) of type \(A\) in context \(\Gamma\) evaluates in the big-step call-by-value semantics both to \(v\) and to \(w\), written \(t \Downarrow v\) and \(t \Downarrow w\), then \(v = w\).

theorem deterministic {t v w : Tm Γ A} (htv : t ⇓ v) (htw : t ⇓ w) : v = w

Uses 6 · Used by 1

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 usesBig-step evaluation implies small-step evaluation · Big-step evaluation produces values · Uniqueness of the value reached by evaluation

Used byA β-redex with a value argument evaluates as its contractum

TheoremClosed simply typed terms have a big-step evaluation#✓fully proved

For every type \(A\) and every closed term \(t\) of type \(A\), that is, a term in the empty typing context, there is a term \(v\) such that \(t\) evaluates to \(v\) in the big-step call-by-value semantics, written \(t \Downarrow v\).

theorem exists_closed (t : Tm [] A) : ∃ v, t ⇓ v

Uses 8

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 usesSmall-step evaluation to a value implies big-step evaluation · Multi-step call-by-value reduction in STLC · Termination of closed terms · Values of STLC · Termination of the call-by-value simply typed lambda calculus

TheoremTermination in terms of big-step evaluation#✓fully proved

For every closed term \(t\) of type \(A\), that is, a term in the empty typing context, \(t\) terminates (it reduces to a value in finitely many left-to-right call-by-value steps) if and only if there is a term \(v\) such that \(t\) evaluates to \(v\) in the big-step semantics, written \(t \Downarrow v\).

theorem terminates_iff_eval {t : Tm [] A} : Terminates t ↔ ∃ v, t ⇓ v

Uses 9

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

Proof usesSmall-step evaluation to a value implies big-step evaluation · Big-step evaluation implies small-step evaluation · Big-step evaluation produces values · Multi-step call-by-value reduction in STLC · Values of STLC

20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.