Power domains
Encyclopedia
In denotational semantics
and domain theory
, power domains are domains of nondeterministic
and concurrent
computations.
The idea of power domains for functions is that a nondeterministic function may be described as a deterministic set-valued function, where the set contains all values the nondeterministic function can take for a given argument. For concurrent systems, the idea is to express the set of all possible computations.
Roughly speaking, a power domain is a domain whose elements are certain subsets of a domain. Taking this approach naively, though, often gives rise to domains that don't quite have the desired properties, and so one is led to increasingly complicated notions of power domain. There are three common variants: the Plotkin, upper, and lower power domains. One way to understand these concepts is as free models of theories of nondeterminism.
For most of this article we use the terms "domain" and of "continuous function" quite loosely, meaning respectively some kind of ordered structure and some kind of limit-preserving function. This flexibility is genuine; for example, in some concurrent systems it is natural to impose the condition that every message sent must eventually be delivered. However, the limit of a chain of approximations in which a message was not delivered, would be a completed computation in which the message was never delivered!
A modern reference to this subject is the chapter of Abramsky and Jung [1994]. Older references include those of Plotkin [1983, Chapter 8] and Smyth [1978].
have come to understand power domains abstractly as free models
for theories of non-determinism. Just as the finite-powerset construction is the free semilattice, the powerdomain constructions should be understood abstractly as free models of theories of non-determinism. By changing the theories of non-determinism, different power domains arise.
The abstract characterisation of powerdomains is often the easiest way to work with them, because explicit descriptions are so intricate. (One exception is the Hoare powerdomain, which has a rather straightforward description.)
s. The theories are not algebraic theories in the conventional sense, because some involve the order of the underlying domain.
All theories have one sort X, and one binary operation ∪. The idea is that the operation ∪:X×X→X takes two combinations and returns the non-deterministic choice of them.
The Plotkin powertheory (after Gordon Plotkin
) has one sort, X, and the following axioms:
The lower (or Hoare, after Tony Hoare
) powertheory consists of the Ploktin powertheory augmented with the inequality
The upper (or Smyth, after M. B. Smyth) powertheory consists of the Ploktin powertheory augmented with the inequality
: it is a semilattice whose carrier is a domain and for which the operation is continuous. Note that the operator need not be a meet or join for the order of the domain. A homomorphism of continuous semilattices is a continuous function between their carriers that respects the lattice operator.
Models of the lower powertheory are called inflationary semilattices; there is an additional requirement that the operator behave a little like a join for the order. For the upper powertheory, models are called deflationary semilattices; here, the operator behaves a little like a meet.
model of the Plotkin powertheory over D. It is defined to be (when it exists) a model P(D) of the Plotkin powertheory (ie a continuous semilattice) equipped with a continuous function X→P(D) such that for any other continuous semilattice L over D, there is a unique continuous semilattice homomorphism P(D)→L making the evident diagram commute.
Other powerdomains are defined abstractly in a similar manner.
In other words, P[D] is the collection of downward-closed subsets of D that are also closed under existing least upper bounds of directed sets in D. Note that while the ordering on P[D] is given by the subset relation, least upper bounds do not in general coincide with unions.
It is important to check which properties of domains are preserved by the power domain constructions. For example, the Hoare powerdomain of an ω-complete domain is again ω-complete.
building on the base domain of Actor event diagrams
, which is incomplete. See Clinger's model.
(which is technically simpler and easier to understand than Clinger's model) building on a base domain of timed Actor event diagrams, which is complete. The idea is to attach an arrival time for each message received by an Actor. See Timed Diagrams Model.
. See, for instance, [Smyth 1983].
Denotational semantics
In computer science, denotational semantics is an approach to formalizing the meanings of programming languages by constructing mathematical objects which describe the meanings of expressions from the languages...
and domain theory
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...
, power domains are domains of nondeterministic
Nondeterministic algorithm
In computer science, a nondeterministic algorithm is an algorithm that can exhibit different behaviors on different runs, as opposed to a deterministic algorithm. There are several ways an algorithm may behave differently from run to run. A concurrent algorithm can perform differently on different...
and concurrent
Concurrency (computer science)
In computer science, concurrency is a property of systems in which several computations are executing simultaneously, and potentially interacting with each other...
computations.
The idea of power domains for functions is that a nondeterministic function may be described as a deterministic set-valued function, where the set contains all values the nondeterministic function can take for a given argument. For concurrent systems, the idea is to express the set of all possible computations.
Roughly speaking, a power domain is a domain whose elements are certain subsets of a domain. Taking this approach naively, though, often gives rise to domains that don't quite have the desired properties, and so one is led to increasingly complicated notions of power domain. There are three common variants: the Plotkin, upper, and lower power domains. One way to understand these concepts is as free models of theories of nondeterminism.
For most of this article we use the terms "domain" and of "continuous function" quite loosely, meaning respectively some kind of ordered structure and some kind of limit-preserving function. This flexibility is genuine; for example, in some concurrent systems it is natural to impose the condition that every message sent must eventually be delivered. However, the limit of a chain of approximations in which a message was not delivered, would be a completed computation in which the message was never delivered!
A modern reference to this subject is the chapter of Abramsky and Jung [1994]. Older references include those of Plotkin [1983, Chapter 8] and Smyth [1978].
Power domains as free models of theories of non-determinism
Domain theoristsDomain 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...
have come to understand power domains abstractly as free models
Free object
In mathematics, the idea of a free object is one of the basic concepts of abstract algebra. It is a part of universal algebra, in the sense that it relates to all types of algebraic structure . It also has a formulation in terms of category theory, although this is in yet more abstract terms....
for theories of non-determinism. Just as the finite-powerset construction is the free semilattice, the powerdomain constructions should be understood abstractly as free models of theories of non-determinism. By changing the theories of non-determinism, different power domains arise.
The abstract characterisation of powerdomains is often the easiest way to work with them, because explicit descriptions are so intricate. (One exception is the Hoare powerdomain, which has a rather straightforward description.)
Theories of non-determinism
We recall three theories of non-determinism. They are variations of the theory of semilatticeSemilattice
In mathematics, a join-semilattice is a partially ordered set which has a join for any nonempty finite subset. Dually, a meet-semilattice is a partially ordered set which has a meet for any nonempty finite subset...
s. The theories are not algebraic theories in the conventional sense, because some involve the order of the underlying domain.
All theories have one sort X, and one binary operation ∪. The idea is that the operation ∪:X×X→X takes two combinations and returns the non-deterministic choice of them.
The Plotkin powertheory (after Gordon Plotkin
Gordon Plotkin
Gordon D. Plotkin, FRS, FRSE is a Scottish computer scientist.Gordon Plotkin is best-known for his introduction of structural operational semantics and his work on denotational semantics. In particular, his notes on A Structural Approach to Operational Semantics of 1981 were very influential...
) has one sort, X, and the following axioms:
- Idempotency: x∪x=x
- Commutativity: x∪y=y∪x
- Associativity: (x∪y)∪z=x∪(y∪z)
The lower (or Hoare, after Tony Hoare
C. A. R. Hoare
Sir Charles Antony Richard Hoare , commonly known as Tony Hoare or C. A. R. Hoare, is a British computer scientist best known for the development of Quicksort, one of the world's most widely used sorting algorithms...
) powertheory consists of the Ploktin powertheory augmented with the inequality
- x≤x∪y.
The upper (or Smyth, after M. B. Smyth) powertheory consists of the Ploktin powertheory augmented with the inequality
- x∪y≤x.
Models of the powertheories
A model of the Plotkin powertheory is a continuous semilatticeSemilattice
In mathematics, a join-semilattice is a partially ordered set which has a join for any nonempty finite subset. Dually, a meet-semilattice is a partially ordered set which has a meet for any nonempty finite subset...
: it is a semilattice whose carrier is a domain and for which the operation is continuous. Note that the operator need not be a meet or join for the order of the domain. A homomorphism of continuous semilattices is a continuous function between their carriers that respects the lattice operator.
Models of the lower powertheory are called inflationary semilattices; there is an additional requirement that the operator behave a little like a join for the order. For the upper powertheory, models are called deflationary semilattices; here, the operator behaves a little like a meet.
Power domains as free models
Let D be a domain. The Plotkin powerdomain on D is the freeFree object
In mathematics, the idea of a free object is one of the basic concepts of abstract algebra. It is a part of universal algebra, in the sense that it relates to all types of algebraic structure . It also has a formulation in terms of category theory, although this is in yet more abstract terms....
model of the Plotkin powertheory over D. It is defined to be (when it exists) a model P(D) of the Plotkin powertheory (ie a continuous semilattice) equipped with a continuous function X→P(D) such that for any other continuous semilattice L over D, there is a unique continuous semilattice homomorphism P(D)→L making the evident diagram commute.
Other powerdomains are defined abstractly in a similar manner.
Explicit descriptions of power domains
Let D be a domain. The lower power domain can be defined by- P[D] = {closure[A] | Ø∈A⊆D} where
-
-
-
- closure[A] = {d∈D | ∃X⊆D, X directed, d =
X, and ∀x∈X ∃a∈A x≤a}.
- closure[A] = {d∈D | ∃X⊆D, X directed, d =
-
-
In other words, P[D] is the collection of downward-closed subsets of D that are also closed under existing least upper bounds of directed sets in D. Note that while the ordering on P[D] is given by the subset relation, least upper bounds do not in general coincide with unions.
It is important to check which properties of domains are preserved by the power domain constructions. For example, the Hoare powerdomain of an ω-complete domain is again ω-complete.
Clinger's power domain
Clinger [1981] constructed a power domain for the Actor modelActor model
In computer science, the Actor model is a mathematical model of concurrent computation that treats "actors" as the universal primitives of concurrent digital computation: in response to a message that it receives, an actor can make local decisions, create more actors, send more messages, and...
building on the base domain of Actor event diagrams
Actor model theory
In theoretical computer science, Actor model theory concerns theoretical issues for the Actor model.Actors are the primitives that form the basis of the Actor model of concurrent digital computation. In response to a message that it receives, an Actor can make local decisions, create more Actors,...
, which is incomplete. See Clinger's model.
Timed diagrams power domain
Hewitt [2006] constructed a power domain for the Actor modelActor model
In computer science, the Actor model is a mathematical model of concurrent computation that treats "actors" as the universal primitives of concurrent digital computation: in response to a message that it receives, an actor can make local decisions, create more actors, send more messages, and...
(which is technically simpler and easier to understand than Clinger's model) building on a base domain of timed Actor event diagrams, which is complete. The idea is to attach an arrival time for each message received by an Actor. See Timed Diagrams Model.
Connections with topology and the Vietoris space
Domains can be understood as topological spaces, and, in this setting, the power domain constructions can be connected with the space of subsets construction introduced by Leopold VietorisLeopold Vietoris
Leopold Vietoris was an Austrian mathematician and a World War I veteran who gained additional fame by becoming a supercentenarian...
. See, for instance, [Smyth 1983].