Probabilistic programs extend ordinary programs by the abilities to sample values from probability distributions and conditioning. They are ubiquitous in modern computing and appear, for example, in randomized algorithms, random sampling, statistical inference routines, cognitive science, and autonomous systems.

A formal (denotational) program semantics associates each program with a function mapping (non-negative) measures over input states to measures over output states. A fundamental computational task in probabilistic programming is to infer a program’s output (posterior) distribution from a given initial (prior) distribution. This problem is challenging, especially for expressive languages that feature loops or unbounded recursion. We aim to push the limits of exact automatic loop analysis. More formally, given a discrete probabilistic loop and a discrete initial distribution over program states, we want to automatically compute an exact representation of the output distribution.

Due to standard undecidability results for while loops, there is no hope for a complete algorithmic solution for exact inference. Our goal is thus to provide heuristics covering reasonably many instances. To achieve this, we combine generating functions as a representation for (infinite-support) distributions with a seemingly less well-known characterization of a loop’s output distribution through its occupation measure due to Sharir et al.