Complete partial order
In mathematics, the phrase complete partial order is variously used to refer to at least three similar, but distinct, classes of partially ordered sets, characterized by particular completeness properties. Complete partial orders play a central role in theoretical computer science: in denotational semantics and domain theory.
Definitions
The term complete partial order, abbreviated cpo, has several possible meanings depending on context.
A partially ordered set is a directed-complete partial order (dcpo) if each of its
A pointed directed-complete partial order (pointed dcpo, sometimes abbreviated cppo), is a dcpo with a
A related notion is that of ω-complete partial order (ω-cpo). These are posets in which every ω-chain () has a supremum that belongs to the poset. The same notion can be extended to other cardinalities of chains. [1]
Every dcpo is an ω-cpo, since every ω-chain is a directed set, but the converse is not true. However, every ω-cpo with a basis is also a dcpo (with the same basis).[2] An ω-cpo (dcpo) with a basis is also called a continuous ω-cpo (or continuous dcpo).
Note that complete partial order is never used to mean a poset in which all subsets have suprema; the terminology complete lattice is used for this concept.
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 partial order 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.
By analogy with the Dedekind–MacNeille completion of a partially ordered set, every partially ordered set can be extended uniquely to a minimal dcpo.[1]
Examples
- Every finite poset is directed complete.
- All complete lattices are also directed complete.
- For any poset, the set of all non-empty subset inclusion, is a dcpo. Together with the empty filter it is also pointed. If the order has binary meets, then this construction (including the empty filter) actually yields a complete lattice.
- 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 in S and no other order relations.
- The set of all bounded complete. This example also demonstrates why it is not always natural to have a greatest element.
- The set of all inclusion.
- The set of all partial choice functions on a collection of non-empty sets, ordered by restriction.
- The set of all prime ideals of a ring, ordered by inclusion.
- The specialization order of any sober spaceis 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. Alfred Tarski's algebraic approach[3][4]). There are interesting theorems that concern a set of deductive systems being a directed-complete partial ordering.[5]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 pointed dcpo), 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.
Characterizations
An ordered set is a dcpo if and only if every non-empty
.Alternatively, an ordered set is a pointed dcpo if and only if every
Continuous functions and fixed-points
A function f between two dcpos P and Q is called (Scott) continuous 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
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 pointed whenever Q is pointed. Thus the complete partial orders with Scott-continuous maps form a cartesian closed category.[9]
Every order-preserving self-map f of a pointed dcpo (P, ⊥) has a least fixed-point.[10] If f is continuous then this fixed-point is equal to the supremum of the iterates (⊥, f (⊥), f (f (⊥)), … f n(⊥), …) of ⊥ (see also the Kleene fixed-point theorem).
Another fixed point theorem is the
See also
- Algebraic posets
- Scott topology
- Completeness
Notes
- ^ a b c
Markowsky, George (1976), "Chain-complete posets and directed sets with applications", Algebra Universalis, 6 (1): 53–68, S2CID 16718857
- ISBN 9780198537625.
- ^ Tarski, Alfred: Bizonyítás és igazság / Válogatott tanulmányok. Gondolat, Budapest, 1990. (Title means: Proof and truth / Selected papers.)
- ^ Stanley N. Burris and H.P. Sankappanavar: A Course in Universal Algebra
- ^ See online in p. 24 exercises 5–6 of §5 in [1]. Or, on paper, see Tar:BizIg.
- ^ Goubault-Larrecq, Jean (February 23, 2015). "Iwamura's Lemma, Markowsky's Theorem and ordinals". Retrieved January 6, 2024.
- ^ Cohn, Paul Moritz. Universal Algebra. Harper and Row. p. 33.
- ^ Goubault-Larrecq, Jean (January 28, 2018). "Markowsky or Cohn?". Retrieved January 6, 2024.
- North-Holland(1984)
- ISBN 0-471-91282-4, where the Knaster–Tarski theorem, formulated over pointed dcpo's, is given to prove as exercise 4.3-5 on page 90.
- S2CID 117826806.
- MR 0039776.
References
- Davey, B.A.; ISBN 0-521-78451-4.