This entry is about domains in domain theory. For other uses, see at domain.
A directed-complete partial order (DCPO), is a poset with all directed joins. Often a DCPO is required to have a bottom element ; then it is called a pointed DCPO or a CPO (but this term is ambiguous).
The morphisms between DCPOs preserve the directed joins; equivalently, they are Scott-continuous. Morphisms between pointed DCPOs may or may not be required to preserve , depending on the application.
In domain theory, a DCPO is interpreted as a type (in the sense of programming languages, cf. data type), and its elements are possible partial (in the sense of a partial function) results of a computation. The bottom element (if there is one) indicates that no result has been obtained; if in , then consists of part of the information in . A directed subset of indicates a collection of partial results which are mutually consistent, since for any two results , there is a partial result that subsumes them both. The required join of is then a partial result encoding the same information as itself.
Recall that a poset consists of a collection of elements equipped with a binary relation such that always and whenever and ; we also consider and to be equal whenever and .
Recall that a subset of is semidirected iff, whenever , there is some such that and . Then is directed iff it is semidirected and inhabited.
Recall that an upper bound of a subset of is an element such that whenever , and a join of is an upper bound such that whenever is an upper bound of . The join of , if one exists, is unique, and we write it (or even put a little arrow on the right flank of the symbol when is directed). A bottom element is a join of the empty subset.
A directed-complete partial order (DCPO) or predomain is a poset in which every directed subset has a join.
A pointed DCPO or complete partial order (CPO) (or inductive partial order (IPO) or semidirected-complete partial order or domain or lift algebra) is a DCPO with a bottom element, equivalently a poset in which every semidirected subset has a join.
Every poset becomes a topological space under the Scott topology, but this is particularly nice for DCPOs, so we review it.
A subset of a DCPO is Scott-open iff it’s an upper subset and any directed subset of whose join belongs to must meet ; it's Scott-closed iff it is a lower subset that is directed-complete in its own right.
The specialisation order of the Scott topology of a DCPO is its original order (but the Scott topology is finer than the specialisation topology).
See the references at domain theory.
See also:
Wikipedia, Scott domain
Wikipeida, Domain theory
D.J. Lehmann, M.B., Smyth, Algebraic specification of data types: A synthetic approach, Math. Systems Theory 14 (1981) 97–139 [doi:10.1007/BF01752392]
Discussion in homotopy type theory/univalent foundations:
Generalization to the context of quantum computation (via quantum sets carrying quantum relations providing categorical semantics for quantum programming languages like Quipper equipped with type recursion):
Last revised on January 20, 2024 at 13:29:43. See the history of this page for a list of all contributions to it.