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.

Destruction of pairs is captured by the two projection operators, defined as follows:

\begin {array}{lcl} \pi _0 : A \times B \rightarrow A & \qquad & \pi _1 : A \times B \rightarrow B \\ \pi _0(x, y) = x & & \pi _1(x, y) = y \\ \end {array}

Given cpos A and B, the product A \times B is itself a cpo, ordered by (x,y) \sqsubseteq _{X \times Y} (x',y') \quad \text {iff} \quad x \sqsubseteq _X x' \land y \sqsubseteq _Y y' with bottom value \bot _{X \times Y} being (\bot _A, \bot _B). Least upper bounds are found by taking the lubs of each component:

The projection functions \pi _0 and \pi _1 are continuous.

For continuous functions f and g, the split function \langle f, g \rangle is continuous.

Given f : A \rightarrow C and g : B \rightarrow D, we overload the \times operator for products to denote the combined function f \times g : A \times B \rightarrow C \times D, given below:

\begin {array}{l} f \times g : A \times B \rightarrow C \times D \\ f \times g = \langle f \circ \pi _0 , g \circ \pi _1 \rangle \end {array}

Express the function \mathit {juggle} (a, (b,c)) = ((a,b),c) using just our primitive combinators for projection and split.

The following properties of our projection and split functions follow from the pictorial reasoning we see on the right:

\pi _0 \circ \langle f , g \rangle = f
\pi _1 \circ \langle f , g \rangle = g
\langle \pi _0 \circ h , \pi _1 \circ h \rangle = h

Prove that the three properties in § [dt-0027] are equivalent to the universal property for products

As commuting diagram on the category \mathbf {Cpo}:

The universal property is called such because all the familiar properties of products follow from it – thinking in pictures helps to see how (Indeed, the universal property characterises products up to isomorphism):

1. \pi _0 \circ (f \times g) = f \circ \pi _0
2. \pi _1 \circ (f \times g) = g \circ \pi _1
3. (f \times g) \circ \langle h , i \rangle = \langle f \circ h, g \circ i \rangle
4. \langle f , g \rangle \circ h = \langle f \circ h, g \circ h \rangle
5. \mathsf {id}_A \times \mathsf {id}_B = \mathsf {id}_{A \times B} \quad (*)
6. (f \circ g) \times (h \circ i) = (f \times h) \circ (g \times i) \quad (**)

These last two statements (*) and (**) show that \times is a bifunctor on the category \textbf {Cpo}, i.e., a functor \textbf {Cpo} \times \textbf {Cpo} \rightarrow \textbf {Cpo}.

Show using the universal property that \langle f, g \rangle \circ h = \langle f \circ h , g \circ h \rangle

If A and B are cpos, the set of continuous functions A \twoheadrightarrow B is a cpo under the pointwise ordering: f \sqsubseteq g\;\; \text {iff}\;\; \forall a \in A.\ f(a) \sqsubseteq g(a) The intuition of this ordering in terms of information is that we increase the information content of a function overall by increasing the information content of any (or many) argument values. To prove this, we must show:

1. A \twoheadrightarrow B has a least element. \bot _{A \twoheadrightarrow B} is the constant function that returns \bot _B, i.e. \lambda a.\ \bot _B.
2. \bigsqcup X exists for all directed X \subseteq A \twoheadrightarrow B. Our lub of a set of continuous functions \bigsqcup X is the function \Phi where: \Phi (a) = \bigsqcup \{ f(a) \mid f \in X\} We must show a number of properties of this lub \Phi . Specifically:
   1. \bigsqcup \{ f(a) \mid f \in X\} exists in B.

      Proof.

      • Liam O'Connor

      We want to show that the set \{ f(a) \mid f \in X\} is directed. Take two values g(a), h(a) \in \{ f(a) \mid f \in X\}. Since X is directed, there exists a function k \in X such that g \sqsubseteq k and h \sqsubseteq k. By applying the definition of \sqsubseteq for functions above, we have g(a) \sqsubseteq k(a) and h(a) \sqsubseteq k(a). Thus k(a) is an upper bound of these two values g(a), h(a), and thus \{ f(a) \mid f \in X\} is directed, and thus its lub exists since B is a cpo.
   2. \Phi (a) = \bigsqcup \{ f(a) \mid f \in X \} is continuous.

      Proof.

      • Liam O'Connor

      Using the alternative characterisation of continuity

      \begin {array}{lclr} \Phi (\bigsqcup Y) &=& \bigsqcup \{ f(\bigsqcup Y) \mid f \in X \} & \text {(defn. $\Phi $)}\\ & = & \bigsqcup \{\bigsqcup \{ f(y) \mid y \in Y \} \mid f \in X \} & \text {($f$ is continuous)}\\ & = & \bigsqcup \{\bigsqcup \{ f(y) \mid f \in X \} \mid y \in Y \} & \text {(swap lubs)}\\ & = & \bigsqcup \{ \Phi (y) \mid y \in Y \} & \text {(defn. $\Phi $)}\\ \end {array} Monotonicity is similar to prove.
   3. \Phi is an upper bound for X \subseteq A \twoheadrightarrow B.

      Proof.

      • Liam O'Connor

      Let g \in X. Then for any a \in A we have g(a) \in \{ f(a) \mid f \in X\}. Now, by 2a and lubs, we have g(a) \sqsubseteq \bigsqcup \{ f(a) \mid f \in X \}, which by the definition of \Phi gives g(a) \sqsubseteq \Phi (a). Hence, by the definition of \sqsubseteq on functions, we can conclude g \sqsubseteq \Phi .
   4. \Phi is the least upper bound for X.

      Proof.

      • Liam O'Connor

      Let g \in A \twoheadrightarrow B be an upper bound for X \subseteq A \twoheadrightarrow B. Then (using \sqsubseteq on functions) g(a) is an upper bound for \{f(a) \mid f \in X\} for all a \in A. Now, by 2a and lubs, we have \bigsqcup \{f(a) \mid f \in X\} \sqsubseteq g(a), i.e. \Phi (a) \sqsubseteq g(a), which, by the definition of \sqsubseteq on functions, allows us to conclude \Phi \sqsubseteq g.

At each step "upwards" on this cpo, one arrow that ends in \bot now points to a non-\bot value (moving up the cpo \mathbb {B}_\bot ).

For the \twoheadrightarrow operator on cpos (Definition [dt-002F]) to be the object mapping for a bifunctor \textbf {Cpo} \times \textbf {Cpo} \rightarrow \textbf {Cpo} like \times is (see Corollary [dt-002C]), we would need to define a morphism mapping f \twoheadrightarrow g that, given two functions f : A \twoheadrightarrow B and g : C \twoheadrightarrow D, gives a function (A \twoheadrightarrow C) \twoheadrightarrow (B \twoheadrightarrow D). But such a function is not implementable: \begin {array}{l} f \twoheadrightarrow g : (A \twoheadrightarrow C) \twoheadrightarrow (B \twoheadrightarrow D) \\ (f \twoheadrightarrow g)(h)(b) =\ \textcolor {red}{???}\\ \end {array} In the above hole \textcolor {red}{???}, h : A \twoheadrightarrow C and b \in B. Given the value b \in B, none of our functions f, g or h take elements of B, so there would be no way to produce the D value required. This is because our function f : A \twoheadrightarrow B goes the wrong way. If f were a function B \twoheadrightarrow A, things would be a lot easier.

The dual of a category \mathbf {C}, written \mathbf {C}^\mathsf {op}, is a category with the same objects as \mathbf {C} but the arrows are reversed, that is, for each morphism A \xrightarrow {m} B in \mathbf {C}, there is a morphism B \xrightarrow {m} A in \mathbf {C}^\mathsf {op}.

The operator \twoheadrightarrow introduced in Definition [dt-002F] is is the object mapping for a binary functor: (\twoheadrightarrow ) : \mathbf {Cpo}^\mathsf {op} \times \mathbf {Cpo} \rightarrow \mathbf {Cpo} The category \mathbf {Cpo}^\mathsf {op} is the dual category to \mathbf {Cpo}.

Thus, a morphism A \xrightarrow {m} B in the category \mathbf {Cpo}^\mathsf {op} is a continuous function m : B \twoheadrightarrow A. Thus, the morphism mapping for our functor must take two functions f : B \twoheadrightarrow A (the morphism from \mathbf {Cpo}^\mathsf {op}) and g : C \twoheadrightarrow D (the morphism from \mathbf {Cpo}), and produce (A \twoheadrightarrow C) \twoheadrightarrow (B \twoheadrightarrow D). As with products, we will overload the \twoheadrightarrow notation for this mapping as well.

The sum construct on cpo A + B denotes a disjoint union of two cpos with a new, dedicated \bot value: A + B = \{ (0, a) \mid a \in A \} \cup \{ (1, b) \mid b \in B \} \cup \{ \bot _{A+B} \} This construct is a cpo under the ordering: x \sqsubseteq y\;\;\text {iff}\;\;\begin {cases} \text {true} & \text {if}\ x=\bot _{A+B}\\ a \sqsubseteq a' & \text {if}\ x = (0,a)\ \text {and}\ y = (0, a') \\ b \sqsubseteq b' & \text {if}\ x = (1,b)\ \text {and}\ y = (1, b') \\ \text {false} & \text {otherwise} \end {cases} Intuitively, this says that the ordering on A + B is the same as A and B separately, except that \bot _{A+B} is less than anything.

The only directed sets are those that do not contain a mixture of elements from both A and from B, so the least upper bound operator is essentially the same as the least upper bounds for A and for B. Formally: \bigsqcup X \;\; = \;\; \begin {cases} (0,\bigsqcup \{ a \mid (0,a) \in X \}) & \text {if}\ \{ a \mid (0,a) \in X \} \neq \emptyset \\ (1,\bigsqcup \{ b \mid (1,b) \in X \}) & \text {if}\ \{ b \mid (1,b) \in X \} \neq \emptyset \\ \bot _{A+B} & \text {otherwise}\\ \end {cases}

We can see by the definitions of case and our constructors that [f,g] \circ \mathit {inl} = f and [f,g] \circ \mathit {inr} = g, or, in a commutative diagram:

Note that this diagram is like the dual of the diagram seen in the universal property for products — the arrows are reversed. That is because, generally speaking, sums are dual to products. However, because of our additional \bot value, our cpo sums are only weakly universal — the h arrow is not unique.

ExampleWeak universality of cpo sums [dt-003A]

• Liam O'Connor

Consider this scenario with the cpos \textbf {2} = \{ \top , \bot \} and \textbf {1} = \{\bot \}:

In this case, setting the function h = \lambda x.\ \top makes the diagram commute, but (\lambda x.\ \top ) \neq [\lambda x.\ \top , \lambda x.\ \top ] due to the different handling of \bot _{\textbf {1}+\textbf {1}}.

With these, we can define the morphism mapping for the sum bifunctor (+) : \textbf {Cpo} \times \textbf {Cpo} \rightarrow \textbf {Cpo}. Just as with products and functions, we will overload the + notation for morphisms as well as objects in the category \mathbf {Cpo}.

The ordering and lubs are, mutatis mutandis, as with the non-strict Construction [dt-002L].

The ordering and lubs are, mutatis mutandis, as with the non-strict Construction [dt-0021]. This operator is called a smash product because the two \bot values from A and B are "smashed" into one \bot value.

The ordering and lubs are, mutatis mutandis, as with the non-strict Construction [dt-0031]. This operator is called a smash sum because the two \bot values from A and B are "smashed" into one \bot value.

The strict cpo constructions satisfy all the usual isomorphisms, including:

• (A \mathbin {\circ \hspace{-0.4em}\twoheadrightarrow } B) \times (A \mathbin {\circ \hspace{-0.4em}\twoheadrightarrow } C)\;\; \simeq \;\; A \mathbin {\circ \hspace{-0.4em}\twoheadrightarrow } (B\otimes C)
• (A \otimes B \mathbin {\circ \hspace{-0.4em}\twoheadrightarrow } C) \;\; \simeq \;\; A \mathbin {\circ \hspace{-0.4em}\twoheadrightarrow } (B \mathbin {\circ \hspace{-0.4em}\twoheadrightarrow } C)
• (A \mathbin {\circ \hspace{-0.4em}\twoheadrightarrow } C) \times (B \mathbin {\circ \hspace{-0.4em}\twoheadrightarrow } C)\;\; \simeq \;\; (A\oplus B) \mathbin {\circ \hspace{-0.4em}\twoheadrightarrow } C

The category \mathbf {Cpo_\bot } is the category where the objects are cpos, the morphisms are strict continuous functions between these cpos, and composition and identity are as in \mathbf {Cpo}.

The lifting operator (\cdot )_\bot adds a new \bot value to a cpo. That is, for a cpo X: X_\bot = X \cup \{\bot \} \quad \text {(where $\bot \notin X$)} For all x \in X (including \bot _X), our new bottom value \bot \sqsubseteq x.

With the lifting operator, we can relate the lazy constructions like product and sum with strict constructions like smash product and sum via isomorphism:

• A\twoheadrightarrow B \simeq A_\bot \mathbin {\circ \hspace{-0.4em}\twoheadrightarrow } B
• A + B \simeq A_\bot \oplus B_\bot
• (A \times B)_\bot \simeq A_\bot \otimes B_\bot

The language for Programming Computable Functions (PCF) is a variant of typed \lambda -calculus with minimal extensions to be Turing-complete. \begin {array}{lcl} e & \Coloneqq & n \mid x \mid \lambda x : \tau .\ e \mid e_1\ e_2\mid \mathsf {succ} \mid \mathsf {pred} \mid \mathsf {ifz}\ e_1\ \mathsf {then}\ e_2\ \mathsf {else}\ e_3 \mid \mathsf {fix}\ x : \tau .\ e \\ \tau & \Coloneqq & \mathsf {nat} \mid \tau _1 \rightarrow \tau _2 \end {array}

\dfrac {n \in \mathbb {N}}{\Gamma \vdash n : \mathsf {nat}}\quad \dfrac {x : \tau \in \Gamma }{\Gamma \vdash x : \tau }\quad \dfrac {\Gamma , x : \tau _1 \vdash e : \tau _2 }{ \Gamma \vdash \lambda x : \tau _1.\ e : \tau _1 \rightarrow \tau _2}\quad \dfrac {\Gamma \vdash e_1 : \tau _1 \rightarrow \tau _2 \quad \Gamma \vdash e_2 : \tau _1}{\Gamma \vdash e_1\ e_2 : \tau _2}\\[2em] \dfrac { }{ \Gamma \vdash \mathsf {succ} : \mathsf {nat} \rightarrow \mathsf {nat}}\quad \dfrac { }{ \Gamma \vdash \mathsf {pred} : \mathsf {nat} \rightarrow \mathsf {nat}}\quad \dfrac { \Gamma \vdash e_1 : \mathsf {nat} \quad \Gamma \vdash e_2 : \tau \quad \Gamma \vdash e_3 : \tau }{ \Gamma \vdash \mathsf {ifz}\ e_1\ \mathsf {then}\ e_2\ \mathsf {else}\ e_3 : \tau }\quad \dfrac { \Gamma , x : \tau \vdash e : \tau }{\Gamma \vdash \mathsf {fix}\ x : \tau .\ e : \tau }

Because PCF is typed, we shall assign denotations only to well-typed expressions. The range of our denotation function for expressions is determined by the type of its input expression. That is, the denotation of a type \tau is the cpo whose elements will be the denotations of expressions of type \tau . The denotation of the type \mathsf {nat}, then, is merely the flat domain of the natural numbers \mathbb {N}_\bot : \llbracket \mathsf {nat} \rrbracket = \mathbb {N}_\bot And, the denotation of the function type is the domain of continuous functions on cpos: \llbracket \tau _1 \rightarrow \tau _2 \rrbracket = \llbracket \tau _1 \rrbracket \twoheadrightarrow \llbracket \tau _2 \rrbracket A closed term e : \tau with no free variables denotes an element of \llbracket \tau \rrbracket , so we might be tempted to define our denotation function for expressions e : \tau like so: \llbracket e \rrbracket : \llbracket \tau \rrbracket However, if e : \tau involves free variables from our context \Gamma , the valuation of e will depend on the values assigned to all the variables. Thus, the denotation of a typed expression \Gamma \vdash e : \tau is defined instead as a continuous function: \llbracket e \rrbracket _\Gamma : \llbracket \Gamma \rrbracket \twoheadrightarrow \llbracket \tau \rrbracket where the meaning of a context \Gamma = (x_0 : \tau _0, x_1 : \tau _1,\dots , x_n : \tau _n) will be a a big n-tuple of the values assigned to each variable: \llbracket \Gamma \rrbracket = \llbracket \tau _0 \rrbracket \times \llbracket \tau _1 \rrbracket \times \cdots \times \llbracket \tau _n \rrbracket

Given an n-tuple, i.e. elements of the n-ary product X_0 \times X_1 \times X_2 \times \dots \times X_n, we typically denote the entire n-tuple as in vector notation: \vec {x} : X_0 \times X_1 \times X_2 \times \dots \times X_n And individual elements of the tuple are accessed with numeric subscripts: x_0 : X_0 \quad x_2 : X_2 \quad \cdots

We shall extend the syntax of PCF with a new type former, \tau _1 \times \tau _2 and three expression-level constructs for constructing and deconstructing pairs: \begin {array}{lcl} e & \Coloneqq & \cdots \mid (e_1,e_2) \mid \mathsf {fst}\ e \mid \mathsf {snd}\ e \\ \tau & \Coloneqq & \cdots \mid \tau _1 \times \tau _2 \end {array} Adding to our typing rules similarly: \dfrac {\Gamma \vdash e_1 : \tau _1 \quad e_2 : \tau _2}{(e_1,e_2) : \tau _1 \times \tau _2}\\[2em] \dfrac {\Gamma \vdash e : \tau _1 \times \tau _2}{\Gamma \vdash \mathsf {fst}\ e : \tau _1}\quad \dfrac {\Gamma \vdash e : \tau _1 \times \tau _2}{\Gamma \vdash \mathsf {snd}\ e : \tau _2} To extend our semantics, we make the product type \tau _1 \times \tau _2 denote the product cpo \llbracket \tau _1 \rrbracket \times \llbracket \tau _2 \rrbracket , and our expression semantics are expressed straightforwardly using our projection and split operations for products: \begin {array}{lcl} \llbracket (e_1, e_2) \rrbracket _\Gamma &=& \langle \llbracket e_1 \rrbracket _\Gamma , \llbracket e_2 \rrbracket _\Gamma \rangle \\ \llbracket \mathsf {fst}\ e \rrbracket _\Gamma & = & \pi _0 \circ \llbracket e \rrbracket _\Gamma \\ \llbracket \mathsf {snd}\ e \rrbracket _\Gamma & = & \pi _1 \circ \llbracket e \rrbracket _\Gamma \\ \end {array}

We shall extend the syntax of PCF with a new type former, \tau _1 + \tau _2 and three expression-level constructs for constructing and deconstructing sums: \begin {array}{lcl} e & \Coloneqq & \cdots \mid \mathsf {inl}\ e \mid \mathsf {inr}\ e \mid \mathsf {case}\ e_0\ \mathsf {of}\ \mathsf {inl}\ x \rightarrow e_1 ; \mathsf {inr}\ y \rightarrow e_2 \\ \tau & \Coloneqq & \cdots \mid \tau _1 + \tau _2 \end {array} Adding to our typing rules similarly: \dfrac {\Gamma \vdash e : \tau _1}{\Gamma \vdash \mathsf {inl}\ e : \tau _1 + \tau _2}\quad \dfrac {\Gamma \vdash e : \tau _2}{\Gamma \vdash \mathsf {inr}\ e : \tau _1 + \tau _2}\\[2em] \dfrac {\Gamma \vdash e_0 : \tau _1 + \tau _2 \quad \Gamma , x : \tau _1 \vdash e_1 : \tau \quad \Gamma , y : \tau _2 \vdash e_2 : \tau }{ \Gamma \vdash \mathsf {case}\ e_0\ \mathsf {of}\ \mathsf {inl}\ x \rightarrow e_1 ; \mathsf {inr}\ y \rightarrow e_2 : \tau } To extend our semantics, we make the sum type \tau _1 + \tau _2 denote the sum cpo \llbracket \tau _1 \rrbracket + \llbracket \tau _2 \rrbracket , and our expression semantics are expressed using our primitive functions for sums. \begin {array}{lcl} \llbracket \mathsf {inl}\ e \rrbracket _\Gamma & = & \mathit {inl} \circ \llbracket e \rrbracket _\Gamma \\ \llbracket \mathsf {inr}\ e \rrbracket _\Gamma & = & \mathit {inr} \circ \llbracket e \rrbracket _\Gamma \end {array} \begin {array}{l}\llbracket \mathsf {case}\ e_0\ \mathsf {of}\ \mathsf {inl}\ x \rightarrow e_1 ; \mathsf {inr}\ y \rightarrow e_2 \rrbracket _\Gamma (\vec {z}) \\ \quad = [ \boldsymbol {\lambda }v. \llbracket e_1 \rrbracket _{\Gamma ,x:\tau _1}(\vec {z},v), \boldsymbol {\lambda }v. \llbracket e_2 \rrbracket _{\Gamma ,y:\tau _2}(\vec {z},v)] (\llbracket e_0 \rrbracket _\Gamma (\vec {z}))\end {array}

Suppose we have a language with recursive data types, such as this \mathit {List} type in Haskell-style syntax: \textbf {data}\ \mathit {List} = \mathsf {Nil} \mid \mathsf {Cons}\ (\mathit {Int} \times \mathit {List}) As in PCF, the denotation of a type \tau is the domain which contains all the denotations of all closed expressions of type \tau . What, then, is the domain that corresponds to \mathit {List}\ a? We need a cpo L that satisfies the below equation (where \mathbf {1} is the cpo containing just one element \bot ): L \simeq \mathbf {1} + (\mathbb {Z}_\bot \times L)

If we take PCF, discard the type system, \textbf {fix}, natural number primitives and any other superfluous features, and just boil our language down to a minimal, Turing-complete subset, we end up with the untyped \lambda -calculus — a language consisting only of untyped functions.

Trying to give a semantics to the untyped \lambda calculus poses an issue: we can no longer rely on the type of an expression to select an appropriate semantic domain. Instead, we we must pick a single domain D which, since functions can be applied to themselves, must apparently include the set of functions D \twoheadrightarrow D: D \simeq D\twoheadrightarrow D

This recursive equation for lists: L \simeq \mathbf {1} + (\mathbb {Z}_\bot \times L) Can be expressed as the least fixed point of this mapping (specifically an endofunctor) \mathcal {F} on cpos: \mathcal {F}(A) \triangleq \mathbf {1} + (\mathbb {Z}_\bot \times A)

An endofunctor on the category \textbf {Cpo} is a functor \textbf {Cpo} \rightarrow \textbf {Cpo}, i.e. a mapping \mathcal {F} on cpos together with a mapping \mathcal {F} on continuous functions, such that:

1. If f : A \twoheadrightarrow B then \mathcal {F}(f) : \mathcal {F}(A)\twoheadrightarrow \mathcal {F}(B)
2. \mathcal {F}(\mathsf {id}_A : A\twoheadrightarrow A) = \mathsf {id}_{\mathcal {F}(A)} : \mathcal {F}(A)\twoheadrightarrow \mathcal {F}(A)
3. \mathcal {F}(f \circ g) = \mathcal {F}(f) \circ \mathcal {F}(g)

Observe that, given the information ordering for cpos where A \sqsubseteq B if there exists a continuous function A \twoheadrightarrow B, the functor laws necessarily imply monotonicity for all endofunctors \mathcal {F}.

An endofunctor \mathcal {F} is cocontinuous iff it preserves colimits of \omega -chains of cpos. That is, given a chain where A is a colimit:

A fixed point of an endofunctor on cpos \mathcal {F} is a cpo \mathcal {F} such that \mathcal {F}(A) \simeq A.

Every cocontinuous endofunctor \mathcal {F} on cpos has a least fixed point, given by the colimit of the \omega -chain:

Consider the Haskell-style data type: \textbf {data}\ \mathit {Bin} = \mathsf {Zero}\ \mathit {Bin} \mid \mathsf {Empty} \mid \mathsf {One}\ \mathit {Bin} So, e.g. \mathsf {One}\ (\mathsf {Zero}\ (\mathsf {One}\ \mathsf {Empty})) : \mathit {Bin}.

The recursive domain equation is, expressed as a fixed point: B \simeq \mathcal {F}(B)\quad \text {where}\ \mathcal {F}(X) = X + \mathbf {1} + X We wish to show that \mathcal {F} is a cocontinuous endofunctor.

We have a mapping \mathcal {F} on cpos (objects of the category \textbf {Cpo}), but for it to be a functor we additionally need a mapping \mathcal {F} on continuous functions (morphisms of the category \textbf {Cpo}).

Recalling our sum construction, we may remember that sums are already a bifunctor \textbf {Cpo} \times \textbf {Cpo} \rightarrow \textbf {Cpo} (Theorem [dt-0038]). Thus, our mapping on continuous functions \mathcal {F} can be derived from our mapping on cpos \mathcal {F} by using the morphism mapping from the sum construction (Definition [dt-0037]). Given a continuous function f : A \twoheadrightarrow B, our morphism mapping is:

Proof that this endofunctor is cocontinuous is left for the reader. Hence the semantics of the type \mathit {Bin}, i.e. \llbracket \mathit {Bin} \rrbracket : \textbf {Cpo} is the least fixed point of \mathcal {F}, i.e. the colimit of the \omega -chain:

Let us visualise this chain. Here the sum injections have been written as \textsf {Z, E, O} rather than (combinations of) \textsf {inl} and \textsf {inr} to keep the connection with the Haskell data type clear.

Thus, the nth cpo in the chain contains binary numbers with at most n defined digits. The colimit of the chain contains all binary numbers (finite, partial, and infinite!).

Show that \mathcal {F}(X) \triangleq \mathbf {1} + X and \mathcal {F}(f) \triangleq \mathsf {id}_\mathbf {1} + f (using our + operator for functions) define an endofunctor \mathbf {Cpo} \rightarrow \mathbf {Cpo}, i.e. that they satisfy the functor laws.

If we have a mapping on cpos \mathcal {F} : \textbf {Cpo} \rightarrow \textbf {Cpo} that is made up of the primitives \times , +, \otimes , \oplus , \mathbf {1} and (\cdot )_\bot , we can generate a corresponding morphism mapping on continuous functions \mathcal {F} : (A\twoheadrightarrow B) \rightarrow (\mathcal {F}(A)\twoheadrightarrow \mathcal {F}(B)) by using the corresponding morphism mappings of each of these operators. Thus any such mapping can be turned into an endofunctor.

The lazy natural numbers, also called conats, are defined as the least solution to the equation X \simeq \mathbf {1} + X.

1. Sketch the first four approximations to the least fixed point. Call the two sum injections \mathsf {zero} and \mathsf {succ}.

   Solution.

   • Liam O'Connor

   \begin {array}{lcl} A_0 & = & \{\bot \} \\ A_1 & = & \{\mathsf {zero}\ \bot , \mathsf {succ}\ \bot , \bot \} \\ A_2 & = & \{\mathsf {zero}\ \bot , \mathsf {succ}\ \bot , \mathsf {succ}\ (\mathsf {zero}\ \bot ), \mathsf {succ}\ (\mathsf {succ}\ \bot ), \bot \} \\ A_3 & = & \{\mathsf {zero}\ \bot , \mathsf {succ}\ \bot , \mathsf {succ}\ (\mathsf {zero}\ \bot ), \mathsf {succ}\ (\mathsf {succ}\ \bot ), \mathsf {succ}\ (\mathsf {succ}\ (\mathsf {zero}\ \bot )), \mathsf {succ}\ (\mathsf {succ}\ (\mathsf {succ}\ \bot )), \bot \} \\ \end {array}
2. Repeat this exercise assuming:
   1. \mathsf {zero} is strict (i.e. \mathsf {zero}\ \bot = \bot )

      Solution.

      • Liam O'Connor

      \begin {array}{lcl} A_0 & = & \{\bot \} \\ A_1 & = & \{\mathsf {succ}\ \bot , \bot \} \\ A_2 & = & \{\mathsf {succ}\ \bot , \mathsf {succ}\ (\mathsf {succ}\ \bot ), \bot \} \\ A_3 & = & \{\mathsf {succ}\ \bot , \mathsf {succ}\ (\mathsf {succ}\ \bot ), \mathsf {succ}\ (\mathsf {succ}\ (\mathsf {succ}\ \bot )), \bot \} \\ \end {array}
   2. \mathsf {succ} is strict (i.e. \mathsf {succ}\ \bot = \bot )

      Solution.

      • Liam O'Connor

      \begin {array}{lcl} A_0 & = & \{\bot \} \\ A_1 & = & \{\mathsf {zero}\ \bot , \bot \} \\ A_2 & = & \{\mathsf {zero}\ \bot , \mathsf {succ}\ (\mathsf {zero}\ \bot ), \bot \} \\ A_3 & = & \{\mathsf {zero}\ \bot , \mathsf {succ}\ (\mathsf {zero}\ \bot ), \mathsf {succ}\ (\mathsf {succ}\ (\mathsf {zero}\ \bot )), \bot \} \\ \end {array}

We cannot get morphism mappings in the category \textbf {Cpo} as easily as § [dt-0050] when our object mapping makes use of the function operators \mathbin {\circ \hspace{-0.4em}\twoheadrightarrow } and \twoheadrightarrow , as they are contravariant in their first argument. This means the functor that they extend to is not \textbf {Cpo} \rightarrow \textbf {Cpo} but \textbf {Cpo}^\textsf {op} \rightarrow \textbf {Cpo}, where \textbf {Cpo}^\textsf {op} is the dual category of \textbf {Cpo}. The morphisms end up the wrong way around.

As an example, consider \mathcal {F}(X) = X\twoheadrightarrow \mathbb {Z}_\bot . Then, recalling the morphism mapping of the \twoheadrightarrow functor: \dfrac {f : A \twoheadrightarrow B \quad g : C\twoheadrightarrow D}{f\twoheadrightarrow g : (B\twoheadrightarrow C)\twoheadrightarrow (A\twoheadrightarrow D)} We can generate a morphism mapping for \mathcal {F}: \mathcal {F}(f)\; =\; f\twoheadrightarrow \mathsf {id}_{\mathbb {Z}_\bot }\; =\; (\lambda h.\ \mathsf {id}_{\mathbb {Z}_\bot }\circ h \circ f)\; = \;(\lambda h.\ h \circ f) However, this mapping has the wrong type. For f : A\twoheadrightarrow B, then \mathcal {F}(f) : (B\twoheadrightarrow \mathbb {Z}_\bot ) \rightarrow (A\twoheadrightarrow \mathbb {Z}_\bot ), which is \mathcal {F}(B)\twoheadrightarrow \mathcal {F}(A), not the required \mathcal {F}(A)\twoheadrightarrow \mathcal {F}(B). This is because the generated functor is contravariant, not covariant.

Show that, in contrast to \mathcal {F}(X) = X\twoheadrightarrow \mathbb {Z}_\bot from Problem [dt-0053], the mapping \mathcal {G}(X) = \mathbb {Z}_\bot \twoheadrightarrow X can be extended to continuous functions giving a covariant endofunctor on \textbf {Cpo}.

A retraction pair (f,g) on cpos A to B consists of two continuous functions A \xtofrom [g]{f} B such that:

1. g \circ f = \mathsf {id}_A\quad (i.e. \forall x \in A.\ g(f(x)) = x )
2. f \circ g \sqsubseteq \mathsf {id}_B\quad (i.e. \forall y \in B.\ f(g(y)) \sqsubseteq y )

Retraction pairs are weakenings of isomorphisms. Intuitively, going A \twoheadrightarrow B\twoheadrightarrow A, all information is preserved due to requirement 1, but going B\twoheadrightarrow A\twoheadrightarrow B, we may lose some information (hence the use of \sqsubseteq in requirement 2).

Here are two examples of retraction pairs:

The following, however, are not retraction pairs A \xtofrom [g]{f} B:

(y \mapsto b \mapsto z but z \not \sqsubseteq y)	(b \mapsto x \mapsto a but a \neq b)

We can compose retraction pairs by composing their embedding and projection:

It follows from the definition of retraction pairs that, for a pair \xtofrom [g]{f}:

1. f and g are strict, i.e. f(\bot ) = \bot and g(\bot ) = \bot .
2. g is uniquely determined by f and vice-versa, so if another retraction pair \xtofrom [g']{f} exists, then g = g'. To see why, remember that f and g must be continuous and therefore monotonic.
3. A is isomorphic to the range of f, i.e. A \simeq \{ f(x) \mid x \in A\} \subseteq B.

The category \textbf {Cpo}^\textbf {R} is the category where the objects are cpos, the morphisms are retraction pairs, composition is as in Definition [dt-0056] and identity is just the retraction pair A \xtofrom [\lambda x. x]{\lambda x. x} A.

The third point in Corollary [dt-0057] suggests a notion of approximation, or information ordering, for cpos. Rather than say, as we did in § [dt-004O], that for cpos A and B, A \sqsubseteq B iff there exists a continuous function A\twoheadrightarrow B, we now say:

All of our other notions for \textbf {Cpo} naturally generalise to a setting with retraction pairs \textbf {Cpo}^\textbf {R}: least elements, \omega -chains, upper bounds, colimits, cocontinuous endofunctors and so on.

Definition\omega -chains of cpos in the category \mathbf {Cpo}^\textbf {R} [dt-005C]

• Liam O'Connor

An \omega -chain of cpos in the category \mathbf {Cpo}^\textbf {R} consists of a family of cpos \{D_i \mid i \in \mathbb {N} \}, together with a family of retraction pairs D_i \xtofrom [g_i]{f_i} D_{i+1}, shown below:

DefinitionUpper bounds in the category \mathbf {Cpo}^\mathbf {R} [dt-005G]

A cpo A is an upper bound of an \omega -chain of cpos A_i in the category \mathbf {Cpo}^\textbf {R} if there is a family of retraction pairs A_i \xtofrom [g_i]{f_i} A such that the following diagram commutes (i.e. for all i \in \mathbb {N}, (f_i, g_i) = (f_{i+1},g_{i+1}) \circ (s_i,t_i), where \circ is composition of retraction pairs):

DefinitionCocontinuous endofunctors on \textbf {Cpo}^\textbf {R} [dt-005E]

An endofunctor \mathcal {F} is cocontinuous iff it preserves colimits of \omega -chains of cpos. That is, given a chain where A is a colimit:

Then \mathcal {F}(A) is a colimit for the following chain:

If \mathcal {F} is a mapping on cpos built up from basic cpos using the constructions \times , \otimes , +, \oplus , (\cdot )_\bot , as well as \twoheadrightarrow and \mathbin {\circ \hspace{-0.4em}\twoheadrightarrow }, then \mathcal {F} extends to a (covariant!) cocontinuous functor on \textbf {Cpo}^\mathbf {R}. We shall detail the construction for products and functions here, but the other constructions are all similar.

Every cocontinuous endofunctor \mathcal {F} on \mathbf {Cpo}^\textbf {R} has a least fixed point, given by the colimit of the ascending \omega -chain:

Given an \omega -chain:

The colimit (or inverse limit) is the cpo of \omega -tuples: D_\infty \; \triangleq \; \left \{ (x_0, x_1, \dots ) \mid x_i \in D_i \land x_i = g_i(x_{i+1}) \right \} That is, it is countable sequence of elements, one for each domain D_i, where each element is consistent with earlier elements.

Ordering: The ordering is the pointwise ordering of products, naturally generalised to \omega -tuples. Under this ordering, D_\infty is a cpo. In fact if each D_i is a Scott domain, so is D_\infty .

Proof.

• Liam O'Connor

We shall prove that D_\infty is an upper bound of the \omega -chain. Proof that it is the least upper bound is straightforward but tedious, and is omitted.

We must construct a family of retraction pairs: \left \{ D_i \xtofrom [\theta _{\infty ,i}]{\theta _{i,\infty }} D_\infty \middle |\;\; i \in \mathbb {N}\;\; \right \} such that the following diagram commutes:

Defining the projection of the retraction pair D_i \xtofrom [\theta _{\infty ,i}]{\theta _{i,\infty }} D_\infty is straightforward: \theta _{\infty ,i}(x_0,x_1,\dots ) \; \triangleq \; x_i However, to define the embedding \theta _{i,\infty } requires us to, for a given value x \in D_i, produce an \omega -tuple of values consistent with x in every domain D_k. We do this by defining \theta _{i,\infty } in terms of helper functions \theta _{i,j}: \theta _{i,\infty }(x) \; \triangleq \; (\theta _{i,0}(x),\theta _{i,1}(x),\theta _{i,2}(x),\dots ) The helper functions \theta _{i,j} are defined by composing sequences of embeddings (fs) or projections (gs), depending on whether i < j or j < i. For example, when i = 2: \begin {array}{lcl} \theta _{2,\infty }(x) &=& (\theta _{i,0}(x),\theta _{i,1}(x),\theta _{i,2}(x),\theta _{i,3}(x),\theta _{i,4}(x),\dots ) \\[1em] &=& (\underbrace {g_0(g_1(x))), g_1(x)}_{\text {\emph {approximations} to}\ x}, x, \underbrace {f_2(x), f_3(f_2(x)),\dots }_{\text {\emph {equivalent} to}\ x}) \end {array}

Untyped \lambda -calculus consists only of untyped (higher-order) functions: e \; \Coloneqq \; x \mid \lambda x. e \mid e_1\ e_2

Using the new functions \textbf {\textsf {up}} and \textbf {\textsf {down}}, it is now straightforward to define a semantics for untyped \lambda -calculus, where \sigma is an environment \mathsf {Var} \rightarrow D_\infty : \llbracket \cdot \rrbracket : (\mathsf {Var} \rightarrow D_\infty )\twoheadrightarrow D_\infty \begin {array}{lcl} \llbracket x \rrbracket \sigma & = & \sigma (x) \\ \llbracket e_0\ e_1 \rrbracket \sigma & = & \textbf {\textsf {up}}(\llbracket e_0 \rrbracket \sigma ) (\llbracket e_1 \rrbracket \sigma )\\ \llbracket \lambda x.\ e \rrbracket \sigma & = & \textbf {\textsf {down}}(\boldsymbol {\lambda } v \in D_{\infty }.\ \llbracket e \rrbracket \ \sigma (x \mapsto v) ) \end {array} This semantics does not distinguish non-terminating computations from terminating ones. To model call-by-value more faithfully, we could use the equation D \simeq D\twoheadrightarrow D_\bot instead, and for call-by-name we could use D \simeq D_\bot \twoheadrightarrow D_\bot . The constructions are very similar.

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 \mid \mathsf {while}\ \mathcal {B}\ \mathsf {do}\ \mathcal {C}\ \mathsf {od}\\ x & \in & \mathcal {V}\; \textit {(variables)}\\ n & \in & \mathbb {N} \end {array}

A monad on the category \textbf {C} consists of an endofunctor \mathcal {M} : \textbf {C} \rightarrow \textbf {C} and two operations (natural transformations) for all \mathbf {C}-objects X: \mu _X : \mathcal {M}(\mathcal {M}(X)) \rightarrow \mathcal {M}(X) and \eta _X : X \rightarrow \mathcal {M}(X), such that the following diagrams commute:

1. \mu _X \circ \mathcal {M}(\mu _X) = \mu _X \circ \mu _{\mathcal {M}(X)}
2. \mu _X \circ \mathcal {M}(\eta _X) = \mu _X \circ \eta _{\mathcal {M}(X)} = \mathsf {id}_{\mathcal {M}(X)}

The flat domain lifting operation (\cdot )_\bot forms a monad, where the endofunctor \mathcal {M}(X) = X_\bot , the operation \mu _X : (X_\bot )_\bot \rightarrow X_\bot collapses the two \bot values, and \eta _X : X \rightarrow X_\bot is simply \eta _X(x) = x.

For a monad (\mathcal {M}, \mu , \eta ) over the category \mathbf {C}, the Kleisli category has the same objects as \mathbf {C}, but the morphisms A \xrightarrow {h} B are those morphisms h of \mathbf {C} that have the form A \xrightarrow {h} \mathcal {M}(B). Composition is defined as follows, for morphisms A \xrightarrow {f} \mathcal {M}(B) and B \xrightarrow {g} \mathcal {M}(C): g \circ _K f = \mu _C \circ \mathcal {M}(g) \circ f Identity morphisms for this category are just \eta .

We define our semantics generically in terms of a monad (\mathcal {M},\mu ,\eta ), using the Kleisli composition operator for \mathcal {M}: \begin {array}{l} \mathsf {ite} : (\Sigma \rightarrow \mathbb {B}) \times (\Sigma \rightarrow \mathcal {M}(\Sigma )) \times (\Sigma \rightarrow \mathcal {M}(\Sigma )) \rightarrow (\Sigma \rightarrow \mathcal {M}(\Sigma ))\\ \mathsf {ite}(b,t,e)(\sigma ) = \begin {cases}t(\sigma ) & \text {if}\ b(\sigma ) = T \\ e(\sigma ) & \text {otherwise} \end {cases} \end {array} \begin {array}{lcl} \llbracket \cdot \rrbracket _\mathcal {C} : \mathcal {C} \rightarrow \Sigma \rightarrow \mathcal {M}(\Sigma )\\[0.4em] \llbracket \mathsf {skip} \rrbracket _\mathcal {C} & = & \eta _\Sigma \\ \llbracket x := e \rrbracket _\mathcal {C} & = & \boldsymbol {\lambda } \sigma .\ \eta _\Sigma (\sigma \left (x \mapsto \llbracket e \rrbracket _\mathcal {E}\right )) \\ \llbracket c_1 ; c_2 \rrbracket _\mathcal {C} & = & \llbracket c_2 \rrbracket _\mathcal {C} \circ _K \llbracket c_1 \rrbracket _\mathcal {C} \\[0.3em] \llbracket \textsf {if}\ b\ \textsf {then}\ c_1\ \textsf {else}\ c_2 \rrbracket _\mathcal {C} & = & \mathsf {ite}(\llbracket b \rrbracket _\mathcal {B},\llbracket c_1 \rrbracket _\mathcal {C},\llbracket c_2 \rrbracket _\mathcal {C})\\ \llbracket \textsf {while}\ b\ \textsf {do}\ c\ \textsf {od} \rrbracket _\mathcal {C} & = & \mathbf {\mathbf {fix}}(\boldsymbol {\lambda } f.\ \mathsf {ite}(\llbracket b \rrbracket _\mathcal {B}, f \circ _K \llbracket c \rrbracket _\mathcal {C}, \eta _\Sigma ) ) \end {array}

Instantiating our monadic semantics where the monad \mathcal {M} is flat domain lifting, we recover our original semantics of \mathcal {C}.

Let us instantiate our monadic semantics with the monad \mathcal {M}(X) = X_\bot \oplus \mathbf {1}, where the added value (from \mathbf {1}) is called \mathsf {fail}. The operation \mu _X : (X_\bot \oplus \mathbf {1})_\bot \oplus \mathbf {1} \rightarrow X_\bot \oplus \mathbf {1} collapses the two possible \bot values to \bot and the two possible \mathsf {fail} values to \mathsf {fail}, and the operation \eta _X : X \rightarrow X_\bot \oplus \mathbf {1} is the straightforward injection.

Then we may extend our language with lightweight exception constructs: \mathcal {C} ::= \dots \mid \mathsf {throw} \mid \mathsf {try}\ \mathcal {C}_1\ \mathsf {catch}\ \mathcal {C}_2 and define their semantics, leaving our existing semantics unchanged: \begin {array}{lcl} \llbracket \mathsf {throw} \rrbracket \ \sigma &=& \mathsf {fail} \\ \llbracket \mathsf {try}\ c_1\ \mathsf {catch}\ c_2 \rrbracket \ \sigma &=& \begin {cases} \llbracket c_2 \rrbracket \ \sigma & \text {if}\ \llbracket c_1 \rrbracket \ \sigma = \mathsf {fail} \\ \llbracket c_1 \rrbracket \ \sigma & \text {otherwise}\end {cases} \end {array}

When modelling programming languages we sometimes require a way to be imprecise about some aspects of a program — usually, this takes the form of non-determinism. Non-determinism can be hard for beginners to grasp, but it typically has to be employed when modelling real programs. For example, suppose we had a greeting program that differed depending on the physical location of the computer: \begin {array}{l} \textsf {\textbf {if}}\ \mathit {currentLocation}() = \text {Korea}\ \textsf {\textbf {then}} \\ \quad \textsf {\textbf {say}}\ \text {``안녕하세요''} \\ \textsf {\textbf {else}} \\ \quad \textsf {\textbf {say}}\ \text {``Hello!''}\\ \textsf {\textbf {fi}} \end {array} If we wanted to mathematically model the behaviour of this program, it would be frightfully inconvenient to include the geography of Earth and the computer's physical location in our model. That's where non-determinism comes in. If we abstract away from the geographical details, and instead regard the program as choosing between the two options based on some unspecified criteria, then we can get away with modelling less, at the cost of some detail: \begin {array}{l} \textsf {\textbf {if}}\ \mathit {???}\ \textsf {\textbf {then}} \\ \quad \textsf {\textbf {say}}\ \text {``안녕하세요''} \\ \textsf {\textbf {else}} \\ \quad \textsf {\textbf {say}}\ \text {``Hello!''}\\ \textsf {\textbf {fi}} \end {array} Such underspecified conditionals are usually called non-deterministic choice, where our conditional \textsf {\textbf {if}}\ \mathit {???}\ \textsf {\textbf {then}}\ P\ \textsf {\textbf {else}}\ Q\ \textsf {\textbf {fi}} is written simply as P + Q.

While we tend to view our physical machines as deterministic automata, the state upon which each decision is deterministically made includes a number of external things which are tedious to model mathematically. We can also use non-determinism to ignore details that we don't care about for our particular domain — a common example is memory allocation, where it is very convenient (for some programs) to think of memory as infinite, and allocation as an operation that can potentially fail, without specifying exactly when and how this failure can occur. This is normally modelled as a choice between successful allocation and a failure state.

Our initial semantics for \mathcal {C} (without loops) was functions on states \Sigma \rightarrow \Sigma . When adding loops, we used a cpo \Sigma \twoheadrightarrow \Sigma _\bot for our semantic domain. Since non-deterministic programs can have more than one outcome, a natural choice of semantic domain would be \Sigma \twoheadrightarrow \mathcal {P}(\Sigma _\bot ) \setminus \emptyset , i.e., functions from an initial state to a non-empty set of possible outcomes.

We can provide \eta and \mu operations for our proposed monad for non-determinism \mathcal {M}(X) = \mathcal {P}(X_\bot ) \setminus \emptyset : \begin {array}{l} \eta : X \rightarrow \mathcal {P}(X_\bot ) \setminus \emptyset \\ \eta (x) = \{ x \}\\ \mu : \mathcal {P}{((\mathcal {P}(X_\bot ) \setminus \emptyset )_\bot )}\rightarrow \mathcal {P}(X_\bot ) \setminus \emptyset \\ \mu (S) = (\bigcup _{X \neq \bot \in S} X) \cup (S \cap \{ \bot \}) \end {array} And, with this semantics, we can easily add a denotation for a non-deterministic choice operator, in terms of union: \llbracket c_1 + c_2 \rrbracket _\mathcal {C} = \lambda \sigma . \llbracket c_1 \rrbracket _\mathcal {C} \sigma \cup \llbracket c_2 \rrbracket _\mathcal {C} \sigma Unfortunately this is only the beginning of our troubles. While we have given a valuation function above, its definition uses \textbf {fix}, and therefore our domain \Sigma \rightarrow \mathcal {M}(\Sigma ) must be a cpo, and all our operations continuous. It is not clear how to order elements of \mathcal {P}(X_\bot ) \setminus \emptyset . A natural choice of ordering would be subset inclusion \subseteq . However, as we lack \emptyset , there is no least element for this ordering. Furthermore, simply using \subseteq as our ordering would mean that the deterministic, terminating program that always returns a single state \{ \sigma \} would be considered less informative than the program that may diverge \{ \bot , \sigma \}. This would make most of our operations non-continuous.

Instead, we shall examine three separate orderings on this set, each of which carries a different view of non-determinism. More generally, we wish to come up with a construction analogous to the powerset operator \mathcal {P}, but for our semantic domains — a powerdomain. However, for these orderings to produce valid partial orders, we require a certain theorem that only applies to a certain class of cpos, called "algebraic" cpos. Thus, we will first introduce a richer class of cpos, called Scott domains, and then return to the problem of non-determinism.

We begin by formalising the notion of an element in a cpo representing a finite amount of information.

Following the above intuition, we might be tempted to say that the "infinite" elements of a cpo are those which are the lub of an interesting set, but this notion is too weak. Consider this cpo X:

In the example cpo X above, all the elements except \infty and x would be compact. Thus, compactness better captures our notion of an element representing a finite amount of information. This understanding of compact elements is a generalisation of the notion of a finite element from the theory of algebraic lattices.

ExampleCompact elements with infinitely many approximations [dt-003X]

• Liam O'Connor

Compact elements may still have an infinite number of approximations. Consider the cpo \mathbb {N} \cup \{ \infty , \infty + 1 \}, where we have tacked on an additional top element \infty + 1 to our normal cpo of natural numbers extended with infinity. Then, while \infty is not compact, \infty + 1 is compact — it is not the lub of an interesting directed set. If \infty + 1 is the lub of a set X then \infty + 1 must be in the set X. Nonetheless, there are an infinite number of approximations to \infty + 1, i.e., elements x such that x \sqsubseteq \infty + 1.

As an aside, requiring that our compact elements have a truly finite number of approximations is the basis for the theory of Berry domains and stable functions.