PLS Lab

Directed Complete Partial Order

A partial order (D, \sqsubseteq) is directed complete (or a dcpo) just if it has least upper bounds for every directed subset.

What is a directed subset?

Let S \subseteq D be a nonempty subset of D. S is directed whenever every pair x, y \in S has an upper bound in S, i.e. an element z \in S such that x \sqsubseteq z and y \sqsubseteq z.

Directedness means that every pair of elements of S carries compatible information: there is at least one element that is more informative than both (and hence, the information that x and y carry is not contradictory).

Thus, S is "going somewhere": its elements can be seen as approximants that can be combined into better approximants. Directed-completeness means that every such "set with a purpose" has a least upper bound, i.e. a least informative element fitting the "specification" given by all the approximants.