| |
|
| Table of contents |
|
2 Formal definitions 3 Important results 4 Literature |
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 syntactic 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), that have the property f(Y) = Y(f).
In order to obtain a model for the lambda calculus, one would like to associate a "real" function with each lambda term. This, actually, is the intuition that people often have when dealing with lambda terms. The problem is that the function that should be associated with Y then has to compute a fixed point for every input function f. However, not every real function has a (unique) fixed point. Just take the successor function as an example for a case where the computation of a fixed point would never halt.
Scott's crucial idea was to introduce the idea of "partial" or "incomplete" information in order to account for the situation where a computation does not return a result. This was modelled 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 modelled by 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 fixed points of monotone functions can be guaranteed to exist and, under additional restrictions, can be approximated from below.
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 will nonetheless be introduced below.
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.
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).
Motivation and intuition
Formal definitions
One says that x approximates y or that x is way below y.Important results
Literature