Hoare powerdomain

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.

Definition

Let (D, \sqsubseteq) be an algebraic dcpo. Moreover, we write \textsf{K}(D) for the compact elements of D.

Simple construction

We define \mathcal{L}(D) to consist of the subsets X \subseteq \textsf{K}(D) of compact elements of D which are

1. Nonempty, i.e. X \neq \emptyset, and also
2. Lower sets, i.e. y \sqsubseteq x \in X \Longrightarrow y \in X.

This becomes a cpo under the inclusion order.

This description can be found in Winskel 1985.

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_H B\ \triangleq\ \forall a \in A.\ \exists b \in B.\ a \sqsubseteq b

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

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

X \sqsubseteq X \cup_H Y

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

Smyth characterisation

Smyth 1983 showed that the Hoare powerdomain can also be obtained as the set of nonempty Scott-closed subsets of (D, \sqsubseteq), ordered under inclusion.

History

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.

See also

• Powerdomains
• Smyth powerdomain
• Plotkin powerdomain

References

• The Smyth characterisation first appeared in the following ICALP 1983 paper:

@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}
}

• Some comments on the historical origins of the Smyth powerdomain are given in

@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},
}

• The intuition for why the Hoare powerdomain models angelic 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}
}