A complete partial order or cpo (more specifically a directed complete partial order or dcpo) is a poset where lubs exist for the empty set and for all directed subsets. That is, a cpo is a poset A such that:

1. A has a bottom element \bot \in A, that is the lub of the empty set, and
2. \bigsqcup X exists for all directed X \subseteq A.

In Definition [dt-001D] we defined cpos in terms of directed completeness. We may consider chain completeness instead, where, rather than require lubs for every directed subset of our poset A, we require lubs for every chain X \subseteq A. We know from Theorem [dt-0012] that all chains are directed, so every directed complete cpo is also chain complete. It is also known that every chain complete cpo is also directed complete, so the notions are equivalent, although the proof is non-trivial, relying on transfinite induction (see these lecture notes for details).

If we weaken our completeness requirement to require lubs only for the countable \omega -chains and not necessarily all chains, we get what is called an \omega -cpo. All \omega -chains are chains and are therefore directed, but not all chains are \omega -chains.

Working with just \omega -cpos is common in denotational semantics practice, but working with directed completeness simplifies some of the properties we will discuss later.

For each of the following posets, determine if it is a cpo or not. If it is, describe the lubs. If it is not, give a directed set which has no lub.

1. A finite pointed poset
2. (\mathcal {P}(S), \subseteq ) for some set S
3. (\mathbb {N},\leq )
4. (\mathbb {N} \cup \{\infty \}, \leq )
5. ([0,1] \subseteq \mathbb {R}, \leq )
6. ([0,1) \subseteq \mathbb {R}, \leq )
7. (\mathbb {Q}, \leq )
8. A flat domain S_\bot for some set S.

The limit of the ascending Kleene chain of a monotonic function f : X \rightarrow X is the same as the least upper bound of the set \{ f^n(\bot ) \mid n \in \mathbb {N}\} (where f^n is the n-fold self-composition of the function f). If we require that our semantic domain X is a cpo, we know that this limit exists.

1. Show that if A and B are posets and X \subseteq A \times B is directed (by the ordering in Construction [dt-000E]), then the subsets \pi _0(X) \subseteq A and \pi _1(X) \subseteq B (defined below) are also directed. \begin {array}{lcl} \pi _0(X) & = & \{ a \in A \mid \exists b \in B.\ (a,b) \in X \}\\ \pi _1(X) & = & \{ b \in B \mid \exists a \in A.\ (a,b) \in X \}\\ \end {array}

   Solution.

   • Liam O'Connor

   Given two elements x,y \in \pi _0(X), we know that there exists b_x, b_y \in B such that (x,b_x) \in X and (y,b_y) \in X. Because X is directed, we can conclude that there exists an upper bound (z, b_z) \in X where x \sqsubseteq z and y \sqsubseteq z. As z \in \pi _0(X), z is an upper bound in \pi _0(X) for both x and y and thus \pi _0(X) is directed. The proof for \pi _1 is analogous.

2. Give an example of a set X \subseteq \{\top ,\bot \}\times \{\top ,\bot \} such that \pi _0(X) and \pi _1(X) are directed, but X is not.

   Solution.

   • Liam O'Connor

   X = \{(\top ,\bot ), (\bot ,\top )\} is not directed as the two elements are not comparable, but \pi _0(X) = \pi _1(X) = \{\top ,\bot \} which is directed as \bot \sqsubseteq \top .

3. Show that if A and B are cpos and X \subseteq A \times B is directed, then \bigsqcup X = \left (\bigsqcup \pi _0(X), \bigsqcup \pi _1(X)\right ) Note: Together with \bot _{A\times B} = (\bot _A, \bot _B) this shows that the Cartesian product of two cpos is itself a cpo.

Solution.

• Liam O'Connor

Let (x,y) = \left (\bigsqcup \pi _0(X), \bigsqcup \pi _1(X)\right ). Because of the ordering in Construction [dt-000E], (x,y) is certainly a upper bound of the directed set X. To show it is the least upper bound, assume for the sake of contradiction that (x,y) is not the least upper bound of X. Then, there must be a (v,w)\sqsubset (x,y) such that \forall x \in X.\ x \sqsubseteq (v,w). But then, v would be a lesser upper bound for \pi _0(X) than x, which is supposed to be the lub. Thus there is a contradiction, and (x,y) must be the lub of X.