Simple Types for Probabilistic Termination

Authors Willem Heijltjes , Georgina Majury



PDF
Thumbnail PDF

File

LIPIcs.CSL.2025.31.pdf
  • Filesize: 0.82 MB
  • 21 pages

Document Identifiers

Author Details

Willem Heijltjes
  • Department of Computer Science, University of Bath, UK
Georgina Majury
  • Department of Computer Science, University of Bath, UK

Acknowledgements

We would like to thank Melissa Antonelli, Ugo Dal Lago, and Paolo Pistone for the constructive conversation about both our approaches, and the anonymous referees for their helpful commentary.

Cite As Get BibTex

Willem Heijltjes and Georgina Majury. Simple Types for Probabilistic Termination. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 31:1-31:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.CSL.2025.31

Abstract

We present a new typing discipline to guarantee the probability of termination in probabilistic lambda-calculi. The main contribution is a particular naturality and simplicity: our probabilistic types are as simple types, but generated from probabilities as base types, representing a least probability of termination. Simple types are recovered by restricting probabilities to one.
Our vehicle is the Probabilistic Event Lambda-Calculus by Dal Lago, Guerrieri, and Heijltjes, which presents a solution to the issue of confluence in probabilistic lambda-calculi. Our probabilistic type system provides an alternative solution to that using counting quantifiers by Antonelli, Dal Lago, and Pistone, for the same calculus.
The problem that both type systems address is to give a lower bound on the probability that terms head-normalize. Following the recent Functional Machine Calculus by Heijltjes, our development takes the (simplified) Krivine machine as primary, and proceeds via an extension of the calculus with sequential composition and identity on the machine. Our type system then gives a natural account of termination probability on the Krivine machine, reflected back onto head-normalization for the original calculus. In this way we are able to avoid the use of counting quantifiers, while improving on the termination bounds given by Antonelli, Dal Lago, and Pistone.

Subject Classification

ACM Subject Classification
  • Theory of computation → Lambda calculus
  • Theory of computation → Type theory
  • Theory of computation → Probabilistic computation
Keywords
  • lambda-calculus
  • probabilistic termination
  • simple types

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads

References

  1. Melissa Antonelli, Ugo Dal Lago, and Paolo Pistone. Curry and howard meet borel. In Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS`22), pages 45:1-45:13. ACM, 2022. URL: https://doi.org/10.1145/3531130.3533361.
  2. Martin Avanzini, Ugo Dal Lago, and Akihisa Yamada. On probabilistic term rewriting. In John P. Gallagher and Martin Sulzmann, editors, Proc. Functional and Logic Programming - 14th International Symposium, FLOPS 2018, volume 10818 of Lecture Notes in Computer Science, pages 132-148. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-90686-7_9.
  3. Chris Barrett, Willem Heijltjes, and Guy McCusker. The Functional Machine Calculus II: Semantics. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023), volume 252 of Leibniz International Proceedings in Informatics (LIPIcs), pages 10:1-10:18, 2023. URL: https://doi.org/10.4230/LIPIcs.CSL.2023.10.
  4. Raven Beutner and Luke Ong. On probabilistic termination of functional programs with continuous distributions. In Stephen N. Freund and Eran Yahav, editors, Proceedings 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI), pages 1312-1326. ACM, 2021. URL: https://doi.org/10.1145/3453483.3454111.
  5. Flavien Breuvart and Ugo Dal Lago. On intersection types and probabilistic lambda calculi. In roceedings of the 20th International Symposium on Principles and Practice of Declarative Programming, PPDP 2018, pages 8:1-8:13. ACM, 2018. URL: https://doi.org/10.1145/3236950.3236968.
  6. Fredrik Dahlqvist and Dexter Kozen. Semantics of higher-order probabilistic programs with conditioning. Proceedings of the ACM on Programming Languages, 4(POPL):57:1-57:29, 2020. URL: https://doi.org/10.1145/3371125.
  7. Ugo Dal Lago, Claudia Faggian, and Simona Ronchi Della Rocca. Intersection types and (positive) almost-sure termination. Proceedings of the ACM on Programming Languages, 5(POPL):1-32, 2021. URL: https://doi.org/10.1145/3434313.
  8. Ugo Dal Lago and Charles Grellois. Probabilistic termination by monadic affine sized typing. ACM Transactions on Programming Languages and Systems, 41(2):10:1-10:65, 2019. URL: https://doi.org/10.1145/3293605.
  9. Ugo Dal Lago, Giulio Guerrieri, and Willem Heijltjes. Decomposing probabilistic lambda-calculi. In Proceedings of Foundations of Software Science and Computation Structures (FoSSaCS), volume 12077 of LNCS, pages 136-156, 2020. URL: https://doi.org/10.1007/978-3-030-45231-5_8.
  10. Ugo Dal Lago and Margherita Zorzi. Probabilistic operational semantics for the lambda calculus. RAIRO - Theoretical Informatics and Applications, 46(3):413-450, 2012. URL: https://doi.org/10.1051/ita/2012012.
  11. Karel de Leeuw, Edward F. Moore, Claude E. Shannon, and Norman Shapiro. Computability by probabilistic machines. Automata studies, 34:183-198, 1956. Google Scholar
  12. Ugo De'Liguoro and Adolfo Piperno. Non deterministic extensions of untyped lambda-calculus. Information and Computation, 122(2):149-177, 1995. URL: https://doi.org/10.1006/inco.1995.1145.
  13. Rémi Douence and Pascal Fradet. A systematic study of functional language implementations. ACM Transactions on Programming Languages and Systems, 20(2):344-387, 1998. URL: https://doi.org/10.1145/276393.276397.
  14. Thomas Ehrhard and Giulio Guerrieri. The bang calculus: An untyped lambda-calculus generalizing call-by-name and call-by-value. In Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming (PPDP'16), pages 174-187, 2016. URL: https://doi.org/10.1145/2967973.2968608.
  15. Thomas Ehrhard and Christine Tasson. Probabilistic call by push value. Logical Methods in Computer Science, 15(1), 2019. URL: https://doi.org/10.23638/LMCS-15(1:3)2019.
  16. Claudia Faggian and Simona Ronchi Della Rocca. Lambda calculus and probabilistic computation. In 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019, pages 1-13, 2019. URL: https://doi.org/10.1109/LICS.2019.8785699.
  17. Jean Goubault-Larrecq. A probabilistic and non-deterministic call-by-push-value language. In 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019, pages 1-13. IEEE Computer Society, 2019. URL: https://doi.org/10.1109/LICS.2019.8785809.
  18. Willem Heijltjes. The functional machine calculus. In Proceedings of the 38th Conference on the Mathematical Foundations of Programming Semantics, MFPS XXXVIII, volume 1 of ENTICS, 2022. URL: https://doi.org/10.46298/ENTICS.10513.
  19. C. Jones and G. D. Plotkin. A probabilistic powerdomain of evaluations. In Proceedings of the Fourth Annual Symposium on Logic in Computer Science (LICS '89), pages 186-195. IEEE Computer Society, 1989. URL: https://doi.org/10.1109/LICS.1989.39173.
  20. Achim Jung and Regina Tix. The troublesome probabilistic powerdomain. Electronic Notes in Theoretical Computer Science, 13:70-91, 1998. URL: https://doi.org/10.1016/S1571-0661(05)80216-6.
  21. Benjamin Kaminski. Advanced Weakest Precondition Calculi for Probabilistic Programs. PhD thesis, Fakultät für Mathematik, Informatik und Naturwissenschaften, RWTH Aachen University, 2019. URL: https://doi.org/10.18154/RWTH-2019-01829.
  22. Naoki Kobayashi, Ugo Dal Lago, and Charles Grellois. On the termination problem for probabilistic higher-order recursive programs. In Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019, pages 1-14. IEEE, 2019. URL: https://doi.org/10.1109/LICS.2019.8785679.
  23. Jean-Louis Krivine. A call-by-name lambda-calculus machine. Higher-Order and Symbolic Computation, 20(3):199-207, 2007. URL: https://doi.org/10.1007/s10990-007-9018-9.
  24. Thomas Leventis. A deterministic rewrite system for the probabilistic λ-calculus. Mathematical Structures in Computer Science, 29(10):1479-1512, 2019. URL: https://doi.org/10.1017/S0960129519000045.
  25. Paul Blain Levy. Call-by-push-value: A functional/imperative synthesis, volume 2 of Semantic Structures in Computation. Springer Netherlands, 2003. URL: https://doi.org/10.1007/978-94-007-0954-6.
  26. Udi Manber and Martin Tompa. Probabilistic, nondeterministic, and alternating decision trees. In 14th Annual ACM Symposium on Theory of Computing, pages 234-244, 1982. URL: https://doi.org/10.1145/800070.802197.
  27. Annabelle McIver and Carroll Morgan. Abstraction and refinement in probabilistic systems. SIGMETRICS Perform. Eval. Rev., 32(4):41-47, March 2005. URL: https://doi.org/10.1145/1059816.1059824.
  28. A.J. Power and Hayo Thielecke. Closed Freyd- and κ-categories. In International Colloquium on Automata, Languages, and Programming (ICALP), volume 1644 of Lecture Notes in Computer Science, pages 625-634. Springer, 1999. URL: https://doi.org/10.1007/3-540-48523-6_59.
  29. Norman Ramsey and Avi Pfeffer. Stochastic lambda calculus and monads of probability distributions. In Conference Record of POPL 2002: The 29th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '02, pages 154-165, 2002. URL: https://doi.org/10.1145/503272.503288.
  30. Nasser Saheb-Djahromi. Probabilistic LCF. In Mathematical Foundations of Computer Science 1978, Proceedings, 7th Symposium, volume 64 of Lecture Notes in Computer Science, pages 442-451. Springer, 1978. URL: https://doi.org/10.1007/3-540-08921-7_92.
  31. Davide Sangiorgi and Valeria Vignudelli. Environmental bisimulations for probabilistic higher-order languages. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, pages 595-607, 2016. URL: https://doi.org/10.1145/2837614.2837651.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail