Higher-order functions — functions that take functions as arguments — are incredibly useful as a programming abstraction. But what does a higher-order probabilistic program actually mean? We are used to thinking of program functions as mathematical functions, but does this make sense in the context of measure and integration? What’s a semantic foundation for probability theory that supports higher-order functions and a monad of measures? We argue that quasi-Borel spaces are just that.

A quasi-Borel space is a set *X* together with a set of functions *M *⊆ (ℜ → *X*). The idea is that the reals ℜ are the source of randomness and *M* is a set of allowed random elements. Thus quasi-Borel spaces put the focus on random elements rather than σ-algebras, just as probabilists do.

Authors: Chris Heunen, Ohad Kammar, Sean Moss, Adam Ścibior, Sam Staton, Matthijs Vákár, Hongseok Yang.

Extended abstract: [pdf]

See also our LICS 2017 paper, A Convenient Category for Higher-Order Probability Theory, and our POPL 2018 paper, Denotational validation of higher-order Bayesian inference.

Slides:

http://users.ox.ac.uk/~magd3996/research/09-01-2018-LA.pdf