Completeness (order Theory) - Completions of Domains

Completions of Domains

According to Clinger, often there is an intuitive sense in which some elements of partially ordered sets are finite. E.g., in denotational semantics, they may be partial functions defined for only finitely many values or they may be finite partial computations in the Actor model. This sense of finiteness lies behind the following abstract definition:

Let (D, ≤) be a partially ordered set. An element x∈D is isolated if and only if whenever A⊆D is directed, ∪A exists and x≤∪A, there exists a∈A with x≤a. In other words, x is isolated if one must go through x to get up to or above x via the limit process. As examples, the finite sets are the isolated elements of the power set of ω ordered by inclusion; the ordinal ω+1 is isolated in the set of countable ordinals under the usual ordering.

The least element of a partially ordered set is always isolated provided it exists. 0 is the least element of the nonnegative rationals under the usual ordering, and it is also the only isolated element. The entire set of rationals has no isolated elements under the usual ordering.

For purposes of programming language semantics, partially ordered sets with least elements form too general a category. The partially ordered sets of greatest interest for computer science are those whose isolated elements are dense in the sense that every element is a least upper bound of a countable set of isolated elements. To avoid transfinite induction, and to make directed completeness equivalent to ω-completeness, it is convenient to assume also that there are only countably many isolated elements which motivates the following definition.

Definition. A domain is a partially ordered set (D, ≤) such that

1. D has a least element Λ
2. Every element of D is the least upper bound of a countable increasing sequence of isolated elements.
3. The isolated elements of D are countable.

The above definition is a generalization of the traditional definition. The traditional definition requires also that D be ω-complete, so that ω-continuous functions from D to D will have fixed points.

An ω-complete domain is complete in the sense that every directed subset has a least upper bound. An ω-complete domain is also known as a countably algebraic complete partial order .

Every domain D can be embedded in an ω-complete domain completion (called the ω-completion or simply the completion of D) that is, in a precise sense, the smallest ω-complete domain containing D. The isolated elements of completion are precisely the isolated elements of D, but in general completion contains limit points that are not found in D. completion is uniquely determined up to isomorphism. In Clinger, it is shown that for any domain D the power domain of D is isomorphic to the power domain of completion. So why not use ω-complete domains only, as is traditional? Because the power domain is interpreted with reference to the domain from which it is built. As explained in denotational semantics of concurrency, the underlying domain is incomplete in Actor semantics.