We review a third way to specify the semantics of a programming language: denotational semantics
A denotational semantics defines the meaning of each program as a mathematical object
⟦ ⟧ : syntax → semantics
A key property of denotational semantics is compositionality: The meaning of a compound statement should be defined in terms of the meaning of its components
This disqualifies
⟦c⟧ = {st | ⟨c, st.1⟩ ⟹ st.2}
because operational semantics are not compositional
In short, we want
⟦c ; c'⟧ = ... ⟦c⟧ ... ⟦c'⟧ ...
⟦if b then c else c'⟧ = ... ⟦c⟧ ... ⟦c'⟧ ...
⟦while b do c⟧ = ... ⟦c⟧ ...
An evaluation function (eval) on arithmetic expressions (aexp) is a denotational semantics; now we want the same for imperative programs
A fixpoint (or fixpoint) of f is a solution for X in the equation
X = f X
In general, fixpoints may not exist for all f (cf. f = nat.succ)
But under some conditions on f, a (unique) least fixpoint and a greatest fixpoint are guaranteed to exist
Consider this fixpoint equation:
X = (λ(p : ℕ → Prop) (n : ℕ), n = 0 ∨ ∃m : ℕ, n = m + 2 ∧ p m) X
= λn : ℕ, n = 0 ∨ ∃m : ℕ, n = m + 2 ∧ X m
where X : ℕ → Prop and f = λ(p : ℕ → Prop) (n : ℕ), n = 0 ∨ ∃m : ℕ, n = m + 2 ∧ p m
The above example admits only one fixpoint; the fixpoint equation uniquely specifies X as the set of even numbers
In general, the least and greatest fixpoint may be different:
X = id X
= X
Here, the least fixpoint is (λ_, False) and the greatest fixpoint is (λ_, True)
Conventionally, False < True, and thus (λ_, False) < (λ_, True)
Similarly, ∅ < @set.univ α if α is inhabited
Key observation: Inductive predicates correspond to least fixpoints, but they are built into Lean's logic (CIC)
For the semantics of programming languages:
X will have type set (state × state) (or e.g. state → state → Prop), represeting relations between states
f will correspond to either taking one iteration of the loop (if the condition b is true) or the identity (if b is false)
The least fixpoint corresponds to finite executions of a program, which is all we care about
A function f : α → β is monotone if
a ≤ b → f a ≤ f b for all a, b
We assume a partial order ≤ on the types α and β
Many operations on sets (e.g. ∪), relations (e.g. ◯), and functions (e.g. const) are monotone
The set of monotone functions is also well behaved: The identity function is monotone, the composition of monotone functions is again monotone, etc.
All monotone functions f : α → α, where α is a complete lattice, admit least and greatest fixpoints
⎧ s ∪ {a} if a ∉ s
f s = ⎨
⎩ ∅ otherwise
so ∅ ⊆ {a}, but f ∅ = {a} ⊈ ∅ = f {a}
To define the (least) fixpoints on sets, we only need one operation: intersection ⋂
Complete lattices capture this concept abstractly
A complete lattice α is an ordered type for which each set α has an infimum
A complete lattice consists of: a partial order ≤ : α → α → Prop (i.e. reflexive, transitive, and antisymmetric), and an operator ⨅ : set α → α, called infimum, or greatest lower bound (glb)
⨅s is the infimum of s:
⨅s is a lower bound of s
⨅s ≤ b for all b ∈ s
⨅s is the greatest lower bound
b ≤ ⨅s for all b, s.t. ∀x∈s, b ≤ x
Warning: ⨅s is not necessary in s
set α is an instance w.r.t. ⊆ and ⋂ for all types α
Prop is an instance w.r.t. → and ∀, i.e. ⨅s := ∀p ∈ s, p
We define
lfp f := ⨅{x | f x ≤ x}
Characteristic theorems, for any monotone function f:
lfp f is a fixpoint: lfp f = f (lfp f)
lfp f is smaller than any other fixpoint: X = f X → lfp f ≤ X
X ⨅{} = ?
/ \ ⨅{X} = ?
A B ⨅{A, B} = ?
\ / ⨅{X, A} = ?
Y ⨅{X, A, B, Y} = ?
enat := ℕ ∪ {∞}
ereal := ℝ ∪ {- ∞, ∞}
...
For α a complete lattice, then also β → α is a complete lattice
For α, β complete lattices, then also α × β is a complete lattice
ℕ, ℤ, ℚ, ℝ: no infimum for ∅, ⨅ℕ, ...
erat := ℚ ∪ {- ∞, ∞}, for example ⨅{q | 2 < q * q} = sqrt 2 is not in ℚ
Our denotational semantics interprets (or "compiles") programs to relations between states
Relations are equivalent to functions from states to set of states:
set (state × state) ≃ (state → set state)
We interpret relations as functions set → set state, transforming states to new states with non-determinism and non-termination effects
If we want to model more effects (probability, I/O, heap, ...), we can use monads:
state → M state
skip and assign are interpreted as pure (i.e. effectless) functions, and if translates to an if ... then ... else ...
The interesting interpretations are for seq and while:
⟦ seq p₁ p₂ ⟧ is interpreted as the composition of two monadic effects for which we use the bind operator (>>=), or more concise the Kleisli operator (>=>)
⟦ seq p₁ p₂ ⟧ := ⟦ p₁ ⟧ >=> ⟦ p₂ ⟧ -- i.e. λs, ⟦ p₁ ⟧ s >>= ⟦ p₂ ⟧
while can not be interpreted in an arbitrary monad (think about M := id). We need a monad with an additional interface, e.g. monad_lfp M (which includes that M α is a complete lattice):
mlfp {α : Type} (f : (α → M α) → (α → M α)) (hf : monotone f) : α → M α
With this we define
⟦ while c f ⟧ := mlfp (λW s, if c s then f s >>= W else skip) ...
Some ideas for verification projects
Computer science:
functional data structures (balanced trees, ...)
functional algorithms (bubble sort, merge sort, Tarjan's algorithm, ...)
compiler from expressions or imperative programs to e.g. stack machine
type systems (e.g. Benjamin Pierce's Types and Programming Languages)
security properties (e.g. Volpano–Smith-style noninterference analysis)
theory of first-order terms, including matching, term rewriting
extending WHILE with static arrays or other features
automata theory
normalization of context-free grammars or regular expressions
process algebras and bisimilarity
soundness and possibly completeness of proof systems (e.g. Genzen's sequent calculus, natural deduction, tableaux)
separation logic
Mathematics:
graphs
combinatorics
number theory
These notes are largely inspired by Concrete Semantics: With Isabelle/HOL by Tobias Nipkow and Gerwin Klein and their slides