2017/01/31 by Chris Heunen, Ohad Kammar, Sam Staton +1 · 96 citations
Computer Science · Mathematics · #Algebra over a field #Cartesian closed category #Computability, Logic, AI Algorithms #Convolution of probability distributions #Discrete mathematics #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Mathematics #Measurable function #Order (exchange) #Probabilistic logic #Probability density function #Probability distribution #Probability mass function #Probability measure #Probability theory #Pure mathematics #Statistics #cs.AI #cs.LO #cs.PL #math.CT #math.PR
paper · pdf · doi:10.1109/lics.2017.8005137
published as Logic in Computer Science 2017
openalex publication_date 2017/06/01 · openalex created_date 2019/06/27 · arxiv created 2020/11/20 · arxiv updated 2020/12/03 · openalex updated_date 2026/08/05
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.