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.