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

Cite as @amorim_etal_2021_lics (helia, typst) · \cite{amorim_etal_2021_lics} (LaTeX)
BibTeX
bibtex · 9 lines
@inproceedings{amorim_etal_2021_lics,
 title = {Universal Semantics for the Stochastic Lambda-Calculus},
 author = {Amorim, Pedro H. Azevedo de and Kozen, Dexter and Mardare, Radu and Panangaden, Prakash and Roberts, Michael},
 year = {2021},
 doi = {10.1109/LICS52264.2021.9470747},
 url = {https://arxiv.org/abs/2011.13171},
 booktitle = {36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2021)},
 publisher = {IEEE}
}
hayagriva YAML (typst)
yaml · 17 lines
amorim_etal_2021_lics:
  type: article
  title: Universal Semantics for the Stochastic Lambda-Calculus
  author:
  - Amorim, Pedro H. Azevedo de
  - Kozen, Dexter
  - Mardare, Radu
  - Panangaden, Prakash
  - Roberts, Michael
  date: 2021
  url: https://arxiv.org/abs/2011.13171
  serial-number:
    doi: 10.1109/LICS52264.2021.9470747
  parent:
    type: proceedings
    title: 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2021)
    publisher: IEEE
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.
PDF · DOI · pldb

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

DOI · arXiv

Semantics for probabilistic programming: higher-order functions, continuous distributions, and soft constraints staton-2016-semantics

DOI · arXiv
amorim_etal_2021_lics reference entries/refs/amorim_etal_2021_lics/amorim_etal_2021_lics.hel