We identify two problems with Wingate et al. lightweight implementation technique for probabilistic programs. Simple examples demonstrate that common, what should be semantic-preserving program transformations drastically alter the program behavior. We briefly describe an alternative technique that does respect the program refactoring. There remains a question of how to be really, formally sure that the MCMC acceptance ratio is computed correctly.… Read the rest
Monthly Archives: December 2015
We extend a stream-processing programming language, whose denotational semantics is given using the domain of streams, so that it can support probabilistic action. We give a denotational semantics to the extended language (which we call SProcP). We take the domain of probability distributions over streams as the denotational domain; it constitutes a cpo according to Saheb-Djaromi .… Read the rest
Structural operational semantics for probabilistic programming languages typically characterize each elementary step in an execution terms of
- The resulting value and/or changes to the environment.
- Effects on the probability of the execution.
In many probabilistic programming languages, the elementary steps in an execution can be separated into 3 categories
- Deterministic steps, which have no effect on the probability of the execution.
This is an abstract of a poster by Larry Moss, and Chung-chieh Shan, and Alexandra Silva. The one sentence summary of our proposal is to adapt ideas from coalgebraic semantics to the probabilistic setting, thereby obtaining intuitive semantics for probabilistic processes of various sorts.… Read the rest
QuickCheck-style property-based random testing requires efficient generators for well-distributed random data satisfying complex logical predicates. Writing such generators by hand can be difficult and error prone.
We propose a domain-specific language, Luck, in which generators are expressed by decorating predicates with lightweight annotations controlling both the distribution of generated values and the amount of constraint solving that happens before each variable is instantiated. Generators in
Luck are compact, readable, and maintainable, with efficiency close to custom handwritten generators.… Read the rest
In our view, one of the key contributions of the probabilistic programming language Church is a class of constructs, called exchangeable random primitives (or XRPs for short), that can be used to extend the language with stochastic primitives whose implementations use stateful computation.… Read the rest
While working on a Hoare logic for probabilistic programs , we encountered an interesting choice for how to define the operational semantics of the underlying probabilistic imperative language PRIMP. We could either define commands as mapping from states to states and then “lift” those commands to apply to distributions, or define those commands over state distributions as a whole.… Read the rest
We propose to write denotational semantics for a probabilistic programming language in terms of reproducing kernel Hilbert spaces for characteristic kernels. This opens up possibilities for providing convergence guarantees for approximate expansions, as well as practical advantages of using kernel methods for machine learning.… Read the rest
The goal of this paper is to advertise the application of fixed points and -complete partial orders (-cpos) in the formalization and analysis of probabilistic programming languages. The presented work is formalized in the Isabelle theorem prover.
By applying -cpos to the analysis of MDPs we get a nice theory of fixed points.… Read the rest