A characterization of the consistent Hoare powerdomains over dcpos

TL;DR

This paper provides a new direct characterization of the consistent Hoare powerdomain over dcpos using the notion of -existing sets, and establishes an isomorphism with F-Scott closed sets.

Contribution

It introduces the concept of -existing sets for a direct characterization of the consistent Hoare powerdomain over dcpos.

Findings

The set of -existing Scott closed subsets forms the consistent Hoare powerdomain.

The Scott closed set lattice of a dcpo is isomorphic to F-Scott closed sets of its powerdomain.

Abstract

It has been shown that for a dcpo P, the Scott closure of \Gamma_c(P) in \Gamma(P) is a consistent Hoare powerdomain of P, where \Gamma_c(P) is the family of nonempty, consistent and Scott closed subsets of P, and \Gamma(P) is the collection of all nonempty Scott closed subsets of P. In this paper, by introducing the notion of a \vee-existing set, we present a direct characterization of the consistent Hoare powerdomain: the set of all \vee-existing Scott closed subsets of a dcpo P is exactly the consistent Hoare powerdomain of P. We also introduce the concept of an F-Scott closed set over each dcpo-\vee-semilattice. We prove that the Scott closed set lattice of a dcpo P is isomorphic to the family of all F-Scott closed sets of P's consistent Hoare powerdomain.