Monthly Archives: December 2015

Problems of the Lightweight Implementation of Probabilistic Programming

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. … Read the rest

A Denotational Semantics of a Probabilistic Stream-Processing Language: Yohei Miyamoto, Kohei Suenaga, and Koji Nakazawa

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 [3].… Read the rest

An Interface for Black Box Learning in Probabilistic Programs

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

1. Deterministic steps, which have no effect on the probability of the execution.
Posted in Uncategorized | Comments Off on An Interface for Black Box Learning in Probabilistic Programs

Coalgebraic Trace Semantics for Probabilistic Processes (Preliminary Proposal)

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

Making our Own Luck: A Language for Writing Random Generators

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. … Read the rest

Posted in Uncategorized | 2 Comments

eXchangeable Random Primitives

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

Models for Probabilistic Programs with an Adversary

While working on a Hoare logic for probabilistic programs [1], 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

Posted in Uncategorized | | 4 Comments

Reproducing kernel Hilbert space semantics for probabilistic programs

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 $\omega$-complete partial orders ($\omega$-cpos) in the formalization and analysis of probabilistic programming languages. The presented work is formalized in the Isabelle theorem prover.
By applying $\omega$-cpos to the analysis of MDPs we get a nice theory of fixed points.… Read the rest