Example. Binary Numbers [dt-004Y]

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