The Hoare (or lower powerdomain) is one of the three main powerdomain constructions.
The Hoare powerdomain is useful for modelling angelic nondeterminism [Søndergaard and Sestoft 1992].
Let be an algebraic dcpo. Moreover, we write for the compact elements of .
We define to consist of the subsets of compact elements of which are
This becomes a cpo under the inclusion order.
This description can be found in [Winskel 1985].
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 Hoare 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 more domain-theoretic information than any of its components.
[Smyth 1983] showed that the Hoare powerdomain can also be obtained as the set of nonempty Scott-closed subsets of , ordered under inclusion.
The Hoare powerdomain has been independently invented by a number of people. Here is a quote from [Winskel 1985] on its historical origins:
This powerdomain has been called the Hoare powerdomain by Plotkin because of its relation with C.A.R. Hoare's work on partial correctness. To be fair, this powerdomain has been invented independently by many people, Plotkin and D. Park to name two while the 'Traces model' for a version of CSP [7] provides an instance of this powerdomain. The Hoare powerdomain ignores the divergence of computations completely but like the Smyth powerdomain works smoothly within the category of consistently complete algebraic domains.
Smyth, M. B. 1983. ‘Power Domains and Predicate Transformers: A Topological View’. In Automata, Languages and Programming, edited by Josep Diaz, 154:662–75. Lecture Notes in Computer Science. Springer-Verlag. https://doi.org/10.1007/BFb0036946.
@inproceedings{smyth_1983,
series = {Lecture {Notes} in {Computer} {Science}},
title = {Power domains and predicate transformers: {A} topological view},
volume = {154},
doi = {10.1007/BFb0036946},
booktitle = {Automata, {Languages} and {Programming}},
publisher = {Springer-Verlag},
author = {Smyth, M. B.},
editor = {Diaz, Josep},
year = {1983},
pages = {662--675}
}
Winskel, Glynn. 1985. ‘On Powerdomains and Modality’. Theoretical Computer Science 36: 127–37. https://doi.org/10.1016/0304-3975(85)90037-4.
@article{winskel_1985,
title = {On powerdomains and modality},
volume = {36},
doi = {10.1016/0304-3975(85)90037-4},
journal = {Theoretical Computer Science},
author = {Winskel, Glynn},
year = {1985},
pages = {127--137},
}
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}
}