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].
Let be an algebraic cpo, and let be its set of compact elements.
Let
be the set of nonempty, finite sets of compact elements. We put a preorder on this set as follows:
The Smyth powerdomain is then the ideal completion of this preorder . Consequently, it is an algebraic cpo too, and its compact elements are the principal ideals .
This ideal completion consists of directed lower sets of . It carries a natural union operation
which is associative, commutative, and idempotent. Moreover, it satisfies
Intuitively, this means that a nondeterministic choice holds less domain-theoretic information than any of its components.
[Smyth 1983] showed that, if is coherent, then the Smyth powerdomain can also be obtained as the set of nonempty Scott-compact upper sets of , ordered under reverse inclusion.
Smyth, M.B. 1978. ‘Power Domains’. Journal of Computer and System Sciences 16 (1): 23–36. https://doi.org/10.1016/0022-0000(78)90048-X.
@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},
}
Søndergaard, H., and P. Sestoft. 1992. ‘Non-Determinism in Functional Languages’. The Computer Journal 35 (5): 514–23. https://doi.org/10.1093/comjnl/35.5.514.
@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}
}