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 - CHAP
TI - Commutative Semantics for Probabilistic Programming
AU - Staton, Sam
T2 - Programming Languages and Systems
A2 - Yang, Hongseok
AB - We show that a measure-based denotational semantics for probabilistic programming is commutative. The idea underlying probabilistic programming languages (Anglican, Church, Hakaru, ...) is that programs express statistical models as a combination of prior distributions and likelihood of observations. The product of prior and likelihood is an unnormalized posterior distribution, and the inference problem is to ﬁnd the normalizing constant. One common semantic perspective is thus that a probabilistic program is understood as an unnormalized posterior measure, in the sense of measure theory, and the normalizing constant is the measure of the entire semantic domain.
CY - Berlin, Heidelberg
DA - 2017///
PY - 2017
DP - Crossref
VL - 10201
SP - 855
EP - 879
LA - en
PB - Springer Berlin Heidelberg
SN - 978-3-662-54433-4 978-3-662-54434-1
UR - http://link.springer.com/10.1007/978-3-662-54434-1_32
Y2 - 2019/11/23/16:35:50
KW - Bayesianism
KW - Probabilistic programming
KW - Programming language theory
KW - Semantics
ER -