TY - SLIDE
TI - Diffeological Spaces and Denotational Semantics for Differential Programming
A2 - Kammar, Ohad
A2 - Staton, Sam
A2 - Vákár, Matthijs
DA - 2018///
PY - 2018
LA - en
KW - Automatic differentiation
KW - Differentiation
KW - Programming language theory
ER -
TY - JOUR
TI - Functional programming for modular Bayesian inference
AU - Ścibior, Adam
AU - Kammar, Ohad
AU - Ghahramani, Zoubin
T2 - Proceedings of the ACM on Programming Languages
DA - 2018/07/30/
PY - 2018
DO - 10/gft39x
DP - Crossref
VL - 2
IS - ICFP
SP - 1
EP - 29
LA - en
SN - 24751421
UR - http://dl.acm.org/citation.cfm?doid=3243631.3236778
Y2 - 2019/11/27/19:47:09
KW - Bayesian inference
KW - Implementation
KW - Probabilistic programming
ER -
TY - JOUR
TI - A Domain Theory for Statistical Probabilistic Programming
AU - Vákár, Matthijs
AU - Kammar, Ohad
AU - Staton, Sam
T2 - arXiv:1811.04196 [cs]
AB - 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.
DA - 2018/11/10/
PY - 2018
DP - arXiv.org
UR - http://arxiv.org/abs/1811.04196
Y2 - 2019/10/10/11:49:16
ER -
TY - JOUR
TI - A Convenient Category for Higher-Order Probability Theory
AU - Heunen, Chris
AU - Kammar, Ohad
AU - Staton, Sam
AU - Yang, Hongseok
T2 - arXiv:1701.02547 [cs, math]
AB - 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.
DA - 2017/01/10/
PY - 2017
DP - arXiv.org
UR - http://arxiv.org/abs/1701.02547
Y2 - 2019/10/10/11:48:09
ER -
TY - JOUR
TI - Semantics for probabilistic programming: higher-order functions, continuous distributions, and soft constraints
AU - Staton, Sam
AU - Yang, Hongseok
AU - Heunen, Chris
AU - Kammar, Ohad
AU - Wood, Frank
T2 - Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science - LICS '16
AB - We study the semantic foundation of expressive probabilistic programming languages, that support higher-order functions, continuous distributions, and soft constraints (such as Anglican, Church, and Venture). We define a metalanguage (an idealised version of Anglican) for probabilistic computation with the above features, develop both operational and denotational semantics, and prove soundness, adequacy, and termination. They involve measure theory, stochastic labelled transition systems, and functor categories, but admit intuitive computational readings, one of which views sampled random variables as dynamically allocated read-only variables. We apply our semantics to validate nontrivial equations underlying the correctness of certain compiler optimisations and inference algorithms such as sequential Monte Carlo simulation. The language enables defining probability distributions on higher-order functions, and we study their properties.
DA - 2016///
PY - 2016
DO - 10/ggdf97
DP - arXiv.org
SP - 525
EP - 534
ST - Semantics for probabilistic programming
UR - http://arxiv.org/abs/1601.04943
Y2 - 2019/11/23/16:36:30
KW - Bayesianism
KW - Probabilistic programming
KW - Programming language theory
KW - Semantics
ER -
TY - JOUR
TI - Denotational validation of higher-order Bayesian inference
AU - Ścibior, Adam
AU - Kammar, Ohad
AU - Vákár, Matthijs
AU - Staton, Sam
AU - Yang, Hongseok
AU - Cai, Yufei
AU - Ostermann, Klaus
AU - Moss, Sean K.
AU - Heunen, Chris
AU - Ghahramani, Zoubin
T2 - Proceedings of the ACM on Programming Languages
AB - 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.
DA - 2017/12/27/
PY - 2017
DO - 10.1145/3158148
DP - arXiv.org
VL - 2
IS - POPL
SP - 1
EP - 29
J2 - Proc. ACM Program. Lang.
SN - 24751421
UR - http://arxiv.org/abs/1711.03219
Y2 - 2019/10/10/11:49:49
ER -