Complete partial order
Encyclopedia
In mathematics
, directed complete partial orders and ω-complete partial orders (abbreviated to dcpo, ωcpo or sometimes just cpo) are special classes of partially ordered set
s, characterized by particular completeness properties
. Complete partial orders play a central role in theoretical computer science
, in denotational semantics
and domain theory
.
has a supremum
. Recall that a subset of a partial order is directed if it is non-empty and every pair of elements has an upper bound in the set. In the literature, dcpos sometimes also appear under the label up-complete poset or simply cpo.
In some contexts, the phrase ω-cpo (or just cpo) is used to describe a poset in which every ω-chain (x1≤x2≤x3≤x4≤...) has a supremum. Every dcpo is an ω-cpo.
An important role is played by dcpo's with a least element. They are sometimes called pointed dcpos, or cppos, or just cpos.
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.
if it maps directed sets to directed sets while preserving their suprema:
Note that every continuous function between dcpos is a monotone function
.
This notion of continuity is equivalent to the topological continuity 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 again a dcpo, and a cpo whenever Q is a cpo.
Thus the complete partial orders with Scott continuous maps form a cartesian closed category
.
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(⊥)), … fn(⊥), …) of ⊥ (see also the Kleene fixpoint theorem
).
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.
Mathematics
Mathematics is the study of quantity, space, structure, and change. Mathematicians seek out patterns and formulate new conjectures. Mathematicians resolve the truth or falsity of conjectures by mathematical proofs, which are arguments sufficient to convince other mathematicians of their validity...
, directed complete partial orders and ω-complete partial orders (abbreviated to dcpo, ωcpo or sometimes just cpo) are special classes of partially ordered set
Partially ordered set
In mathematics, especially order theory, a partially ordered set formalizes and generalizes the intuitive concept of an ordering, sequencing, or arrangement of the elements of a set. A poset consists of a set together with a binary relation that indicates that, for certain pairs of elements in the...
s, characterized by particular completeness properties
Completeness (order theory)
In the mathematical area of order theory, completeness properties assert the existence of certain infima or suprema of a given partially ordered set . A special use of the term refers to complete partial orders or complete lattices...
. Complete partial orders play a central role in theoretical computer science
Theoretical computer science
Theoretical computer science is a division or subset of general computer science and mathematics which focuses on more abstract or mathematical aspects of computing....
, in denotational semantics
Denotational semantics
In computer science, denotational semantics is an approach to formalizing the meanings of programming languages by constructing mathematical objects which describe the meanings of expressions from the languages...
and domain theory
Domain theory
Domain theory is a branch of mathematics that studies special kinds of partially ordered sets commonly called domains. Consequently, domain theory can be considered as a branch of order theory. The field has major applications in computer science, where it is used to specify denotational...
.
Definitions
A partially ordered set is a directed complete partial order (dcpo) if each of its directed subsetsDirected set
In mathematics, a directed set is a nonempty set A together with a reflexive and transitive binary relation ≤ , with the additional property that every pair of elements has an upper bound: In other words, for any a and b in A there must exist a c in A with a ≤ c and b ≤...
has a supremum
Supremum
In mathematics, given a subset S of a totally or partially ordered set T, the supremum of S, if it exists, is the least element of T that is greater than or equal to every element of S. Consequently, the supremum is also referred to as the least upper bound . If the supremum exists, it is unique...
. Recall that a subset of a partial order is directed if it is non-empty and every pair of elements has an upper bound in the set. In the literature, dcpos sometimes also appear under the label up-complete poset or simply cpo.
In some contexts, the phrase ω-cpo (or just cpo) is used to describe a poset in which every ω-chain (x1≤x2≤x3≤x4≤...) has a supremum. Every dcpo is an ω-cpo.
An important role is played by dcpo's with a least element. They are sometimes called pointed dcpos, or cppos, or just cpos.
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
Domain theory
Domain theory is a branch of mathematics that studies special kinds of partially ordered sets commonly called domains. Consequently, domain theory can be considered as a branch of order theory. The field has major applications in computer science, where it is used to specify denotational...
.
The dual
Duality (order theory)
In the mathematical area of order theory, every partially ordered set P gives rise to a dual partially ordered set which is often denoted by Pop or Pd. This dual order Pop is defined to be the set with the inverse order, i.e. x ≤ y holds in Pop if and only if y ≤ x holds in P...
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.
Examples
- Every finite poset is directed complete.
- All complete latticeComplete latticeIn mathematics, a complete lattice is a partially ordered set in which all subsets have both a supremum and an infimum . Complete lattices appear in many applications in mathematics and computer science...
s are also directed complete. - For any poset, the set of all non-empty filtersFilter (mathematics)In mathematics, a filter is a special subset of a partially ordered set. A frequently used special case is the situation that the ordered set under consideration is just the power set of some set, ordered by set inclusion. Filters appear in order and lattice theory, but can also be found in...
, ordered by subset inclusion, is a dcpo. Together with the empty filter it is also pointed. If the order has binary meetsJoin and meetIn mathematics, join and meet are dual binary operations on the elements of a partially ordered set. A join on a set is defined as the supremum with respect to a partial order on the set, provided a supremum exists...
, then this construction (including the empty filter) actually yields a complete latticeComplete latticeIn mathematics, a complete lattice is a partially ordered set in which all subsets have both a supremum and an infimum . Complete lattices appear in many applications in mathematics and computer science...
. - The set of all partial functionPartial functionIn mathematics, a partial function from X to Y is a function ƒ: X' → Y, where X' is a subset of X. It generalizes the concept of a function by not forcing f to map every element of X to an element of Y . If X' = X, then ƒ is called a total function and is equivalent to a function...
s 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 graphsGraph of a functionIn mathematics, the graph of a function f is the collection of all ordered pairs . In particular, if x is a real number, graph means the graphical representation of this collection, in the form of a curve on a Cartesian plane, together with Cartesian axes, etc. Graphing on a Cartesian plane is...
.) This order is a pointed dcpo, 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 spaceSober spaceIn mathematics, a sober space is a topological spacesuch that every irreducible closed subset of X is the closure of exactly one point of X: that is, has a unique generic point.-Properties and examples :...
is a dcpo. - Let us use the term “deductive systemDeductive systemA deductive system consists of the axioms and rules of inference that can be used to derive the theorems of the 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 consequences 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.
Properties
An ordered set P is a pointed dcpo if and only if every chain has a supremum in P. Alternatively, an ordered set P is a pointed dcpo if and only if every order-preserving self-map of P has a least fixpoint. Every set S can be turned into a pointed dcpo by adding a least element ⊥ and introducing a flat order with ⊥ ≤ s and s ≤ 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 (Scott) continuousScott continuity
In mathematics, given two partially ordered sets P and Q a function f : P \rightarrow Q between them is Scott-continuous if it preserves all directed suprema, i.e...
if it maps directed sets to directed sets while preserving their suprema:
-
is directed for every directed 
. -
for every directed 
.
Note that every continuous function between dcpos is a monotone function
Monotone
Monotone refers to a sound, for example speech or music, that has a single unvaried tone.Monotone or monotonicity may also refer to:*Monotone , an open source revision control system*Monotone class theorem, in measure theory...
.
This notion of continuity is equivalent to the topological continuity induced by the Scott topology.
The set of all continuous functions between two dcpos P and Q is denoted
Thus the complete partial orders with Scott continuous maps form a cartesian closed category
Cartesian closed category
In category theory, a category is cartesian closed if, roughly speaking, any morphism defined on a product of two objects can be naturally identified with a morphism defined on one of the factors. These categories are particularly important in mathematical logic and the theory of programming, in...
.
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
Iterated function
In mathematics, an iterated function is a function which is composed with itself, possibly ad infinitum, in a process called iteration. In this process, starting from some initial value, the result of applying a given function is fed again in the function as input, and this process is repeated...
(⊥, f(⊥), f(f(⊥)), … fn(⊥), …) of ⊥ (see also the Kleene fixpoint theorem
Kleene fixpoint theorem
In the mathematical areas of order and lattice theory, the Kleene fixed-point theorem, named after American mathematician Stephen Cole Kleene, states the following:...
).
See also
Directed completeness relates in various ways to other completenessCompleteness (order theory)
In the mathematical area of order theory, completeness properties assert the existence of certain infima or suprema of a given partially ordered set . A special use of the term refers to complete partial orders or complete lattices...
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.