CPOs as Concrete Domains: Lattices of Abstract Domains and Complements

It is well known that for a given concrete domain $C$ which is a complete lattice, the abstract domains of $C$ form the so-called lattice of abstract interpretations of $C$. In general lattice-theoretic terms, this reads as Ward's [1942] theorem stating that closure operators on a complete lattice, ordered pointwise, give rise to a complete lattice. This result plays an important role in the general field of semantic domain theory. We strengthen Ward's theorem by showing that closure operators on any directed-complete partial order (CPO) still form a complete lattice. This result therefore applies straight to the lattice of abstract interpretations. Furthermore, we exploit it in order to significantly extend the operation of abstract domain complementation, so that, e.g., it can be applied to any abstract domain which is a mere poset satisfying the ascending chain condition.