Abstract
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.
Chapter PDF
Similar content being viewed by others
References
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–13. IEEE Computer Society (2019). https://doi.org/10.1109/LICS.2019.8785725
Barendregt, H.P.: The Lambda Calculus – Its Syntax and Semantics, Studies in logic and the foundations of mathematics, vol. 103. North-Holland (1984)
Borgström, 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–46. ACM (2016). https://doi.org/10.1145/2951913.2951942
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–8:13. ACM (2018). https://doi.org/10.1145/3236950.3236968
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–845. ACM (2017). https://doi.org/10.1145/3009837
Dal Lago, U., Grellois, C.: Probabilistic termination by monadic affine sized typing. ACM Transactions on Programming Languages and Systems 41(2), 10:1–10:65 (2019). https://doi.org/10.1145/3293605
Dal Lago, U., Guerrieri, G., Heijltjes, W.: Decomposing probabilistic lambda-calculi (long version) (2020), https://arxiv.org/abs/2002.08392
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 ’14. pp. 297–308. ACM (2014). https://doi.org/10.1145/2535838.2535872
Dal Lago, U., Zorzi, M.: Probabilistic operational semantics for the lambda calculus. RAIRO - Theoretical Informatics and Applications 46(3), 413–450 (2012). https://doi.org/10.1051/ita/2012012
Danos, V., Ehrhard, T.: Probabilistic coherence spaces as a model of higher-order probabilistic computation. Information and Computation 209(6), 966–991 (2011). https://doi.org/10.1016/j.ic.2011.02.001
de’Liguoro, U., Piperno, A.: Non deterministic extensions of untyped lambda-calculus. Information and Computation 122(2), 149–177 (1995). https://doi.org/10.1006/inco.1995.1145
Dershowitz, N.: Orderings for term-rewriting systems. Theoretical Computer Science 17, 279–301 (1982). https://doi.org/10.1016/0304-3975(82)90026-3
Ehrhard, T., Pagani, M., Tasson, C.: Full abstraction for probabilistic PCF. Journal of the ACM 65(4), 23:1–23:44 (2018). https://doi.org/10.1145/3164540
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
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–13. IEEE Computer Society (2019). https://doi.org/10.1109/LICS.2019.8785699
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–13. IEEE Computer Society (2019). https://doi.org/10.1109/LICS.2019.8785809
Jones, C., Plotkin, G.D.: A probabilistic powerdomain of evaluations. In: Proceedings of the Fourth Annual Symposium on Logic in Computer Science (LICS ’89). pp. 186–195. IEEE Computer Society (1989). https://doi.org/10.1109/LICS.1989.39173
Jung, A., Tix, R.: The troublesome probabilistic powerdomain. Electronic Notes in Theoretical Computer Science 13, 70–91 (1998). https://doi.org/10.1016/S1571-0661(05)80216-6
Leventis, T.: Probabilistic Böhm trees and probabilistic separation. In: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018. pp. 649–658. IEEE Computer Society (2018). https://doi.org/10.1145/3209108.3209126
Leventis, T.: A deterministic rewrite system for the probabilistic \(\lambda \)-calculus. Mathematical Structures in Computer Science 29(10), 1479–1512 (2019). https://doi.org/10.1017/S0960129519000045
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/
Manber, U., Tompa, M.: Probabilistic, nondeterministic, and alternating decision trees. In: 14th Annual ACM Symposium on Theory of Computing. pp. 234–244 (1982). https://doi.org/10.1145/800070.802197
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–165. POPL ’02 (2002). https://doi.org/10.1145/503272.503288
Saheb-Djahromi, N.: Probabilistic LCF. In: Mathematical Foundations of Computer Science 1978, Proceedings, 7th Symposium. Lecture Notes in Computer Science, vol. 64, pp. 442–451. Springer (1978). https://doi.org/10.1007/3-540-08921-7_92
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–607 (2016). https://doi.org/10.1145/2837614.2837651
Takahashi, M.: Parallel reductions in lambda-calculus. Information and Computation 118(1), 120–127 (1995). https://doi.org/10.1006/inco.1995.1057
Zantema, H., van de Pol, J.: A rewriting approach to binary decision diagrams. The Journal of Logic and Algebraic Programming 49(1–2), 61–86 (2001). https://doi.org/10.1016/S1567-8326(01)00013-3
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
© 2020 The Author(s)
About this paper
Cite this paper
Dal Lago, U., Guerrieri, G., Heijltjes, W. (2020). Decomposing Probabilistic Lambda-Calculi. In: Goubault-Larrecq, J., König, B. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2020. Lecture Notes in Computer Science(), vol 12077. Springer, Cham. https://doi.org/10.1007/978-3-030-45231-5_8
Download citation
DOI: https://doi.org/10.1007/978-3-030-45231-5_8
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-45230-8
Online ISBN: 978-3-030-45231-5
eBook Packages: Mathematics and StatisticsMathematics and Statistics (R0)