{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,2]],"date-time":"2026-10-02T07:58:56Z","timestamp":1790927936802,"version":"4.1.0"},"reference-count":39,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T00:00:00Z","timestamp":1641945600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc-sa\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000038","name":"Natural Sciences and Engineering Research Council of Canada","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100000038","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2022,1,16]]},"abstract":"<jats:p>\n            Metareasoning can be achieved in probabilistic programming languages (PPLs) using agent models that\n            <jats:italic>recursively nest<\/jats:italic>\n            inference queries inside inference queries. However, the semantics of this powerful, reflection-like language feature has defied an operational treatment, much less reasoning principles for contextual equivalence. We give formal semantics to a core PPL with continuous distributions, scoring, general recursion, and nested queries. Unlike prior work, the presence of nested queries and general recursion makes it impossible to stratify the definition of a sampling-based operational semantics and that of a measure-theoretic semantics\u2014the two semantics must be defined mutually recursively. A key yet challenging property we establish is that probabilistic programs have well-defined meanings: limits exist for the step-indexed measures they induce. Beyond a semantics, we offer relational reasoning principles for probabilistic programs making nested queries. We construct a step-indexed, biorthogonal logical-relations model. A soundness theorem establishes that logical relatedness implies contextual equivalence. We demonstrate the usefulness of the reasoning principles by proving novel equivalences of practical relevance\u2014in particular, game-playing and decisionmaking agents. We mechanize our technical developments leading to the soundness proof using the Coq proof assistant. Nested queries are an important yet theoretically underdeveloped linguistic feature in PPLs; we are first to give them semantics in the presence of general recursion and to provide them with sound reasoning principles for contextual equivalence.\n          <\/jats:p>","DOI":"10.1145\/3498677","type":"journal-article","created":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T17:03:12Z","timestamp":1642006992000},"page":"1-28","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":20,"title":["Reasoning about \u201creasoning about reasoning\u201d: semantics and contextual equivalence for probabilistic programs with nested queries and recursion"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8206-4694","authenticated-orcid":false,"given":"Yizhou","family":"Zhang","sequence":"first","affiliation":[{"name":"University of Waterloo, Canada"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Nada","family":"Amin","sequence":"additional","affiliation":[{"name":"Harvard University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2022,1,12]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2011.49"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/11693024_6"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/504709.504712"},{"key":"e_1_2_2_4_1","volume-title":"Dynamic Programming","author":"Bellman Richard E.","unstructured":"Richard E. Bellman . 1957. Dynamic Programming . Princeton University Press . Richard E. Bellman. 1957. Dynamic Programming. Princeton University Press."},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89884-1_6"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46678-0_18"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951942"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_14"},{"key":"e_1_2_2_9_1","unstructured":"Owain Evans Andreas Stuhlm\u00fcller John Salvatier and Daniel Filan. 2017. Modeling Agents with Probabilistic Programs. https:\/\/agentmodels.org.  Owain Evans Andreas Stuhlm\u00fcller John Salvatier and Daniel Filan. 2017. Modeling Agents with Probabilistic Programs. https:\/\/agentmodels.org."},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90014-7"},{"key":"e_1_2_2_11_1","volume-title":"Tenenbaum","author":"Freer Cameron E.","year":"2014","unstructured":"Cameron E. Freer , Daniel M. Roy , and Joshua B . Tenenbaum . 2014 . Towards Common Sense Reasoning via Conditional Simulation : Legacies of Turing in Artificial Intelligence. Turing's Legacy 42 ( 2014 ). arXiv: 1212. 4799 Cameron E. Freer, Daniel M. Roy, and Joshua B. Tenenbaum. 2014. Towards Common Sense Reasoning via Conditional Simulation: Legacies of Turing in Artificial Intelligence. Turing's Legacy 42 ( 2014 ). arXiv: 1212. 4799"},{"key":"e_1_2_2_12_1","volume-title":"Amortized Inference in Probabilistic Reasoning. In Annual Meeting of the Cognitive Science Society (CogSci). https:\/\/cogsci.mindmodeling.org\/2014\/papers\/098\/paper098","author":"Samuel","unstructured":"Samuel J. Gershman and Noah D. Goodman. 2014 . Amortized Inference in Probabilistic Reasoning. In Annual Meeting of the Cognitive Science Society (CogSci). https:\/\/cogsci.mindmodeling.org\/2014\/papers\/098\/paper098 .pdf Samuel J. Gershman and Noah D. Goodman. 2014. Amortized Inference in Probabilistic Reasoning. In Annual Meeting of the Cognitive Science Society (CogSci). https:\/\/cogsci.mindmodeling.org\/2014\/papers\/098\/paper098.pdf"},{"key":"e_1_2_2_13_1","volume-title":"Tenenbaum","author":"Goodman Noah D.","year":"2008","unstructured":"Noah D. Goodman , Vikash K. Mansinghka , Daniel Roy , Keith Bonawitz , and Joshua B . Tenenbaum . 2008 . Church : A Language for Generative Models. In Uncertainty in Artificial Intelligence (UAI) . arXiv:1206.3255 Noah D. Goodman, Vikash K. Mansinghka, Daniel Roy, Keith Bonawitz, and Joshua B. Tenenbaum. 2008. Church: A Language for Generative Models. In Uncertainty in Artificial Intelligence (UAI). arXiv:1206.3255"},{"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":"Symbolic Exact Inference for Discrete Probabilistic Programs. ( 2019 ). arXiv","author":"Holtzen Steven","year":"1904","unstructured":"Steven Holtzen , Todd Millstein , and Guy Van den Broeck . 2019. Symbolic Exact Inference for Discrete Probabilistic Programs. ( 2019 ). arXiv : 1904 .02079 Steven Holtzen, Todd Millstein, and Guy Van den Broeck. 2019. Symbolic Exact Inference for Discrete Probabilistic Programs. ( 2019 ). arXiv: 1904.02079"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428208"},{"key":"e_1_2_2_17_1","volume-title":"Dynamic Programming and Markov Processes","author":"Howard Ronald A.","unstructured":"Ronald A. Howard . 1960. Dynamic Programming and Markov Processes . The MIT Press . Ronald A. Howard. 1960. Dynamic Programming and Markov Processes. The MIT Press."},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1017\/9781108770750.004"},{"key":"e_1_2_2_19_1","volume-title":"Beyond Almost-Sure Termination. In Annual Meeting of the Cognitive Science Society (CogSci). https: \/\/cogsci.mindmodeling.org\/2017\/papers\/0430\/paper0430","author":"Icard Thomas","year":"2017","unstructured":"Thomas Icard . 2017 . Beyond Almost-Sure Termination. In Annual Meeting of the Cognitive Science Society (CogSci). https: \/\/cogsci.mindmodeling.org\/2017\/papers\/0430\/paper0430 .pdf Thomas Icard. 2017. Beyond Almost-Sure Termination. In Annual Meeting of the Cognitive Science Society (CogSci). https: \/\/cogsci.mindmodeling.org\/2017\/papers\/0430\/paper0430.pdf"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1979.38"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1080\/01621459.1998.10473765"},{"key":"e_1_2_2_22_1","unstructured":"Theofrastos Mantadelis and Gerda Janssens. 2011. Nesting Probabilistic Inference. ( 2011 ). arXiv: 1112. 3785  Theofrastos Mantadelis and Gerda Janssens. 2011. Nesting Probabilistic Inference. ( 2011 ). arXiv: 1112. 3785"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800000125"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3156018"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1452044.1452048"},{"key":"e_1_2_2_28_1","unstructured":"Andrew Pitts and Ian Stark. 1998. Operational Reasoning for Functions with Local State. In Higher Order Operational Techniques in Semantics. https:\/\/homepages.inf.ed.ac.uk\/stark\/operfl.pdf  Andrew Pitts and Ian Stark. 1998. Operational Reasoning for Functions with Local State. In Higher Order Operational Techniques in Semantics. https:\/\/homepages.inf.ed.ac.uk\/stark\/operfl.pdf"},{"key":"e_1_2_2_29_1","volume-title":"Uncertainty in Artificial Intelligence (UAI). arXiv","author":"Rainforth Tom","year":"1803","unstructured":"Tom Rainforth . 2018. Nesting Probabilistic Programs . In Uncertainty in Artificial Intelligence (UAI). arXiv : 1803 .06328 Tom Rainforth. 2018. Nesting Probabilistic Programs. In Uncertainty in Artificial Intelligence (UAI). arXiv: 1803.06328"},{"key":"e_1_2_2_30_1","volume-title":"Nested Reasoning About Autonomous Agents Using Probabilistic Programs. ( 2020 ). arXiv","author":"Seaman Iris Rubi","year":"1812","unstructured":"Iris Rubi Seaman , Jan-Willem van de Meent , and David Wingate . 2020. Nested Reasoning About Autonomous Agents Using Probabilistic Programs. ( 2020 ). arXiv : 1812 .01569 Iris Rubi Seaman, Jan-Willem van de Meent, and David Wingate. 2020. Nested Reasoning About Autonomous Agents Using Probabilistic Programs. ( 2020 ). arXiv: 1812.01569"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(85)80001-2"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_32"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2935313"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.2307\/j.ctvd58v18"},{"key":"e_1_2_2_36_1","volume-title":"Goodman","author":"Stuhlm\u00fcller Andreas","year":"2012","unstructured":"Andreas Stuhlm\u00fcller and Noah D . Goodman . 2012 . A Dynamic Programming Algorithm for Inference in Recursive Probabilistic Programs . ( 2012 ). arXiv: 1206. 3555 Andreas Stuhlm\u00fcller and Noah D. Goodman. 2012. A Dynamic Programming Algorithm for Inference in Recursive Probabilistic Programs. ( 2012 ). arXiv: 1206. 3555"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.cogsys.2013.07.003"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-55089-9_3"},{"key":"e_1_2_2_39_1","volume-title":"The Random Conditional Distribution for Higher-Order Probabilistic Inference. ( 2019 ). arXiv","author":"Tavares Zenna","year":"1903","unstructured":"Zenna Tavares , Xin Zhang , Edgar Minaysan , Javier Burroni , Rajesh Ranganath , and Armando Solar-Lezama . 2019. The Random Conditional Distribution for Higher-Order Probabilistic Inference. ( 2019 ). arXiv : 1903 .10556 Zenna Tavares, Xin Zhang, Edgar Minaysan, Javier Burroni, Rajesh Ranganath, and Armando Solar-Lezama. 2019. The Random Conditional Distribution for Higher-Order Probabilistic Inference. ( 2019 ). arXiv: 1903.10556"},{"key":"e_1_2_2_40_1","volume-title":"Probabilistic Programs with Stochastic Conditioning. ( 2021 ). arXiv","author":"Tolpin David","year":"2010","unstructured":"David Tolpin , Yuan Zhou , and Hongseok Yang . 2021. Probabilistic Programs with Stochastic Conditioning. ( 2021 ). arXiv : 2010 .00282 David Tolpin, Yuan Zhou, and Hongseok Yang. 2021. Probabilistic Programs with Stochastic Conditioning. ( 2021 ). arXiv: 2010.00282"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1007720632734"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236782"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3498677","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3498677","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:30:28Z","timestamp":1750188628000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3498677"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,1,12]]},"references-count":39,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2022,1,16]]}},"alternative-id":["10.1145\/3498677"],"URL":"https:\/\/doi.org\/10.1145\/3498677","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,1,12]]},"assertion":[{"value":"2022-01-12","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}