# Lecture 3.3: Programming Semantics — Denotational Semantics
We review a third way to specify the semantics of a programming language: denotational semantics
## 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
## Fixpoints
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)
## Least fixpoints
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
## Monotone functions
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
### Example for a nonmonotone function on sets
⎧ s ∪ {a} if a ∉ s
f s = ⎨
⎩ ∅ otherwise
so `∅ ⊆ {a}`, but `f ∅ = {a} ⊈ ∅ = f {a}`
## Complete lattices
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`
### Finite example
X ⨅{} = ?
/ \ ⨅{X} = ?
A B ⨅{A, B} = ?
\ / ⨅{X, A} = ?
Y ⨅{X, A, B, Y} = ?
### Other examples
enat := ℕ ∪ {∞}
ereal := ℝ ∪ {- ∞, ∞}
...
For `α` a complete lattice, then also `β → α` is a complete lattice
For `α`, `β` complete lattices, then also `α × β` is a complete lattice
### Non-examples
* `ℕ`, `ℤ`, `ℚ`, `ℝ`: no infimum for `∅`, `⨅ℕ`, ...
* `erat := ℚ ∪ {- ∞, ∞}`, for example `⨅{q | 2 < q * q} = sqrt 2` is not in `ℚ`
## Demo
[`33_lecture.lean`](33_lecture.lean)
## Connection to monads (optional)
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) ...
## Project ideas
Some ideas for verification projects
Computer science:
* functional data structures (balanced trees, ...)
* functional algorithms (bubble sort, merge sort, [Tarjan's algorithm](https://arxiv.org/pdf/1810.11979.pdf), ...)
* 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
## Reference
* [_Concrete Semantics: With Isabelle/HOL_](http://www.concrete-semantics.org/concrete-semantics.pdf) by Tobias Nipkow and Gerwin Klein, Chapter 11
## Acknowledgment
These notes are largely inspired by [_Concrete Semantics: With Isabelle/HOL_](http://www.concrete-semantics.org/) by Tobias Nipkow and Gerwin Klein and their slides