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 | Leave a comment

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 | Leave a comment

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 | Leave a comment

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 | 4 Comments

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 | Leave a comment

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 | Leave a comment

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 | Leave a comment