摘要：We consider mixed powerdomains combining ordinary nondeterminism andprobabilistic nondeterminism. We characterise them as free algebras forsuitable (in)equation-al theories; we establish functional representationtheorems; and we show equivalencies between state transformers andappropriately healthy predicate transformers. The extended nonnegative realsserve as `truth-values'. As usual with powerdomains, everything comes in threeflavours: lower, upper, and order-convex. The powerdomains are suitable convexsets of subprobability valuations, corresponding to resolving nondeterministicchoice before probabilistic choice. Algebraically this corresponds to theprobabilistic choice operator distributing over the nondeterministic choiceoperator. (An alternative approach to combining the two forms of nondeterminismwould be to resolve probabilistic choice first, arriving at a domain-theoreticversion of random sets. However, as we also show, the algebraic approach thenruns into difficulties.) Rather than working directly with valuations, we take a domain-theoreticfunctional-analytic approach, employing domain-theoretic abstract convex setscalled Kegelspitzen; these are equivalent to the abstract probabilisticalgebras of Graham and Jones, but are more convenient to work with. So wedefine power Kegelspitzen, and consider free algebras, functionalrepresentations, and predicate transformers. To do so we make use of previouswork on domain-theoretic cones (d-cones), with the bridge between the two ofthem being provided by a free d-cone construction on Kegelspitzen.
