Smyth powerdomain

The Smyth powerdomain is one of the three basic powerdomain constructions.

The Smyth powerdomain is useful in modelling demonic nondeterminism Søndergaard and Sestoft 1992.

Construction

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 put a preorder on this set as follows:

A \sqsubseteq_0 B\ \triangleq\ \forall b \in B.\ \exists a \in A.\ a \sqsubseteq b

The Smyth powerdomain is then the ideal completion of this preorder \mathcal{M}(D). Consequently, it is an algebraic cpo too, and its compact elements are the principal ideals \mathop{\downarrow} X \triangleq \{ Y \subseteq 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_0 Y \triangleq \{ A \cup B \mid A \in X \text{ and } B \in Y \}

which is associative, commutative, and idempotent. Moreover, it satisfies

X \cup_0 Y \sqsubseteq X

Intuitively, this means that a nondeterministic choice holds less domain-theoretic information than any of its components.

Smyth characterisation for coherent domains

Smyth 1983 showed that, if D is coherent, then the Smyth powerdomain can also be obtained as the set of nonempty Scott-compact upper sets of (D, \sqsubseteq), ordered under reverse inclusion.

See also

• Powerdomains
• Hoare powerdomain
• Plotkin powerdomain

References

• The Smyth powerdomain was introduced in

@article{smyth_power_1978,
	title = {Power domains},
	volume = {16},
	issn = {00220000},
	doi = {10.1016/0022-0000(78)90048-X},
	number = {1},
	journal = {Journal of Computer and System Sciences},
	author = {Smyth, M.B.},
	year = {1978},
	pages = {23--36},
	file = {Smyth - 1978 - Power domains.pdf:C\:\\Users\\tz20861\\Zotero\\storage\\IJE44UDE\\Smyth - 1978 - Power domains.pdf:application/pdf},
}

• The intuition for why the Smyth powerdomain models demonic nondeterminism is spelled out 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}
}