Some Consistent Power Constructions
Chengyu Zhou, Qingguo Li
TL;DR
The paper advances consistent power constructions by embedding them into a categorical framework for dcpos, introducing sub o.b.d-algebras and a method to modify monads to carry consistent algebraic features. It constructs two new free power-domain families, the consistent Plotkin index power domain IV^c_p and the consistent probabilistic power domain V_{≤1}^c, grounding them in D-algebraic theory and Kegelspitzen. These results provide robust semantic tools for modeling nondeterminism and probabilistic choice within Moggi-style computational effects, enabling more flexible and principled domain-theoretic semantics for functional languages.
Abstract
Consistent Hoare, Smyth and Plotkin power domains are introduced and discussed by Yuan and Kou. The consistent algebraic operation $+$ defined by them is a binary partial Scott continuous operation satisfying the requirement: $a+b$ exists whenever there exists a $c$ which is greater than $a$ and $b$. We extend the consistency to be a categorical concept and obtain an approach to generating consistent monads from monads on dcpos whose images equipped with some algebraic operations. Then we provide two new power constructions over domains: the consistent Plotkin index power domain and the consistent probabilistic power domain. Moreover, we verify these power constructions are free.