A Powerdomain Primer: A Tutorial for The Bulletin of the EATCS
Abstract
The order-theoretic approach to programming semantics uses certain partially-ordered sets, called domains. Typically, the elements of a domain D are the "machine states" in which a computation may proceed, and a program is represented by a state-transformation function f : D --> D. The meaning of such a function is this: when the program is started in a state x epsilon D, then it will end in the state f (x). This "end-state" might be a special element of D which indicates that the program never terminated. This special element is usually considered to be just another "state" -- one that we frequently want to avoid. Of course, this is not the entire story of order-theoretic semantics: for example, I have not even mentioned what kind of partial-order a domain possesses, or the reason for the order. But this is enough of the story to motivate powerdomains. The motivation comes from a problem with the "typical" situation described above. We assumed that the state-transition relationship was a function, so that given a start-state x epsilon D, there is a single end-state f (x) epsilon D which will be reached by the program. But, some programs are nondeterministic -- meaning that a given start-state does not uniquely determine an end-state. We may also be uncertain about precisely which state a nondeterministic program starts in. Powerdomains are the solution to this problem. Intuitively, a powerdomain P is a special kind of domain whose elements are various "nondeterministic combinations of elements" from another domain. In this setting, a nondetermimstic program represents a function f : P --> P. The meaning of such a function is this: when the program is started in one of the states indicated by the nondeterministic combination X epsilon P, then it will end in one of the states of f (x). In general, different notions of powerdomains are based on different intuitions about what constitutes a "nondeterministic combination of elements".
Document Details
- Document Type
- Technical Report
- Publication Date
- Sep 01, 1987
- Accession Number
- ADA462121
Entities
People
- Michael G. Main
Organizations
- University of Colorado Boulder