World Library  
Flag as Inappropriate
Email this Article

Complete partial order

Article Id: WHEBN0000572352
Reproduction Date:

Title: Complete partial order  
Author: World Heritage Encyclopedia
Language: English
Subject: Glossary of order theory, Scott domain, Completeness (order theory), Complete lattice, Apply
Collection: Order Theory
Publisher: World Heritage Encyclopedia
Publication
Date:
 

Complete partial order

In mathematics, directed-complete partial orders and ω-complete partial orders (abbreviated to dcpo, ωcpo or sometimes just cpo) are special 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.

Contents

  • Definitions 1
  • Examples 2
  • Properties 3
  • Continuous functions and fixpoints 4
  • See also 5
  • Notes 6
  • References 7

Definitions

A partially ordered set is a directed-complete partial order (dcpo) if each of its directed subsets 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 subset. In the literature, dcpos sometimes also appear under the label up-complete poset or simply cpo.

The phrase ω-cpo (or just cpo) is used to describe a poset in which every ω-chain (x1x2x3x4≤...) has a supremum. Every dcpo is an ω-cpo, since every ω-chain is a directed set, but the converse is not true.

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.

Examples

  • Every finite poset is directed complete.
  • All complete lattices are also directed complete.
  • For any poset, the set of all non-empty filters, ordered by 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.
  • The set of all partial functions 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 graphs.) 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 space is 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. Tarski's algebraic approach[1][2]). There are interesting theorems which concern a set of deductive systems being a directed complete partial ordering.[3] 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) continuous if it maps directed sets to directed sets while preserving their suprema:

  • f(D) \subseteq Q is directed for every directed D \subseteq P.
  • f(\sup D) = \sup f(D) for every directed D \subseteq P.

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.[4]

Every order-preserving self-map f of a cpo (P, ⊥) has a least fixpoint.[5] 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).

See also

Directed completeness relates in various ways to other completeness notions such as chain completeness. 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.

Notes

  1. ^ Tarski, Alfred: Bizonyítás és igazság / Válogatott tanulmányok. Gondolat, Budapest, 1990. (Title means: Proof and truth / Selected papers.)
  2. ^ Stanley N. Burris and H.P. Sankappanavar: A Course in Universal Algebra
  3. ^ See online in p. 24 exercises 5–6 of §5 in BurSan:UnivAlg. Or, on paper, see Tar:BizIg.
  4. ^ Barendregt, Henk, The lambda calculus, its syntax and semantics, North-Holland (1984)
  5. ^ See Knaster–Tarski theorem; The foundations of program verification, 2nd edition, Jacques Loeckx and Kurt Sieber, John Wiley & Sons, ISBN 0-471-91282-4, Chapter 4; the Knaster-Tarski theorem, formulated over cpo's, is given to prove as exercise 4.3-5 on page 90.

References

  • Davey, B.A., and Priestley, H. A. (2002). Introduction to Lattices and Order (Second ed.). Cambridge University Press.  
This article was sourced from Creative Commons Attribution-ShareAlike License; additional terms may apply. World Heritage Encyclopedia content is assembled from numerous content providers, Open Access Publishing, and in compliance with The Fair Access to Science and Technology Research Act (FASTR), Wikimedia Foundation, Inc., Public Library of Science, The Encyclopedia of Life, Open Book Publishers (OBP), PubMed, U.S. National Library of Medicine, National Center for Biotechnology Information, U.S. National Library of Medicine, National Institutes of Health (NIH), U.S. Department of Health & Human Services, and USA.gov, which sources content from all federal, state, local, tribal, and territorial government publication portals (.gov, .mil, .edu). Funding for USA.gov and content contributors is made possible from the U.S. Congress, E-Government Act of 2002.
 
Crowd sourced content that is contributed to World Heritage Encyclopedia is peer reviewed and edited by our editorial staff to ensure quality scholarly research articles.
 
By using this site, you agree to the Terms of Use and Privacy Policy. World Heritage Encyclopedia™ is a registered trademark of the World Public Library Association, a non-profit organization.
 


Copyright © World Library Foundation. All rights reserved. eBooks from Project Gutenberg are sponsored by the World Library Foundation,
a 501c(4) Member's Support Non-Profit Organization, and is NOT affiliated with any governmental agency or department.