A Complete Axiomatisation of Equivalence for Discrete Probabilistic Programming
Robin Piedeleu, Mateo Torres-Ruiz, Alexandra Silva, Fabio Zanasi
TL;DR
The paper addresses the challenge of deciding when discrete probabilistic programs are equivalent by translating them into probabilistic circuits expressed as string diagrams in symmetric monoidal categories, enabling a complete equational theory. It provides a two-stage completeness result: first for the conditioning-free fragment and then for the full language, with a compositional semantics that ensures diagrammatic equality corresponds to semantic equality of the induced distributions. It further connects to Markov categories by presenting a generators-and-equations presentation of the category of Markov kernels restricted to objects that are powers of the $2$-element set, deepening the axiomatic understanding of probability in this framework. The work enables exact, diagrammatic reasoning about discrete probabilistic programs and supports principled reasoning about equivalence, optimization, and verification of probabilistic models within a categorical setting.
Abstract
We introduce a sound and complete equational theory capturing equivalence of discrete probabilistic programs, that is, programs extended with primitives for Bernoulli distributions and conditioning, to model distributions over finite sets of events. To do so, we translate these programs into a graphical syntax of probabilistic circuits, formalised as string diagrams, the two-dimensional syntax of symmetric monoidal categories. We then prove a first completeness result for the equational theory of the conditioning-free fragment of our syntax. Finally, we extend this result to a complete equational theory for the entire language. Note these developments are also of interest for the development of probability theory in Markov categories: our first result gives a presentation by generators and equations of the category of Markov kernels, restricted to objects that are powers of the two-elements set.