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

lmcs:2578 - Logical Methods in Computer Science, January 24, 2017, Volume 13, Issue 1 - https://doi.org/10.23638/LMCS-13(1:2)2017
Mixed powerdomains for probability and nondeterminism

Authors: Klaus Keimel ; Gordon D. Plotkin

    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.


    Volume: Volume 13, Issue 1
    Published on: January 24, 2017
    Accepted on: January 24, 2017
    Submitted on: January 24, 2017
    Keywords: Computer Science - Logic in Computer Science

    Share

    Consultation statistics

    This page has been seen 852 times.
    This article's PDF has been downloaded 303 times.