Search

Probability theory and statistics are fundamental disciplines in a data-driven world. Synthetic probability theory is a general, axiomatic formalism to describe their underlying structures and methods in a elegant and high-level way, abstracting away from the mathematical foundations such as measure theory. We showcase the value of synthetic probabilistic reasoning to computer science by presenting a novel, synthetic analysis of three situations: the Beta-Bernoulli process, exact conditioning on continuous random variables and an investigation into the relationship of random higher-order functions and fresh name generation. The synthetic approach to probability has merit not only by matching statistical practice and achieving greater conceptual clarity, but it also lets us transfer and generalize probabilistic ideas and language to other domains: A wide range of computational phenomena admit a probabilistic analysis, such as nondeterminism, generativity (e.g. name generation), unification, exchangeable random primitives and local state. This perspective is particularly useful if we wish to compare or combine those effects with actual probability: We develop a purely stochastic model of name generation (gensym) which is not only a tight semantic fit, but also uncovers striking parallels to the theory of random functions. Probabilistic programming is an emergent flavor of Bayesian machine learning where complex statistical models are expressed through code. We argue that probabilistic programming and synthetic probability theory are two sides of the same coin. Not only do they share a similar goal, namely to act as an accessible, high-level interface to statistics, but synthetic probability theories are also the natural semantic domains for probabilistic programs. Conversely, every probabilistic language defines its own internal theory of probability. This is a probabilistic version of the Curry-Howard correspondence: Statistical models are programs. This opens up the analysis and optimization of statistical inference procedures to tools from programming language theory. Much as category theory has served as a unifying model for logic and programming, we argue that probabilistic programming languages arise precisely as the internal languages of categorical probability theories. Our methods and examples draw from diverse areas of computer science and mathematics such as rewriting theory, logical relations, linear and universal algebra, categorical logic, measure theory and descriptive set theory.