Denotational Semantics of IMP
We now have every tool we need — domains
and the least-fixed-point construction
— to give the while-language IMP a fully denotational meaning. The plan is uncompromising:
to every syntactic phrase we assign a mathematical object, written in
semantic brackets \llbracket \cdot \rrbracket ("Scott
brackets"). An expression denotes a value; a command denotes a function on states. No machine
runs, no configuration steps — the meaning simply is, computed by structural recursion on the
syntax.
The prize for this austerity is compositionality: the meaning of a compound phrase is a
fixed function of the meanings of its parts, and of nothing else. That is what lets us reason
about programs equationally — to prove two programs equal by showing their denotations coincide, with no
appeal to how either one executes.
States, and the semantics of expressions
Fix a set \mathbf{Var} of variables. A state is a function
assigning an integer to each variable,
\sigma \in \Sigma \;=\; \mathbf{Var} \to \mathbb{Z},
so a state is the store, as a mathematical function. Arithmetic and boolean expressions never
diverge and never change the state, so their meanings are total functions reading a state:
\mathcal{A}\llbracket a \rrbracket : \Sigma \to \mathbb{Z}, \qquad \mathcal{B}\llbracket b \rrbracket : \Sigma \to \{\mathsf{tt}, \mathsf{ff}\}.
These are defined by structural recursion, and this is where compositionality first shows its face —
each clause combines the meanings of sub-expressions:
\mathcal{A}\llbracket n \rrbracket\,\sigma = n, \qquad \mathcal{A}\llbracket x \rrbracket\,\sigma = \sigma(x), \qquad \mathcal{A}\llbracket a_1 + a_2 \rrbracket\,\sigma = \mathcal{A}\llbracket a_1 \rrbracket\,\sigma + \mathcal{A}\llbracket a_2 \rrbracket\,\sigma.
The + on the left is a piece of syntax; the
+ on the right is real addition in \mathbb{Z}. The
brackets are exactly the bridge from one to the other.
The semantics of commands
A command may fail to terminate, so its denotation is a partial function on states —
an element of the CPO
[\Sigma \rightharpoonup \Sigma] (equivalently
\Sigma \to \Sigma_\bot), where \bot records
divergence:
\mathcal{C}\llbracket c \rrbracket : \Sigma \rightharpoonup \Sigma.
Four of the five constructs are immediate. Below, \sigma[x \mapsto v] is the
state that agrees with \sigma everywhere except that
x now holds v, and
\circ is function composition:
\mathcal{C}\llbracket \mathtt{skip} \rrbracket = \mathrm{id}_\Sigma, \qquad \mathcal{C}\llbracket x := a \rrbracket\,\sigma = \sigma\big[x \mapsto \mathcal{A}\llbracket a \rrbracket\,\sigma\big],
\mathcal{C}\llbracket c_1 ; c_2 \rrbracket = \mathcal{C}\llbracket c_2 \rrbracket \circ \mathcal{C}\llbracket c_1 \rrbracket,
\mathcal{C}\llbracket \mathtt{if}\ b\ \mathtt{then}\ c_1\ \mathtt{else}\ c_2 \rrbracket\,\sigma = \begin{cases} \mathcal{C}\llbracket c_1 \rrbracket\,\sigma & \text{if } \mathcal{B}\llbracket b \rrbracket\,\sigma = \mathsf{tt},\\[2pt] \mathcal{C}\llbracket c_2 \rrbracket\,\sigma & \text{if } \mathcal{B}\llbracket b \rrbracket\,\sigma = \mathsf{ff}. \end{cases}
Read the sequencing clause carefully: c_1 runs "first", yet it is written on
the right of the \circ — because
(g \circ f)(\sigma) = g(f(\sigma)), the inner function applies first. And
because \bot is strict under composition (if
c_1 diverges, so does c_1;c_2), partiality
propagates automatically. Every clause names only the denotations of sub-phrases — compositionality by
construction.
The while loop, as a least fixed point
Only \mathtt{while} resists a direct definition, and for exactly the reason
recursion did: its meaning refers to itself. Unfolding the loop once gives the defining equation
\mathcal{C}\llbracket \mathtt{while}\ b\ \mathtt{do}\ c \rrbracket = \mathcal{C}\llbracket \mathtt{if}\ b\ \mathtt{then}\ (c\,;\ \mathtt{while}\ b\ \mathtt{do}\ c)\ \mathtt{else}\ \mathtt{skip} \rrbracket.
The loop's denotation appears on both sides — a fixed-point equation. So we read off the functional
whose fixed point it must be. Writing W = \mathcal{C}\llbracket \mathtt{while}\ b\ \mathtt{do}\ c \rrbracket,
the loop denotes the least fixed point of the continuous functional
\Phi on the CPO [\Sigma \rightharpoonup \Sigma]:
\Phi(W)\,\sigma \;=\; \begin{cases} W\big(\mathcal{C}\llbracket c \rrbracket\,\sigma\big) & \text{if } \mathcal{B}\llbracket b \rrbracket\,\sigma = \mathsf{tt},\\[2pt] \sigma & \text{if } \mathcal{B}\llbracket b \rrbracket\,\sigma = \mathsf{ff}, \end{cases} \qquad \mathcal{C}\llbracket \mathtt{while}\ b\ \mathtt{do}\ c \rrbracket \;=\; \mathrm{fix}(\Phi) \;=\; \bigsqcup_{n} \Phi^n(\bot).
The Kleene chain here has a beautiful reading: \Phi^n(\bot) is "the loop that
gives up (diverges) after at most n iterations". As
n grows, more starting states get a real answer; the lub is the loop that
runs as long as it needs. Reveal the chain of finite approximations:
Because \Sigma \rightharpoonup \Sigma is a pointed CPO and
\Phi is continuous, the previous page's Kleene theorem guarantees
\mathrm{fix}(\Phi) exists and equals the lub of this chain. The while loop is
not a special case bolted on — it is the same least-fixed-point machinery that tamed recursion.
Computing the loop's denotation by iteration
Let us make \Phi^n(\bot) concrete for the loop
while (x > 0) do x := x − 1 on a one-variable state. We build the approximations
\Phi^0(\bot), \Phi^1(\bot), \dots as partial functions (returning
undefined for "still diverges here") and watch them converge to "set
x to 0".
// State = just the value of x here. A partial function returns undefined ( = ⊥ ) where it diverges.
type Sigma = number;
type Cmd = (s: Sigma) => Sigma | undefined;
const bottom: Cmd = (_s) => undefined; // ⊥ : diverge everywhere
const b = (s: Sigma) => s > 0; // loop guard x > 0
const body = (s: Sigma) => s - 1; // loop body x := x - 1
// Φ(W) : one guarded unfolding of the loop, delegating the rest to approximation W.
function Phi(W: Cmd): Cmd {
return (s: Sigma) => {
if (b(s)) {
return W(body(s)); // still looping — hand off to W
}
return s; // guard false — halt, return state
};
}
// Build Φ⁰(⊥), Φ¹(⊥), … and report the largest x each approximation can finish.
let approx: Cmd = bottom;
for (let n = 0; n <= 5; n++) {
const finishes: number[] = [];
for (let x = 0; x <= 6; x++) if (approx(x) !== undefined) finishes.push(x);
console.log(`Φ^${n}(⊥) terminates for x in {${finishes.join(",")}}`
+ (finishes.length ? ` (each ends at x=${approx(finishes[finishes.length - 1])})` : " (diverges everywhere)"));
approx = Phi(approx);
}
console.log("Limit fix(Φ): while (x>0) x:=x-1 maps every x >= 0 to 0.");
\Phi^n(\bot) terminates precisely for the states needing fewer than
n iterations — start with x = n and the
n-th approximation still says \bot. The chain never
revises an answer once given (monotonicity), and its lub sends every
x \ge 0 to 0. That lub is
\mathcal{C}\llbracket \mathtt{while}\ (x>0)\ \mathtt{do}\ x := x-1 \rrbracket.
Denotational meets operational
We now have two accounts of IMP: the operational one, which runs the program via a transition
relation, and this denotational one, which is a function. They had better agree — and they do.
For every command c and states
\sigma, \sigma',
\langle c, \sigma \rangle \Downarrow \sigma' \quad\Longleftrightarrow\quad \mathcal{C}\llbracket c \rrbracket\,\sigma = \sigma'.
Operationally, c started in \sigma terminates in
\sigma' if and only if its denotation, applied to
\sigma, yields \sigma' (and the denotation is
\bot exactly when execution diverges).
The proof is a pair of inductions — one on the operational derivation, one (the harder direction, for
the loop) on the Kleene chain. It is the theorem that certifies denotational semantics as a
faithful re-description of behaviour, not a rival to it. See the operationally-defined
IMP while-language
for the other side of this coin.
Operational semantics is simpler to write, but it is not compositional: to know what
c_1 ; c_2 does you must trace an execution across the seam between the two
commands, and "what c_1 does" is entangled with the machinery of the whole
run. Denotational semantics buys a strong guarantee: \mathcal{C}\llbracket c_1;c_2 \rrbracket
depends on c_1 and c_2 only through their
denotations \mathcal{C}\llbracket c_1 \rrbracket and
\mathcal{C}\llbracket c_2 \rrbracket. So if two commands have equal
denotations they are interchangeable in every context — the licence behind compiler
optimisations, program-equivalence proofs, and the whole enterprise of reasoning about code as algebra.
Strachey's slogan was that meaning should be a homomorphism from syntax to a world of mathematical
values; compositionality is that slogan made precise.
It is tempting to "define" \mathcal{C}\llbracket \mathtt{while}\ b\ \mathtt{do}\ c \rrbracket
by literally substituting its own unfolding on the right-hand side and calling it a day. That is
circular text, not a definition — nothing pins down a unique function, and a divergent loop has
no obvious value to plug in. The only rigorous move is to name the functional
\Phi (which has no self-reference) and take
\mathrm{fix}(\Phi) = \bigsqcup_n \Phi^n(\bot), the least
fixed point. Choosing a non-least fixed point would invent terminating behaviour for loops that actually
spin forever. And note the meaning is a partial function on states: a total function on
\Sigma cannot model divergence, which is precisely why we lifted to
\Sigma_\bot in the first place.