Monthly Archives: December 2016

Support and influence analysis for visualizing posteriors of probabilistic programs

A common way to interpret the results of any computational model is to visualize its output. For probabilistic programming, this often means visualizing a posterior probability distribution. The webppl language has a visualization library called webppl-viz that facilitates this process. A useful feature of webppl-viz is that it does some amount of automatic visualization—the user simply passes in the posterior and the library tries to construct a useful visual representation of it.… Read the rest

Posted in Uncategorized | Comments Off on Support and influence analysis for visualizing posteriors of probabilistic programs

Reasoning about Inference in Probabilistic Programs

Some of the fundamental errors that occur in probabilistic programs are due
to incorrect statistical models, ignoring dependence between random variables,
or, using wrong hyper-parameters (such as sample size) for inference. To prevent these errors, the solution most probabilistic programming languages adopt is to keep inference external to the core language semantics.… Read the rest

Posted in Uncategorized | Comments Off on Reasoning about Inference in Probabilistic Programs

Reducing Probabilistic Choice to Nondeterministic Choice

Okay, this isn’t really semantics, just a simple way to use ordinary invariants to reason about probabilistic transition systems (or programs). The trick is to to prove invariants of the form M + L >= 0, where L (“luck”) is a linear combination of “gambling balance” ghost variables that are initially 0 and are only updated with (state-dependent) fair bets on probabilistic choices.… Read the rest

Posted in Uncategorized | Comments Off on Reducing Probabilistic Choice to Nondeterministic Choice

Commutativity logic for probabilistic trace equivalence: complete or not?

Joint work with Nathan Bowler.

There’s a well-known monad (on Set) for probabilistic choice – the probability distribution monad.  And there’s a well-known monad for I/O – the free monad on a signature (set of operations).  We’ve developed a new monad for the combination of probabilistic choice and I/O using trace semantics. … Read the rest

Posted in Uncategorized | Comments Off on Commutativity logic for probabilistic trace equivalence: complete or not?

An Application of Computable Distributions to the Semantics of Probabilistic Programs: Part 2

We continue our previous work [5] on giving semantics to probabilistic programs using computable distributions. First, we highlight a gap in our previous semantics involving the measurability of an environment lookup function and address it. Second, we suggest topological domains, a category of domains proposed in the literature that supports both Type-2 computability and domain-theoretic constructions, as an alternative to DCPOs in giving semantics to probabilistic programs based on computable distributions.

Read the rest
Posted in Uncategorized | Comments Off on An Application of Computable Distributions to the Semantics of Probabilistic Programs: Part 2

Probabilistic Programming and a Domain Theoretic Approach to Skorohod’s Theorem

Skorohod’s Theorem is a fundamental result from stochastic process theory. It makes two assertions:

  1. Any Borel probability measure $latex \mu$ on a Polish space $latex P$ can be realized as $latex \mu = X_*\,\lambda$ for some random variable $latex X\colon [0,1]\to P$, where $latex \lambda$ denotes Lebesgue measure and $latex X_*\, \lambda$ is the “law of $latex X$,” the push forward of $latex \lambda$ under $latex X$.
Read the rest
Posted in Uncategorized | Comments Off on Probabilistic Programming and a Domain Theoretic Approach to Skorohod’s Theorem

The Extended Semantics For Probabilistic Programming Languages

Generative modeling languages, i.e., probabilistic programming languages (PPLs), offer only limited support for continuous variables; theorems concerning semantics and algorithmic correctness are often limited to discrete variables or, in some cases, bounded continuous variables.

We show natural examples that violate these restrictions and break standard algorithms.… Read the rest

Posted in Uncategorized | Comments Off on The Extended Semantics For Probabilistic Programming Languages

Efficient exact inference in discrete Anglican programs

The design of a general probabilistic programming system involves a balancing act between two deeply conflicting concerns. On the one hand, the system should provide as uniform and flexible an interface for specifying models as possible; on the other, it should be capable of doing efficient inference for any particular model specified.

Read the rest
Posted in Uncategorized | Comments Off on Efficient exact inference in discrete Anglican programs

A Weakest Pre-Expectation Semantics for Mixed-Sign Expectations

We propose a weakest-precondition-style calculus for reasoning about the expected values (pre-expectations) of mixed-sign unbounded random variables after execution of a probabilistic program. The semantics of a while-loop is well-defined as the limit of iteratively applying a functional to a zero-element just as in the traditional weakest pre-expectation calculus, even though a standard least fixed point argument is not applicable in this context.… Read the rest

Posted in Uncategorized | Comments Off on A Weakest Pre-Expectation Semantics for Mixed-Sign Expectations