Denotational semantics of IMP

11 fully proved

IMP

DefinitionOne-step unfolding functional of a while loop#✓fully proved

Given a Boolean expression \(b\) (the guard) and a binary relation \(B\) on states (the body relation), the functional sends a relation \(R\) on states to the relation that relates \(s\) to \(s'\) exactly when either \(b\) evaluates to false in \(s\) and \(s' = s\), or \(b\) evaluates to true in \(s\) and there is a state \(m\) with \(B\) relating \(s\) to \(m\) and \(R\) relating \(m\) to \(s'\).

def whileFun (guard : BExp) (body : State → State → Prop)
    (R : State → State → Prop) : State → State → Prop :=
  fun s s' => (guard.eval s = false ∧ s' = s) ∨
    (guard.eval s = true ∧ ∃ m, body s m ∧ R m s')

inductive BExp where
  | truth (value : Bool)
  | eq (left right : AExp)
  | le (left right : AExp)
  | not (body : BExp)
  | and (left right : BExp)
  deriving DecidableEq, Repr

CSLibExt/Languages/IMP/Syntax.lean:46

abbrev State := Nat → Nat

CSLibExt/Languages/IMP/Syntax.lean:34

Uses 3 · Used by 6

Statement usesBoolean expressions of IMP · Evaluation of IMP Boolean expressions · IMP program states

Used byDenotational executions are big-step executions · The while denotation is a fixed point · Monotonicity of the while-loop unfolding functional · Unfolding equation for the while denotation · Park induction for while loops · The while-loop functional as a monotone map

TheoremMonotonicity of the while-loop unfolding functional#✓fully proved

Let \(b\) be a Boolean expression, \(B\) a binary relation on states, and \(\Phi\) the one-step unfolding functional of a while loop with guard \(b\) and body relation \(B\). Then \(\Phi\) is monotone for inclusion of relations: for all relations \(R_1\) and \(R_2\) on states with \(R_1 \subseteq R_2\), we have \(\Phi(R_1) \subseteq \Phi(R_2)\).

theorem whileFun_mono {guard : BExp} {body : State → State → Prop} :
    Monotone (whileFun guard body)

inductive BExp where
  | truth (value : Bool)
  | eq (left right : AExp)
  | le (left right : AExp)
  | not (body : BExp)
  | and (left right : BExp)
  deriving DecidableEq, Repr

CSLibExt/Languages/IMP/Syntax.lean:46

abbrev State := Nat → Nat

CSLibExt/Languages/IMP/Syntax.lean:34

def whileFun (guard : BExp) (body : State → State → Prop)
    (R : State → State → Prop) : State → State → Prop :=
  fun s s' => (guard.eval s = false ∧ s' = s) ∨
    (guard.eval s = true ∧ ∃ m, body s m ∧ R m s')

CSLibExt/Languages/IMP/Denotational.lean:32

Uses 4 · Used by 1

Statement usesBoolean expressions of IMP · IMP program states · One-step unfolding functional of a while loop

Proof usesEvaluation of IMP Boolean expressions

Used byThe while-loop functional as a monotone map

DefinitionThe while-loop functional as a monotone map#✓fully proved

For a boolean guard \(b\) and a relation \(B\) between states (the body denotation), this is the map \(\Phi\) on relations between states, ordered by inclusion, where \(\Phi(R)\) relates \(s\) to \(s'\) exactly when either \(b\) is false in \(s\) and \(s' = s\), or \(b\) is true in \(s\) and there is a state \(m\) with \(B(s, m)\) and \(R(m, s')\). The map \(\Phi\) is monotone: \(R_1 \subseteq R_2\) implies \(\Phi(R_1) \subseteq \Phi(R_2)\).

def whileOrderHom (guard : BExp) (body : State → State → Prop) :
    (State → State → Prop) →o (State → State → Prop) :=
  ⟨whileFun guard body, whileFun_mono⟩

inductive BExp where
  | truth (value : Bool)
  | eq (left right : AExp)
  | le (left right : AExp)
  | not (body : BExp)
  | and (left right : BExp)
  deriving DecidableEq, Repr

CSLibExt/Languages/IMP/Syntax.lean:46

abbrev State := Nat → Nat

CSLibExt/Languages/IMP/Syntax.lean:34

def whileFun (guard : BExp) (body : State → State → Prop)
    (R : State → State → Prop) : State → State → Prop :=
  fun s s' => (guard.eval s = false ∧ s' = s) ∨
    (guard.eval s = true ∧ ∃ m, body s m ∧ R m s')

CSLibExt/Languages/IMP/Denotational.lean:32

theorem whileFun_mono {guard : BExp} {body : State → State → Prop} :
    Monotone (whileFun guard body)

CSLibExt/Languages/IMP/Denotational.lean:38

Uses 4 · Used by 3

Statement usesBoolean expressions of IMP · IMP program states · One-step unfolding functional of a while loop · Monotonicity of the while-loop unfolding functional

Used byRelational denotational semantics of IMP · The while denotation is a fixed point · Park induction for while loops

DefinitionRelational denotational semantics of IMP#✓fully proved

The denotation of an IMP command is a binary relation on states, defined by recursion on the command. The command \(\mathtt{skip}\) relates \(s\) to \(s'\) iff \(s' = s\). For a variable identifier \(x\) and an arithmetic expression \(a\), the assignment \(x := a\) relates \(s\) to \(s'\) iff \(s'\) is \(s\) with \(x\) updated to the value of \(a\) in \(s\). The sequence \(c_1; c_2\) relates \(s\) to \(s'\) iff there is a state \(m\) such that \(c_1\) relates \(s\) to \(m\) and \(c_2\) relates \(m\) to \(s'\). For a Boolean expression \(b\), the conditional \(\mathtt{if}\ b\ \mathtt{then}\ t\ \mathtt{else}\ e\) relates \(s\) to \(s'\) iff either \(b\) evaluates to true in \(s\) and \(t\) relates \(s\) to \(s'\), or \(b\) evaluates to false in \(s\) and \(e\) relates \(s\) to \(s'\). The denotation of \(\mathtt{while}\ b\ \mathtt{do}\ c\) is the least fixed point, for inclusion of relations, of the one-step unfolding functional of a while loop with guard \(b\) and body relation the denotation of \(c\).

def Denote : Cmd → State → State → Prop
  | .skip => fun s s' => s' = s
  | .assign n a => fun s s' => s' = Function.update s n (a.eval s)
  | .seq c₁ c₂ => fun s s' => ∃ m, Denote c₁ s m ∧ Denote c₂ m s'
  | .ite b t e => fun s s' =>
      (b.eval s = true ∧ Denote t s s') ∨ (b.eval s = false ∧ Denote e s s')
  | .while b c => (whileOrderHom b (Denote c)).lfp

inductive Cmd where
  | skip
  | assign (name : Nat) (value : AExp)
  | seq (first second : Cmd)
  | ite (guard : BExp) (thenBranch elseBranch : Cmd)
  | while (guard : BExp) (body : Cmd)
  deriving DecidableEq, Repr

CSLibExt/Languages/IMP/Syntax.lean:55

abbrev State := Nat → Nat

CSLibExt/Languages/IMP/Syntax.lean:34

def whileOrderHom (guard : BExp) (body : State → State → Prop) :
    (State → State → Prop) →o (State → State → Prop) :=
  ⟨whileFun guard body, whileFun_mono⟩

CSLibExt/Languages/IMP/Denotational.lean:46

Uses 7 · Used by 9

Statement usesArithmetic expressions of IMP · Evaluation of IMP arithmetic expressions · Boolean expressions of IMP · Evaluation of IMP Boolean expressions · Commands of IMP · IMP program states · The while-loop functional as a monotone map

Used byPartial-correctness Hoare logic matches the denotational semantics · Total-correctness Hoare logic is sound and complete for the denotational semantics · Denotational executions are big-step executions · Big-step executions are denotational executions · The denotational semantics of IMP is deterministic · Agreement of the denotational and big-step semantics of IMP · The while denotation is a fixed point · Unfolding equation for the while denotation · Park induction for while loops

Denotations and big-step semantics

TheoremThe while denotation is a fixed point#✓fully proved

Let \(b\) be a Boolean expression and \(c\) an IMP command, let \(W\) be the relational denotation of \(\mathtt{while}\ b\ \mathtt{do}\ c\), and let \(\Phi\) be the one-step unfolding functional of a while loop with guard \(b\) and body relation the denotation of \(c\). Then \(W = \Phi(W)\).

theorem while_eq {b : BExp} {c : Cmd} :
    Denote (.while b c) = whileFun b (Denote c) (Denote (.while b c))

inductive BExp where
  | truth (value : Bool)
  | eq (left right : AExp)
  | le (left right : AExp)
  | not (body : BExp)
  | and (left right : BExp)
  deriving DecidableEq, Repr

CSLibExt/Languages/IMP/Syntax.lean:46

inductive Cmd where
  | skip
  | assign (name : Nat) (value : AExp)
  | seq (first second : Cmd)
  | ite (guard : BExp) (thenBranch elseBranch : Cmd)
  | while (guard : BExp) (body : Cmd)
  deriving DecidableEq, Repr

CSLibExt/Languages/IMP/Syntax.lean:55

def Denote : Cmd → State → State → Prop
  | .skip => fun s s' => s' = s
  | .assign n a => fun s s' => s' = Function.update s n (a.eval s)
  | .seq c₁ c₂ => fun s s' => ∃ m, Denote c₁ s m ∧ Denote c₂ m s'
  | .ite b t e => fun s s' =>
      (b.eval s = true ∧ Denote t s s') ∨ (b.eval s = false ∧ Denote e s s')
  | .while b c => (whileOrderHom b (Denote c)).lfp

CSLibExt/Languages/IMP/Denotational.lean:56

def whileFun (guard : BExp) (body : State → State → Prop)
    (R : State → State → Prop) : State → State → Prop :=
  fun s s' => (guard.eval s = false ∧ s' = s) ∨
    (guard.eval s = true ∧ ∃ m, body s m ∧ R m s')

CSLibExt/Languages/IMP/Denotational.lean:32

Uses 6 · Used by 1

Statement usesBoolean expressions of IMP · Commands of IMP · Relational denotational semantics of IMP · IMP program states · One-step unfolding functional of a while loop

Proof usesThe while-loop functional as a monotone map

Used byUnfolding equation for the while denotation

TheoremUnfolding equation for the while denotation#✓fully proved

For every Boolean expression \(b\), IMP command \(c\) and states \(s\) and \(s'\), the relational denotation of \(\mathtt{while}\ b\ \mathtt{do}\ c\) relates \(s\) to \(s'\) if and only if either \(b\) evaluates to false in \(s\) and \(s' = s\), or \(b\) evaluates to true in \(s\) and there is a state \(m\) such that the denotation of \(c\) relates \(s\) to \(m\) and the denotation of the loop relates \(m\) to \(s'\).

theorem while_iff {b : BExp} {c : Cmd} {s s' : State} :
    Denote (.while b c) s s' ↔
      (b.eval s = false ∧ s' = s) ∨
        (b.eval s = true ∧ ∃ m, Denote c s m ∧ Denote (.while b c) m s')

inductive BExp where
  | truth (value : Bool)
  | eq (left right : AExp)
  | le (left right : AExp)
  | not (body : BExp)
  | and (left right : BExp)
  deriving DecidableEq, Repr

CSLibExt/Languages/IMP/Syntax.lean:46

inductive Cmd where
  | skip
  | assign (name : Nat) (value : AExp)
  | seq (first second : Cmd)
  | ite (guard : BExp) (thenBranch elseBranch : Cmd)
  | while (guard : BExp) (body : Cmd)
  deriving DecidableEq, Repr

CSLibExt/Languages/IMP/Syntax.lean:55

abbrev State := Nat → Nat

CSLibExt/Languages/IMP/Syntax.lean:34

def Denote : Cmd → State → State → Prop
  | .skip => fun s s' => s' = s
  | .assign n a => fun s s' => s' = Function.update s n (a.eval s)
  | .seq c₁ c₂ => fun s s' => ∃ m, Denote c₁ s m ∧ Denote c₂ m s'
  | .ite b t e => fun s s' =>
      (b.eval s = true ∧ Denote t s s') ∨ (b.eval s = false ∧ Denote e s s')
  | .while b c => (whileOrderHom b (Denote c)).lfp

CSLibExt/Languages/IMP/Denotational.lean:56

Uses 7 · Used by 1

Statement usesBoolean expressions of IMP · Evaluation of IMP Boolean expressions · Commands of IMP · Relational denotational semantics of IMP · IMP program states

Proof usesThe while denotation is a fixed point · One-step unfolding functional of a while loop

Used byBig-step executions are denotational executions

TheoremPark induction for while loops#✓fully proved

Let \(b\) be a Boolean expression, \(c\) an IMP command and \(P\) a binary relation on states, and let \(\Phi\) be the one-step unfolding functional of a while loop with guard \(b\) and body relation the denotation of \(c\). If \(\Phi(P) \subseteq P\), then for all states \(s\) and \(s'\) related by the relational denotation of \(\mathtt{while}\ b\ \mathtt{do}\ c\), \(P\) relates \(s\) to \(s'\).

theorem while_ind {b : BExp} {c : Cmd} {P : State → State → Prop}
    (hP : ∀ s s', whileFun b (Denote c) P s s' → P s s')
    {s s' : State} (h : Denote (.while b c) s s') : P s s'

inductive BExp where
  | truth (value : Bool)
  | eq (left right : AExp)
  | le (left right : AExp)
  | not (body : BExp)
  | and (left right : BExp)
  deriving DecidableEq, Repr

CSLibExt/Languages/IMP/Syntax.lean:46

inductive Cmd where
  | skip
  | assign (name : Nat) (value : AExp)
  | seq (first second : Cmd)
  | ite (guard : BExp) (thenBranch elseBranch : Cmd)
  | while (guard : BExp) (body : Cmd)
  deriving DecidableEq, Repr

CSLibExt/Languages/IMP/Syntax.lean:55

abbrev State := Nat → Nat

CSLibExt/Languages/IMP/Syntax.lean:34

def whileFun (guard : BExp) (body : State → State → Prop)
    (R : State → State → Prop) : State → State → Prop :=
  fun s s' => (guard.eval s = false ∧ s' = s) ∨
    (guard.eval s = true ∧ ∃ m, body s m ∧ R m s')

CSLibExt/Languages/IMP/Denotational.lean:32

def Denote : Cmd → State → State → Prop
  | .skip => fun s s' => s' = s
  | .assign n a => fun s s' => s' = Function.update s n (a.eval s)
  | .seq c₁ c₂ => fun s s' => ∃ m, Denote c₁ s m ∧ Denote c₂ m s'
  | .ite b t e => fun s s' =>
      (b.eval s = true ∧ Denote t s s') ∨ (b.eval s = false ∧ Denote e s s')
  | .while b c => (whileOrderHom b (Denote c)).lfp

CSLibExt/Languages/IMP/Denotational.lean:56

Uses 6 · Used by 1

Statement usesBoolean expressions of IMP · Commands of IMP · Relational denotational semantics of IMP · IMP program states · One-step unfolding functional of a while loop

Proof usesThe while-loop functional as a monotone map

Used byDenotational executions are big-step executions

TheoremDenotational executions are big-step executions#✓fully proved

For every IMP command \(c\) and all states \(s\) and \(s'\), if the relational denotation of \(c\) relates \(s\) to \(s'\), then executing \(c\) from \(s\) terminates in \(s'\) according to the big-step semantics.

theorem bigStep_of_denote {c : Cmd} {s s' : State} (h : Denote c s s') :
    BigStep c s s'

inductive Cmd where
  | skip
  | assign (name : Nat) (value : AExp)
  | seq (first second : Cmd)
  | ite (guard : BExp) (thenBranch elseBranch : Cmd)
  | while (guard : BExp) (body : Cmd)
  deriving DecidableEq, Repr

CSLibExt/Languages/IMP/Syntax.lean:55

abbrev State := Nat → Nat

CSLibExt/Languages/IMP/Syntax.lean:34

def Denote : Cmd → State → State → Prop
  | .skip => fun s s' => s' = s
  | .assign n a => fun s s' => s' = Function.update s n (a.eval s)
  | .seq c₁ c₂ => fun s s' => ∃ m, Denote c₁ s m ∧ Denote c₂ m s'
  | .ite b t e => fun s s' =>
      (b.eval s = true ∧ Denote t s s') ∨ (b.eval s = false ∧ Denote e s s')
  | .while b c => (whileOrderHom b (Denote c)).lfp

CSLibExt/Languages/IMP/Denotational.lean:56

inductive BigStep : Cmd → State → State → Prop
  | skip (state) : BigStep .skip state state
  | assign (state) (name) (value) :
      BigStep (.assign name value) state (Function.update state name (value.eval state))
  | seq {first second initial middle final}
      (firstStep : BigStep first initial middle)
      (secondStep : BigStep second middle final) :
      BigStep (.seq first second) initial final
  | iteTrue {guard thenBranch elseBranch initial final}
      (guardTrue : guard.eval initial = true)
      (branchStep : BigStep thenBranch initial final) :
      BigStep (.ite guard thenBranch elseBranch) initial final
  ⋯

CSLibExt/Languages/IMP/BigStep.lean:34

Uses 10 · Used by 1

Statement usesBig-step semantics of IMP · Commands of IMP · Relational denotational semantics of IMP · IMP program states

Proof usesArithmetic expressions of IMP · Evaluation of IMP arithmetic expressions · Boolean expressions of IMP · Evaluation of IMP Boolean expressions · Park induction for while loops · One-step unfolding functional of a while loop

Used byAgreement of the denotational and big-step semantics of IMP

TheoremBig-step executions are denotational executions#✓fully proved

For every IMP command \(c\) and all states \(s\) and \(s'\), if executing \(c\) from \(s\) terminates in \(s'\) according to the big-step semantics, then the relational denotation of \(c\) relates \(s\) to \(s'\).

theorem denote_of_bigStep {c : Cmd} {s s' : State} (h : BigStep c s s') :
    Denote c s s'

inductive Cmd where
  | skip
  | assign (name : Nat) (value : AExp)
  | seq (first second : Cmd)
  | ite (guard : BExp) (thenBranch elseBranch : Cmd)
  | while (guard : BExp) (body : Cmd)
  deriving DecidableEq, Repr

CSLibExt/Languages/IMP/Syntax.lean:55

abbrev State := Nat → Nat

CSLibExt/Languages/IMP/Syntax.lean:34

inductive BigStep : Cmd → State → State → Prop
  | skip (state) : BigStep .skip state state
  | assign (state) (name) (value) :
      BigStep (.assign name value) state (Function.update state name (value.eval state))
  | seq {first second initial middle final}
      (firstStep : BigStep first initial middle)
      (secondStep : BigStep second middle final) :
      BigStep (.seq first second) initial final
  | iteTrue {guard thenBranch elseBranch initial final}
      (guardTrue : guard.eval initial = true)
      (branchStep : BigStep thenBranch initial final) :
      BigStep (.ite guard thenBranch elseBranch) initial final
  ⋯

CSLibExt/Languages/IMP/BigStep.lean:34

def Denote : Cmd → State → State → Prop
  | .skip => fun s s' => s' = s
  | .assign n a => fun s s' => s' = Function.update s n (a.eval s)
  | .seq c₁ c₂ => fun s s' => ∃ m, Denote c₁ s m ∧ Denote c₂ m s'
  | .ite b t e => fun s s' =>
      (b.eval s = true ∧ Denote t s s') ∨ (b.eval s = false ∧ Denote e s s')
  | .while b c => (whileOrderHom b (Denote c)).lfp

CSLibExt/Languages/IMP/Denotational.lean:56

Uses 9 · Used by 1

Statement usesBig-step semantics of IMP · Commands of IMP · Relational denotational semantics of IMP · IMP program states

Proof usesArithmetic expressions of IMP · Evaluation of IMP arithmetic expressions · Boolean expressions of IMP · Evaluation of IMP Boolean expressions · Unfolding equation for the while denotation

Used byAgreement of the denotational and big-step semantics of IMP

TheoremAgreement of the denotational and big-step semantics of IMP#✓fully proved

For every IMP command \(c\) and all states \(s\) and \(s'\), the relational denotation of \(c\) relates \(s\) to \(s'\) if and only if executing \(c\) from \(s\) terminates in \(s'\) according to the big-step semantics.

theorem iff_bigStep {c : Cmd} {s s' : State} :
    Denote c s s' ↔ BigStep c s s'

inductive Cmd where
  | skip
  | assign (name : Nat) (value : AExp)
  | seq (first second : Cmd)
  | ite (guard : BExp) (thenBranch elseBranch : Cmd)
  | while (guard : BExp) (body : Cmd)
  deriving DecidableEq, Repr

CSLibExt/Languages/IMP/Syntax.lean:55

abbrev State := Nat → Nat

CSLibExt/Languages/IMP/Syntax.lean:34

def Denote : Cmd → State → State → Prop
  | .skip => fun s s' => s' = s
  | .assign n a => fun s s' => s' = Function.update s n (a.eval s)
  | .seq c₁ c₂ => fun s s' => ∃ m, Denote c₁ s m ∧ Denote c₂ m s'
  | .ite b t e => fun s s' =>
      (b.eval s = true ∧ Denote t s s') ∨ (b.eval s = false ∧ Denote e s s')
  | .while b c => (whileOrderHom b (Denote c)).lfp

CSLibExt/Languages/IMP/Denotational.lean:56

inductive BigStep : Cmd → State → State → Prop
  | skip (state) : BigStep .skip state state
  | assign (state) (name) (value) :
      BigStep (.assign name value) state (Function.update state name (value.eval state))
  | seq {first second initial middle final}
      (firstStep : BigStep first initial middle)
      (secondStep : BigStep second middle final) :
      BigStep (.seq first second) initial final
  | iteTrue {guard thenBranch elseBranch initial final}
      (guardTrue : guard.eval initial = true)
      (branchStep : BigStep thenBranch initial final) :
      BigStep (.ite guard thenBranch elseBranch) initial final
  ⋯

CSLibExt/Languages/IMP/BigStep.lean:34

Uses 6 · Used by 3

Statement usesBig-step semantics of IMP · Commands of IMP · Relational denotational semantics of IMP · IMP program states

Proof usesDenotational executions are big-step executions · Big-step executions are denotational executions

Used byPartial-correctness Hoare logic matches the denotational semantics · Total-correctness Hoare logic is sound and complete for the denotational semantics · The denotational semantics of IMP is deterministic

TheoremThe denotational semantics of IMP is deterministic#✓fully proved

For every IMP command \(c\) and all states \(s\), \(s_1\) and \(s_2\), if the relational denotation of \(c\) relates \(s\) to \(s_1\) and \(s\) to \(s_2\), then \(s_1 = s_2\).

The proof goes through the agreement with the deterministic big-step semantics.

theorem deterministic {c : Cmd} {s s₁ s₂ : State}
    (h₁ : Denote c s s₁) (h₂ : Denote c s s₂) : s₁ = s₂

inductive Cmd where
  | skip
  | assign (name : Nat) (value : AExp)
  | seq (first second : Cmd)
  | ite (guard : BExp) (thenBranch elseBranch : Cmd)
  | while (guard : BExp) (body : Cmd)
  deriving DecidableEq, Repr

CSLibExt/Languages/IMP/Syntax.lean:55

abbrev State := Nat → Nat

CSLibExt/Languages/IMP/Syntax.lean:34

def Denote : Cmd → State → State → Prop
  | .skip => fun s s' => s' = s
  | .assign n a => fun s s' => s' = Function.update s n (a.eval s)
  | .seq c₁ c₂ => fun s s' => ∃ m, Denote c₁ s m ∧ Denote c₂ m s'
  | .ite b t e => fun s s' =>
      (b.eval s = true ∧ Denote t s s') ∨ (b.eval s = false ∧ Denote e s s')
  | .while b c => (whileOrderHom b (Denote c)).lfp

CSLibExt/Languages/IMP/Denotational.lean:56

Uses 6

Statement usesCommands of IMP · Relational denotational semantics of IMP · IMP program states

Proof usesBig-step semantics of IMP · Determinism of IMP big-step semantics · Agreement of the denotational and big-step semantics of IMP

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.