@article{baudart_reactive_2019,
title = {Reactive {Probabilistic} {Programming}},
url = {http://arxiv.org/abs/1908.07563},
abstract = {Synchronous reactive languages were introduced for designing and implementing real-time control software. These domain-specific languages allow for writing a modular and mathematically precise specification of the system, enabling a user to simulate, test, verify, and, finally, compile the system into executable code. However, to date these languages have had limited modern support for modeling uncertainty -- probabilistic aspects of the software's environment or behavior -- even though modeling uncertainty is a primary activity when designing a control system. In this paper we extend Z{\textbackslash}'elus, a synchronous programming language, to deliver ProbZ{\textbackslash}'elus, the first synchronous probabilistic programming language. ProbZ{\textbackslash}'elus is a probabilistic programming language in that it provides facilities for probabilistic models and inference: inferring latent model parameters from data. We present ProbZ{\textbackslash}'elus's measure-theoretic semantics in the setting of probabilistic, stateful stream functions. We then demonstrate a semantics-preserving compilation strategy to a first-order functional core calculus that lends itself to a simple semantic presentation of ProbZ{\textbackslash}'elus's inference algorithms. We also redesign the delayed sampling inference algorithm to provide bounded and streaming delayed sampling inference for ProbZ{\textbackslash}'elus models. Together with our evaluation on several reactive programs, our results demonstrate that ProbZ{\textbackslash}'elus provides efficient, bounded memory probabilistic inference.},
urldate = {2019-11-28},
journal = {arXiv:1908.07563 [cs]},
author = {Baudart, Guillaume and Mandel, Louis and Atkinson, Eric and Sherman, Benjamin and Pouzet, Marc and Carbin, Michael},
month = aug,
year = {2019},
note = {ZSCC: 0000001
arXiv: 1908.07563},
keywords = {Bayesian inference, Denotational semantics, Implementation, Probabilistic programming, Programming language theory}
}
@inproceedings{dal_lago_geometry_2019,
title = {The {Geometry} of {Bayesian} {Programming}},
doi = {10/ggdk85},
author = {Dal Lago, Ugo and Hoshino, Naohiko},
month = jun,
year = {2019},
note = {ZSCC: 0000000},
keywords = {Bayesian inference, Denotational semantics, Linear logic, Probabilistic programming, Programming language theory, Rewriting theory, Transition systems},
pages = {1--13}
}
@article{vakar_domain_2018,
title = {A {Domain} {Theory} for {Statistical} {Probabilistic} {Programming}},
url = {http://arxiv.org/abs/1811.04196},
abstract = {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.},
urldate = {2019-10-10},
journal = {arXiv:1811.04196 [cs]},
author = {Vákár, Matthijs and Kammar, Ohad and Staton, Sam},
month = nov,
year = {2018},
note = {arXiv: 1811.04196}
}
@article{scibior_denotational_2017,
title = {Denotational validation of higher-order {Bayesian} inference},
volume = {2},
issn = {24751421},
url = {http://arxiv.org/abs/1711.03219},
doi = {10.1145/3158148},
abstract = {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.},
number = {POPL},
urldate = {2019-10-10},
journal = {Proceedings of the ACM on Programming Languages},
author = {Ścibior, Adam and Kammar, Ohad and Vákár, Matthijs and Staton, Sam and Yang, Hongseok and Cai, Yufei and Ostermann, Klaus and Moss, Sean K. and Heunen, Chris and Ghahramani, Zoubin},
month = dec,
year = {2017},
note = {arXiv: 1711.03219},
pages = {1--29}
}
@incollection{yang_commutative_2017,
address = {Berlin, Heidelberg},
title = {Commutative {Semantics} for {Probabilistic} {Programming}},
volume = {10201},
isbn = {978-3-662-54433-4 978-3-662-54434-1},
url = {http://link.springer.com/10.1007/978-3-662-54434-1_32},
abstract = {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.},
language = {en},
urldate = {2019-11-23},
booktitle = {Programming {Languages} and {Systems}},
publisher = {Springer Berlin Heidelberg},
author = {Staton, Sam},
editor = {Yang, Hongseok},
year = {2017},
doi = {10.1007/978-3-662-54434-1_32},
note = {ZSCC: NoCitationData[s0] },
keywords = {Bayesianism, Probabilistic programming, Programming language theory, Semantics},
pages = {855--879}
}
@article{jacobs_formal_2017,
title = {A {Formal} {Semantics} of {Influence} in {Bayesian} {Reasoning}},
url = {http://drops.dagstuhl.de/opus/volltexte/2017/8089/},
doi = {10/ggdgbc},
abstract = {This paper proposes a formal deﬁnition of inﬂuence in Bayesian reasoning, based on the notions of state (as probability distribution), predicate, validity and conditioning. Our approach highlights how conditioning a joint entwined/entangled state with a predicate on one of its components has ‘crossover’ inﬂuence on the other components. We use the total variation metric on probability distributions to quantitatively measure such inﬂuence. These insights are applied to give a rigorous explanation of the fundamental concept of d-separation in Bayesian networks.},
language = {en},
urldate = {2019-11-24},
journal = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH, Wadern/Saarbruecken, Germany},
author = {Jacobs, Bart and Zanasi, Fabio},
year = {2017},
note = {ZSCC: 0000012},
keywords = {Bayesianism, Categorical probability theory, Programming language theory, Semantics}
}
@article{jacobs_predicate/state_2016,
series = {The {Thirty}-second {Conference} on the {Mathematical} {Foundations} of {Programming} {Semantics} ({MFPS} {XXXII})},
title = {A {Predicate}/{State} {Transformer} {Semantics} for {Bayesian} {Learning}},
volume = {325},
issn = {1571-0661},
url = {http://www.sciencedirect.com/science/article/pii/S1571066116300883},
doi = {10/ggdgbb},
abstract = {This paper establishes a link between Bayesian inference (learning) and predicate and state transformer operations from programming semantics and logic. Specifically, a very general definition of backward inference is given via first applying a predicate transformer and then conditioning. Analogously, forward inference involves first conditioning and then applying a state transformer. These definitions are illustrated in many examples in discrete and continuous probability theory and also in quantum theory.},
language = {en},
urldate = {2019-11-24},
journal = {Electronic Notes in Theoretical Computer Science},
author = {Jacobs, Bart and Zanasi, Fabio},
month = oct,
year = {2016},
note = {ZSCC: 0000030},
keywords = {Bayesianism, Categorical ML, Categorical probability theory, Effectus theory, Programming language theory, Semantics},
pages = {185--200}
}
@article{staton_semantics_2016,
title = {Semantics for probabilistic programming: higher-order functions, continuous distributions, and soft constraints},
shorttitle = {Semantics for probabilistic programming},
url = {http://arxiv.org/abs/1601.04943},
doi = {10/ggdf97},
abstract = {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.},
urldate = {2019-11-23},
journal = {Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science - LICS '16},
author = {Staton, Sam and Yang, Hongseok and Heunen, Chris and Kammar, Ohad and Wood, Frank},
year = {2016},
note = {ZSCC: 0000071
arXiv: 1601.04943},
keywords = {Bayesianism, Probabilistic programming, Programming language theory, Semantics},
pages = {525--534}
}