Staton has recently argued convincingly that first-order functional probabilistic programs with sampling from continuous distributions and soft constraints correspond precisely to so-called s-finite kernels. This class of possibly infinite kernels is a little studied extension of their better known σ-finite cousins, obtained by closing them under kernel integration – or pushforwards along measurable functions.

Staton has demonstrated that this class of kernels has various desirable properties like closure under composition and a Fubini-Tonelli result on swapping order of integration. Still, s-finite measures and kernels remain poorly understood and their basic theory still needs to be established.

We characterise their precise relationship to σ-finite and probability measures and kernels. This lets us establish basic results in the s-finite setting like Randomisation, Radon-Nikodým and Disintegration Theorems. These results explicate, respectively, how to understand s-finite probabilistic computation as deterministic computation with access to a Lebesgue measure oracle, when we can apply importance sampling in this setting and that s-finite measures have a well-defined theory of conditional probability.

Further, we sketch how s-finite kernels work together well with traditional game semantics techniques to give fully abstract models of higher-order probabilistic programming languages. The key insight here is that the intensional level of description of game semantics restricts higher-order functions to be tame enough such that classical measure theory (standard Borel spaces) suffices to describe function types, thus circumventing Aumann’s celebrated no-go theorem. Perhaps this explains why this no-go theorem is not encountered as an obstruction in implementing higher-order probabilistic languages?

Authors: Luke Ong, Matthijs Vákár.

Extended abstract: [pdf]

Poster: [pdf]