Document Open Access Logo

Interpreting Lambda Calculus in Domain-Valued Random Variables

Authors Robert Furber , Radu Mardare , Prakash Panangaden , Dana Scott

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2026.48.pdf
  • Filesize: 0.83 MB
  • 20 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation
  • Theory of computation → Probabilistic computation
  • Theory of computation → Lambda calculus
  • Theory of computation → Denotational semantics
Keywords
  • lambda calculus
  • domain theory
  • random variables

Metrics

Abstract

We develop Boolean-valued domain theory and show how the lambda-calculus can be interpreted using domain-valued random variables. We focus on the reflexive domain construction rather than the language and its semantics. We develop the Boolean-valued set theory needed from scratch and then develop Boolean-valued domain theory on top of that. The notions of equality and partial order have to be given Boolean-valued interpretations; when we say that an equation is valid in the model we mean that its interpretation is the top element of the Boolean algebra.

Cite As Get BibTex

Robert Furber, Radu Mardare, Prakash Panangaden, and Dana Scott. Interpreting Lambda Calculus in Domain-Valued Random Variables. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 48:1-48:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.CSL.2026.48

Author Details

Robert Furber
  • Heriot-Watt University, Edinburgh, UK
Radu Mardare
  • Heriot-Watt University, Edinburgh, UK
Prakash Panangaden
  • McGill University, Montreal, Canada
Dana Scott
  • Carnegie Mellon University, Pittsburgh, PA, USA

References

  1. Nathanael L. Ackerman, Cameron E. Freer, and Daniel M. Roy. Noncomputable conditional distributions. In Logic in Computer Science (LICS), 2011 26th Annual IEEE Symposium on, pages 107-116. IEEE, 2011. URL: https://doi.org/10.1109/LICS.2011.49.
  2. Nathanael L. Ackerman, Cameron E. Freer, and Daniel M. Roy. On the computability of conditional probability. J. ACM, 66(3):23:1-23:40, 2019. URL: https://doi.org/10.1145/3321699.
  3. Giorgio Bacci, Robert Furber, Dexter Kozen, Radu Mardare, Prakash Panangaden, and Dana Scott. Boolean-valued semantics for the stochastic λ-calculus. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, pages 669-678. ACM, 2018. URL: https://doi.org/10.1145/3209108.3209175.
  4. Henk P. Barendregt. The Lambda Calculus: Its Syntax and Semantics. North-Holland, Amsterdam, 1984. Google Scholar
  5. John L. Bell. Set Theory: Boolean-Valued Models and Independence Proofs, volume 47 of Oxford Logic Guides. Oxford University Press, third edition, 2005. Google Scholar
  6. Johannes Borgström, Ugo Dal Lago, Andrew D. Gordon, and Marcin Szymczak. A lambda-calculus foundation for universal probabilistic programming. In Jacques Garrigue, Gabriele Keller, and Eijiro Sumii, editors, Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, Nara, Japan, September 18-22, 2016, pages 33-46. ACM, 2016. URL: https://doi.org/10.1145/2951913.2951942.
  7. Fredrik Dahlqvist and Dexter Kozen. Semantics of higher-order probabilistic programs with conditioning. Proc. ACM Program. Lang., 4(POPL):57:1-57:29, 2020. URL: https://doi.org/10.1145/3371125.
  8. Pedro H. Azevedo de Amorim, Dexter Kozen, Radu Mardare, Prakash Panangaden, and Michael Roberts. Universal semantics for the stochastic λ-calculus. In Proceedings of the ACM-IEEE Symposium on Logic in Computer Science, 2021. arXiv preprint:2011.13171. Google Scholar
  9. Thomas Ehrhard, Michele Pagani, and Christine Tasson. Measurable cones and stable, measurable functions: a model for probabilistic higher-order programming. Proceedings of the ACM Symposium on Principles of Programming Languages, 2(POPL):1-28, 2017. URL: https://doi.org/10.1145/3158147.
  10. Thomas Ehrhard, Christine Tasson, and Michele Pagani. Probabilistic coherence spaces are fully abstract for probabilistic pcf. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 309-320, 2014. URL: https://doi.org/10.1145/2535838.2535865.
  11. Erwin Engeler. Algebras and Combinators. Algebra Universalis, 13(1):389-392, December 1981. URL: https://doi.org/10.1007/BF02483849.
  12. Michael P. Fourman and Dana S. Scott. Sheaves and Logic. In Michael Fourman, Christopher Mulvey, and Dana Scott, editors, Applications of Sheaves: Proceedings of the Research Symposium on Applications of Sheaf Theory to Logic, Algebra, and Analysis, Durham, July 9-21, 1977, pages 302-401. Springer Berlin Heidelberg, 1979. URL: https://doi.org/10.1007/BFb0061824.
  13. David H. Fremlin. Measure Theory, Volume 3. https://www.essex.ac.uk/maths/people/fremlin/mt.htm, 2002.
  14. Gerhard Gierz, Karl H. Hofmann, Klaus Keimel, Jimmie D. Lawson, Michael W. Mislove, and Dana S. Scott. Continuous Lattices and Domains, volume 93 of Encyclopedia of Mathematics and its Applications. Cambridge University Press, 2003. Google Scholar
  15. Robert Goldblatt. Topoi: The Categorial Analysis of Logic. Dover, 2006. Google Scholar
  16. Noah Goodman, Vikash Mansingkha, Daniel Roy, Keith Bonawitz, and Joshua Tenenbaum. Church: a language for generative models. In Proceedings of the 24th Conference on Uncertainty in Artificial Intelligence, pages 220-229, 2008. Google Scholar
  17. Chris Heunen, Ohad Kammar, Sam Staton, and Hongseok Yang. A convenient category for higher-order probability theory. In Proceedings of the Thirty-second Annual ACM-IEEE Symposium on Logic in Computer Science, pages 1-12, 2017. URL: https://doi.org/10.1109/LICS.2017.8005137.
  18. Martin Hyland, Misao Nagayama, John Power, and Giuseppe Rosolini. A Category Theoretic Formulation for Engeler-style Models of the Untyped λ-Calculus. Electronic Notes in Theoretical Computer Science, 161:43-57, 2006. Proceedings of the Third Irish Conference on the Mathematical Foundations of Computer Science and Information Technology (MFCSIT 2004). URL: https://doi.org/10.1016/j.entcs.2006.04.024.
  19. Thomas J. Jech. Set Theory. Springer, 3rd Millennium edition, 2003. Google Scholar
  20. Stephen C. Kleene and Emil L. Post. The Upper Semi-Lattice of Degrees of Recursive Unsolvability. Annals of Mathematics, 59(3):379-407, 1954. URL: https://doi.org/10.2307/1969708.
  21. Anatoly G. Kusraev and Semën S. Kutateladze. Boolean Valued Analysis, volume 494 of Mathematics and Its Applications. Springer, 1999. URL: https://doi.org/10.1007/978-94-011-4443-8.
  22. Radu Mardare, Prakash Panangaden, and Gordon Plotkin. Quantitative algebraic reasoning. In Proceedings of the 31st Annual ACM-IEEE Symposium on Logic in Computer Science, pages 700-709, 2016. URL: https://doi.org/10.1145/2933575.2934518.
  23. Gordon P. Monro. A Category-theoretic Approach to Boolean-valued Models of Set Theory. Journal of Pure and Applied Algebra, 42(3):245-274, 1986. URL: https://doi.org/10.1016/0022-4049(86)90010-1.
  24. Gordon P. Monro. Quasitopoi, Logic and Heyting-valued Models. Journal of Pure and Applied Algebra, 42(2):141-164, 1986. URL: https://doi.org/10.1016/0022-4049(86)90077-0.
  25. Dan Roy. Computability, inference and modeling in probabilistic programming. PhD thesis, MIT, June 2011. Google Scholar
  26. Dana Scott. A proof of the independence of the continuum hypothesis. Mathematical Systems Theory, 1(2):89-111, 1967. URL: https://doi.org/10.1007/BF01705520.
  27. Dana Scott. Continuous Lattices. In F. William Lawvere, editor, Toposes, Algebraic Geometry and Logic, pages 97-136. Springer Berlin Heidelberg, 1972. URL: https://doi.org/10.1007/BFb0073967.
  28. Dana Scott. Stochastic λ-calculi. Journal of Applied Logic, 12(3):369-376, 2014. Google Scholar
  29. Robert I. Soare. Recursively Enumerable Sets and Degrees. Perspectives in Mathematical Logic. Springer, 1987. Google Scholar
  30. Clifford Spector. Measure-Theoretic Construction of Incomparable Hyperdegrees. Journal of Symbolic Logic, 23(3):280-288, September 1958. URL: https://doi.org/10.2307/2964288.
  31. Sam Staton, Hongseok Yang, Frank Wood, Chris Heunen, and Ohad Kammar. Semantics for probabilistic programming: higher-order functions, continuous distributions, and soft constraints. In Proceedings of the 31st Annual ACM-IEEE Symposium On Logic In Computer Science, pages 525-534, 2017. Google Scholar
  32. Matthijs Vákár, Ohad Kammar, and Sam Staton. A domain theory for statistical probabilistic programming. Proceedings of the ACM Conference on Principles of Programming Languages, 3(POPL):1-29, 2019. URL: https://doi.org/10.1145/3290349.
  33. Frank Wood, Jan Willem van de Meent, and Vikash Mansinghka. A new approach to probabilistic programming inference. In Proceedings of the 17th International conference on Artificial Intelligence and Statistics, pages 1024-1032, 2014. URL: http://proceedings.mlr.press/v33/wood14.html.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact