# 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

## 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

## 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

## 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.

## On computable representations of exchangeable data

Exchangeable sequences are models for homogeneous data sets and serve as building blocks from which more interesting dependency structures in statistical models are produced. A sequence of random variables is exchangeable when its distribution does not depend on the ordering of its elements.… Read the rest

## 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 $\mu$ on a Polish space $P$ can be realized as $\mu = X_*\,\lambda$ for some random variable $X\colon [0,1]\to P$, where $\lambda$ denotes Lebesgue measure and $X_*\, \lambda$ is the “law of $X$,” the push forward of $\lambda$ under $X$.

## 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