|
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. Details on this intuition in the context of denotational semantics are to be found in the introductory article on 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 and related articles
Directed completeness relates in various way to other completeness notions. This is documented in the article on completeness (order theory). Directed completeness alone is quite a basic property that occurs often in other order theoretic investigations. For instance, theorems involving directed completeness (and characterizations thereof) are to be found in the articles on continuous posets, algebraic posets, and the Scott topology. Functions between dcpos are often required to be monotone or even Scott continuous.
Examples
- 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.
- Consider the set of all partial functions on some set S, i.e. functions defined only on some subset (its domain) of S. For two such functions f and g, define f ≤ g iff 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. In this case, we say that g extends f. This order is a cpo, where the least element is the no-where 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.
- Every finite poset is directed complete, every finite poset with a least element is a cpo.
- All complete lattices are of course also directed complete and thus provide numerous (though not particularly instructive) examples for dcpos.
|
