# 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`

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, ...)

• 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

## Acknowledgment

These notes are largely inspired by Concrete Semantics: With Isabelle/HOL by Tobias Nipkow and Gerwin Klein and their slides