{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:14:22Z","timestamp":1775873662608,"version":"3.50.1"},"reference-count":54,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2018,1,3]],"date-time":"2018-01-03T00:00:00Z","timestamp":1514937600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Excellence Initiative of the German federal and state government, the CDZ project CAP","award":["GZ 1023"],"award-info":[{"award-number":["GZ 1023"]}]},{"name":"DFG Research Training Group","award":["2236 UnRAVeL"],"award-info":[{"award-number":["2236 UnRAVeL"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2018,3,31]]},"abstract":"<jats:p>This article investigates the semantic intricacies of conditioning, a main feature in probabilistic programming. Our study is based on an extension of the imperative probabilistic guarded command language pGCL with conditioning. We provide a weakest precondition (wp) semantics and an operational semantics. To deal with possibly diverging program behavior, we consider liberal preconditions. We show that diverging program behavior plays a key role when defining conditioning. We establish that weakest preconditions coincide with conditional expected rewards in Markov chains\u2014the operational semantics\u2014and that the wp-semantics conservatively extends the existing semantics of pGCL (without conditioning). An extension of these results with nondeterminism turns out to be problematic: although an operational semantics using Markov decision processes is rather straightforward, we show that providing an inductive wp-semantics in this setting is impossible. Finally, we present two program transformations that eliminate conditioning from any program. The first transformation hoists conditioning while updating the probabilistic choices in the program, while the second transformation replaces conditioning\u2014in the same vein as rejection sampling\u2014by a program with loops. In addition, we present a last program transformation that replaces an independent identically distributed loop with conditioning.<\/jats:p>","DOI":"10.1145\/3156018","type":"journal-article","created":{"date-parts":[[2018,1,3]],"date-time":"2018-01-03T13:19:43Z","timestamp":1514985583000},"page":"1-50","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":40,"title":["Conditioning in Probabilistic Programming"],"prefix":"10.1145","volume":"40","author":[{"given":"Federico","family":"Olmedo","sequence":"first","affiliation":[{"name":"Department of Computer Science, University of Chile, Chile"}]},{"given":"Friedrich","family":"Gretz","sequence":"additional","affiliation":[{"name":"Bosch Corporate Research, Germany"}]},{"given":"Nils","family":"Jansen","sequence":"additional","affiliation":[{"name":"Radboud University Nijmegen, The Netherlands"}]},{"given":"Benjamin Lucien","family":"Kaminski","sequence":"additional","affiliation":[{"name":"RWTH Aachen University, Germany"}]},{"given":"Joost-Pieter","family":"Katoen","sequence":"additional","affiliation":[{"name":"RWTH Aachen University, Germany"}]},{"given":"Annabelle","family":"Mciver","sequence":"additional","affiliation":[{"name":"Macquarie University, Sydney, Australia"}]}],"member":"320","published-online":{"date-parts":[[2018,1,3]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2011.49"},{"key":"e_1_2_1_2_1","volume-title":"Andr\u00e9s and Peter van Rossum","author":"Miguel","year":"2008","unstructured":"Miguel E. Andr\u00e9s and Peter van Rossum. 2008. Conditional probabilities over probabilistic and nondeterministic systems. In TACAS (LNCS), Vol. 4963. Springer, 157--172."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2007.09.002"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-1674-2"},{"key":"e_1_2_1_5_1","volume-title":"Principles of Model Checking","author":"Baier Christel","unstructured":"Christel Baier and Joost-Pieter Katoen. 2008. Principles of Model Checking. MIT Press."},{"key":"e_1_2_1_6_1","volume-title":"TACAS (LNCS)","author":"Baier Christel","unstructured":"Christel Baier, Joachim Klein, Sascha Kl\u00fcppelholz, and Steffen M\u00e4rcker. 2014. Computing conditional probabilities in Markovian models efficiently. In TACAS (LNCS), Vol. 8413. Springer, 515--530."},{"key":"e_1_2_1_7_1","volume-title":"Luis Mar\u00eda Ferrer Fioriti, and Justin Hsu","author":"Barthe Gilles","year":"2016","unstructured":"Gilles Barthe, Thomas Espitau, Luis Mar\u00eda Ferrer Fioriti, and Justin Hsu. 2016. Synthesizing probabilistic invariants via doob\u2019s decomposition. In CAV (LNCS), Vol. 9779. Springer, 43--61."},{"key":"e_1_2_1_8_1","volume-title":"Programming Languages and Their Definition","author":"Beki\u0107 Hans","unstructured":"Hans Beki\u0107. 1984. Definable operation in general algebras, and the theory of automata and flowcharts. In Programming Languages and Their Definition. Springer, 30--55."},{"key":"e_1_2_1_9_1","volume-title":"ESOP (LNCS)","author":"Borgstr\u00f6m Johannes","unstructured":"Johannes Borgstr\u00f6m, Andrew D. Gordon, Michael Greenberg, James Margetson, and Jurgen Van Gael. 2011. Measure transformer semantics for Bayesian machine learning. In ESOP (LNCS), Vol. 6602. Springer, 77--96."},{"key":"e_1_2_1_10_1","first-page":"247","article-title":"Acceptance--rejection sampling from the conditional distribution of independent discrete random variables, given their sum","volume":"34","author":"Brostr\u00f6m G\u00f6ran","year":"2000","unstructured":"G\u00f6ran Brostr\u00f6m and Leif Nilsson. 2000. Acceptance--rejection sampling from the conditional distribution of independent discrete random variables, given their sum. Statistics J. Theoret. Appl. Stat. 34, 3 (2000), 247--257.","journal-title":"Statistics J. Theoret. Appl. Stat."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509136.2509546"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_34"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10936-7_6"},{"key":"e_1_2_1_14_1","volume-title":"Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs","author":"Chatterjee Krishnendu","unstructured":"Krishnendu Chatterjee, Hongfei Fu, Petr Novotn\u00fd, and Rouzbeh Hasheminezhad. 2016. Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs. In POPL. ACM Press, 327--342."},{"key":"e_1_2_1_15_1","volume-title":"Bayesian inference using data flow analysis","author":"Claret Guillaume","unstructured":"Guillaume Claret, Sriram K. Rajamani, Aditya V. Nori, Andrew D. Gordon, and Johannes Borgstr\u00f6m. 2013. Bayesian inference using data flow analysis. In ESEC\/SIGSOFT FSE. ACM Press, 92--102."},{"key":"e_1_2_1_16_1","volume-title":"pGCL for Isabelle. Archive of Formal Proofs","author":"Cock David","year":"2014","unstructured":"David Cock. 2014. pGCL for Isabelle. Archive of Formal Proofs (2014)."},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28869-2_9"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1142\/S012905410200114X"},{"key":"e_1_2_1_19_1","volume-title":"A Discipline of Programming","author":"Dijkstra Edsger W.","unstructured":"Edsger W. Dijkstra. 1976. A Discipline of Programming. Prentice Hall."},{"key":"e_1_2_1_20_1","volume-title":"Jonas Vlasselaer, and Luc De Raedt.","author":"Dries Anton","year":"2015","unstructured":"Anton Dries, Angelika Kimmig, Wannes Meert, Joris Renkens, Guy Van den Broeck, Jonas Vlasselaer, and Luc De Raedt. 2015. ProbLog2: Probabilistic logic programming. In ECML\/PKDD (3) (LNCS), Vol. 9286. Springer, 312--315."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2013.03.005"},{"key":"e_1_2_1_22_1","volume-title":"Goodman and Andreas Stuhlm\u00fcller","author":"Noah","year":"2014","unstructured":"Noah D. Goodman and Andreas Stuhlm\u00fcller. 2014. The Design and Implementation of Probabilistic Programming Languages. (electronic). http:\/\/dippl.org."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535850"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2593882.2593900"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.peva.2013.11.004"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292558"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-010-0157-0"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2666356.2594303"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.08.005"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-46520-3_5"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2015.12.013"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-48057-1_24"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005153"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-23506-6_4"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15769-1_24"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-010-0097-6"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(81)90036-2"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(85)90012-1"},{"key":"e_1_2_1_39_1","first-page":"1","article-title":"Operational semantics and generalized weakest preconditions. Sci","volume":"22","author":"Lukkien Johan J.","year":"1994","unstructured":"Johan J. Lukkien. 1994. Operational semantics and generalized weakest preconditions. Sci. Comput. Program. 22, 1--2 (1994), 137--155.","journal-title":"Comput. Program."},{"key":"e_1_2_1_40_1","volume-title":"Refinement and Proof for Probabilistic Systems","author":"McIver Annabelle","unstructured":"Annabelle McIver and Carroll Morgan. 2005. Abstraction, Refinement and Proof for Probabilistic Systems. Springer."},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/229542.229547"},{"key":"e_1_2_1_42_1","volume-title":"R2: An efficient MCMC sampler for probabilistic programs","author":"Nori Aditya V.","unstructured":"Aditya V. Nori, Chung-Kil Hur, Sriram K. Rajamani, and Selva Samuel. 2014. R2: An efficient MCMC sampler for probabilistic programs. In AAAI. AAAI Press, 2476--2482."},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2935317"},{"key":"e_1_2_1_44_1","first-page":"1935","article-title":"A compilation target for probabilistic programming languages","volume":"32","author":"Paige Brooks","year":"2014","unstructured":"Brooks Paige and Frank Wood. 2014. A compilation target for probabilistic programming languages. In ICML (Proc. of JMLR), Vol. 32. 1935--1943.","journal-title":"ICML (Proc. of JMLR)"},{"key":"e_1_2_1_45_1","volume-title":"Practical Probabilistic Programming","author":"Pfeffer Avi","unstructured":"Avi Pfeffer. 2016. Practical Probabilistic Programming. Manning Publications Co."},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1002\/9780470316887"},{"key":"e_1_2_1_47_1","volume-title":"Monte Carlo Statistical Methods","author":"Robert Christian","unstructured":"Christian Robert and George Casella. 2013. Monte Carlo Statistical Methods. Springer Science 8 Business Media."},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/2666356.2594294"},{"key":"e_1_2_1_49_1","volume-title":"A Computational Introduction to Number Theory and Algebra","author":"Shoup Victor","unstructured":"Victor Shoup. 2009. A Computational Introduction to Number Theory and Algebra. Cambridge University Press."},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2935313"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511619052"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129505005074"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-76771-5"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-39519-7_16"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3156018","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3156018","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:38:44Z","timestamp":1750221524000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3156018"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,1,3]]},"references-count":54,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2018,3,31]]}},"alternative-id":["10.1145\/3156018"],"URL":"https:\/\/doi.org\/10.1145\/3156018","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"value":"0164-0925","type":"print"},{"value":"1558-4593","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,1,3]]},"assertion":[{"value":"2016-10-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2017-09-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2018-01-03","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}