In mathematics, directed complete partial orders and complete partial orders are special classes of partially ordered sets. These orders, called dcpos and cpos for short, are characterized by particular completeness properties. Both dcpos and cpos are considered in domain theory and have major applications in theoretical computer science and denotational semantics.

Definition

A partially ordered set is a directed complete partial order (dcpo) if each of its directed subsets has a supremum. A complete partial order (cpo) is a dcpo with a least element. In the literature, dcpos sometimes also appear under the label up-complete poset or, confusingly, simply "cpo". A dcpo with a least element is sometimes called a pointed dcpo or a pointed cpo.

Requiring the existence of directed suprema can be motivated by viewing directed sets as generalized approximation sequences and suprema as limits of the respective (approximative) computations. This intuition, in the context of denotational semantics, was the motivation behind the development of domain theory.

The dual notion of a directed complete poset is called a filtered complete partial order. However, this concept occurs far less frequently in practice, since one usually can work on the dual order explicitly.

Properties

An ordered set P is a cpo if and only if every chain has a supremum in P. Alternatively, an ordered set P is a cpo if and only if every order-preserving self-map of P has a least fixpoint. Every set S can be turned into a cpo by adding a least element ⊥ and introducing a flat order with ⊥ ≤ s for every s ∈ S and no other order relations.

Continuous functions and fixpoints

A function f between two dcpos P and Q is called continuous if it maps directed sets to directed sets while preserving their suprema:

• $f(D)\; subseteq\; Q$ is directed for every directed $D\; subseteq\; P$.
• $f(sup\; D)\; =\; sup\; f(D)$ for every directed $D\; subseteq\; P$.

A function f between two cpos (P, ⊥_P) and (Q, ⊥_Q) is called continuous if it furthermore preserves the least element:

• $f(bot\_P)\; =\; bot\_Q$

This notion of continuity is equivalent to that induced by the Scott topology.

The set of all continuous functions between two dcpos P and Q is denoted [P → Q]. Equipped with the pointwise order, this is a dcpo, and a cpo whenever Q is a cpo.

Every continuous function between cpos is order-preserving but not vice versa. Every order-preserving self-map f of a cpo (P, ⊥) has a least fixpoint. If f is continuous then this fixpoint is equal to the supremum of the iterates (⊥, f(⊥), f(f(⊥)), … fⁿ(⊥), …) of ⊥ (see also the Kleene fixpoint theorem).

See also

Directed completeness relates in various ways to other completeness notions. Directed completeness alone is quite a basic property that occurs often in other order theoretic investigations, using for instance algebraic posets and the Scott topology. Functions between dcpos are often required to be monotone or even Scott continuous. The complete partial orders with Scott continuous maps form a cartesian closed category, denoted CPO.

Examples

• Every finite poset is directed complete, every finite poset with a least element is a cpo.
• All complete lattices are also directed complete.
• For any poset, the set of all non-empty filters, ordered by subset inclusion, is a dcpo, even a cpo if the poset has a greatest element. Together with the empty filter it is also guaranteed to be a cpo. If the order is a meet-semilattice (or even a lattice), then this construction (including the empty filter) actually yields a complete lattice.
• The set of all partial functions on some given set S can be ordered by defining f ≤ g for functions f and g if and only if g extends f, i.e. if the domain of f is a subset of the domain of g and the values of f and g agree on all inputs for which both functions are defined. (Equivalently, f ≤ g if and only if f ⊆ g where f and g are identified with their respective graphs.) This order is a cpo, where the least element is the nowhere defined function (with empty domain). In fact, ≤ is also bounded complete. This example also demonstrates why it is not always natural to have a greatest element.
• The specialization order of any sober space is a dcpo.
• Let us use the term “deductive system” as a set of sentences closed under consequence (for defining notion of consequence, let us use e.g. Tarski's algebraic approach). There are interesting theorems which concern a set of deductive systems being a directed complete partial ordering. Also, a set of deductive systems can be chosen to have a least element in a natural way (so that it can be also a complete partial ordering), because the set of all conseqences of the empty set (i.e. “the set of the logically provable / logically valid sentences”) is (1) a deductive system (2) contained by all deductive systems.

Notes

References

• Davey, B.A., and Priestley, H. A. (2002). Introduction to Lattices and Order. Second Edition, Cambridge University Press. ISBN 0-521-78451-4.