The Hoare and Smyth power domain constructors commute under composition

摘要

This paper examines the composition of the Smyth and Hoare power domains (PS and PH) applied over the class of consistently complete algebraic partial orders represented by Scott's category of information systems. It is proposed that both orders of application yield equivalent domains. This is motivated by interpreting data elements in the Smyth as disjunction of propositions and those in the Hoare as conjunctions (as suggested by Scott), giving the two conjunctive-disjunctive forms for each of the double power domains. Then, using elementary category theory, it is shown that the images of any object under PS ○ PH and under PH ○ PS are isomorphic, and hence that both constructors are equivalent as functors.