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.