powerdomain

Powerdomain is a construction in domain theory used to model nondeterministic computations in denotational semantics. Given a domain D, which is a structured partially ordered set of possible values with a notion of approximation, the powerdomain P(D) yields a new domain whose elements represent sets of potential results rather than a single outcome. The construction preserves key domain-theoretic properties such as continuity, enabling the use of fixed-point semantics for recursive definitions that involve nondeterminism.

There are several standard variants of the powerdomain, named Hoare, Smyth, and Plotkin. Each variant uses a different mathematical representation of nondeterministic choices and defines a corresponding refinement relation between elements. Hoare (lower) powerdomain uses downward-closed representations, Smyth (upper) powerdomain uses upward-closed representations, and Plotkin (convex) powerdomain uses convex representations. These diverse representations allow the powerdomain framework to model different flavors of nondeterminism and observation semantics found in programming languages.

Powerdomains are widely used to provide denotational semantics for languages and systems that involve nondeterminism, concurrency, or asynchronous I/O. They generalize the plain powerset construction from set theory while maintaining the order-theoretic structure required for domain-theoretic analysis. In particular, they enable reasoning about how nondeterministic computations refine or relate to one another in a mathematically rigorous way.

Example: if D is a simple domain of values with a bottom element, a nondeterministic computation that may yield several possible results can be represented in the corresponding powerdomain as a set of those results. The chosen powerdomain variant affects how the computation’s behavior and refinement are observed and compared within the semantic model.