# 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
