Power domains

From Wikipedia, the free encyclopedia

In denotational semantics power domains are used to construct denotations of programs.

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.

[edit] Explanation

According to Clinger [1981], power domains can be constructed from incomplete domains as follows:

Definition. Let <D, ≤> be a domain. Its power domain is <P[D], ⊆> where

P[D] = {closure[A] | Ø∈A⊆D} where

closure[A] = {d∈D | ∃X⊆D, X directed, d = X, and ∀x∈X ∃a∈A x≤a}

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.

The next theorem gives several nice properties of the power domain. In particular, it is an ω-complete domain, so ω-continuous functions have fixed points.

Definition. A countably based continuous complete lattice is an ω-complete domain such that for any subset X of the domain both a least upper bound X and a greatest lower bound X exist.

Theorem. If <D, ≤> is a domain, then <P[D], ⊆> is a countably based continuous complete lattice.

[edit] Theorem

The following theorem says that at a certain level of abstraction P[D] is the same as the traditional power domain of D. While P[D] can be used to provide denotational semantics for concurrent Actor-based programming languages with unbounded nondeterminism, the conventional power domain is usually considered incapable of expressing unbounded nondeterminism. This points out the importance of the concrete interpretaton placed upon elements of the power domain.

Theorem. If <D, ≤> is a domain, then <P[D], ⊆> is isomorphic to <completion[finiteFrontiers[D]], ⊆> where

finiteFrontiers[D] = {A⊆D | A is a nonempty finite set of isolated elements, and

∀x,y∈A x≤y implies x=y}

Each element A in the range of the finiteFrontiers of a domain is both minimal and maximal in A.

[edit] References

• Irene Greif. Semantics of Communicating Parallel Professes MIT EECS Doctoral Dissertation. August 1975.
• Joseph E. Stoy, Denotational Semantics: The Scott-Strachey Approach to Programming Language Semantics. MIT Press, Cambridge, Massachusetts, 1977. (A classic if dated textbook.)
• Gordon Plotkin. A powerdomain construction SIAM Journal of Computing September 1976.
• Carl Hewitt and Henry Baker Actors and Continuous Functionals Proceeding of IFIP Working Conference on Formal Description of Programming Concepts. August 1-5, 1977.
• Henry Baker. Actor Systems for Real-Time Computation MIT EECS Doctoral Dissertation. January 1978.
• Michael Smyth. Power domains Journal of Computer and System Sciences. 1978.
• George Milne and Robin Milner. Concurrent processes and their syntax JACM. April, 1979.
• CAR Hoare. Communicating Sequential Processes CACM. August, 1978.
• Nissim Francez, CAR Hoare, Daniel Lehmann, and Willem de Roever. Semantics of nondeterminism, concurrency, and communication Journal of Computer and System Sciences. December 1979.
• Jerald Schwartz Denotational semantics of parallelism in Semantics of Concurrent Computation. Springer-Verlag. 1979.
• William Wadge. An extensional treatment of dataflow deadlock Semantics of Concurrent Computation. Springer-Verlag. 1979.
• Ralph-Johan Back. Semantics of Unbounded Nondeterminism ICALP 1980.
• David Park. On the semantics of fair parallelism Proceedings of the Winter School on Formal Software Specification. Springer-Verlarg. 1980.
• Will Clinger, Foundations of Actor Semantics. MIT Mathematics Doctoral Dissertation, June 1981.
• Carl Hewitt, What is Commitment? Physical, Organizational, and Social COIN@AAMAS. April 27, 2006.