has the following axioms: Idempotency: x ∪ x = x Commutativity: x ∪ y = y ∪ x Associativity: (x ∪ y) ∪ z = x ∪ (y ∪ z) The lower (or Hoare, after Tony Hoare) powertheory consists of the Plotkin powertheory augmented with the inequality x ≤ x ∪ y. The upper (or Smyth, after M. B. Smyth) powertheory consists of the Plotkin powertheory augmented with the inequality x ∪ y ≤ x. Models of the powertheories A model of the Plotkin powertheory is a continuous semilattice: it is a semilattice whose carrier is a domain and for which the operation is continuous. Note that the operator need not be a meet or join for the order of the domain. A homomorphism of continuous semilattices is a continuous function between their carriers that respects the lattice operator. Models of the lower powertheory are called inflationary semilattices; there is an additional requirement that the operator behave a little like a join for the order. For the upper powertheory, models are called deflationary semilattices; here, the operator behaves a little like a meet. Power domains as free models Let D be a domain. The Plotkin powerdomain on D is the free model of the Plotkin powertheory over D. It is defined to be (when it exists) a model P(D) of the Plotkin powertheory (i.e. a continuous semilattice) equipped with a continuous function D → P(D) such that for any other continuous semilattice L over D, there is a unique continuous semilattice homomorphism P(D) → L making the evident diagram commute. Other powerdomains are defined abstractly in a similar manner. Explicit descriptions of power domains Let D be a domain. The lower power domain can be defined by P[D] = {closure[A] | Ø ∈ A ⊆ D} where closure[A] = {d ∈ D | ∃ X ⊆ D, X directed, d = X, and ∀x ∈ X ∃ a ∈ A x ≤ a}. In other words, P[D] is the collection of downward-closed subsets of D that are also closed under existing least upper bounds of directed sets in D. Note that while the ordering on P[D] is given by the subset relation, least upper bounds do not in general coincide with unions. It is important to check which properties of domains are preserved by the power domain constructions. For example, the Hoare powerdomain of an ω-complete domain is again ω-complete.