A Convenient Category for Higher-Order Probability Theory

Abstract

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.

References in corpus (7)

• Church: a language for generative models
• Semantics for probabilistic programming: higher-order functions, continuous distributions, and soft constraints
• Computable de Finetti measures
• QRB-Domains and the Probabilistic Powerdomain
• Some Notes on Standard Borel and Related Spaces
• An Application of Computable Distributions to the Semantics of Probabilistic Programs
• Computability in Basic Quantum Mechanics

Cited by in corpus (33)

• A synthetic approach to Markov kernels, conditional independence and theorems on sufficient statistics
• Denotational validation of higher-order Bayesian inference
• A Domain Theory for Statistical Probabilistic Programming
• Measurable Cones and Stable, Measurable Functions
• Formal verification of higher-order probabilistic programs
• Commutative Monads for Probabilistic Programming Languages
• ADEV: Sound Automatic Differentiation of Expected Values of Probabilistic Programs
• Probabilistic call by push value
• Dilations and information flow axioms in categorical probability
• A Monad for Probabilistic Point Processes
• The Theory of Traces for Systems with Nondeterminism, Probability, and Termination
• Paradoxes of Probabilistic Programming
• Synthetic topology in Homotopy Type Theory for probabilistic programming
• Probability monads with submonads of deterministic states - Extended version
• Categorical Stochastic Processes and Likelihood
• Monads for Measurable Queries in Probabilistic Databases
• Domains and Stochastic Processes
• Higher-Order Bayesian Networks, Exactly (Extended version)
• A Framework for Universality in Physics, Computer Science, and Beyond
• Cyber Kittens, or Some First Steps Towards Categorical Cybernetics
• Probabilistic programming interfaces for random graphs: Markov categories, graphons, and nominal sets
• Concrete categories and higher-order recursion (With applications including probability, differentiability, and full abstraction)
• Free complete Wasserstein algebras
• Polynomial Life: the Structure of Adaptive Systems
• Divergences on Monads for Relational Program Logics
• The Geometry of Bayesian Programming
• String Diagrams with Factorized Densities
• A model of stochastic memoization and name generation in probabilistic programming: categorical semantics via monads on presheaf categories
• A Cartesian Closed Category for Random Variables
• On Higher-Order Probabilistic Subrecursion
• (Towards a) Statistical Probabilistic Lazy Lambda Calculus
• Compositional Inference Metaprogramming with Convergence Guarantees
• GradInf: Gradient Estimation as Probabilistic Inference