7 QBS–Kernel Bridge
This chapter bridges the QBS probability monad with the s-finite kernel infrastructure from mathcomp-analysis (the merged kernel hierarchy kernel.v, originally from PR #896). S-finite kernels provide the standard semantic foundation for first-order probabilistic programs (Staton, ESOP 2017): they are closed under composition, unlike \(\sigma \)-finite kernels. The bridge developed here shows that QBS probabilities induce s-finite measures and that QBS morphisms between standard Borel spaces lift to probability kernels, so kernel-based programs embed faithfully into the QBS world while gaining higher-order function types.
7.1 S-Finiteness of Probability Measures
Every probability measure assigns a finite extended-real value to every measurable set.
Every probability measure is s-finite, since it is finite (and hence \(\sigma \)-finite).
For any QBS probability \(p : P(X)\) with \(X\) standard Borel, the induced measure \(\texttt{qbs\_ to\_ giry}(p)\) is s-finite.
Pushforward of a probability measure along a measurable map is a probability measure.
7.2 Dirac Kernels and QBS Return
Pointwise: \(\mathrm{kdirac}(f)(x)(U) = \delta _{f(x)}(U)\).
For standard Borel \(M\), transporting a Dirac measure through giry_to_qbs and back recovers the original Dirac measure.
Every measurable function \(f : M_1 \to M_2\) induces a Dirac probability kernel \(x \mapsto \delta _{f(x)}\).
The Dirac kernel of a measurable function is a probability kernel (not just s-finite).
7.3 QBS Morphisms as Kernels
Every QBS morphism between standard Borel spaces is measurable (full faithfulness of the \(R\) functor).
A QBS morphism between standard Borel spaces lifts to a Dirac probability kernel.
The Dirac kernel of a QBS morphism between standard Borel spaces is a probability kernel.
7.4 Constant Kernels and Equivalence
Every QBS probability \(p\) on a standard Borel space induces a constant kernel: \(x \mapsto \texttt{qbs\_ to\_ giry}(p)\).
The constant-kernel construction is a measurable family.
Equivalent QBS probabilities (via qbs_prob_equiv) yield equal classical Giry probability measures.
7.5 Pushforward and Kernel Composition
Applying qbs_to_giry to a mapped probability equals the pushforward of the original Giry measure.
The pushforward through a QBS morphism agrees with the classical Giry pushforward.
Pointwise: \(\mathrm{kdirac}(g \circ f) = \mathrm{kdirac}(g) \circ _{\mathrm{ker}} f\).
Composition of Dirac kernels equals the Dirac kernel of the function composition (functoriality at the kernel level).
The standard-Borel encode/decode round-trip lifts to the kernel level via kcomp.
7.6 Bind, Return, and Integration at the Kernel Level
Binding the return of a function with \(f\) equals the return of the function (the monad law at the kernel level).
The QBS integral against a probability \(p\) equals the Lebesgue integral against \(\texttt{qbs\_ to\_ giry}(p)\).
Sending a Dirac kernel through the QBS-Giry round-trip preserves it.
General kernel round-trip property via the QBS-Giry bridge.