Denotational semantics

Remarks

Example: for a language of commands acting on states $\Sigma$, take as domain the partial functions $\Sigma \rightharpoonup \Sigma$, ordered by extension of graphs. Set $[\![C_1; C_2]\!] = [\![C_2]\!] \circ [\![C_1]\!]$. For a loop, $[\![\mathsf{while}\ b\ \mathsf{do}\ C]\!]$ is the least fixed point of a map $\Phi$ on partial functions. The map $\Phi$ sends $w$ to the partial function equal to $w \circ [\![C]\!]$ on states where $b$ holds and to the identity where $b$ fails. The approximations $\Phi^k(\bot)$ describe the runs that exit the loop after fewer than $k$ iterations, and their union is the meaning of the loop. The loop $\mathsf{while}\ \mathsf{true}\ \mathsf{do}\ \mathsf{skip}$ gets the empty partial function, since every $\Phi^k(\bot)$ is empty.

Non-example: let the meaning of a command be the truth value "the command terminates from every state". Clause 1 fails for sequencing. The commands $x := 0$ and $x := 1$ both get the value true, and $W = \mathsf{while}\ x \ne 0\ \mathsf{do}\ \mathsf{skip}$ gets false. Yet $x := 0; W$ always terminates and $x := 1; W$ never does, so no function $F$ computes the meaning of $C_1; C_2$ from the meanings of $C_1$ and $C_2$.

A denotational semantics is adequate for an operational semantics if equal denotations imply equal observable behaviour, and fully abstract if the converse also holds.