Power domain constructions

Continuous lattices and posets, applications (06B35) Applications of universal algebra in computer science (08A70) Semantics in the theory of computing (68Q55)

Review text

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}|)\).

Recommendations

Cited in

(30)

This page was built for publication: Power domain constructions

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1183553)