Mixed powerdomains for probability and nondeterminism

TL;DR

This paper develops a domain-theoretic framework for mixed powerdomains combining nondeterminism and probability, using convex sets called Kegelspitzen to represent probabilistic algebras and establishing their algebraic and functional properties.

Contribution

It introduces power Kegelspitzen as a new domain-theoretic model for mixed nondeterminism and probability, providing algebraic characterizations and functional representations.

Findings

Power Kegelspitzen are equivalent to probabilistic algebras of Graham and Jones.

Powerdomains are suitable convex sets of subprobability valuations.

The algebraic approach faces difficulties when probabilistic choice is resolved first.

Abstract

We consider mixed powerdomains combining ordinary nondeterminism and probabilistic nondeterminism. We characterise them as free algebras for suitable (in)equation-al theories; we establish functional representation theorems; and we show equivalencies between state transformers and appropriately healthy predicate transformers. The extended nonnegative reals serve as `truth-values'. As usual with powerdomains, everything comes in three flavours: lower, upper, and order-convex. The powerdomains are suitable convex sets of subprobability valuations, corresponding to resolving nondeterministic choice before probabilistic choice. Algebraically this corresponds to the probabilistic choice operator distributing over the nondeterministic choice operator. (An alternative approach to combining the two forms of nondeterminism would be to resolve probabilistic choice first, arriving at a domain-theoretic version of random sets. However, as we also show, the algebraic approach then runs into difficulties.) Rather than working directly with valuations, we take a domain-theoretic functional-analytic approach, employing domain-theoretic abstract convex sets called Kegelspitzen; these are equivalent to the abstract probabilistic algebras of Graham and Jones, but are more convenient to work with. So we define power Kegelspitzen, and consider free algebras, functional representations, and predicate transformers. To do so we make use of previous work on domain-theoretic cones (d-cones), with the bridge between the two of them being provided by a free d-cone construction on Kegelspitzen.