Domain theory is a branch of mathematics that studies special kinds of ordered sets commonly called domains. The fields has major applications in computer science, where it is used to specify denotational semantics, especially for functional programming languages.

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
1 Formal definitions
2 Important results
3 Literature

Formal definitions

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:

  • x << y iff for all directed subsets S of D, y≤VS implies xs for some s in S.
One says that x approximates y or that x is way below y.

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.

Important results

A poset D is a dcpo iff each chain in D has a supremum. However, directed sets are strictly more powerful than chains.

A poset D with a least element is a dcpo iff every monotone function f on D has a fixed point. If f is continuous then it has even a least fixed point, given as the least upper bound of all finite iterations of f on the least element 0: Vn in N f n(0).

Of course, there are many other important results, depending on the application area where domain theory is to be applied. Please see the literature (and contribute).

Literature