The intuitive idea underlying the theory is that the ordering of a domain represents a hierarchy of information or knowledge. The higher an element is within the order, the more specific it is and the more information it contains. Lower elements represent incomplete knowledge or intermediate results. Computation then may consist of applying monotone functions repeatedly on elements of the domain in order to refine a result. Reaching a fixed point is equivalent to finishing a calculation. Domains provide a superior setting for these ideas since (among other advantages) fixed points of monotone functions can be guaranteed to exist.
Domain theory has close relations to topology and the theory of computation, because it formalizes the ideas of approximation and convergence in a very general way. An alternative approach to semantics in the spirit of the above intuition are metric spaces, where contracting functions may be applied to model computation and approximation.
| Table of contents |
|
2 Important results 3 Literature |
The basic mathematical structures of domain theory are directed complete partial orders or dcpos. A dcpo is a partially ordered set where every directed subset has a least upper bound (not necessarily within the subset itself). Viewing directed subsets as a generalized concept of convergence, this guarantees that all limits of such sets exist. When a dcpo has a least element, it is sometimes called a complete partial order (cpo).
The appropriate morphisms for dcpos are continuous functions. A function f between two dcpos is said to be (Scott-) continuous iff it is monotone and preserves directed suprema.
However, one usually additionally needs a concept of approximation. This is obtained by introducing the approximation order <<. For a dcpo (D, ≤) it is defined by:
We now say that some subset B of D is a base for D if for every x in D, the set {y in D| y << x} ∩ B contains a directed set with supremum x.
A continuous dcpo or continuous domain is a dcpo that has a base. This notion is central to domain theory. It provides the basic requirements for modelling computation, namely that every element can be approximated by a converging directed subset from a given base. A special case is given if the base is countable. In this case we talk about ω-continuous dcpos.
An element of a dcpo is said to be compact or finite iff it approximates itself. These elements cannot be obtained as suprema of directed sets that do not already contain them. If a dcpo has a base of compact elements, it is called an algebraic dcpo or an algebraic domain. For countable bases ω-algebraicity is defined as above.
A number of other important properties have been defined for domains, giving rise to additional classes (and categories) of dcpos. Note that the term domain itself is not exact and thus is only used as an abbreviation when a formal definition has been given before.Formal definitions
One says that x approximates y or that x is way below y.