Domain theory

Domain theory is a branch of mathematics that studies special kinds of partially ordered sets commonly called domains. Consequently, domain theory can be considered as a branch of order theory. The field has major applications in computer science, where it is used to specify denotational semantics, especially for functional programming. Domain theory formalizes the intuitive ideas of approximation and convergence in a very general way and has close relations to topology. An alternative important approach to denotational semantics in computer science are metric spaces.

= Motivation and intuition =

The primary motivation for the study of domains, which was initiated by Dana Scott in the late 1960s, was the search for a denotational semantics of the lambda calculus. In this formalism, one considers functions specified by certain terms in the language. In a purely syntax way, one can go from simple functions to functions that take other functions as their input arguments. Using again just the syntactic transformations available in this formalism, one can obtain so called fixed point combinators (also called Y combinators); these, by definition, have the property that f (Y( f )) = Y( f ) for all functions f .

To formulate such a denotational semantics, one might first try to construct a model for the lambda calculus, in which a genuine (total) function is associated with each lambda term. Such a model would formalize a link between the lambda calculus as a purely syntactic system and the lambda calculus as a notational system for manipulating concrete mathematical functions. Unfortunately, such a model cannot exist, for if it did, it would have to contain a genuine, total function that corresponds to the combinator Y, that is, a function that computes a fixed point (mathematics) of an arbitrary input function f . There can be no such function for Y, because some functions (for example, the successor function ) do not have a fixed point. At best, the genuine function corresponding to Y would have to be a partial function, necessarily undefined at some inputs.

Scott got around this difficulty by formalizing a notion of partial or incomplete information to represent computations that have not yet returned a result. This was modeled by considering, for each domain of computation (e.g. the natural numbers), an additional element that represents an undefined output, i.e. the result of a computation that does never end. In addition, the domain of computation is equipped with an ordering relation , in which the undefined result is the least element.

The important step to find a model for the lambda calculus is to consider only those functions (on such a partially ordered set) which are guaranteed to have least fixed points. The set of these functions, together with an appropriate ordering, is again a domain in the sense of the theory. But the restriction to a subset of all available functions has another great benefit: it is possible to obtain domains that contain their own function spaces, i.e. one gets functions that can be applied to themselves.

Beside these desirable properties, domain theory also allows for an appealing intuitive interpretation. As mentioned above, the domains of computation are always partially ordered. This ordering 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 is modeled by applying monotonic function (mathematics)s repeatedly on elements of the domain in order to refine a result. Reaching a fixed point (mathematics) is equivalent to finishing a calculation. Domains provide a superior setting for these ideas since fixed points of monotone functions can be guaranteed to exist and, under additional restrictions, can be approximated from below.

= A guide to the formal definitions =

In this section, the central concepts and definitions of domain theory will be introduced. The above intuition of domains being information orderings will be emphasized to motivate the mathematical formalization of the theory. The precise formal definitions are to be found in the dedicated articles for each concept. A list of general order-theoretic definitions which include domain theoretic notions as well can be found in the order theory glossary. The most important concepts of domain theory will nonetheless be introduced below.

== Directed sets as converging specifications ==

As mentioned before, domain theory deals with partially ordered sets to model a domain of computation. The goal is to interpret the elements of such an order as pieces of information or (partial) results of a computation , where elements that are higher in the order extend the information of the elements below them in a consistent way. From this simple intuition it is already clear that domains often do not have a greatest element, since this would mean that there is an element that contains the information of all other elements - a rather uninteresting situation.

A concept that plays an important role in the theory is the one of a directed set of a domain, i.e. of a non-empty subset of the order in which each two elements have some upper bound. In view of our intuition about domains, this means that every two pieces of information within the directed subset are consistently extended by some other element in the subset. Hence we can view directed sets as consistent specifications , i.e. as sets of partial results in which no two elements are contradictory. This interpretation can be compared with the notion of a sequence in analysis, where each element is more specific than the preceding one. Indeed, in the theory of metric spaces, sequences play a role that is in many aspects analogue to the role of directed sets in domain theory.

Now, as in the case of sequences, we are interested in the limit of a directed set. According to what was said above, this would be an element that is the most general piece of information which extends the information of all elements of the directed set, i.e. the unique element that contains exactly the information that was present in the directed set - and nothing more. In the formalization of order theory, this is just the least upper bound of the directed set. As in the case of limits of sequences, least upper bounds of directed sets do not always exist.

Naturally, one has a special interest in those domains of computations in which all consistent specifications converge , i.e. in orders in which all directed sets have a least upper bound. This property defines the class of directed complete partial orders, or dcpo for short. Indeed, most considerations of domain theory do only consider orders that are at least directed complete.

From the underlying idea of partially specified results as representing incomplete knowledge, one derives another desirable property: the existence of a least element. Such an element models that state of no information - the place where most computations start. It also can be regarded as the output of a computation that does not return any result at all. Due to their importance for the theory, dcpos with a least element are called complete partial orders or just cpos.

== Computations and domains ==

Now that we have some basic formal descriptions of what a domain of computation should be, we can turn to the computations themselves. Clearly, these have to be functions, taking inputs from some computational domain and returning outputs in some (possibly different) domain. However, one would also expect that the output of a function will contain more information when the information content of the input is increased. Formally, this means that we want a function to be monotonic.

When dealing with dcpos, one might also want computations to be compatible with the formation of limits of a directed set. Formally, this means that, for some function f , the image f ( D ) of a directed set D (i.e. the set of the images of each element of D ) is again directed and has as a least upper bound the image of the least upper bound of D . One could also say that f limit-preserving function (order theory) directed suprema . Also note that, by considering directed sets of two elements, such a function also has to be monotonic. This properties give rise to the notion of a Scott-continuous function. Since this often is not ambiguous one also may speak of continuous functions . Henry Baker (computer scientist) and Carl Hewitt proved that any Actor that behaves like a function is continuous.

An important application of domain theory was its use by Will Clinger in developing the semantics of the Actor model of concurrent computation (see Denotational_semantics#Denotational_semantics_of_concurrency).

== Approximation and finiteness ==

Domain theory is a purely qualitative approach to modeling the structure of information states. One can say that something contains more information, but the amount of additional information is not specified. Yet, there are some situations in which one wants to speak about elements that are in a sense much more simpler (or much more incomplete) than a given state of information. For example, in the natural subset-inclusion ordering on some powerset, any infinite element (i.e. set) is much more informative than any of its finite subsets.

If one wants to model such a relationship, one may first want to consider the induced strict order < of a domain with order ≤. However, while this is a useful notion in the case of total orders, it does not tell us much in the case of partially ordered sets. Considering again inclusion-orders of sets, a set is already strictly smaller than another, possibly infinite, set if it contains just one less element. One would, however, hardly agree that this captures the notion of being much simpler .

A more elaborate approach leads to the definition of the so-called order of approximation, which is more suggestively also called the way-below relation. An element x is way below an element y , if, for every directed set D with supremum sup D ≥ y , there is some element d in D such that x ≤ d . Then one also says that x approximates y and writes x