Compositional Semantics for Probabilistic Programs with Exact Conditioning
This work addresses foundational challenges in probabilistic programming for researchers and practitioners, offering a generalizable framework for exact conditioning, though it is incremental in extending categorical methods to this domain.
The paper tackles the problem of defining a probabilistic programming language with exact conditioning on continuous random variables, which is nontrivial due to probability-zero observations like Borel's paradox, and presents a solution using categorical formulations to derive compositional semantics and properties like exchangeability of conditions.
We define a probabilistic programming language for Gaussian random variables with a first-class exact conditioning construct. We give operational, denotational and equational semantics for this language, establishing convenient properties like exchangeability of conditions. Conditioning on equality of continuous random variables is nontrivial, as the exact observation may have probability zero; this is Borel's paradox. Using categorical formulations of conditional probability, we show that the good properties of our language are not particular to Gaussians, but can be derived from universal properties, thus generalizing to wider settings. We define the Cond construction, which internalizes conditioning as a morphism, providing general compositional semantics for probabilistic programming with exact conditioning.