Complete Partial Order

Definition

A complete partial order is a partially ordered set with enough suprema to interpret limits of approximations.

In common domain-theoretic usage, a complete partial order is a poset $(D,\le )$ such that:

• it has a least element $\perp$
• every directed subset $S\subseteq D$ has a supremum $\bigvee S$

The element $\perp$ is pronounced “bottom”.

Directed subsets

A subset $S\subseteq D$ is directed if it is non-empty and every pair of elements has a common upper bound in $S$. Concretely, this means:

$\forall x,y\in S.\exists z\in S.x\le z\text{ and }y\le z.$

Intuitively, a directed set is a family of compatible approximations: any two pieces of information can be jointly extended.

Omega-CPO

An $\omega$-complete partial order is weaker: it only requires suprema of $\omega$-chains, that is, monotone sequences indexed by $\mathbb{N}$,

$x_0\le x_1\le x_2\le \cdots$

Categorically this are represented by a diagrams from $([\alpha ],{\le }_{\mathrm{Ord}})$ to $(A_{\perp },{\le }_{A_{\perp }})$.

This is weaker than requiring suprema of arbitrary countable chains, since a countable chain may have order type other than $\omega$.

Every complete partial order in the directed-complete sense is an $\omega$-complete partial order, but not conversely.

Computational meaning

In semantics of computation, elements of a complete partial order are often viewed as partial pieces of information.

The order

$x\le y$

means that $y$ is at least as defined or informative as $x$. The bottom element $\perp$ represents no information, undefinedness, or divergence.

A recursive computation can then be approximated by the chain

$\perp \le f(\perp )\le f^2(\perp )\le f^3(\perp )\le \cdots$

and its denotation is the supremum of that chain.

Example

Let

${\mathbb{N}}_{\perp }=\{\perp \}\cup \mathbb{N}$

with order given by

$\perp \le n$

for every $n\in \mathbb{N}$, and no order relation between distinct natural numbers.

Thus:

$\perp \le 0,\perp \le 1,\perp \le 2,\dots$

but $0$ and $1$ are incomparable. This models a computation that has either not yet produced an answer or has terminated with a definite natural number.

Convention

There is some variation in terminology.

• Some authors use CPO for a directed poset with suprema of directed subsets.
• Some additionally require a least element $\perp$.
• Some reserve dcpo for the directed-complete notion and use $\omega$-CPO for the countable-chain version.

So the safest phrasing is to state explicitly whether one means directed-complete or only $\omega$-complete, and whether a bottom element is included.

Related Concepts

• Partial Order
• Directed Poset
• Supremum and Infimum
• Fixed Point
• Partiality Monad