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


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:

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:

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:

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




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:

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:




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