Apt-Plotkin powerdomain

The Apt-Plotkin powerdomain is a powerdomain construction on flat cpo's. It is used to model countable nondeterminism.

Description

Let S be a set that is at most countable.

The Apt-Plotkin powerdomain \mathcal{P}^\omega(S_\bot) on a flat cpo is the set of nonempty subsets of S_\bot:

\{ A \subseteq S_\bot \mid A \neq \emptyset \}

It is ordered by the Egli-Milner order. Equivalently:

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

The least element is \{ \bot \}.

Relationship to the Plotkin powerdomain

The above construction is very closely related to the Plotkin powerdomain.

In fact, the only difference is that we take all nonempty A \subseteq S_\bot, whereas the Plotkin powerdomain takes only those A which are either finite, or contain \bot.

Thus, the Plotkin powerdomain can't model the possible output set \{ 0, 1, 2, \ldots \}, but only the possible output set \{ \bot, 0, 1, 2, \ldots \}.

See also

• Powerdomains
• Plotkin powerdomain

References

• The Apt-Plotkin powerdomain construction is introduced in

@article{apt_1986,
	title = {Countable nondeterminism and random assignment},
	volume = {33},
	doi = {10.1145/6490.6494},
	number = {4},
	journal = {Journal of the ACM},
	author = {Apt, K. R. and Plotkin, G. D.},
	year = {1986},
	pages = {724--767}
}