{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,8,22]],"date-time":"2024-08-22T13:26:46Z","timestamp":1724333206411},"reference-count":39,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2017,12,27]],"date-time":"2017-12-27T00:00:00Z","timestamp":1514332800000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Engi- neering and Physical Sciences Research Council","award":["Early Career Fellowship EP\/L002388\/1 Combining viewpoints in quantum theory , an EPSRC studentship and grants EP\/N007387\/1 Quan- tum computation as a programming language and EP\/M023974\/1 Compositional higher-order model checking: logics, models, and a"]},{"DOI":"10.13039\/501100000288","name":"Royal Society","doi-asserted-by":"crossref","award":["University Research Fellowship"],"id":[{"id":"10.13039\/501100000288","id-type":"DOI","asserted-by":"crossref"}]},{"name":"Institute for Information & Commu- nications Technology Promotion (IITP) grant funded by the Korea government","award":["R0190- 16-2011 Development of Vulnerability Discovery Technologies for IoT Software Security"]},{"name":"Balliol College Oxford","award":["Career Development Fellowship"]},{"DOI":"10.13039\/501100000734","name":"University College Oxford","doi-asserted-by":"crossref","award":["Junior Research Fellowship"],"id":[{"id":"10.13039\/501100000734","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2018,1]]},"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.<\/jats:p>\n 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.<\/jats:p>\n 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.<\/jats:p>","DOI":"10.1145\/3158148","type":"journal-article","created":{"date-parts":[[2017,12,29]],"date-time":"2017-12-29T14:21:49Z","timestamp":1514557309000},"page":"1-29","update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":27,"title":["Denotational validation of higher-order Bayesian inference"],"prefix":"10.1145","volume":"2","author":[{"given":"Adam","family":"\u015acibior","sequence":"first","affiliation":[{"name":"University of Cambridge, UK \/ MPI T\u00fcbingen, Germany"}]},{"given":"Ohad","family":"Kammar","sequence":"additional","affiliation":[{"name":"University of Oxford, UK"}]},{"given":"Matthijs","family":"V\u00e1k\u00e1r","sequence":"additional","affiliation":[{"name":"University of Oxford, UK"}]},{"given":"Sam","family":"Staton","sequence":"additional","affiliation":[{"name":"University of Oxford, UK"}]},{"given":"Hongseok","family":"Yang","sequence":"additional","affiliation":[{"name":"KAIST, South Korea"}]},{"given":"Yufei","family":"Cai","sequence":"additional","affiliation":[{"name":"University of T\u00fcbingen, Germany"}]},{"given":"Klaus","family":"Ostermann","sequence":"additional","affiliation":[{"name":"University of T\u00fcbingen, Germany"}]},{"given":"Sean K.","family":"Moss","sequence":"additional","affiliation":[{"name":"University of Cambridge, UK \/ University of Oxford, UK"}]},{"given":"Chris","family":"Heunen","sequence":"additional","affiliation":[{"name":"University of Edinburgh, UK"}]},{"given":"Zoubin","family":"Ghahramani","sequence":"additional","affiliation":[{"name":"University of Cambridge, UK \/ Uber AI Labs, USA"}]}],"member":"320","published-online":{"date-parts":[[2017,12,27]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1215\/ijm\/1255631584"},{"key":"e_1_2_2_2_1","volume-title":"Andrew D. Gordon, and Marcin Szymczak.","author":"Borgstr\u00f6m Johannes","year":"2015","unstructured":"Johannes Borgstr\u00f6m , Ugo Dal Lago , Andrew D. Gordon, and Marcin Szymczak. 2015 . A Lambda-Calculus Foundation for Universal Probabilistic Programming. CoRR abs\/1512.08990 (2015). http:\/\/arxiv.org\/abs\/1512.08990 Johannes Borgstr\u00f6m, Ugo Dal Lago, Andrew D. Gordon, and Marcin Szymczak. 2015. A Lambda-Calculus Foundation for Universal Probabilistic Programming. CoRR abs\/1512.08990 (2015). http:\/\/arxiv.org\/abs\/1512.08990"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951942"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.18637\/jss.v076.i01"},{"key":"e_1_2_2_5_1","volume-title":"Johansen","author":"Doucet Arnaud","year":"2011","unstructured":"Arnaud Doucet and Adam M . Johansen . 2011 . A Tutorial on Particle Filtering and Smoothing: Fifteen years later. In The Oxford Handbook of Nonlinear Filtering, Dan Crisan and Boris Rozovskii (Eds.). Oxford University Press , 656\u2013704. Arnaud Doucet and Adam M. Johansen. 2011. A Tutorial on Particle Filtering and Smoothing: Fifteen years later. In The Oxford Handbook of Nonlinear Filtering, Dan Crisan and Boris Rozovskii (Eds.). Oxford University Press, 656\u2013704."},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(91)90036-W"},{"key":"e_1_2_2_7_1","volume-title":"List Objects with Algebraic Structure. In 2st International Conference on Formal Structures for Computation and Deduction, FSCD","author":"Fiore Marcelo","year":"2017","unstructured":"Marcelo Fiore and Philip Saville . 2017 . List Objects with Algebraic Structure. In 2st International Conference on Formal Structures for Computation and Deduction, FSCD 2017. Marcelo Fiore and Philip Saville. 2017. List Objects with Algebraic Structure. In 2st International Conference on Formal Structures for Computation and Deduction, FSCD 2017."},{"key":"e_1_2_2_8_1","volume-title":"Reflections on Type Theory, Lambda Calculus, and the Mind, Essays Dedicated to Henk Barendregt on the Occasion of his 60th Birthday. Radboud Universiteit, Nijmegen, 101\u2013114.","author":"Geuvers Herman","unstructured":"Herman Geuvers and Erik Poll . 2007. Iteration and primitive recursion in categorical terms . In Reflections on Type Theory, Lambda Calculus, and the Mind, Essays Dedicated to Henk Barendregt on the Occasion of his 60th Birthday. Radboud Universiteit, Nijmegen, 101\u2013114. Herman Geuvers and Erik Poll. 2007. Iteration and primitive recursion in categorical terms. In Reflections on Type Theory, Lambda Calculus, and the Mind, Essays Dedicated to Henk Barendregt on the Occasion of his 60th Birthday. Radboud Universiteit, Nijmegen, 101\u2013114."},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1201\/b10905-2"},{"key":"e_1_2_2_10_1","unstructured":"Noah Goodman Vikash Mansinghka Daniel M Roy Keith Bonawitz and Joshua B Tenenbaum. 2008. Church: a language for generative models. In UAI. Noah Goodman Vikash Mansinghka Daniel M Roy Keith Bonawitz and Joshua B Tenenbaum. 2008. Church: a language for generative models. In UAI."},{"key":"e_1_2_2_11_1","unstructured":"Noah Goodman and Andreas Stuhlm\u00fcller. 2014. Design and Implementation of Probabilistic Programming Languages. http:\/\/dippl.org . (2014). Noah Goodman and Andreas Stuhlm\u00fcller. 2014. Design and Implementation of Probabilistic Programming Languages. http:\/\/dippl.org . (2014)."},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535850"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.10.028"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005137"},{"key":"e_1_2_2_15_1","volume-title":"35th IARCS Annual Conference on Foundation of Software Technology and Theoretical Computer Science, FSTTCS 2015","author":"Hur Chung-Kil","year":"2015","unstructured":"Chung-Kil Hur , Aditya V. Nori , Sriram K. Rajamani , and Selva Samuel . 2015 . A Provably Correct Sampler for Probabilistic Programs . In 35th IARCS Annual Conference on Foundation of Software Technology and Theoretical Computer Science, FSTTCS 2015 , December 16-18, 2015, Bangalore, India. 475\u2013488. Chung-Kil Hur, Aditya V. Nori, Sriram K. Rajamani, and Selva Samuel. 2015. A Provably Correct Sampler for Probabilistic Programs. In 35th IARCS Annual Conference on Foundation of Software Technology and Theoretical Computer Science, FSTTCS 2015, December 16-18, 2015, Bangalore, India. 475\u2013488."},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796899003500"},{"key":"e_1_2_2_17_1","volume-title":"From Probability Monads to Commutative Effectuses. Journ. of Logical and Algebraic Methods in Programming","author":"Jacobs Bart","year":"2017","unstructured":"Bart Jacobs . 2017. From Probability Monads to Commutative Effectuses. Journ. of Logical and Algebraic Methods in Programming ( 2017 ). To appear. Bart Jacobs. 2017. From Probability Monads to Commutative Effectuses. Journ. of Logical and Algebraic Methods in Programming (2017). To appear."},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0004972700006353"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01304852"},{"key":"e_1_2_2_21_1","first-page":"97","article-title":"Commutative monads as a theory of distributions","volume":"26","author":"Kock Anders","year":"2012","unstructured":"Anders Kock . 2012 . Commutative monads as a theory of distributions . Theory and Applications of Categories 26 , 4 (2012), 97 \u2013 131 . Anders Kock. 2012. Commutative monads as a theory of distributions. Theory and Applications of Categories 26, 4 (2012), 97\u2013131.","journal-title":"Theory and Applications of Categories"},{"key":"e_1_2_2_22_1","unstructured":"Alp Kucukelbir Rajesh Ranganath Andrew Gelman and David Blei. 2015. Automatic Variational Inference in Stan. In NIPS. https:\/\/papers.nips.cc\/paper\/5758-automatic-variational-inference-in-stan Alp Kucukelbir Rajesh Ranganath Andrew Gelman and David Blei. 2015. Automatic Variational Inference in Stan. In NIPS. https:\/\/papers.nips.cc\/paper\/5758-automatic-variational-inference-in-stan"},{"key":"e_1_2_2_23_1","volume-title":"Atilim Gunes Baydin, and Frank Wood","author":"Le Tuan Anh","year":"2017","unstructured":"Tuan Anh Le , Atilim Gunes Baydin, and Frank Wood . 2017 . Inference Compilation and Universal Probabilistic Programming. In AISTATS. http:\/\/www.tuananhle.co.uk\/assets\/pdf\/le2016inference.pdf Tuan Anh Le, Atilim Gunes Baydin, and Frank Wood. 2017. Inference Compilation and Universal Probabilistic Programming. In AISTATS. http:\/\/www.tuananhle.co.uk\/assets\/pdf\/le2016inference.pdf"},{"key":"e_1_2_2_24_1","volume-title":"Perov","author":"Mansinghka Vikash K.","year":"2014","unstructured":"Vikash K. Mansinghka , Daniel Selsam , and Yura N . Perov . 2014 . Venture : a higher-order probabilistic programming platform with programmable inference. arXiv:1404.0099 (2014). http:\/\/arxiv.org\/abs\/1404.0099 Vikash K. Mansinghka, Daniel Selsam, and Yura N. Perov. 2014. Venture: a higher-order probabilistic programming platform with programmable inference. arXiv:1404.0099 (2014). http:\/\/arxiv.org\/abs\/1404.0099"},{"key":"e_1_2_2_25_1","first-page":"84","article-title":"Monads as extension systems \u2014 no iteration is necessary","volume":"24","author":"Marmolejo Francisco","year":"2010","unstructured":"Francisco Marmolejo and Richard J. Wood . 2010 . Monads as extension systems \u2014 no iteration is necessary . Theory and Applications of Categories 24 , 4 (2010), 84 \u2013 113 . Francisco Marmolejo and Richard J. Wood. 2010. Monads as extension systems \u2014 no iteration is necessary. Theory and Applications of Categories 24, 4 (2010), 84\u2013113.","journal-title":"Theory and Applications of Categories"},{"key":"e_1_2_2_26_1","unstructured":"T. Minka J.M. Winn J.P. Guiver S. Webster Y. Zaykov B. Yangel A. Spengler and J. Bronskill. 2014. Infer.NET 2.6. (2014). Microsoft Research Cambridge. http:\/\/research.microsoft.com\/infernet. T. Minka J.M. Winn J.P. Guiver S. Webster Y. Zaykov B. Yangel A. Spengler and J. Bronskill. 2014. Infer.NET 2.6. (2014). Microsoft Research Cambridge. http:\/\/research.microsoft.com\/infernet."},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1989.39155"},{"key":"e_1_2_2_28_1","unstructured":"Lawrence M. Murray. 2013. Bayesian State-Space Modelling on High-Performance Hardware Using LibBi. arXiv:1306.3277. (2013). Lawrence M. Murray. 2013. Bayesian State-Space Modelling on High-Performance Hardware Using LibBi. arXiv:1306.3277. (2013)."},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-29604-3_5"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040320"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.207.2"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503288"},{"key":"e_1_2_2_33_1","doi-asserted-by":"crossref","unstructured":"Adam \u015acibior Zoubin Ghahramani and Andrew Gordon. 2015. Practical Probabilistic Programming with Monads. In Haskell. http:\/\/dl.acm.org\/citation.cfm?id=2804317 Adam \u015acibior Zoubin Ghahramani and Andrew Gordon. 2015. Practical Probabilistic Programming with Monads. In Haskell. http:\/\/dl.acm.org\/citation.cfm?id=2804317","DOI":"10.1145\/2804302.2804317"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_32"},{"key":"e_1_2_2_35_1","volume-title":"BUGS: A program to perform Bayesian inference using Gibbs sampling. Bayesian statistics 4","author":"Thomas Andrew","year":"1992","unstructured":"Andrew Thomas , David J. Spiegelhalter , and W. R. Gilks . 1992 . BUGS: A program to perform Bayesian inference using Gibbs sampling. Bayesian statistics 4 (1992), 837\u2013842. Issue 9. Andrew Thomas, David J. Spiegelhalter, and W. R. Gilks. 1992. BUGS: A program to perform Bayesian inference using Gibbs sampling. Bayesian statistics 4 (1992), 837\u2013842. Issue 9."},{"key":"e_1_2_2_36_1","volume-title":"Blei","author":"Tran Dustin","year":"2017","unstructured":"Dustin Tran , Matthew D. Hoffman , Rif A. Saurous , Eugene Brevdo , Kevin Murphy , and David M . Blei . 2017 . Deep Probabilistic Programming. In ICLR. Dustin Tran, Matthew D. Hoffman, Rif A. Saurous, Eugene Brevdo, Kevin Murphy, and David M. Blei. 2017. Deep Probabilistic Programming. In ICLR."},{"key":"e_1_2_2_37_1","unstructured":"David Wingate Andreas Stuhlm\u00fcller and Noah Goodman. 2011. Lightweight Implementations of Probabilistic Programming Languages Via Transformational Compilation. In AISTATS. https:\/\/web.stanford.edu\/~ngoodman\/papers\/ lightweight-mcmc-aistats2011.pdf The published version contains a serious bug in the definition of alpha that was fixed in revision 3 available at the given URL. David Wingate Andreas Stuhlm\u00fcller and Noah Goodman. 2011. Lightweight Implementations of Probabilistic Programming Languages Via Transformational Compilation. In AISTATS. https:\/\/web.stanford.edu\/~ngoodman\/papers\/ lightweight-mcmc-aistats2011.pdf The published version contains a serious bug in the definition of alpha that was fixed in revision 3 available at the given URL."},{"key":"e_1_2_2_38_1","unstructured":"David Wingate and Theophane Weber. 2013. Automated Variational Inference in Probabilistic Programming. arXiv:1301.1299. (2013). David Wingate and Theophane Weber. 2013. Automated Variational Inference in Probabilistic Programming. arXiv:1301.1299. (2013)."},{"key":"e_1_2_2_39_1","volume-title":"Proceedings of the 17th International conference on Artificial Intelligence and Statistics. 1024\u20131032","author":"Wood Frank","unstructured":"Frank Wood , Jan Willem van de Meent, and Vikash Mansinghka. 2014. A New Approach to Probabilistic Programming Inference . In Proceedings of the 17th International conference on Artificial Intelligence and Statistics. 1024\u20131032 . Frank Wood, Jan Willem van de Meent, and Vikash Mansinghka. 2014. A New Approach to Probabilistic Programming Inference. In Proceedings of the 17th International conference on Artificial Intelligence and Statistics. 1024\u20131032."},{"key":"e_1_2_2_40_1","volume-title":"Proceedings of Uncertainty in Artificial Intelligence.","author":"Zinkov Robert","year":"2017","unstructured":"Robert Zinkov and Chung-chieh Shan. 2017 . Composing inference algorithms as program transformations . In Proceedings of Uncertainty in Artificial Intelligence. Robert Zinkov and Chung-chieh Shan. 2017. Composing inference algorithms as program transformations. In Proceedings of Uncertainty in Artificial Intelligence."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3158148","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,31]],"date-time":"2022-12-31T19:35:43Z","timestamp":1672515343000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3158148"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,12,27]]},"references-count":39,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2018,1]]}},"alternative-id":["10.1145\/3158148"],"URL":"https:\/\/doi.org\/10.1145\/3158148","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,12,27]]},"assertion":[{"value":"2017-12-27","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}