Editing Domain theory (section)

== 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 set]]s 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 that of a '''[[directed set|directed subset]]''' of a domain; a directed subset is a non-empty subset of the order in which any two elements have an [[upper bound]] that is an element of this subset. In view of our intuition about domains, this means that any two pieces of information within the directed subset are ''consistently'' extended by some other element in the subset. Hence we can view directed subsets 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 [[convergent sequence]] in [[Mathematical analysis|analysis]], where each element is more specific than the preceding one. Indeed, in the theory of [[metric space]]s, sequences play a role that is in many aspects analogous 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 that 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 the limit of a sequence, the least upper bound of a directed set does 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 order|directed-complete partial order]]s''', 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.

=== 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 '''[[complete partial order|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. These properties give rise to the notion of a '''[[Scott-continuous]]''' function. Since this often is not ambiguous one also may speak of ''continuous functions''.

=== 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 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".

===Way-below relation===
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 such that

:<math> y \sqsubseteq \sup D </math>,

there is some element ''d'' in ''D'' such that

:<math> x \sqsubseteq d </math>.

Then one also says that ''x'' ''approximates'' ''y'' and writes

:<math> x \ll y </math>.

This does imply that

:<math> x \sqsubseteq y </math>,

since the singleton set {''y''} is directed. For an example, in an ordering of sets, an infinite set is way above any of its finite subsets. On the other hand, consider the directed set (in fact, the [[Total order#Chains|chain]]) of finite sets

:<math> \{0\}, \{0, 1\}, \{0, 1, 2\}, \ldots </math>

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.

:<math> x \ll x</math>.

An element with this property is also called '''[[compact element|compact]]'''. Yet, such elements do not 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.

Many other important results about the way-below relation support the claim that this definition is appropriate to capture many important aspects of a domain.

=== 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 ''finite'' elements. Such a poset is called '''[[algebraic poset|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 '''ω-continuous''' poset. Accordingly, if the countable base consists entirely of finite elements, we obtain an order that is '''ω-algebraic'''.

=== 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 [[complete partial order|cpos]]. Adding even further [[completeness (order theory)|completeness properties]] one obtains [[Lattice (order)#Continuity and algebraicity|continuous lattices]] and [[algebraic lattices]], which are just [[complete lattice]]s with the respective properties. For the algebraic case, one finds broader classes of posets that are still worth studying: historically, the [[Scott domain]]s were the first structures to be studied in domain theory. Still wider classes of domains are constituted by [[SFP-domain]]s, [[L-domain]]s, and [[bifinite domain]]s.

All of these classes of orders can be cast into various [[category (mathematics)|categories]] of dcpos, using functions that are monotone, Scott-continuous, or even more specialized as [[morphism]]s. 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.