Plotkin powerdomain

The Plotkin powerdomain (or convex powerdomain) is one of the three main powerdomain constructions.

The Plotkin powerdomain is useful for modelling erratic nondeterminism Søndergaard and Sestoft 1992.

Description

Through ideal completion

Let D be an algebraic cpo, and let \mathsf{K}(D) be its set of compact elements.

Let

\mathcal{M}(D) \triangleq \{ X \subseteq \mathsf{K}(D) \mid X \neq \emptyset, X \text{ finite} \}

be the set of nonempty, finite sets of compact elements. We order this set according to the Egli-Milner preorder:

A \sqsubseteq_{EM} B
  \quad\triangleq\quad
  (\forall a \in A.\ \exists b \in B.\ a \sqsubseteq b) \land
  (\forall b \in B.\ \exists a \in A.\ a \subseteq b)

The Plotkin powerdomain is then the ideal completion of this preorder (\mathcal{M}(D), \sqsubseteq_{EM}). Consequently, it is an algebraic cpo too, and its compact elements are the principal ideals \mathop{\downarrow} X \triangleq \{ Y \sqsubseteq_{EM} X \mid X \in \mathcal{M}(D) \}.

This ideal completion consists of directed lower sets of \mathcal{M}(D). It carries a natural union operation

X \cup_{EM} Y \triangleq \{ A \cup B \mid A \in X \text{ and } B \in Y \}

which is associative, commutative, and idempotent.

It is not necessarily true that X \cup_{EM} Y \sqsubseteq X, nor that X \sqsubseteq X \cup_{EM} Y.

As a free algebra

The Plotkin powerdomain can also be described as a free continuous algebra for a nondeterministic operation \cup : D \times D \to D on a domain D that is also associative, commutative, and idempotent.

This characterisation is due to Hennessy and Plotkin

On a flat cpo

It is easiest to describe the construction of the Plotkin powerdomain (\mathcal{P}(S_\bot), \sqsubseteq) on a flat cpo S_\bot (for S countable).

We define \mathcal{P}(S_\bot) to be the set

\{
  A \subseteq S_\bot
	  \mid A \neq \emptyset, A \text{ finite} \lor \bot \in A
\}

Notice that this accords with the intuitions of erratic nondeterminism. From Søndergaard and Sestoft 1992:

A set A is interpreted as the set of results which must be possible, and may include \bot indicating that non-termination is possible. All infinite sets also contain \bot to reflect that with erratic non-determinism, if a computation can return infinitely many results, then it can also go on forever.

We define the order as follows Plotkin 1976:

  A \sqsubseteq B
    \quad\triangleq\quad
  (\bot \not\in A \land A = B) \lor (\bot \in A \land A\setminus\{ \bot \} \subseteq B)

Equivalently Giantonio et al. 1995,

  A \sqsubseteq B
    \quad\triangleq\quad
  A = B \lor (\bot \in A \land A\setminus\{ \bot \} \subseteq B)

Finally, this order is equivalent to the Egli-Milner order on the powerset of S_\bot, i.e.

  A \sqsubseteq B
    \quad\triangleq\quad
  (\forall x \in A.\ \exists y \in B.\ x \leqslant y)
    \land
  (\forall y \in B.\ \exists x \in A.\ x \leqslant y)

where \leqslant is the order of the flat cpo.

Notice that the bottom eleent of \{ \bot \}.

See also

• Powerdomains
• Hoare powerdomain
• Smyth powerdomain

References

• The Plotkin powerdomain was introduced in

@article{plotkin_1976,
	title = {A powerdomain construction},
	volume = {5},
	number = {3},
	journal = {SIAM Journal on Computing},
	author = {Plotkin, Gordon D.},
	year = {1976},
	pages = {452--487}
}

• Qualitative features of the Plotkin powerdomain on a flat cpo, in particular when it comes to modelling finite nondeterminism, are discussed in

@article{sondergaard_1992,
	title = {Non-determinism in {Functional} {Languages}},
	volume = {35},
	doi = {10.1093/comjnl/35.5.514},
	number = {5},
	journal = {The Computer Journal},
	author = {Søndergaard, H. and Sestoft, P.},
	year = {1992},
	pages = {514--523}
}

• The characterisation of the Plotkin powerdomain as a free algebra over domains was given in

@inproceedings{hennessy_1979,
	address = {Berlin, Heidelberg},
	series = {Lecture {Notes} in {Computer} {Science}},
	title = {Full abstraction for a simple parallel programming language},
	volume = {74},
	doi = {10.1007/3-540-09526-8_8},
	booktitle = {Mathematical {Foundations} of {Computer} {Science} 1979},
	publisher = {Springer Berlin Heidelberg},
	author = {Hennessy, M. C. B. and Plotkin, G. D.},
	editor = {Bečvář, Jiří},
	year = {1979}
}