What's Domain theory about?
From Wikipedia, the free encyclopedia
(http://en.wikipedia.org/wiki/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
languages. 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.
Contents
* 1 Motivation and intuition
* 2 A guide to the formal definitions
o 2.1 Directed sets as converging specifications
o 2.2 Computations on a domain
o 2.3 Approximation and finiteness
o 2.4 Bases of domains
o 2.5 Special types of domains
* 3 Literature
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 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);
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 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 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 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 subset 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 on a domain
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 preserves 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.
An important application of domain theory was its use by Will Clinger
in developing the semantics of the Actor model of concurrent
computation.
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
\x{2264}. 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 more 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\x{2265}y, there is some
element d in D such that x\x{2264}d. Then one also says that x
approximates y and writes x << y. This also implies that x\x{2264}y,
since the singleton set {y} is directed. For an example, note that in
an order of sets, an infinite set is way above any of its finite
subsets. On the other hand, consider the directed set (in fact: the
chain) of finite sets {0}, {0, 1}, {0, 1, 2}, ... Since the supremum
of this chain is the set of all natural numbers N, this shows that no
infinite set is way below N.
However, being way below some element is a relative notion and does
not reveal much about an element alone. For example, one would like to
characterize finite sets in an order-theoretic way, but even infinite
sets can be way below some other set. The special property of these
finite elements x is that they are way below themselves, i.e. x<
Many other important results about the way-below relation support the
claim that this definition is really highly appropriate to capture
many important aspects of a domain. More details are given in the
article on the way-below relation.
Bases of domains
The previous thoughts raise another question: is it possible to
guarantee that all elements of a domain can be obtained as a limit of
much simpler elements? This is quite relevant in practice, since we
cannot compute infinite objects but we may still hope to approximate
them arbitrarily closely.
More generally, we would like to restrict to a certain subset of
elements as being sufficient for getting all other elements as least
upper bounds. Hence, one defines a base of a poset P as being a subset
B of P, such that, for each x in P, the set of elements in B that are
way below x contains a directed set with supremum x. The poset P is a
continuous poset if it has some base. Especially, P itself is a base
in this situation. In many applications, one restricts to continuous
(d)cpos as a main object of study.
Finally, an even stronger restriction on a partially ordered set is
given by requiring the existence of a base of compact elements. Such a
poset is called algebraic. From the viewpoint of denotational
semantics, algebraic posets are particularly well-behaved, since they
allow for the approximation of all elements even when restricting to
finite ones. As remarked before, not every finite element is "finite"
in a classical sense and it may well be that the finite elements
constitute an uncountable set.
In some cases, however, the base for a poset is countable. In this
case, one speaks of an \x{03C9}-continuous poset. Accordingly, if the
countable base consists entirely of finite elements, we obtain an
order that is \x{03C9}-algebraic.
Special types of domains
Starting from these definitions, one obtains a number of other
interesting special classes of ordered structures that could be
suitable as "domains". We already mentioned continuous posets and
algebraic posets. More special versions of both are continuous and
algebraic cpos. Adding even further completeness properties one
obtains continuous lattices and algebraic lattices, which are just
complete lattices with the respective properties. For the algebraic
case, one finds broader classes of posets which are still worth
studying: historically, the Scott domains were the first structures to
be studied in domain theory. Still wider classes of domains are
constituted by SFP-domains, L-domains, and bifinite domains.
All of these classes of orders can be cast into various categories of
dcpos, using functions which are monotone, Scott-continuous, or even
more specialized as morphisms. Finally, 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 or when the details are
irrelevant.
Literature
Probably one of the most recommendable books on domain theory
today, giving a very clear and detailed view on many parts of the
basic theory:
* G. Gierz, K. H. Hofmann, K. Keimel, J. D. Lawson,
M. Mislove, and D. S. Scott, Continuous Lattices and Domains, In
Encyclopedia of Mathematics and its Applications, Vol. 93, Cambridge
University Press, 2003. ISBN 0521803381
A standard resource on domain theory, which is freely available online:
* S. Abramsky, A. Jung: Domain theory. In S. Abramsky,
D. M. Gabbay, T. S. E. Maibaum, editors, Handbook of Logic in
Computer Science, vol. III. Oxford University Press, 1994. ISBN
019853762X
One of Scott's classical papers:
* D. S. Scott. Data types as lattices. In G. Muller et al.,
editors, Proceedings of the International Summer Institute and Logic
Colloquium, Kiel, volume 499 of Lecture Notes in Mathematics, pages
579-651, Springer-Verlag, 1975.
A general, easy-to-read account of order theory, including an
introduction to domain theory as well:
* B. A. Davey and H. A. Priestley, Introduction to Lattices
and Order, 2nd edition, Cambridge University Press, 2002. ISBN
0521784514
A general, easy-to-read account of the Actor model of concurrent
computation, using only elementary domain theory:
* W. Clinger. Foundations of Actor Semantics MIT Mathematics
Doctoral Dissertation. June 1981.