Definition. Composition of retraction pairs [dt-0056]

Liam O'Connor

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

Context

From $\textbf {Cpo}$ to $\textbf {Cpo}^{\textbf {R}}$ [dt-0052]

Liam O'Connor

Problem. Contravariance in the function arrow [dt-0053]

Liam O'Connor

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.

Exercise. [dt-005O]

Liam O'Connor

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}$ .

Solution.

Liam O'Connor

Given a continuous function $f : A \twoheadrightarrow B$ , we must produce a continuous function $\mathcal {F}(f) : (\mathbb {Z}_\bot \twoheadrightarrow A) \twoheadrightarrow (\mathbb {Z}_\bot \twoheadrightarrow B)$ , defined as follows: $\mathcal {F}(f)(g)(x) = f \circ g(x)$ Composition of continuous functions preserves continuity. The functor laws can be shown straightforwardly.

Definition. Retraction pair [dt-0054]

Liam O'Connor

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

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

In this retraction pair,

f

is called a embedding and

g

is called a projection.

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).

Example. Examples and counterexamples of retraction pairs [dt-0055]

Liam O'Connor

Here are two examples of retraction pairs:

(this demonstrates that there can be many retraction pairs

A \xtofrom [g]{f} B

)

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$ )

Definition. Composition of retraction pairs [dt-0056]

Liam O'Connor

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

Corollary. Derived products of retraction pairs [dt-0057]

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

$f$ and $g$ are strict, i.e. $f(\bot ) = \bot$ and $g(\bot ) = \bot$ .
$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.
$A$ is isomorphic to the range of $f$ , i.e. $A \simeq \{ f(x) \mid x \in A\} \subseteq B$ .

Definition. The category $\textbf {Cpo}^\textbf {R}$ [dt-0058]

Liam O'Connor

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$ .

Definition. Information ordering in $\textbf {Cpo}^\textbf {R}$ [dt-0059]

Liam O'Connor

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:

A \sqsubseteq B

iff there exists a retraction pair

A \xtofrom [g]{f} B

Generalising to $\textbf {Cpo}^\textbf {R}$ [dt-005A]

Liam O'Connor

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:

Definition. Endofunctors on $\textbf {Cpo}^\textbf {R}$ [dt-005D]

Liam O'Connor

An endofunctor on the category $\textbf {Cpo}^\textbf {R}$ is a functor $\textbf {Cpo}^\textbf {R} \rightarrow \textbf {Cpo}^\textbf {R}$ , i.e. a mapping $\mathcal {F}$ on cpos together with a mapping $\mathcal {F}$ on retraction pairs, such that:

If $(f,g)$ is a retraction pair $A \xtofrom [g]{f} B$ then $\mathcal {F}(f,g)$ is a retraction pair $\mathcal {F}(A)\xtofrom []{} \mathcal {F}(B)$
$\mathcal {F}(\mathsf {id}_A : A\xtofrom []{} A) = \mathsf {id}_{\mathcal {F}(A)} : \mathcal {F}(A)\xtofrom []{} \mathcal {F}(A)$
$\mathcal {F}(f \circ g) = \mathcal {F}(f) \circ \mathcal {F}(g)$

\circ

composition of retraction pairs

Definition. Upper 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):

Definition. Colimits in the category $\mathbf {Cpo}^\mathbf {R}$ [dt-005F]

Liam O'Connor

A cpo $A$ is the colimit of an $\omega$ -chain of cpos $A_i$ if is both an upper bound, i.e. there exists retraction pairs $(f_i,g_i) : A_i \xtofrom []{} A$ , and for any other upper bound $B$ , for which there will exist retraction pairs $(m_i,n_i) : A_i \xtofrom []{} B$ , there exists a unique retraction pair $A \xtofrom [k']{k} B$ such that $(m_i,n_i) = (k,k') \circ (f_i,g_i)$ for all $i \in \mathbb {N}$ , where $\circ$ is composition of retraction pairs. Viewed diagramatically, it is the same as Definition [dt-004S] where continuous functions are replaced by retraction pairs.

Definition. Cocontinuous 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:

Extending cpo Mappings to endofunctors on $\textbf {Cpo}^\mathbf {R}$ [dt-005I]

Liam O'Connor

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.

Definition. $\times$ operation for retraction pairs [dt-005J]

Liam O'Connor

Given two retraction pairs $(f,g)$ and $(h,i)$ , our retraction pair for their product is just the product of their embedding and projection, i.e. $(f \times h, g \times i)$ , using our product operation on continuous functions: $\dfrac {A \xtofrom [g]{f} B\quad C \xtofrom [i]{h} D}{A\times C \xtofrom [g \times i]{f \times h} B \times D}$

Definition. $\twoheadrightarrow$ operation for retraction pairs [dt-005K]

Liam O'Connor

We are given two retraction pairs $A \xtofrom [g]{f} B$ and $C \xtofrom [i]{h} D$ . To define a suitable covariant functor, we define our morphism mapping in terms of our $\twoheadrightarrow$ operation on continuous functions: $(f,g) \twoheadrightarrow (h,i) \; \triangleq \; (g\twoheadrightarrow h, f \twoheadrightarrow i)$ Note that the positions of $f$ and $g$ are swapped in the above definition. $\dfrac {A \xtofrom [g]{f} B \quad C \xtofrom [i]{h} D}{A \twoheadrightarrow C \xtofrom [f \twoheadrightarrow i]{g \twoheadrightarrow h} B \twoheadrightarrow D}$ Unlike with the category $\textbf {Cpo}$ , this functor is not contravariant but covariant: Note the positions of $A$ and $B$ are not swapped!

Theorem. Fixed point theorem for endofunctors on $\textbf {Cpo}^\textbf {R}$ [dt-005B]

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

Where the retraction pairs

(f_i, g_i)

are defined by:

\begin {array}{lcl} (f_0,g_0) & \triangleq & (\lambda x. \bot , \lambda x. \bot )\\ (f_{i+1},g_{i+1}) & \triangleq & \mathcal {F}(f_i,g_i) \\ \end {array}

Construction. The colimit $D^\infty$ [dt-005H]

Liam O'Connor

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 (

f

s) or projections (

g

s), 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}

Backlinks

Definition. Colimits in the category $\mathbf {Cpo}^\mathbf {R}$ [dt-005F]

Liam O'Connor

A cpo $A$ is the colimit of an $\omega$ -chain of cpos $A_i$ if is both an upper bound, i.e. there exists retraction pairs $(f_i,g_i) : A_i \xtofrom []{} A$ , and for any other upper bound $B$ , for which there will exist retraction pairs $(m_i,n_i) : A_i \xtofrom []{} B$ , there exists a unique retraction pair $A \xtofrom [k']{k} B$ such that $(m_i,n_i) = (k,k') \circ (f_i,g_i)$ for all $i \in \mathbb {N}$ , where $\circ$ is composition of retraction pairs. Viewed diagramatically, it is the same as Definition [dt-004S] where continuous functions are replaced by retraction pairs.

Definition. Endofunctors on $\textbf {Cpo}^\textbf {R}$ [dt-005D]

Liam O'Connor

An endofunctor on the category $\textbf {Cpo}^\textbf {R}$ is a functor $\textbf {Cpo}^\textbf {R} \rightarrow \textbf {Cpo}^\textbf {R}$ , i.e. a mapping $\mathcal {F}$ on cpos together with a mapping $\mathcal {F}$ on retraction pairs, such that:

If $(f,g)$ is a retraction pair $A \xtofrom [g]{f} B$ then $\mathcal {F}(f,g)$ is a retraction pair $\mathcal {F}(A)\xtofrom []{} \mathcal {F}(B)$
$\mathcal {F}(\mathsf {id}_A : A\xtofrom []{} A) = \mathsf {id}_{\mathcal {F}(A)} : \mathcal {F}(A)\xtofrom []{} \mathcal {F}(A)$
$\mathcal {F}(f \circ g) = \mathcal {F}(f) \circ \mathcal {F}(g)$

\circ

composition of retraction pairs

Definition. The category $\textbf {Cpo}^\textbf {R}$ [dt-0058]

Liam O'Connor

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$ .

Definition. Upper 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):

Related

Definition. Retraction pair [dt-0054]

Liam O'Connor

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

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

In this retraction pair,

f

is called a embedding and

g

is called a projection.

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).