nLab dcpo

Redirected from "DCPO".
DCPOs

This entry is about domains in domain theory. For other uses, see at domain.


Context

(0,1)(0,1)-Category theory

Limits and colimits

DCPOs

Idea

A directed-complete partial order (DCPO), is a poset with all directed joins. Often a DCPO is required to have a bottom element \bot; 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 \bot, depending on the application.

In domain theory, a DCPO PP 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 xyx \leq y in PP, then xx consists of part of the information in yy. A directed subset DD of PP indicates a collection of partial results which are mutually consistent, since for any two results x,yDx, y \in D, there is a partial result that subsumes them both. The required join of DD is then a partial result encoding the same information as DD itself.

Definitions

Recall that a poset PP consists of a collection of elements equipped with a binary relation \leq such that xxx \leq x always and xzx \leq z whenever xyx \leq y and yzy \leq z; we also consider xx and yy to be equal whenever xyx \leq y and yxy \leq x.

Recall that a subset DD of PP is semidirected iff, whenever x,yDx, y \in D, there is some zDz \in D such that xzx \leq z and yzy \leq z. Then DD is directed iff it is semidirected and inhabited.

Recall that an upper bound of a subset DD of PP is an element xx such that yxy \leq x whenever yDy \in D, and a join of DD is an upper bound xx such that xyx \leq y whenever yy is an upper bound of DD. The join of DD, if one exists, is unique, and we write it D\bigvee D (or even put a little arrow on the right flank of the symbol when DD is directed). A bottom element is a join of the empty subset.

Definition

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.

Properties

The Scott topology

Every poset PP becomes a topological space under the Scott topology, but this is particularly nice for DCPOs, so we review it.

A subset AA of a DCPO is Scott-open iff it’s an upper subset and any directed subset of PP whose join belongs to AA must meet AA; 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).

References

See the references at domain theory.

See also:

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.