TY - JOUR
TI - Reactive Probabilistic Programming
AU - Baudart, Guillaume
AU - Mandel, Louis
AU - Atkinson, Eric
AU - Sherman, Benjamin
AU - Pouzet, Marc
AU - Carbin, Michael
T2 - arXiv:1908.07563 [cs]
AB - 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\'elus, a synchronous programming language, to deliver ProbZ\'elus, the first synchronous probabilistic programming language. ProbZ\'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\'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\'elus's inference algorithms. We also redesign the delayed sampling inference algorithm to provide bounded and streaming delayed sampling inference for ProbZ\'elus models. Together with our evaluation on several reactive programs, our results demonstrate that ProbZ\'elus provides efficient, bounded memory probabilistic inference.
DA - 2019/08/20/
PY - 2019
DP - arXiv.org
UR - http://arxiv.org/abs/1908.07563
Y2 - 2019/11/28/10:25:56
KW - Bayesian inference
KW - Denotational semantics
KW - Implementation
KW - Probabilistic programming
KW - Programming language theory
ER -
TY - CONF
TI - The Geometry of Bayesian Programming
AU - Dal Lago, Ugo
AU - Hoshino, Naohiko
DA - 2019/06/01/
PY - 2019
DO - 10/ggdk85
DP - ResearchGate
SP - 1
EP - 13
KW - Bayesian inference
KW - Denotational semantics
KW - Linear logic
KW - Probabilistic programming
KW - Programming language theory
KW - Rewriting theory
KW - Transition systems
ER -
TY - JOUR
TI - Differentials and distances in probabilistic coherence spaces
AU - Ehrhard, Thomas
T2 - arXiv:1902.04836 [cs]
AB - In probabilistic coherence spaces, a denotational model of probabilistic functional languages, mor-phisms are analytic and therefore smooth. We explore two related applications of the corresponding derivatives. First we show how derivatives allow to compute the expectation of execution time in the weak head reduction of probabilistic PCF (pPCF). Next we apply a general notion of "local" differential of morphisms to the proof of a Lipschitz property of these morphisms allowing in turn to relate the observational distance on pPCF terms to a distance the model is naturally equipped with. This suggests that extending probabilistic programming languages with derivatives, in the spirit of the differential lambda-calculus, could be quite meaningful.
DA - 2019/02/13/
PY - 2019
DP - arXiv.org
UR - http://arxiv.org/abs/1902.04836
Y2 - 2019/11/28/11:57:10
KW - Coherence spaces
KW - Denotational semantics
KW - Differential Linear Logic
KW - Differentiation
KW - Linear logic
KW - Probabilistic programming
KW - Programming language theory
ER -
TY - JOUR
TI - Probabilistic call by push value
AU - Ehrhard, Thomas
AU - Tasson, Christine
T2 - arXiv:1607.04690 [cs]
AB - We introduce a probabilistic extension of Levy's Call-By-Push-Value. This extension consists simply in adding a " flipping coin " boolean closed atomic expression. This language can be understood as a major generalization of Scott's PCF encompassing both call-by-name and call-by-value and featuring recursive (possibly lazy) data types. We interpret the language in the previously introduced denotational model of probabilistic coherence spaces, a categorical model of full classical Linear Logic, interpreting data types as coalgebras for the resource comonad. We prove adequacy and full abstraction, generalizing earlier results to a much more realistic and powerful programming language.
DA - 2018///
PY - 2018
DO - 10/ggdk8z
DP - arXiv.org
UR - http://arxiv.org/abs/1607.04690
Y2 - 2019/11/27/20:51:36
KW - Denotational semantics
KW - Linear logic
KW - Probabilistic programming
KW - Programming language theory
ER -
TY - CONF
TI - The concurrent game semantics of Probabilistic PCF
AU - Castellan, Simon
AU - Clairambault, Pierre
AU - Paquet, Hugo
AU - Winskel, Glynn
T2 - the 33rd Annual ACM/IEEE Symposium
AB - We define a new games model of Probabilistic PCF (PPCF) by enriching thin concurrent games with symmetry, recently introduced by Castellan et al, with probability. This model supports two interpretations of PPCF, one sequential and one parallel. We make the case for this model by exploiting the causal structure of probabilistic concurrent strategies. First, we show that the strategies obtained from PPCF programs have a deadlock-free interaction, and therefore deduce that there is an interpretation-preserving functor from our games to the probabilistic relational model recently proved fully abstract by Ehrhard et al. It follows that our model is intensionally fully abstract. Finally, we propose a definition of probabilistic innocence and prove a finite definability result, leading to a second (independent) proof of full abstraction.
C1 - Oxford, United Kingdom
C3 - Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science - LICS '18
DA - 2018///
PY - 2018
DO - 10/ggdjfz
DP - Crossref
SP - 215
EP - 224
LA - en
PB - ACM Press
SN - 978-1-4503-5583-4
UR - http://dl.acm.org/citation.cfm?doid=3209108.3209187
Y2 - 2019/11/26/16:57:36
KW - Denotational semantics
KW - Game semantics
KW - Interactive semantics
KW - Probabilistic programming
KW - Programming language theory
ER -
TY - JOUR
TI - Measurable Cones and Stable, Measurable Functions
AU - Ehrhard, Thomas
AU - Pagani, Michele
AU - Tasson, Christine
T2 - Proceedings of the ACM on Programming Languages
AB - We define a notion of stable and measurable map between cones endowed with measurability tests and show that it forms a cpo-enriched cartesian closed category. This category gives a denotational model of an extension of PCF supporting the main primitives of probabilistic functional programming, like continuous and discrete probabilistic distributions, sampling, conditioning and full recursion. We prove the soundness and adequacy of this model with respect to a call-by-name operational semantics and give some examples of its denotations.
DA - 2017/12/27/
PY - 2017
DO - 10/ggdjf8
DP - arXiv.org
VL - 2
IS - POPL
SP - 1
EP - 28
J2 - Proc. ACM Program. Lang.
SN - 24751421
UR - http://arxiv.org/abs/1711.09640
Y2 - 2019/11/26/17:06:12
KW - Denotational semantics
KW - Probabilistic programming
KW - Programming language theory
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 -
TY - JOUR
TI - Mixed powerdomains for probability and nondeterminism
AU - Keimel, Klaus
AU - Plotkin, Gordon D.
T2 - arXiv:1612.01005 [cs]
AB - We consider mixed powerdomains combining ordinary nondeterminism and probabilistic nondeterminism. We characterise them as free algebras for suitable (in)equation-al theories; we establish functional representation theorems; and we show equivalencies between state transformers and appropriately healthy predicate transformers. The extended nonnegative reals serve as `truth-values'. As usual with powerdomains, everything comes in three flavours: lower, upper, and order-convex. The powerdomains are suitable convex sets of subprobability valuations, corresponding to resolving nondeterministic choice before probabilistic choice. Algebraically this corresponds to the probabilistic choice operator distributing over the nondeterministic choice operator. (An alternative approach to combining the two forms of nondeterminism would be to resolve probabilistic choice first, arriving at a domain-theoretic version of random sets. However, as we also show, the algebraic approach then runs into difficulties.) Rather than working directly with valuations, we take a domain-theoretic functional-analytic approach, employing domain-theoretic abstract convex sets called Kegelspitzen; these are equivalent to the abstract probabilistic algebras of Graham and Jones, but are more convenient to work with. So we define power Kegelspitzen, and consider free algebras, functional representations, and predicate transformers. To do so we make use of previous work on domain-theoretic cones (d-cones), with the bridge between the two of them being provided by a free d-cone construction on Kegelspitzen.
DA - 2017///
PY - 2017
DO - 10/ggdmrp
DP - arXiv.org
UR - http://arxiv.org/abs/1612.01005
Y2 - 2019/11/28/12:04:57
KW - Denotational semantics
KW - Powerdomains
KW - Probabilistic programming
KW - Programming language theory
ER -
TY - JOUR
TI - A Formal Semantics of Influence in Bayesian Reasoning
AU - Jacobs, Bart
AU - Zanasi, Fabio
T2 - Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH, Wadern/Saarbruecken, Germany
AB - 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.
DA - 2017///
PY - 2017
DO - 10/ggdgbc
DP - DataCite
LA - en
UR - http://drops.dagstuhl.de/opus/volltexte/2017/8089/
Y2 - 2019/11/24/12:11:15
KW - Bayesianism
KW - Categorical probability theory
KW - Programming language theory
KW - Semantics
ER -
TY - JOUR
TI - A Predicate/State Transformer Semantics for Bayesian Learning
AU - Jacobs, Bart
AU - Zanasi, Fabio
T2 - Electronic Notes in Theoretical Computer Science
T3 - The Thirty-second Conference on the Mathematical Foundations of Programming Semantics (MFPS XXXII)
AB - 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.
DA - 2016/10/05/
PY - 2016
DO - 10/ggdgbb
DP - ScienceDirect
VL - 325
SP - 185
EP - 200
J2 - Electronic Notes in Theoretical Computer Science
LA - en
SN - 1571-0661
UR - http://www.sciencedirect.com/science/article/pii/S1571066116300883
Y2 - 2019/11/24/12:04:12
KW - Bayesianism
KW - Categorical ML
KW - Categorical probability theory
KW - Effectus theory
KW - Programming language theory
KW - Semantics
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 - CONF
TI - Probabilistic coherence spaces are fully abstract for probabilistic PCF
AU - Ehrhard, Thomas
AU - Tasson, Christine
AU - Pagani, Michele
T2 - the 41st ACM SIGPLAN-SIGACT Symposium
AB - Probabilistic coherence spaces (PCoh) yield a semantics of higherorder probabilistic computation, interpreting types as convex sets and programs as power series. We prove that the equality of interpretations in PCoh characterizes the operational indistinguishability of programs in PCF with a random primitive.
C1 - San Diego, California, USA
C3 - Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages - POPL '14
DA - 2014///
PY - 2014
DO - 10/ggdf9x
DP - Crossref
SP - 309
EP - 320
LA - en
PB - ACM Press
SN - 978-1-4503-2544-8
UR - http://dl.acm.org/citation.cfm?doid=2535838.2535865
Y2 - 2019/11/22/17:00:49
KW - Coherence spaces
KW - Probabilistic programming
KW - Programming language theory
KW - Semantics
ER -
TY - JOUR
TI - Probabilistic coherence spaces as a model of higher-order probabilistic computation
AU - Ehrhard, Thomas
AU - Danos, Vincent
T2 - Information and Computation
AB - We study a probabilistic version of coherence spaces and show that these objects provide a model of linear logic. We build a model of the pure lambda-calculus in this setting and show how to interpret a probabilistic version of the functional language PCF. We give a probabilistic interpretation of the semantics of probabilistic PCF closed terms of ground type. Last we suggest a generalization of this approach, using Banach spaces.
DA - 2011/06/01/
PY - 2011
DO - 10/ctfch6
DP - ScienceDirect
VL - 209
IS - 6
SP - 966
EP - 991
J2 - Information and Computation
LA - en
SN - 0890-5401
UR - http://www.sciencedirect.com/science/article/pii/S0890540111000411
Y2 - 2019/11/22/17:01:53
KW - Coherence spaces
KW - Probabilistic programming
KW - Programming language theory
KW - Semantics
ER -
TY - CONF
TI - The Computational Meaning of Probabilistic Coherence Spaces
AU - Ehrhard, Thomas
AU - Pagani, Michele
AU - Tasson, Christine
T2 - 2011 26th Annual IEEE Symposium on Logic in Computer Science (LICS 2011)
AB - We study the probabilistic coherent spaces — a denotational semantics interpreting programs by power series with non negative real coefﬁcients. We prove that this semantics is adequate for a probabilistic extension of the untyped λ-calculus: the probability that a term reduces to a head normal form is equal to its denotation computed on a suitable set of values. The result gives, in a probabilistic setting, a quantitative reﬁnement to the adequacy of Scott’s model for untyped λ-calculus.
C1 - Toronto, ON, Canada
C3 - 2011 IEEE 26th Annual Symposium on Logic in Computer Science
DA - 2011/06//
PY - 2011
DO - 10/cpv52n
DP - Crossref
SP - 87
EP - 96
LA - en
PB - IEEE
SN - 978-1-4577-0451-2
UR - http://ieeexplore.ieee.org/document/5970206/
Y2 - 2019/11/26/20:50:00
KW - Coherence spaces
KW - Denotational semantics
KW - Probabilistic programming
KW - Programming language theory
ER -
TY - JOUR
TI - Predicate Transformers for Extended Probability and Non-determinism
AU - Keimel, Klaus
AU - Plotkin, Gordon d.
T2 - Mathematical. Structures in Comp. Sci.
AB - We investigate laws for predicate transformers for the combination of non-deterministic choice and (extended) probabilistic choice, where predicates are taken to be functions to the extended non-negative reals, or to closed intervals of such reals. These predicate transformers correspond to state transformers, which are functions to conical powerdomains, which are the appropriate powerdomains for the combined forms of non-determinism. As with standard powerdomains for non-deterministic choice, these come in three flavours – lower, upper and (order-)convex – so there are also three kinds of predicate transformers. In order to make the connection, the powerdomains are first characterised in terms of relevant classes of functionals. Much of the development is carried out at an abstract level, a kind of domain-theoretic functional analysis: one considers d-cones, which are dcpos equipped with a module structure over the non-negative extended reals, in place of topological vector spaces. Such a development still needs to be carried out for probabilistic choice per se; it would presumably be necessary to work with a notion of convex space rather than a cone.
DA - 2009/06//
PY - 2009
DO - 10/bkvgqc
DP - ACM Digital Library
VL - 19
IS - 3
SP - 501
EP - 539
SN - 0960-1295
UR - http://dx.doi.org/10.1017/S0960129509007555
Y2 - 2019/11/26/20:33:27
KW - Denotational semantics
KW - Powerdomains
KW - Programming language theory
ER -
TY - JOUR
TI - Semantic Domains for Combining Probability and Non-Determinism
AU - Tix, Regina
AU - Keimel, Klaus
AU - Plotkin, Gordon
T2 - Electronic Notes in Theoretical Computer Science
AB - We present domain-theoretic models that support both probabilistic and nondeterministic choice. In [36], Morgan and McIver developed an ad hoc semantics for a simple imperative language with both probabilistic and nondeterministic choice operators over a discrete state space, using domain-theoretic tools. We present a model also using domain theory in the sense of D.S. Scott (see e.g. [15]), but built over quite general continuous domains instead of discrete state spaces.
DA - 2009/02//
PY - 2009
DO - 10/d9hwq7
DP - Crossref
VL - 222
SP - 3
EP - 99
LA - en
SN - 15710661
UR - https://linkinghub.elsevier.com/retrieve/pii/S1571066109000036
Y2 - 2019/11/26/19:01:09
KW - Denotational semantics
KW - Powerdomains
KW - Probabilistic programming
KW - Programming language theory
ER -
TY - JOUR
TI - Distributing probability over non-determinism
AU - Varacca, Daniele
AU - Winskel, Glynn
T2 - Mathematical Structures in Computer Science
DA - 2006/02/21/
PY - 2006
DO - 10/czs9sx
DP - Crossref
VL - 16
IS - 01
SP - 87
LA - en
SN - 0960-1295, 1469-8072
UR - http://www.journals.cambridge.org/abstract_S0960129505005074
Y2 - 2019/11/26/20:30:24
KW - Categorical probability theory
KW - Denotational semantics
KW - Programming language theory
ER -
TY - JOUR
TI - The differential lambda-calculus
AU - Ehrhard, Thomas
AU - Regnier, Laurent
T2 - Theoretical Computer Science
AB - We present an extension of the lambda-calculus with differential constructions. We state and prove some basic results (confluence, strong normalization in the typed case), and also a theorem relating the usual Taylor series of analysis to the linear head reduction of lambda-calculus.
DA - 2003/12/02/
PY - 2003
DO - 10/bf3b8v
DP - ScienceDirect
VL - 309
IS - 1
SP - 1
EP - 41
J2 - Theoretical Computer Science
LA - en
SN - 0304-3975
UR - http://www.sciencedirect.com/science/article/pii/S030439750300392X
Y2 - 2019/11/24/17:23:34
KW - Differentiation
KW - Linear logic
KW - Programming language theory
ER -
TY - CONF
TI - Probabilistic game semantics
AU - Danos, Vincent
AU - Harmer, Russell
T2 - ACM Transactions on Computational Logic - TOCL
AB - A category of HO/N-style games and probabilistic strategies is developed where the possible choices of a strategy are quantified so as to give a measure of the likelihood of seeing a given play. A 2-sided die is shown to be universal in this category, in the sense that any strategy breaks down into a composition between some deterministic strategy and that die. The interpretative power of the category is then demonstrated by delineating a Cartesian closed subcategory which provides a fully abstract model of a probabilistic extension of Idealized Algol
DA - 2000/02/01/
PY - 2000
DO - 10/b6k43s
DP - ResearchGate
VL - 3
SP - 204
EP - 213
SN - 978-0-7695-0725-5
KW - Denotational semantics
KW - Game semantics
KW - Interactive semantics
KW - Probabilistic programming
KW - Programming language theory
ER -
TY - JOUR
TI - Probabilistic Non-determinism
AU - Jones, Claire
DA - 1989///
PY - 1989
DP - Zotero
SP - 198
LA - en
KW - Denotational semantics
KW - Probabilistic programming
KW - Programming language theory
ER -
TY - CONF
TI - A Probabilistic Powerdomain of Evaluations
AU - Jones, C.
AU - Plotkin, G.
C1 - Piscataway, NJ, USA
C3 - Proceedings of the Fourth Annual Symposium on Logic in Computer Science
DA - 1989///
PY - 1989
DP - ACM Digital Library
SP - 186
EP - 195
PB - IEEE Press
SN - 978-0-8186-1954-0
UR - http://dl.acm.org/citation.cfm?id=77350.77370
Y2 - 2019/11/26/17:27:23
KW - Denotational semantics
KW - Powerdomains
KW - Probabilistic programming
KW - Programming language theory
ER -