Keimel, Klaus and Plotkin, Gordon D. - Mixed powerdomains for probability and nondeterminism

lmcs:2578 - Logical Methods in Computer Science, January 24, 2017, Volume 13, Issue 1
Mixed powerdomains for probability and nondeterminism

Authors: Keimel, Klaus and Plotkin, Gordon D.

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.

Source :
DOI : 10.23638/LMCS-13(1:2)2017
Volume: Volume 13, Issue 1
Published on: January 24, 2017
Submitted on: January 24, 2017
Keywords: Computer Science - Logic in Computer Science


Consultation statistics

This page has been seen 395 times.
This article's PDF has been downloaded 130 times.