Borel Kernels and their Approximation, Categorically

Understand

This paper introduces a categorical framework to study the exact and approximate semantics of probabilistic programs.

• We construct a dagger symmetric monoidal category of Borel kernels where the dagger-structure is given by Bayesian inversion.
• We show functorial bridges between this category and categories of Banach lattices which formalize the move from kernel-based semantics to predicate transformer (backward) or state transformer (forward) semantics.
• These bridges are related by natural transformations, and we show in particular that the Radon-Nikodym and Riesz representation theorems - two pillars of probability theory - define natural transformations.