**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. Wikibooks Wikiversity has more about this subject: School of Mathematics Wikiquote has a collection of quotations related to: Mathematics Look up Mathematics on Wiktionary, the free dictionary Wikimedia Commons has media related to: Mathematics Bogomolny, Alexander: Interactive Mathematics Miscellany and Puzzles. ...
In mathematics, especially order theory, a partially ordered set (or poset for short) is a set equipped with a partial order relation. ...
Order theory is a branch of mathematics that studies various kinds of binary relations that capture the intuitive notion of a mathematical ordering. ...
Wikibooks Wikiversity has more about this subject: School of Computer Science Open Directory Project: Computer Science Downloadable Science and Computer Science books Collection of Computer Science Bibliographies Belief that title science in computer science is inappropriate Categories: Wikipedia articles needing priority cleanup | Eponymous Wikibooks modules | Computer science ...
In computer science, denotational semantics is one of the approaches to formalize the semantics of computer programs. ...
The Haskell programming language logo Functional programming is a programming paradigm that treats computation as the evaluation of mathematical functions. ...
Topology (Greek topos, place and logos, study) is a branch of mathematics concerned with spatial properties preserved under bicontinuous deformation (stretching without tearing or gluing); these are the topological invariants. ...
In mathematics, a metric space is a set where a notion of distance between elements of the set is defined. ...
## 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*. This article needs cleanup. ...
In computer science, denotational semantics is one of the approaches to formalize the semantics of computer programs. ...
The lambda calculus is a formal system designed to investigate function definition, function application, and recursion. ...
Syntax, originating from the Greek words ÏƒÏ…Î½ (syn, meaning co- or together) and Ï„Î¬Î¾Î¹Ï‚ (tÃ¡xis, meaning sequence, order, arrangement), can be described as the study of the rules, or patterned relations that govern the way the words in a sentence come together. ...
A fixed point combinator (or fixed-point operator) is a higher-order function which computes a fixed point of other functions. ...
Y Combinator is a venture capital firm started by Trevor Blackwell, Paul Graham, Robert Morris, and Jessica Livingston. ...
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. In mathematics, a fixed point of a function is a point that is mapped to itself by the function. ...
This article needs to be cleaned up to conform to a higher standard of quality. ...
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. In mathematics, especially in order theory, the greatest element of a subset S of a partially ordered set is an element of S which is greater than or equal to any other element of S. The term least element is defined dually. ...
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. In mathematics, a function space is a set of functions of a given kind from a set X to a set Y. It is called a space because in most applications, it is a topological space or/and a vector space. ...
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. In mathematics, functions between ordered sets are monotonic (or monotone) if they preserve the given order. ...
In mathematics, a function is a relation, such that each element of a set (the domain) is associated with a unique element of another (possibly the same) set (the codomain, not to be confused with the range). ...
In mathematics, a fixed point of a function is a point that is mapped to itself by the function. ...
## 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. This is a glossary of some terms used in various branches of mathematics that are related to the fields of order, lattice, and domain theory. ...
### 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. In mathematics, especially order theory, a partially ordered set (or poset for short) is a set equipped with a partial order relation. ...
In mathematics, especially in order theory, the greatest element of a subset S of a partially ordered set is an element of S which is greater than or equal to any other element of S. The term least element is defined dually. ...
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. In mathematics, a directed set is a set A together with a binary relation ≤ having the following properties: a ≤ a for all a in A (reflexivity) if a ≤ b and b ≤ c, then a ≤ c (transitivity) for any two a and b in A, there exists a c in A...
In mathematics, especially in order theory, an upper bound of a subset S of some partially ordered set is an element which is greater than or equal to every element of S. The term lower bound is defined dually. ...
This is a page about mathematics. ...
An analysis is a critical evaluation, usually made by breaking a subject (either material or intellectual) down into its constituent parts, then describing the parts and their relationship to the whole. ...
In mathematics, a metric space is a set where a notion of distance between elements of the set is defined. ...
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. In mathematics, the supremum of an ordered set S is the least element (not necessarily in S) which is greater than or equal to each element of S. Consequently, it is also referred to as the least upper bound. ...
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. In mathematics, directed complete partial orders and complete partial orders are special classes of partially ordered sets. ...
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**. In mathematics, especially in order theory, the greatest element of a subset S of a partially ordered set is an element of S which is greater than or equal to any other element of S. The term least element is defined dually. ...
In mathematics, directed complete partial orders and complete partial orders are special classes of partially ordered sets. ...
### 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**. In mathematics, functions between ordered sets are monotonic (or monotone) if they preserve the given order. ...
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*. Henry Baker and Carl Hewitt proved that any Actor that behaves like a function is continuous. In the mathematical area of order theory, one often speaks about functions that preserve certain limits, i. ...
A monotone function f : P → Q between posets P and Q is Scott-continuous if, for every directed set D that has a supremum sup D in P, the set {fx | x in D} has the supremum f(sup D) in Q. Stated differently, a Scott-continuous function is one...
Henry Baker is the name of a computer scientist who has made contributions in such areas as Garbage collection and the Actor model. ...
Carl Hewitt is a US scientist who is an emeritus professor from MIT. He is known for his design of Planner that was the first Artificial Intelligence programming language based on procedural plans that were invoked using pattern-directed invocation from assertions and goals. ...
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). In computer science, the Actor model, first published in 1973, is a mathematical model of concurrent computation. ...
Parallel programming (also concurrent programming), is a computer programming technique that provides for the execution of operations concurrently, either within a single computer, or across a number of systems. ...
In computer science, denotational semantics is one of the approaches to formalize the semantics of computer programs. ...
### 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 simple (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. In mathematics, given a set S, the power set of S, written P(S) or 2S, is the set of all subsets of S. In formal language, the existence of power set of any set is presupposed by the axiom of power set. ...
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* << *y*. This also implies that *x*≤*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*<<*x*. An element with this property is also called **compact**. Yet, such elements neither have to be "finite" nor "compact" in any other mathematical usage of the terms. The notation is nonetheless motivated by certain parallels to the respective notions in set theory and topology. The compact elements of a domain have the important special property that they cannot be obtained as a limit of a directed set in which they did not already occur. In the mathematical area of order theory, the compact or finite elements of a partially ordered set are those elements that cannot be subsumed by a supremum of any directed set that does not already contain members above the compact element. ...
Set theory is the mathematical theory of sets, which represent collections of abstract objects. ...
Topology (Greek topos, place and logos, study) is a branch of mathematics concerned with spatial properties preserved under bicontinuous deformation (stretching without tearing or gluing); these are the topological invariants. ...
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 mathematics, an uncountable set is a set which is not countable. ...
In some cases, however, the base for a poset is countable. In this case, one speaks of an **ω-continuous** poset. Accordingly, if the countable base consists entirely of finite elements, we obtain an order that is *ω-algebraic*. In mathematics the term countable set is used to describe the size of a set, e. ...
### Special types of domains A simple special case of a domain is known as an **elementary** or **flat domain**. This consists of a set of incomparable elements, such as the integers, along with a single "bottom" element considered smaller than all other elements. One can obtain 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. In mathematics, directed complete partial orders and complete partial orders are special classes of partially ordered sets. ...
In the mathematical area of order theory, completeness properties assert the existence of certain infima or suprema of a given partially ordered set. ...
In mathematics, a complete lattice is a partially ordered set in which all subsets have both a supremum (join) and an infimum (meet). ...
In the mathematical fields of order and domain theory, a Scott domain is an algebraic, bounded complete cpo. ...
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. Category theory is a mathematical theory that deals in an abstract way with mathematical structures and relationships between them. ...
## 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*: V_{n 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 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) (download PDF PS.GZ) *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 readable account of the Laws for Actor systems and how they can be used to prove Scott's continuity criterion:* - Carl Hewitt and Henry Baker
*Actors and Continuous Functionals* Proceeding of IFIP Working Conference on Formal Description of Programming Concepts. August 1-5, 1977. *A general, easy-to-read account of the Actor model of concurrent computation, using only elementary domain theory:* In computer science, the Actor model, first published in 1973, is a mathematical model of concurrent computation. ...
- W. Clinger.
*Foundations of Actor Semantics* MIT Mathematics Doctoral Dissertation. June 1981. |