Consistent Hoare powerdomains

In this paper, we will introduce a new powerdomain construction called the consistent Hoare powerdomain, which is a free algebra over a continuous domain with a Scott continuous binary partial operator delivering least upper bounds (joins) for pairs of elements with an upper bound (consistent pairs), which is thus called consistent join operator (denoted by ∨↑∨↑). We will show that the consistent Hoare powerdomain over a continuous domain exists and is a continuous dcpo-∨↑∨↑-semilattice. Moreover, if the continuous domain is algebraic, then its consistent Hoare powerdomain is an algebraic dcpo-∨↑∨↑-semilattice.