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}