A Powerdomain Construction

TLDR

Powerdomain construction is motivated by the need to model nondeterministic and parallel features in programming languages, yet existing approaches lack a convincing treatment of fair parallelism. The authors aim to develop a powerdomain construction that yields a natural, fully abstract semantics supporting equivalences such as (p par p) = (q par p). They define the powerdomain as the set of finitely generable subsets of a domain D, ordered elementwise when D is discrete and by the coarsest compatible ordering otherwise, and identify a closed class of algebraic inductive partial orders that supports sum, product, exponentiation, and recursive domain equations. The construction yields a closed class enabling recursive domain equations and illustrative semantics, but it remains unproven whether it achieves fully abstract semantics, though the desired equivalences hold.

Abstract

We develop a powerdomain construction, $\mathcal{P}[ \cdot ]$, which is analogous to the powerset construction and also fits in with the usual sum, product and exponentiation constructions on domains. The desire for such a construction arises when considering programming languages with nondeterministic features or parallel features treated in a nondeterministic way. We hope to achieve a natural, fully abstract semantics in which such equivalences as $(p\textit{ par } p) = (q\textit{ par }p)$ hold. The domain ($D \to $ Truthvalues) is not the right one, and instead we take the (finitely) generable subsets of D. When D is discrete they are ordered in an elementwise fashion. In the general case they are given the coarsest ordering consistent, in an appropriate sense, with the ordering given in the discrete case. We then find a restricted class of algebraic inductive partial orders which is closed under $\mathcal{P}[ \cdot ]$ as well as the sum, product and exponentiation constructions. This class permits the solution of recursive domain equations, and we give some illustrative semantics using $\mathcal{P}[ \cdot ]$. It remains to be seen if our powerdomain construction does give rise to fully abstract semantics, although such natural equivalences as the above do hold. The major deficiency is the lack of a convincing treatment of the fair parallel construct.