{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,18]],"date-time":"2026-08-18T14:31:46Z","timestamp":1787063506916,"version":"build-2736575974"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030452308","type":"print"},{"value":"9783030452315","type":"electronic"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>A notion of probabilistic lambda-calculus usually comes with a prescribed reduction strategy, typically call-by-name or call-by-value, as the calculus is non-confluent and these strategies yield different results. This is a break with one of the main advantages of lambda-calculus: confluence, which means results are independent from the choice of strategy. We present a probabilistic lambda-calculus where the probabilistic operator is decomposed into two syntactic constructs: a generator, which represents a probabilistic event; and a consumer, which acts on the term depending on a given event. The resulting calculus, the Probabilistic Event Lambda-Calculus, is confluent, and interprets the call-by-name and call-by-value strategies through different interpretations of the probabilistic operator into our generator and consumer constructs. We present two notions of reduction, one via fine-grained local rewrite steps, and one by generation and consumption of probabilistic events. Simple types for the calculus are essentially standard, and they convey strong normalization. We demonstrate how we can encode call-by-name and call-by-value probabilistic evaluation.<\/jats:p>","DOI":"10.1007\/978-3-030-45231-5_8","type":"book-chapter","created":{"date-parts":[[2020,4,17]],"date-time":"2020-04-17T06:02:53Z","timestamp":1587103373000},"page":"136-156","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Decomposing Probabilistic Lambda-Calculi"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9200-070X","authenticated-orcid":false,"given":"Ugo","family":"Dal Lago","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0469-4279","authenticated-orcid":false,"given":"Giulio","family":"Guerrieri","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Willem","family":"Heijltjes","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2020,4,17]]},"reference":[{"key":"8_CR1","doi-asserted-by":"publisher","unstructured":"Avanzini, M., Dal Lago, U., Ghyselen, A.: Type-based complexity analysis of probabilistic functional programs. In: 34th Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2019. pp. 1\u201313. IEEE Computer Society (2019). https:\/\/doi.org\/10.1109\/LICS.2019.8785725","DOI":"10.1109\/LICS.2019.8785725"},{"key":"8_CR2","unstructured":"Barendregt, H.P.: The Lambda Calculus \u2013 Its Syntax and Semantics, Studies in logic and the foundations of mathematics, vol. 103. North-Holland (1984)"},{"key":"8_CR3","doi-asserted-by":"publisher","unstructured":"Borgstr\u00f6m, J., Dal Lago, U., Gordon, A.D., Szymczak, M.: A lambda-calculus foundation for universal probabilistic programming. In: 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016. pp. 33\u201346. ACM (2016). https:\/\/doi.org\/10.1145\/2951913.2951942","DOI":"10.1145\/2951913.2951942"},{"key":"8_CR4","doi-asserted-by":"publisher","unstructured":"Breuvart, F., Dal Lago, U.: On intersection types and probabilistic lambda calculi. In: Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming, PPDP 2018. pp. 8:1\u20138:13. ACM (2018). https:\/\/doi.org\/10.1145\/3236950.3236968","DOI":"10.1145\/3236950.3236968"},{"key":"8_CR5","doi-asserted-by":"publisher","unstructured":"Dal Lago, U., Faggian, C., Valiron, B., Yoshimizu, A.: The geometry of parallelism: classical, probabilistic, and quantum effects. In: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017. pp. 833\u2013845. ACM (2017). https:\/\/doi.org\/10.1145\/3009837","DOI":"10.1145\/3009837"},{"key":"8_CR6","doi-asserted-by":"publisher","unstructured":"Dal Lago, U., Grellois, C.: Probabilistic termination by monadic affine sized typing. ACM Transactions on Programming Languages and Systems 41(2), 10:1\u201310:65 (2019). https:\/\/doi.org\/10.1145\/3293605","DOI":"10.1145\/3293605"},{"key":"8_CR7","unstructured":"Dal Lago, U., Guerrieri, G., Heijltjes, W.: Decomposing probabilistic lambda-calculi (long version) (2020), https:\/\/arxiv.org\/abs\/2002.08392"},{"key":"8_CR8","doi-asserted-by":"publisher","unstructured":"Dal Lago, U., Sangiorgi, D., Alberti, M.: On coinductive equivalences for higher-order probabilistic functional programs. In: The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL \u201914. pp. 297\u2013308. ACM (2014). https:\/\/doi.org\/10.1145\/2535838.2535872","DOI":"10.1145\/2535838.2535872"},{"key":"8_CR9","doi-asserted-by":"publisher","unstructured":"Dal Lago, U., Zorzi, M.: Probabilistic operational semantics for the lambda calculus. RAIRO - Theoretical Informatics and Applications 46(3), 413\u2013450 (2012). https:\/\/doi.org\/10.1051\/ita\/2012012","DOI":"10.1051\/ita\/2012012"},{"key":"8_CR10","doi-asserted-by":"publisher","unstructured":"Danos, V., Ehrhard, T.: Probabilistic coherence spaces as a model of higher-order probabilistic computation. Information and Computation 209(6), 966\u2013991 (2011). https:\/\/doi.org\/10.1016\/j.ic.2011.02.001","DOI":"10.1016\/j.ic.2011.02.001"},{"key":"8_CR11","doi-asserted-by":"publisher","unstructured":"de\u2019Liguoro, U., Piperno, A.: Non deterministic extensions of untyped lambda-calculus. Information and Computation 122(2), 149\u2013177 (1995). https:\/\/doi.org\/10.1006\/inco.1995.1145","DOI":"10.1006\/inco.1995.1145"},{"key":"8_CR12","doi-asserted-by":"publisher","unstructured":"Dershowitz, N.: Orderings for term-rewriting systems. Theoretical Computer Science 17, 279\u2013301 (1982). https:\/\/doi.org\/10.1016\/0304-3975(82)90026-3","DOI":"10.1016\/0304-3975(82)90026-3"},{"key":"8_CR13","doi-asserted-by":"publisher","unstructured":"Ehrhard, T., Pagani, M., Tasson, C.: Full abstraction for probabilistic PCF. Journal of the ACM 65(4), 23:1\u201323:44 (2018). https:\/\/doi.org\/10.1145\/3164540","DOI":"10.1145\/3164540"},{"key":"8_CR14","doi-asserted-by":"publisher","unstructured":"Ehrhard, T., Tasson, C.: Probabilistic call by push value. Logical Methods in Computer Science 15(1) (2019). https:\/\/doi.org\/10.23638\/LMCS-15(1:3)2019","DOI":"10.23638\/LMCS-15(1:3)2019"},{"key":"8_CR15","doi-asserted-by":"publisher","unstructured":"Faggian, C., Ronchi Della Rocca, S.: Lambda calculus and probabilistic computation. In: 34th Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2019. pp. 1\u201313. IEEE Computer Society (2019). https:\/\/doi.org\/10.1109\/LICS.2019.8785699","DOI":"10.1109\/LICS.2019.8785699"},{"key":"8_CR16","doi-asserted-by":"publisher","unstructured":"Goubault-Larrecq, J.: A probabilistic and non-deterministic call-by-push-value language. In: 34th Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2019. pp. 1\u201313. IEEE Computer Society (2019). https:\/\/doi.org\/10.1109\/LICS.2019.8785809","DOI":"10.1109\/LICS.2019.8785809"},{"key":"8_CR17","doi-asserted-by":"publisher","unstructured":"Jones, C., Plotkin, G.D.: A probabilistic powerdomain of evaluations. In: Proceedings of the Fourth Annual Symposium on Logic in Computer Science (LICS \u201989). pp. 186\u2013195. IEEE Computer Society (1989). https:\/\/doi.org\/10.1109\/LICS.1989.39173","DOI":"10.1109\/LICS.1989.39173"},{"key":"8_CR18","doi-asserted-by":"publisher","unstructured":"Jung, A., Tix, R.: The troublesome probabilistic powerdomain. Electronic Notes in Theoretical Computer Science 13, 70\u201391 (1998). https:\/\/doi.org\/10.1016\/S1571-0661(05)80216-6","DOI":"10.1016\/S1571-0661(05)80216-6"},{"key":"8_CR19","doi-asserted-by":"publisher","unstructured":"Leventis, T.: Probabilistic B\u00f6hm trees and probabilistic separation. In: Proceedings of the 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2018. pp. 649\u2013658. IEEE Computer Society (2018). https:\/\/doi.org\/10.1145\/3209108.3209126","DOI":"10.1145\/3209108.3209126"},{"key":"8_CR20","doi-asserted-by":"publisher","unstructured":"Leventis, T.: A deterministic rewrite system for the probabilistic $$\\lambda $$-calculus. Mathematical Structures in Computer Science 29(10), 1479\u20131512 (2019). https:\/\/doi.org\/10.1017\/S0960129519000045","DOI":"10.1017\/S0960129519000045"},{"key":"8_CR21","unstructured":"Loader, R.: Notes on simply typed lambda calculus. Reports of the laboratory for foundations of computer science ECS-LFCS-98-381, University of Edinburgh, Edinburgh (1998), http:\/\/www.lfcs.inf.ed.ac.uk\/reports\/98\/ECS-LFCS-98-381\/"},{"key":"8_CR22","doi-asserted-by":"publisher","unstructured":"Manber, U., Tompa, M.: Probabilistic, nondeterministic, and alternating decision trees. In: 14th Annual ACM Symposium on Theory of Computing. pp. 234\u2013244 (1982). https:\/\/doi.org\/10.1145\/800070.802197","DOI":"10.1145\/800070.802197"},{"key":"8_CR23","doi-asserted-by":"publisher","unstructured":"Ramsey, N., Pfeffer, A.: Stochastic lambda calculus and monads of probability distributions. In: Conference Record of POPL 2002: The 29th SIGPLAN-SIGACT Symposium on Principles of Programming Languages. pp. 154\u2013165. POPL \u201902 (2002). https:\/\/doi.org\/10.1145\/503272.503288","DOI":"10.1145\/503272.503288"},{"key":"8_CR24","doi-asserted-by":"publisher","unstructured":"Saheb-Djahromi, N.: Probabilistic LCF. In: Mathematical Foundations of Computer Science 1978, Proceedings, 7th Symposium. Lecture Notes in Computer Science, vol. 64, pp. 442\u2013451. Springer (1978). https:\/\/doi.org\/10.1007\/3-540-08921-7_92","DOI":"10.1007\/3-540-08921-7_92"},{"key":"8_CR25","doi-asserted-by":"publisher","unstructured":"Sangiorgi, D., Vignudelli, V.: Environmental bisimulations for probabilistic higher-order languages. In: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016. pp. 595\u2013607 (2016). https:\/\/doi.org\/10.1145\/2837614.2837651","DOI":"10.1145\/2837614.2837651"},{"key":"8_CR26","doi-asserted-by":"publisher","unstructured":"Takahashi, M.: Parallel reductions in lambda-calculus. Information and Computation 118(1), 120\u2013127 (1995). https:\/\/doi.org\/10.1006\/inco.1995.1057","DOI":"10.1006\/inco.1995.1057"},{"key":"8_CR27","doi-asserted-by":"publisher","unstructured":"Zantema, H., van de Pol, J.: A rewriting approach to binary decision diagrams. The Journal of Logic and Algebraic Programming 49(1\u20132), 61\u201386 (2001). https:\/\/doi.org\/10.1016\/S1567-8326(01)00013-3","DOI":"10.1016\/S1567-8326(01)00013-3"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-45231-5_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,1,7]],"date-time":"2021-01-07T08:24:12Z","timestamp":1610007852000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-45231-5_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030452308","9783030452315"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-45231-5_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"17 April 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FoSSaCS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Foundations of Software Science and Computation Structures","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Dublin","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Ireland","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 April 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 April 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fossacs2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.etaps.org\/2020\/fossacs","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"98","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"31","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"32% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"12","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference could not take place due to the COVID-19 pandemic. There was an online event on July 2, 2020.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}