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].
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 order this set according to the Egli-Milner preorder:
The Plotkin 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.
It is not necessarily true that , nor that .
The Plotkin powerdomain can also be described as a free continuous algebra for a nondeterministic operation on a domain that is also associative, commutative, and idempotent.
This characterisation is due to [Hennessy and Plotkin
It is easiest to describe the construction of the Plotkin powerdomain on a flat cpo (for countable).
We define to be the set
Notice that this accords with the intuitions of erratic nondeterminism. From [Søndergaard and Sestoft 1992]:
A set is interpreted as the set of results which must be possible, and may include indicating that non-termination is possible. All infinite sets also contain 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]:
Equivalently [Giantonio et al. 1995],
Finally, this order is equivalent to the Egli-Milner order on the powerset of , i.e.
where is the order of the flat cpo.
Notice that the bottom eleent of .
Plotkin, Gordon D. 1976. ‘A Powerdomain Construction’. SIAM Journal on Computing 5 (3): 452–87. [pdf]
@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}
}
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}
}
Hennessy, M. C. B., and G. D. Plotkin. 1979. ‘Full Abstraction for a Simple Parallel Programming Language’. In Mathematical Foundations of Computer Science 1979, edited by Jiří Bečvář, 74:108–20. Lecture Notes in Computer Science. Berlin, Heidelberg: Springer Berlin Heidelberg. https://doi.org/10.1007/3-540-09526-8_8.
@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}
}