Reference. Denotational validation of higher-order Bayesian inference

We present a modular semantic account of Bayesian inference algorithms for probabilistic programming languages, as used in data science and machine learning. Sophisticated inference algorithms are often explained in terms of composition of smaller parts. However, neither their theoretical justification nor their implementation reflects this modularity. We show how to conceptualise and analyse such inference algorithms as manipulating intermediate representations of probabilistic programs using higher-order functions and inductive types, and their denotational semantics. Semantic accounts of continuous distributions use measurable spaces. However, our use of higher-order functions presents a substantial technical difficulty: it is impossible to define a measurable space structure over the collection of measurable functions between arbitrary measurable spaces that is compatible with standard operations on those functions, such as function application. We overcome this difficulty using quasi-Borel spaces, a recently proposed mathematical structure that supports both function spaces and continuous distributions. We define a class of semantic structures for representing probabilistic programs, and semantic validity criteria for transformations of these representations in terms of distribution preservation. We develop a collection of building blocks for composing representations. We use these building blocks to validate common inference algorithms such as Sequential Monte Carlo and Markov Chain Monte Carlo. To emphasize the connection between the semantic manipulation and its traditional measure theoretic origins, we use Kock’s synthetic measure theory. We demonstrate its usefulness by proving a quasi-Borel counterpart to the Metropolis-Hastings-Green theorem.

Cite

Cite as @scibior-2017-denotational (helia, typst) · \cite{scibior-2017-denotational} (LaTeX)
BibTeX
bibtex · 19 lines
@article{scibior-2017-denotational,
  author    = {Adam Scibior and
               Ohad Kammar and
               Matthijs V{\'{a}}k{\'{a}}r and
               Sam Staton and
               Hongseok Yang and
               Yufei Cai and
               Klaus Ostermann and
               Sean K. Moss and
               Chris Heunen and
               Zoubin Ghahramani},
  title     = {Denotational validation of higher-order Bayesian inference},
  journal   = {{PACMPL}},
  volume    = {2},
  number    = {{POPL}},
  pages     = {60:1--60:29},
  year      = {2018},,
  doi       = {10.1145/3158148},
}
hayagriva YAML (typst)
yaml · 24 lines
scibior-2017-denotational:
  type: article
  title: Denotational validation of higher-order Bayesian inference
  author:
  - Ścibior, Adam
  - Kammar, Ohad
  - Vákár, Matthijs
  - Staton, Sam
  - Yang, Hongseok
  - Cai, Yufei
  - Ostermann, Klaus
  - Moss, Sean
  - Heunen, Chris
  - Ghahramani, Zoubin
  date: 2018
  page-range: 60:1–60:29
  serial-number:
    doi: 10.1145/3158148
  parent:
    type: periodical
    title: PACMPL
    publisher: Association for Computing Machinery (ACM)
    issue: POPL
    volume: 2
Cited by (3)

A Higher-Order Language for Markov Kernels and Linear Operators amorim_2023_fossacs

Much work has been done to give semantics to probabilistic programming languages. In recent years, most of the semantics used to reason about probabilistic programs fall in two categories: semantics based on Markov kernels and semantics based on linear operators.

Both styles of semantics have found numerous applications in reasoning about probabilistic programs, but they each have their strengths and weaknesses. Though it is believed that there is a connection between them there are no languages that can handle both styles of programming.

In this work we address these questions by defining a two-level calculus and its categorical semantics which makes it possible to program with both kinds of semantics. From the logical side of things we see this language as an alternative resource interpretation of linear logic, where the resource being kept track of is sampling instead of variable use.

DOI

Fully abstract models for effectful λ-calculi via category-theoretic logical relations kammar-2022-fully

We present a construction which, under suitable assumptions, takes a model of Moggi’s computational λ-calculus with sum types, effect operations and primitives, and yields a model that is adequate and fully abstract. The construction, which uses the theory of fibrations, categorical glueing, ⊤⊤-lifting, and ⊤⊤-closure, takes inspiration from O’Hearn & Riecke’s fully abstract model for PCF. Our construction can be applied in the category of sets and functions, as well as the category of diffeological spaces and smooth maps and the category of quasi-Borel spaces, which have been studied as semantics for differentiable and probabilistic programming.
PDF · DOI · pldb

A domain theory for statistical probabilistic programming vakar-2019-a

We give an adequate denotational semantics for languages with recursive higher-order types, continuous probability distributions, and soft constraints. These are expressive languages for building Bayesian models of the kinds used in computational statistics and machine learning. Among them are untyped languages, similar to Church and WebPPL, because our semantics allows recursive mixed-variance datatypes. Our semantics justifies important program equivalences including commutativity. Our new semantic model is based on ‘quasi-Borel predomains’. These are a mixture of chain-complete partial orders (cpos) and quasi-Borel spaces. Quasi-Borel spaces are a recent model of probability theory that focuses on sets of admissible random elements. Probability is traditionally treated in cpo models using probabilistic powerdomains, but these are not known to be commutative on any class of cpos with higher order functions. By contrast, quasi-Borel predomains do support both a commutative probabilistic powerdomain and higher-order functions. As we show, quasi-Borel predomains form both a model of Fiore’s axiomatic domain theory and a model of Kock’s synthetic measure theory.
PDF · DOI · pldb
Cites 40 works (1 here)
With notes (1)

A convenient category for higher-order probability theory heunen-2017-a

DOI · arXiv
External (39)
scibior-2017-denotational reference entries/refs/scibior-2017-denotational/scibior-2017-denotational.hel