Using notation similar to Backus-Naur Form (BNF): \begin {array}{lcl} \mathcal {E} & \Coloneqq & n \mid x \mid \mathcal {E}_1 + \mathcal {E}_2 \mid \mathcal {E}_1 - \mathcal {E}_2\\ \mathcal {B} & \Coloneqq & \mathsf {false} \mid \mathsf {true} \mid \neg \mathcal {B} \mid \mathcal {E}_1 = \mathcal {E}_2\\ \mathcal {C} & \Coloneqq & \mathsf {skip} \mid x := \mathcal {E} \mid \mathcal {C}_1 ; \mathcal {C}_2 \mid \mathsf {if}\ \mathcal {B}\ \mathsf {then}\ \mathcal {C}_1\ \mathsf {else}\ \mathcal {C}_2\\ x & \in & \mathcal {V}\; \textit {(variables)}\\ n & \in & \mathbb {N} \end {array}

A denotational semantics consists of, for each syntactic class \mathcal {X} in a language:

1. A semantic domain D which can be any set of mathematical objects (although, as we will see later, it is helpful if it obeys certain properties).
2. A valuation function \llbracket \cdot \rrbracket : \mathcal {X} \rightarrow D. We require that this function be a homomorphism, that is that it is compositional. This means that the valuation (or denotation) of an expression should be made from the denotation of its components. In other words, for each syntactic constructor C(e_1,e_2,\dots ), we should have a mathematical operation f(x_1,x_2,\dots ) such that the denotation of C can be defined as: \llbracket C(e_1, e_2, \dots ) \rrbracket = f(\llbracket e_1 \rrbracket , \llbracket e_2 \rrbracket , \dots )

The choices of semantic domain and valuation function are, essentially, arbitrary: we choose objects that reflect those aspects of our programs that we are interested in. For most of the simple languages we will examine, we are only concerned with the results of the computation, which is a semantics suitable for reasoning about program behaviour and correctness. However, there also exist denotational cost models that compositionally assign a measure of program performance to syntax. This measure is just another kind of denotational semantics.

We shall first select a semantic domain for each syntactic class: \begin {array}{lcl} \mathbf {E} & \triangleq & \Sigma \rightarrow \mathbb {Z} \\ \mathbf {B} & \triangleq & \Sigma \rightarrow \mathbb {B} \\ \mathbf {C} & \triangleq & \Sigma \rightarrow \Sigma \\ \end {array} Here, \Sigma represents the set of states, which contains the values assigned to all variables: \Sigma \;\triangleq \; \mathcal {V} \rightarrow \mathbb {Z}

Now, we define our valuation functions, \llbracket \cdot \rrbracket _\mathcal {E} : \mathcal {E} \rightarrow \mathbf {E} : \begin {array}{lcl} \llbracket n \rrbracket _\mathcal {E}\ \sigma & = & n \\ \llbracket x \rrbracket _\mathcal {E}\ \sigma & = & \sigma (x) \\ \llbracket e_1 + e_2 \rrbracket _\mathcal {E}\ \sigma & = & \llbracket e_1 \rrbracket _\mathcal {E}\ \sigma + \llbracket e_2 \rrbracket _\mathcal {E}\ \sigma \\ \llbracket e_1 - e_2 \rrbracket _\mathcal {E}\ \sigma & = & \llbracket e_1 \rrbracket _\mathcal {E}\ \sigma - \llbracket e_2 \rrbracket _\mathcal {E}\ \sigma \\[2em] \end {array} and \llbracket \cdot \rrbracket _\mathcal {B} : \mathcal {B} \rightarrow \mathbf {B}: \begin {array}{lcl} \llbracket \mathsf {false} \rrbracket _\mathcal {B}\ \sigma & = & \mathit {F} \\ \llbracket \mathsf {true} \rrbracket _\mathcal {B}\ \sigma & = & \mathit {T} \\ \llbracket \neg b \rrbracket _\mathcal {B}\ \sigma & = & \begin {cases}\mathit {F} & \text {if}\ \llbracket b \rrbracket _\mathcal {B}\ \sigma = \mathit {T} \\ \mathit {T} & \text {otherwise} \end {cases} \\[1.1em] \llbracket e_1 = e_2 \rrbracket _\mathcal {B}\ \sigma & = & \begin {cases}\mathit {T} & \text {if}\ \llbracket e_1 \rrbracket _\mathcal {E}\ \sigma = \llbracket e_2 \rrbracket _\mathcal {E}\ \sigma \\ \mathit {F} & \text {otherwise} \end {cases} \end {array} and \llbracket \cdot \rrbracket _\mathcal {C} : \mathcal {C} \rightarrow \mathbf {C}: \begin {array}{lcl} \llbracket \mathsf {skip} \rrbracket _\mathcal {C}\ \sigma & = & \sigma \\ \llbracket x := e \rrbracket _\mathcal {C}\ \sigma & = & \sigma \left (x \mapsto \llbracket e \rrbracket _\mathcal {E}\right ) \\ \llbracket c_1 ; c_2 \rrbracket _\mathcal {C}\ \sigma & = & \llbracket c_2 \rrbracket _\mathcal {C}\ \left (\llbracket c_1 \rrbracket _\mathcal {C}\ \sigma \right ) \\[0.3em] \llbracket \textsf {if}\ b\ \textsf {then}\ c_1\ \textsf {else}\ c_2 \rrbracket _\mathcal {C}\ \sigma & = & \begin {cases}\llbracket c_1 \rrbracket _\mathcal {C}\ \sigma & \text {if}\ \llbracket b \rrbracket _\mathcal {B}\ \sigma = \mathit {T} \\ \llbracket c_2 \rrbracket _\mathcal {C}\ \sigma & \text {otherwise} \end {cases} \end {array}

Suppose we extended the \mathcal {C} language with a while loop construct: \mathcal {C}\; \Coloneqq \; \cdots \mid \mathsf {while}\ \mathcal {B}\ \mathsf {do}\ \mathcal {C}\ \mathsf {od} The intuitive way to assign a semantics would be to use a recursive function: \llbracket \mathsf {while}\ b\ \mathsf {do}\ c\ \mathsf {od} \rrbracket _\mathcal {C}\ \sigma \; = \; \begin {cases} \llbracket \mathsf {while}\ b\ \mathsf {do}\ c\ \mathsf {od} \rrbracket _\mathcal {C}\ (\llbracket c \rrbracket _\mathcal {C}\ \sigma ) & \text {if}\ \llbracket b \rrbracket _\mathcal {B}\ \sigma = \mathit {T} \\ \sigma & \text {otherwise} \end {cases} However, such an equation is not a good definition. If we consider the trivial infinite loop program L \triangleq \mathsf {while}\ \mathsf {true}\ \mathsf {do}\ \mathsf {skip}\ \mathsf {od}, and compute its semantics, we end up with: \llbracket \mathsf {while}\ \mathsf {true}\ \mathsf {do}\ \mathsf {skip}\ \mathsf {od} \rrbracket _\mathcal {C}\ \sigma \; = \; \llbracket \mathsf {while}\ \mathsf {true}\ \mathsf {do}\ \mathsf {skip}\ \mathsf {od} \rrbracket _\mathcal {C}\ \sigma This equation is satisfied by any function \Sigma \rightarrow \Sigma , so it doesn't tell us which function corresponds to the program L.

More generally, allowing our functions to be (generally) recursive causes these issues. The loop program L gives rise to the recursive equation \ell (x) = \ell (x), which has an infinite number of solutions.

If we add recursion to our programming language, we could have programs that give rise to more complex recursive equations like f(x) = f(x) + 1. By contrast to \ell (x), f(x) has no solutions (assuming f(x) operates on integers).

Suppose we extend our notion of expressions in the \mathcal {C} language with parameterless higher-order procedures: \begin {array}{l} \mathcal {E}\; \Coloneqq \; \cdots \mid \mathsf {proc}\ \mathcal {C}\\ \mathcal {C}\; \Coloneqq \; \cdots \mid x \end {array}

For our denotational semantics, our domains now take this form (\textcolor {blue}{\text {blue}} parts are new vs. Example [dt-0004]), where \uplus denotes disjoint union: \begin {array}{lcl} \mathbf {E} & \triangleq & \Sigma \rightarrow \mathbb {Z}\textcolor {blue}{\ \uplus \ \mathbf {C}}\\ \mathbf {B} & \triangleq & \Sigma \rightarrow \mathbb {B} \\ \mathbf {C} & \triangleq & \Sigma \rightarrow \Sigma \\[0.2em] \Sigma & \triangleq & \mathcal {V} \rightarrow \mathbb {Z}\textcolor {blue}{\ \uplus \ \mathbf {C}} \end {array}

Any kind of higher-order construct leads to such recursive domain equations.

Following Scott, we introduce a special bottom value \bot to our semantic domains. \bot \ \text {represents}\ \begin {cases}\text {an undefined value;}\\\text {an error value;}\\\text {a \emph {non-terminating} computation.} \end {cases}

Given a set X, the flat domain (or lifted set) X_\bot is just the set X \cup \{ \bot \} (where \bot \notin X).

An information ordering is a partial order on denotations, written a \sqsubseteq b. This indicates that b is approximated by, or carries more information than, or is more well-defined than a. Naturally, the bottom value, being totally uninformative, is always the least element in this ordering.

Consider a flat domain X_\bot . There is a natural information ordering \sqsubseteq on X_\bot :

Formally, we say x \sqsubseteq y iff (x = y \lor x = \bot ).

A pointed poset is a partially ordered set with a bottom value.

Given two pointed posets X and Y, the product poset X \times Y is ordered as follows: (x,y) \sqsubseteq _{X \times Y} (x',y') \quad \text {iff} \quad x \sqsubseteq _X x' \land y \sqsubseteq _Y y' Intuitively, this says that "the information content of a pair of values is increased by increasing the information of either or both of its component values".

This product poset is also pointed, with bottom value \bot _{X \times Y} being (\bot _A, \bot _B).

As can be seen above, the domain \mathbb {B}_\bot \times \mathbb {B}_\bot is not flat, but it is still a pointed poset.

The function H : \mathbb {B}_\bot \rightarrow \mathbb {B}_\bot seems to let us solve the halting problem, assuming \bot represents non-termination: H(v) \; = \; \begin {cases} F & \text {if}\ v = \bot \\ T & \text {otherwise} \end {cases}

A function f : X \rightarrow Y between posets X and Y is monotone (or monotonic) if, for all x, y \in X: x \sqsubseteq y\; \text {implies}\; f(x) \sqsubseteq f(y)

A function f : X \rightarrow Y on pointed posets X and Y is strict if it preserves the bottom value, i.e. f(\bot _X) = \bot _Y.

Consider the functions \mathbb {B}_\bot \rightarrow \mathbb {B}_\bot . Which ones are monotonic? There are a total of 27 such functions but only three significant classes.

Let \mathbf {K}_K denote the chain of values x_1, x_2, x_3, \dots , x_K where a \leq b implies x_a \sqsubseteq x_b. There is one monotonic function \mathbf {K}_1 \rightarrow \mathbf {K}_1:

And there are three monotonic functions \mathbf {K}_2 \rightarrow \mathbf {K}_2:

1. Write down the monotonic functions \mathbf {K}_3 \rightarrow \mathbf {K}_3.

Solution.

• Liam O'Connor

When drawn as a diagram like the above, the monotonic functions are all those whose lines do not cross.

2. Write a simple recursive program to calculate the number of monotonic functions \mathbf {K}_n \rightarrow \mathbf {K}_m.

Solution.

• Liam O'Connor

In Haskell:

monotonics :: Int -> Int -> Int
monotonics n 1 = 1
monotonics n m = sum [monotonics (n-x) (m-1) | x <- [0..n]]

Consider our recursive \mathsf {while} loop semantics from § [dt-0006]: \llbracket \mathsf {while}\ b\ \mathsf {do}\ c\ \mathsf {od} \rrbracket _\mathcal {C}\ \sigma \; = \; \begin {cases} \llbracket \mathsf {while}\ b\ \mathsf {do}\ c\ \mathsf {od} \rrbracket _\mathcal {C}\ (\llbracket c \rrbracket _\mathcal {C}\ \sigma ) & \text {if}\ \llbracket b \rrbracket _\mathcal {B}\ \sigma = \mathit {T} \\ \sigma & \text {otherwise} \end {cases} How do we ensure that solutions exist for such recursive equations? And, if multiple solutions exist, how do we decide which one to pick? To address these questions, let's factor out everything in our definition except the recursion into a separate (higher-order) function: \begin {array}{l} \llbracket \mathsf {while}\ b\ \mathsf {do}\ c\ \mathsf {od} \rrbracket _\mathcal {C} = f(\llbracket \mathsf {while}\ b\ \mathsf {do}\ c\ \mathsf {od} \rrbracket _\mathcal {C}) \\[0.5em] \qquad \text {where}\; f(X)\ \sigma \; \triangleq \; \begin {cases} X\ (\llbracket c \rrbracket _\mathcal {C}\ \sigma ) & \text {if}\ \llbracket b \rrbracket _\mathcal {B}\ \sigma = \mathit {T} \\ \sigma & \text {otherwise} \end {cases} \end {array} Looking at it this way, we can see that any solution to this equation must be an element of our semantic domain X \in \mathbf {C} such that f(X) = X. In other words, the problem of finding solutions to our recursive equations can be cast as the problem of finding a fixed point for non-recursive higher-order functions.

A value x is a fixed point of a function f if f(x) = x.

So, requiring our functions to be monotonic is insufficient to guarantee that a single "best" solution exists.

Intuitively, recursive programs are executed by "unfolding" as much as necessary to get a result. We would like to characterise our domains to ensure that solutions always exist, and to allow us to pick the solutions that are "minimal" in the sense that they rely on a minimal amount of unfolding.

After converting a recursive program into a non-recursive monotonic higher order function f, the fixed point we desire would intuitively be the limit of the ascending Kleene chain of f, i.e. f(f(f(f(\dots )))):

Each successive element of this chain is another "unfolding" of the recursion.

While \omega -chains are technically sufficient for denotational semantics, for our purposes it is a little more convenient to think in terms of directed sets rather than chains.

DefinitionDirected set [dt-0010]

• Liam O'Connor

Formally, a non-empty subset Y \subseteq X of a poset (X,\sqsubseteq ) is directed iff: \forall x, y \in Y.\ \exists z \in Y.\ x \sqsubseteq z \land y \sqsubseteq z

The z above is an upper bound of x and y. Hence, a non-empty set is directed iff every pair of values has an upper bound in the set.

Intuitively, directed sets are "going somewhere" — given two elements we can always find a "greater" one in the set.

ExamplePower sets are directed [dt-0011]

The power set of any set X is directed under \subseteq .

Below: \cal {P}(\{1,2,3\}):

DefinitionConsistent subset [dt-0013]

A subset Y \subseteq X of a poset X is consistent iff \exists x \in X.\ \forall y \in Y.\ y \sqsubseteq x Such an x is called an upper bound of Y.

By choosing a cpo for our semantic domain, we can ensure that the Kleene chain has a limit. However, it is not guaranteed that the limit we find will be a fixed point to our monotonic function f.

To address this problem, we shall strengthen our requirement on functions from mere monotonicity to continuity.

Armed with the \textbf {fix} operator, we can return to our semantics of \mathsf {while} loops from § [dt-0006] and § [dt-000R], and at last define their semantics without relying on dubious recursive definitions: \begin {array}{l} \llbracket \mathsf {while}\ b\ \mathsf {do}\ c\ \mathsf {od} \rrbracket _\mathcal {C} = \textbf {fix}(f)\\[0.5em] \qquad \text {where}\; f(X)\ \sigma \; \triangleq \; \begin {cases} X\ (\llbracket c \rrbracket _\mathcal {C}\ \sigma ) & \text {if}\ \llbracket b \rrbracket _\mathcal {B}\ \sigma = \mathit {T} \\ \sigma & \text {otherwise} \end {cases} \end {array}

Proof that f is continuous is technically required but is omitted here.

Consider the function \Phi \in (\mathbb {N}_\bot \rightarrow \mathbb {N}_\bot ) \rightarrow (\mathbb {N}_\bot \rightarrow \mathbb {N}_\bot ), given by: \Phi (f) = \lambda n.\ \text {if}\ n = 0\ \text {then}\ 1\ \text {else}\ n\cdot f(n-1) Looking at the first few elements of our Kleene chain, we get: \begin {array}{lcl} \Phi ^0(\bot ) & = & \lambda n.\ \bot \quad \text {(i.e. $\bot _{\mathbb {N}_\bot \rightarrow \mathbb {N}_\bot }$)}\\ \Phi ^1(\bot ) & = & \lambda n.\ \text {if}\ n = 0\ \text {then}\ 1\ \text {else}\ \bot \\ \Phi ^2(\bot ) & = & \lambda n.\ \text {if}\ n = 0\ \text {then}\ 1\ \text {else}\ n\cdot (\text {if}\ n - 1 = 0\ \text {then}\ 1\ \text {else}\ \bot )\\ \cdots \end {array} Continuing on, we see that the mth approximation \Phi ^m(\bot ) to \textbf {fix}(\Phi ) is the function that gives x! for all x up to m, and diverges (\bot ) for all other arguments. Hence the limit \textbf {fix}(\Phi ) is the factorial function on \mathbb {N}_\bot !

1. Write down the first few approximations \Phi ^m(\bot ) to \textbf {fix}(\Phi ), where the higher order function \Phi : (\mathbb {Z}_\bot \rightarrow [\mathbb {Z}_\bot ]) \rightarrow (\mathbb {Z}_\bot \rightarrow [\mathbb {Z}_\bot ]) is given by: \Phi (f) = \lambda n.\ n :: f (n+1) What is \Phi ^m(\bot )? What is \textbf {fix}(\Phi )?

Solution.

• Liam O'Connor

The approximations are \{ \lambda n.\ \bot , \lambda n.\ n :: \bot , \lambda n.\ n :: (n + 1) :: \bot , \dots \}. The limit is a function that, given a natural number n, produces the infinite list of natural numbers starting from n.

2. Repeat the same process, but this time for a new higher order function \Phi : (\mathbb {Z}_\bot \rightarrow \mathbb {Z}_\bot ) \rightarrow (\mathbb {Z}_\bot \rightarrow \mathbb {Z}_\bot ) given by: \Phi (f) = \lambda n.\ \text {if}\ n = 0\ \text {then}\ 0\ \text {else}\ f(n-2)

Solution.

• Liam O'Connor

The nth approximation returns 0 if the input number is non-negative, even and less than 2n, otherwise it diverges (returns \bot ). The limit returns 0 for any non-negative even number, and diverges otherwise.