PaperlayerView exact revision on arXiv

Source-linked AI summary

A Convenient Category for Higher-Order Probability Theory

Chris Heunen, Ohad Kammar, Sam Staton, Hongseok Yang

arXiv:1701.02547v4cs.PLcs.AIcs.LOmath.CTmath.PR

TL;DR

Higher-order probabilistic programs can define continuous distributions over functions, but measurable spaces are not cartesian closed and do not handle higher-order functions well. The paper introduces quasi-Borel spaces as a random-variable-based formalism with cartesian closed and probabilistic structure, and demonstrates it through randomization and de Finetti results.

  • Problem

    Higher-order probabilistic programs may define continuous probability distributions on functions, which standard measurable-space probability theory does not handle well because Meas is not cartesian closed.

  • Method

    The paper replaces measurable spaces with quasi-Borel spaces, sets equipped with collections of random variables, and develops their categorical and probabilistic structure.

  • Results

    Quasi-Borel spaces are cartesian closed, support probability measures and a commutative monad, rephrase randomization as a quotient construction, and validate de Finetti’s theorem for all quasi-Borel spaces.

  • Takeaways & Limitations

    Quasi-Borel spaces provide a convenient category for higher-order probability theory and semantics for probabilistic programming in the monadic style.

Abstract

from arXiv · show

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.

I. INTRODUCTION

Higher-order probabilistic languages express sophisticated models compactly, but measurable spaces cannot adequately represent probability distributions on higher-order functions. The paper introduces quasi-Borel spaces as a replacement with categorical and probabilistic structure supporting such models.

  • I. INTRODUCTION: Higher-order probabilistic languages combine advanced programming and probability features with generic inference for succinctly expressing sophisticated models.Examples include Church, Venture, and Anglican, which support queries such as marginalization and posterior computation.
  • I. INTRODUCTION: Standard measure-theoretic probability struggles with higher-order functions because the category of measurable spaces is not cartesian closed.Anglican Bayesian linear regression illustrates the gap by defining a probability distribution on functions.
  • I. INTRODUCTION: Quasi-Borel spaces replace measurable spaces with a formalism based on collections of random variables, while retaining useful categorical structure.The collection of functions R → X is treated as the random variables of type X.
  • I. INTRODUCTION: The category of quasi-Borel spaces is well-pointed and cartesian closed, supporting equational reasoning and probability distributions on higher-order functions.Its morphisms are structure-preserving functions, and its function-space construction supports higher-order functions.
  • I. INTRODUCTION: Quasi-Borel spaces support probability measures and a commutative probability monad, providing semantics for monadic probabilistic programming.The space of all probability measures is itself a quasi-Borel space.
  • I. INTRODUCTION: The paper demonstrates the formalism through Bayesian regression, a randomization lemma reformulation, and de Finetti’s theorem for all quasi-Borel spaces.De Finetti’s theorem is extended beyond standard Borel and other well-behaved measurable spaces.

A. Standard Borel spaces

The paper motivates quasi-Borel spaces by treating random variables as fundamental and choosing R as a well-behaved source of randomness. This preserves the useful measurable-space setting while enabling function-space constructions.

  • A. Standard Borel spaces: Standard Borel spaces include spaces isomorphic to R, countable discrete spaces, and spaces with a complete separable metric and its Borel σ-algebra.They support properties unavailable for arbitrary measurable spaces, including conditional probability kernels and de Finetti’s theorem.
  • A. Standard Borel spaces: Measurable spaces are not cartesian closed, so there is no measurable space of functions R → R and random functions cannot generally be curried.The evaluation function fails to be measurable regardless of the chosen σ-algebra on the function space.
  • A. Standard Borel spaces: Quasi-Borel spaces take random variables as the primitive structure: a set X is equipped with a collection MX of functions R → X satisfying closure conditions.The randomness of these variables originates from a probability distribution on R.
  • A. Standard Borel spaces: Every measurable space induces a quasi-Borel structure whose elements are its measurable X-valued random variables.For R, these are measurable functions R → R; for the discrete two-element space, they are characteristic functions of Borel sets.
  • A. Standard Borel spaces: A quasi-Borel probability measure is a pair consisting of a random variable α in MX and a probability measure µ on R.The construction assumes R as the sample space, though any uncountable standard Borel space can serve equivalently.

A. Morphisms and integration

Quasi-Borel morphisms preserve the designated random variables and form a category with push-forward and integration operations. These operations reduce probabilistic constructions to functions and measures on R.

  • A. Morphisms and integration: A quasi-Borel morphism is a function f : X → Y such that composing f with every α in MX yields an element of MY.Elements of MX are precisely morphisms from the quasi-Borel real line to X.
  • A. Morphisms and integration: Morphisms compose as ordinary functions and include identity functions, so quasi-Borel spaces form a category QBS.They are analogous to measurable functions while supporting corresponding measure-theoretic constructions.
  • A. Morphisms and integration: Two canonical quasi-Borel structures on a set X are provided by all functions R → X and by functions generated through measurable maps, countable partitions, and countable-valued choices.These structures are respectively right and left adjoints to the forgetful functor from QBS to Set.
  • A. Morphisms and integration: A morphism pushes a quasi-Borel probability measure (α, µ) forward to (f ◦ α, µ) on the target space.Closure of the target random-variable collection guarantees that f ◦ α is admissible.
  • A. Morphisms and integration: Integrating a real-valued morphism with respect to (α, µ) formally reduces to integration on R.The morphism is composed with α and integrated using µ.

B. Relationship to measurable spaces

Quasi-Borel spaces retain an underlying measurable-space structure while adding designated random variables, and their morphisms relate systematically to measurable functions. They also support categorical products, coproducts, and function spaces.

  • B. Relationship to measurable spaces: A measurable subset of a quasi-Borel space is one whose characteristic function is a quasi-Borel morphism, and these subsets form a σ-algebra.Thus the measurable structure is recovered from the designated random variables.
  • B. Relationship to measurable spaces: Every quasi-Borel morphism is measurable for the induced σ-algebras, although the converse need not hold in general.This makes QBS morphisms more restrictive than ordinary measurable functions in general.
  • B. Relationship to measurable spaces: For any measurable target space, measurable functions from a quasi-Borel source are exactly morphisms into its induced quasi-Borel structure.This is the first part of the relationship between QBS and measurable spaces.
  • B. Relationship to measurable spaces: For standard Borel sources, morphisms between induced quasi-Borel structures coincide exactly with measurable functions.This gives a full and faithful correspondence on standard Borel spaces.
  • B. Relationship to measurable spaces: Quasi-Borel spaces support products, coproducts, and function spaces, providing the basic constructions for interpreting simple type theory.The function-space evaluation map is a morphism with the universal property, making QBS cartesian closed.

A. Relationship with standard Borel spaces

Quasi-Borel spaces conservatively extend standard Borel spaces while preserving key countable type-theoretic constructions and enabling higher-order functions.

  • Relationship with standard Borel spaces: Standard Borel spaces embed fully and faithfully into quasi-Borel spaces, preserving their countable products, coproducts, and available function spaces.This makes quasi-Borel spaces a conservative extension of standard Borel spaces that supports simple type theory.
  • Relationship with standard Borel spaces: The embedding preserves countable products of standard Borel spaces.
  • Relationship with standard Borel spaces: The embedding preserves spaces of functions between standard Borel spaces when the domain is countable and discrete.
  • Relationship with standard Borel spaces: The quasi-Borel function space R^R does not arise from a standard Borel space, and the left adjoint to the embedding does not generally preserve products.For these spaces, the measurable structure generated on the product can be strictly larger than the product of the generated measurable structures.
  • Relationship with standard Borel spaces: Quasi-Borel spaces support a commutative probability monad whose construction generalizes the Giry monad for measurable spaces.

B. Kernels and the Giry monad

The paper constructs probability measures on quasi-Borel spaces as a strong commutative monad, relating them to kernels and the Giry monad through measurable push-forwards.

  • Kernels and the Giry monad: A probability kernel is a measurable family of probability measures, equivalently represented by a measurable function from X to the measurable space of probability measures on Y.
  • Kernels and the Giry monad: The Giry construction assigns each measurable space a space of probability measures and forms a monad with Dirac unit and measure sequencing.
  • Kernels and the Giry monad: Quasi-Borel probability measures identify pairs of random variables and source measures when they induce the same push-forward measure.The equivalence can also be characterized by equality of integration operators over all morphisms into R.
  • Kernels and the Giry monad: Its bind operation combines a quasi-Borel probability measure with a morphism by using the Giry bind on the underlying source randomness.
  • Kernels and the Giry monad: The resulting construction P is a strong commutative monad on quasi-Borel spaces and maps to the Giry monad through a faithful monad opfunctor.

VI. EXAMPLE: BAYESIAN REGRESSION

The Bayesian regression example places a prior over functions, weights sampled functions by noisy observations, and computes a posterior over functions compositionally in quasi-Borel semantics.

  • Prior: The regression prior is a probability measure over functions f: R → R, represented by random slope and intercept variables with independent normal distributions.The slope and intercept each use a normal distribution with mean 0 and standard deviation 3.
  • Posterior: The posterior is formed by pushing the prior forward to function–weight pairs, multiplying by likelihood weights, and dividing by a normalizing constant.
  • Posterior: The complete program denotes a posterior measure in P(R^R), whose calculation with Anglican’s lmh inference algorithm produces the plot in Figure 1.
  • Defunctionalized regression and non-linear regression: The semantics supports compositional adaptation to other function classes, including polynomials and programs from a small domain-specific language, by changing the prior.

VII. RANDOM FUNCTIONS

The section shows why measurable spaces cannot support random functions cleanly and presents quasi-Borel spaces as a setting where function spaces, pushforwards, and randomization results are available.

  • Motivation: Measurable spaces cannot generally form function spaces or curry random functions, preventing pushforward of measures along random functions.This follows from the failure of cartesian closure in the category of measurable spaces.
  • Quasi-Borel spaces: A quasi-Borel probability measure on a function space is essentially equivalent to a random function through the cartesian closed structure.A measure is represented by a probability measure on R and a morphism R → Y^X, which corresponds to a morphism R × X → Y.
  • Randomization: Quasi-Borel spaces provide quotient-space structure for expressing the randomization lemma as a relation between probability kernels and random functions.The space (P(R))^X of kernels is a quotient of P(R^X), the space of random functions.
  • Randomization: The quotient morphism q maps a random function with source measure µ to the kernel obtained by evaluating that function at each x.Specifically, q([α, µ])(x) = [λr. α(r)(x), µ].
  • Randomization: The proof establishes q’s surjectivity by representing kernels through measurable functions driven by the uniform distribution on [0, 1], then currying them into random functions.The argument also shows every morphism into the kernel space factors through q.

VIII. DE FINETTI’S THEOREM

The section extends de Finetti’s theorem from well-behaved measurable spaces to quasi-Borel spaces. Every exchangeable sequence has finite prefixes generated by first sampling a random probability measure, then drawing independent samples from it.

  • Background: Classical de Finetti theory represents exchangeable sequences by randomly selecting a probability measure and then generating independent samples from it.The classical result is established for standard Borel spaces or measurable spaces arising from suitable topologies, but not arbitrary measurable spaces.
  • Theorem: Weak de Finetti for quasi-Borel spaces states that every exchangeable probability measure on X^ω admits a representing probability measure in P(P(X)).For every n ≥ 1, the induced independent-sampling measure agrees with the corresponding finite-prefix measure on the product measurable space.
  • Interpretation: The representation samples a probability measure on X, generates independent X-valued samples from it, and forms each finite prefix of the sequence.The sampled probability measure is itself the value of a random variable governed by (β, ν).
  • Limitations: The theorem is weak because equality is asserted on the product σ-algebra, and the construction provides no morphism implementing iid sampling for infinite sequences.The result is therefore stated only for finite prefixes.
  • Proof strategy: The proof rewrites quasi-Borel definitions in standard measure-theoretic terms and constructs the representation using conditional probability kernels over the randomness source R.Exchangeability supplies the identities needed to establish the finite-prefix representation.

A. Quasi-topological spaces and categories of functors

The paper places quasi-Borel spaces within a broader pattern of concrete, extensional spaces that form cartesian closed categories. It characterizes quasi-Borel spaces categorically and highlights their concrete advantages over an earlier functor-category construction.

  • Related generalized spaces: Quasi-topological, subsequential, and diffeological spaces, like quasi-Borel spaces, are presented as structures built from selected functions and form cartesian closed categories.Subsequential spaces use convergent sequences, while diffeological spaces use plots from Euclidean open sets.
  • Functor characterization: A functor J maps quasi-Borel spaces into Set-valued functors on standard Borel spaces, and this mapping is full and faithful.The paper uses this embedding to relate quasi-Borel spaces to extensional presheaf constructions.
  • Functor characterization: Proposition 34 characterizes exactly which functors arise from quasi-Borel spaces: those naturally isomorphic to J(X, M_X).This gives quasi-Borel spaces a canonical categorical status.
  • Functor characterization: The same characterization requires preservation of countable products and extensionality, expressed by injectivity of the maps i(X,Σ_X).Extensionality identifies elements through their observable values on points represented as maps from the terminal object.
  • Advantages: Compared with an earlier functor category, quasi-Borel spaces are more concrete and give better intuitions for constructions such as measures.The earlier approach built measures abstractly using left Kan extensions, whereas quasi-Borel spaces provide a more direct presentation.
  • Categorical direction: Quasi-Borel spaces add objects to make the category of measurable spaces cartesian closed, while a future direction is adding morphisms to obtain more isomorphisms.The latter goal would identify a cartesian closed subcategory with stronger structural equivalences.

B. Domains and valuations

The paper situates quasi-Borel spaces alongside valuation- and domain-theoretic approaches to probability semantics. It reports established connections and identifies recursion and formal integration with related random-variable models as ongoing directions.

  • Foundational choices: The paper starts from σ-algebras and probability measures, preserving access to the established body of probability theory.It contrasts this foundation with approaches based on topologies and valuations.
  • Valuations and domains: Valuations form a monad analogous to the paper’s probability monad, but the appropriate cartesian closed category remains debated.The cited alternatives include probabilistic coherence spaces and topological domain theory.
  • Valuations and domains: Domains of random variables arose from concerns about probabilistic powerdomains, and quasi-Borel measures are described as intuitively reminiscent of continuous random variables on a dcpo.The paper states that it has not yet established a formal connection with this work.
  • Open directions: An advantage of domain-theoretic approaches is natural support for recursion, motivating ongoing work on ordered quasi-Borel spaces enriched over dcpos.This direction is framed as an investigation rather than a completed result.
  • Probabilistic programming semantics: The paper differs from operational studies of higher-order probabilistic languages because its semantics are denotational, while related work has justified basic inference algorithms operationally.The cited operational approaches address higher-order languages with continuous distributions.
  • Paper outcomes: The completed development supports higher-order functions, probability-measure spaces, Bayesian regression, the randomization lemma, and de Finetti’s theorem.These applications illustrate the formalism across semantics and probability-theoretic constructions.
Loading 1701.02547v4…