The Hoare powerdomain [dt-0061]
We write \mathcal {P}_f^\ast (S) to denote finite non-empty subsets of S. Let X, Y \in \mathcal {P}_f^\ast (\mathsf {K}(A)) be finite, non-empty sets of compact elements of a Scott domain A. The Hoare powerdomain construction is based on the following ordering: X \preceq _H Y\quad \text {iff}\quad (\forall x \in X.\ \exists y \in Y.\ x \sqsubseteq _A y) The intuition behind this is that "Anything X can do, Y can do better". This ordering has some desirable properties: The least element is \{\bot \}, as we might expect. It also satisfies the equation X \preceq _H X \cup Y, which intuitively means that a non-deterministic choice is considered to have more information than any of its components. When specialised to the case where A is a flat domain like \Sigma _\bot , it simplifies to: X \preceq _H Y\quad \text {iff}\quad X \setminus \{\bot \} \subseteq Y This is, however, not a proper order, but a preorder, as it fails antisymmetry. Even in the flat domain case, \{ x, \bot \} \preceq _H \{x \} and \{ x \} \preceq _H \{x, \bot \} but they are not equal. However, any preorder does induce an equivalence relation, where X \approx _H Y iff X \preceq _H Y and Y \preceq _H X. Furthermore, if we take the ideal completion of \mathcal {P}_f^\ast (K(A)) with respect to the preorder \preceq _H (i.e., the set of all \preceq _H-downwards-closed directed subsets of \mathcal {P}_f^\ast (\mathsf {K}(A))), we can order them by inclusion to obtain an algebraic domain with compact elements which correspond to equivalence classes of elements under \approx _H. We have a lub operation for these ideals: A \sqcup _H B = \{ X \cup Y \mid X \in A \land Y \in B \}