A convenient category for higher-order probability theory

By Chris Heunen, Ohad Kammar, S. Staton, Hongseok Yang. 2017

188 citations recorded by the source corpus.

Higher-order probabilistic programming languages allow programmers to write sophisticated models in machine learning and statistics in a succinct and structured way, but step outside the standard measure-theoretic formalization of probability theory. Programs may use both higher-order functions and continuous distributions, or even define a probability distribution on functions. But standard probability theory does not handle higher-order functions well: the category of measurable spaces is not cartesian closed. Here we introduce quasi-Borel spaces. We show that these spaces: form a new formalization of probability theory replacing measurable spaces; form a cartesian closed category and so support higher-order functions; form a well-pointed category and so support good proof principles for equational reasoning; and support continuous probability distributions. We demonstrate the use of quasi-Borel spaces for higher-order functions and probability by: showing that a well-known construction of probability theory involving random functions gains a cleaner expression; and generalizing de Finetti's theorem, that is a crucial theorem in probability theory, to quasi-Borel spaces.

Subfields: Artificial Intelligence, Computational Theory and Mathematics, Probabilistic & Bayesian Methods

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Computational Theory and Mathematics

In Probabilistic & Bayesian Methods

Citations in the corpus

An Introduction to Probabilistic Programming (2018, methodology): “Hongseok Yang was supported by the Engineering Research Center Program through the National Research Foundation of Korea (NRF) funded by the Korean Government MSIT (NRF-2018R1A5A1059921), and also by Next-Generation Information Computing Development Program through the National Research Foundation o”
Denotational validation of higher-order Bayesian inference (2017, methodology): “In this section we resolve these problems by combining some recent discoveries [Heunen et al. 2017; Staton 2017], and exhibit a model of synthetic measure theory which contains classical measure theory, for instance:”
Commutative Semantics for Probabilistic Programming (2017, background): “( For a more concrete variant, see also [14].)”