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

Context

Lecture. Domain theory › Monadic semantics, Scott domains and nondeterminism [dt-005V]

Backlinks

Remark. Angelic nondeterminism [dt-0063]

Example. Hoare powerdomain of \mathbb {N}_\bot [dt-0062]

Aside. Scott's original solution: using complete lattices [dt-004D]

The Plotkin powerdomain [dt-0067]

The Smyth powerdomain [dt-0064]

Related

Definition. Algebraicity [dt-0041]

Definition. Antisymmetry [dm-0003]

Definition. Compactness [dt-003U]

Definition. Directed set [dt-0010]

Definition. Down-closure [dt-0047]

Definition. Equivalence class [dm-000X]

Equivalence relation [dm-000W]

Definition. Flat domain [dt-0008]

Definition. Ideal [dt-0048]

Definition. Ideal completion [dt-0046]

Definition. Least upper bound [dt-0017]

Preorder [dm-000V]