Guaranteed Inference for Probabilistic Programs: A Parallelisable, Small-Step Operational Approach

We put forward an approach to the semantics of probabilistic programs centered on an action-based language equipped with a small-step operational semantics. This approach provides benefits in terms of both clarity and effective implementation. Discrete and continuous distributions can be freely mixed, unbounded loops are allowed. In measure-theoretic terms, a product of Markov kernels is used to formalize the small-step operational semantics. This approach directly leads to an exact sampling algorithm that can be efficiently SIMD-parallelized. An observational semantics is also introduced based on a probability space of infinite sequences, along with a finite approximation theorem. Preliminary experiments with a proof-of-concept implementation based on TensorFlow show that our approach compares favourably to state-of-the-art tools for probabilistic programming and inference.