TY - JOUR
TI - A Domain Theory for Statistical Probabilistic Programming
AU - Vákár, Matthijs
AU - Kammar, Ohad
AU - Staton, Sam
T2 - arXiv:1811.04196 [cs]
AB - We give an adequate denotational semantics for languages with recursive higher-order types, continuous probability distributions, and soft constraints. These are expressive languages for building Bayesian models of the kinds used in computational statistics and machine learning. Among them are untyped languages, similar to Church and WebPPL, because our semantics allows recursive mixed-variance datatypes. Our semantics justifies important program equivalences including commutativity. Our new semantic model is based on `quasi-Borel predomains'. These are a mixture of chain-complete partial orders (cpos) and quasi-Borel spaces. Quasi-Borel spaces are a recent model of probability theory that focuses on sets of admissible random elements. Probability is traditionally treated in cpo models using probabilistic powerdomains, but these are not known to be commutative on any class of cpos with higher order functions. By contrast, quasi-Borel predomains do support both a commutative probabilistic powerdomain and higher-order functions. As we show, quasi-Borel predomains form both a model of Fiore's axiomatic domain theory and a model of Kock's synthetic measure theory.
DA - 2018/11/10/
PY - 2018
DP - arXiv.org
UR - http://arxiv.org/abs/1811.04196
Y2 - 2019/10/10/11:49:16
ER -
TY - JOUR
TI - Mixed powerdomains for probability and nondeterminism
AU - Keimel, Klaus
AU - Plotkin, Gordon D.
T2 - arXiv:1612.01005 [cs]
AB - 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.
DA - 2017///
PY - 2017
DO - 10/ggdmrp
DP - arXiv.org
UR - http://arxiv.org/abs/1612.01005
Y2 - 2019/11/28/12:04:57
KW - Denotational semantics
KW - Powerdomains
KW - Probabilistic programming
KW - Programming language theory
ER -
TY - JOUR
TI - Predicate Transformers for Extended Probability and Non-determinism
AU - Keimel, Klaus
AU - Plotkin, Gordon d.
T2 - Mathematical. Structures in Comp. Sci.
AB - We investigate laws for predicate transformers for the combination of non-deterministic choice and (extended) probabilistic choice, where predicates are taken to be functions to the extended non-negative reals, or to closed intervals of such reals. These predicate transformers correspond to state transformers, which are functions to conical powerdomains, which are the appropriate powerdomains for the combined forms of non-determinism. As with standard powerdomains for non-deterministic choice, these come in three flavours – lower, upper and (order-)convex – so there are also three kinds of predicate transformers. In order to make the connection, the powerdomains are first characterised in terms of relevant classes of functionals. Much of the development is carried out at an abstract level, a kind of domain-theoretic functional analysis: one considers d-cones, which are dcpos equipped with a module structure over the non-negative extended reals, in place of topological vector spaces. Such a development still needs to be carried out for probabilistic choice per se; it would presumably be necessary to work with a notion of convex space rather than a cone.
DA - 2009/06//
PY - 2009
DO - 10/bkvgqc
DP - ACM Digital Library
VL - 19
IS - 3
SP - 501
EP - 539
SN - 0960-1295
UR - http://dx.doi.org/10.1017/S0960129509007555
Y2 - 2019/11/26/20:33:27
KW - Denotational semantics
KW - Powerdomains
KW - Programming language theory
ER -
TY - JOUR
TI - Semantic Domains for Combining Probability and Non-Determinism
AU - Tix, Regina
AU - Keimel, Klaus
AU - Plotkin, Gordon
T2 - Electronic Notes in Theoretical Computer Science
AB - We present domain-theoretic models that support both probabilistic and nondeterministic choice. In [36], Morgan and McIver developed an ad hoc semantics for a simple imperative language with both probabilistic and nondeterministic choice operators over a discrete state space, using domain-theoretic tools. We present a model also using domain theory in the sense of D.S. Scott (see e.g. [15]), but built over quite general continuous domains instead of discrete state spaces.
DA - 2009/02//
PY - 2009
DO - 10/d9hwq7
DP - Crossref
VL - 222
SP - 3
EP - 99
LA - en
SN - 15710661
UR - https://linkinghub.elsevier.com/retrieve/pii/S1571066109000036
Y2 - 2019/11/26/19:01:09
KW - Denotational semantics
KW - Powerdomains
KW - Probabilistic programming
KW - Programming language theory
ER -
TY - CONF
TI - A Probabilistic Powerdomain of Evaluations
AU - Jones, C.
AU - Plotkin, G.
C1 - Piscataway, NJ, USA
C3 - Proceedings of the Fourth Annual Symposium on Logic in Computer Science
DA - 1989///
PY - 1989
DP - ACM Digital Library
SP - 186
EP - 195
PB - IEEE Press
SN - 978-0-8186-1954-0
UR - http://dl.acm.org/citation.cfm?id=77350.77370
Y2 - 2019/11/26/17:27:23
KW - Denotational semantics
KW - Powerdomains
KW - Probabilistic programming
KW - Programming language theory
ER -