A Complete Axiomatisation of Equivalence for Discrete Probabilistic Programming

TL;DR

This paper develops a comprehensive axiomatic framework for determining when discrete probabilistic programs are equivalent, using graphical syntax and category theory, with completeness results for both conditioning-free and full languages.

Contribution

It introduces a complete equational theory for discrete probabilistic programs, extending to conditioning primitives and connecting to Markov categories.

Findings

Proves a completeness result for the conditioning-free fragment.

Extends the completeness to the entire language with conditioning.

Provides a categorical presentation of Markov kernels for finite objects.

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.