Reference. Universal Semantics for the Stochastic Lambda-Calculus
We define sound and adequate denotational and operational semantics for the stochastic lambda calculus. These two semantic approaches build on previous work that used similar techniques to reason about higher-order probabilistic programs, but for the first time admit an adequacy theorem relating the operational and denotational views. This resolves the main issue left open in (Bacci et al. 2018).
Cite
Cites 22 works (3 here)
With notes (3)
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.
A convenient category for higher-order probability theory heunen-2017-a
Semantics for probabilistic programming: higher-order functions, continuous distributions, and soft constraints staton-2016-semantics
External (19)
- Commutative monads for probabilistic programming languages (2021)
- Boolean-Valued Semantics for the Stochastic λ-Calculus (2018)
- Behavioral equivalences for higher-order languages with probabilities (2017)
- Measurable cones and stable, measurable functions: a model for probabilistic higher-order programming (2017)
- A lambda-calculus foundation for universal probabilistic programming (2016)
- Stochastic λ-calculi: An extended abstract (2014)
- Probabilistic coherence spaces are fully abstract for probabilistic PCF (2014)
- Church: a language for generative models (2012)
- Computing with Capsules (2012)
- Probabilistic coherence spaces as a model of higher-order probabilistic computation (2011)
- Set Theory: Boolean-Valued Models and Independence Proofs (2011)
- A Structural Approach to Operational Semantics (2004)
- The Troublesome Probabilistic Powerdomain (1998)
- PCF extended with real numbers (1996)
- The Lambda Calculus: Its Syntax and Semantics (1984)
- Set-theoretical models of λ-calculus: theories, expansions, isomorphisms (1983)
- Algebras and combinators (1981)
- Real and complex analysis (1974)
- A proof of the independence of the continuum hypothesis (1967)