Power domain constructions (Q1183553): Difference between revisions

In this very interesting and well written paper, the five known power domain constructions are unified by an axiomatic framework. A power domain construction assigns to each domain \({\mathbf X}\) (i.e., \({\mathbf X}\) is a directed complete poset) another domain \({\mathcal P}{\mathbf X}\) which is a commutative monoid, with a binary operation representing a formal union operation and neutral element \(\theta\), representing the empty set, as well as a singleton map \(\iota: {\mathbf X}\to{\mathcal P}{\mathbf X}\). Lastly, for all domains \({\mathbf X}\), \({\mathbf Y}\) on which \({\mathcal P}\) is defined, there is an extension operation \((f: {\mathbf X}\to{\mathcal P}{\mathbf Y})\mapsto(\overline f: {\mathcal P}{\mathbf X}\to{\mathcal P}{\mathbf Y})\) such that \(f=\overline f\circ\iota\) and some other natural conditions are satisfied. The extension need not be unique, or as the diagram shows, there would be a left adjunction involved. Nevertheless, \(\mathcal P\) determines a functor. Letting \({\mathbf X}\) be the singleton domain \(\mathbf{1}=\{*\}\), one gets a ``logic'' on \({\mathcal P}\mathbf{1}\), which necessarily contains at least two values. The author shows that there is a natural action \({\mathcal P}\mathbf{1}\times{\mathcal P}{\mathbf X}\to{\mathcal P}{\mathbf X}\) which makes \({\mathcal P}{\mathbf X}\) into a \({\mathcal P}\mathbf{1}\) module. When \({\mathcal P}\mathbf{1}\) acts on itself, the action combined with the formal union, make \({\mathcal P}\mathbf{1}\) a semiring, called the characteristic semiring of the power construction \({\mathcal P}\). In the case of the lower power construction, this semiring is \(\{0,1\}\) with \(0<1\) and \(1+1=1\). The upper power construction has another two element semiring with \(1<0\); the Plotkin semiring has a two element subsemiring in which the elements are incomparable. Power morphisms between power constructions \({\mathcal P}\), \({\mathcal Q}\) are certain natural transformations which are monoid homomorphisms preserving the extension structure. When the characteristic semirings of \({\mathcal P}\) and \({\mathcal Q}\) are the same, a power morphism \(H: {\mathcal P}\to{\mathcal Q}\) is linear if \(H\) preserves the action. The main result is that for each semiring \(R={\mathcal P}\mathbf{1}\) there are initial and final objects in the category of power constructions and linear power morphisms. All proofs are given in quite some detail. (Reviewer's remark: The author's \(| R|^{|{\mathbf X}|}\) can be replaced by either \(| R\times{\mathbf X}|\) or \(\aleph_ 0\), since the cardinality of the set \({\mathbf M}^ \#\) on page 116 is at most that of the set of finite sequences of \(| R\times{\mathbf X}|)\).