*** Welcome to piglix ***

Complete partial order


In mathematics, directed-complete partial orders and ω-complete partial orders (abbreviated to dcpo and ω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.

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 that belongs to the underlying set of the poset. 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). An ω-cpo (dcpo) with a basis is also called a continuous ω-cpo (continuous dcpo).

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.

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.


...
Wikipedia

...