Document Open Access Logo

The Lambda Calculus Is Quantifiable

Authors Valentin Maestracci , Paolo Pistone

PDF HTML 5

Files

Thumbnail PDF
PDF
LIPIcs.CSL.2025.34.pdf
  • Filesize: 0.89 MB
  • 23 pages
HTML5 Logo HTML (experimental)
LIPIcs.CSL.2025.34.html

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Lambda calculus
  • Theory of computation → Program semantics
Keywords
  • Lambda-calculus
  • Scott semantics
  • Partial metric spaces
  • Böhm trees
  • Taylor expansion

Metrics

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

Abstract

In this paper we introduce several quantitative methods for the lambda-calculus based on partial metrics, a well-studied variant of standard metric spaces that have been used to metrize non-Hausdorff topologies, like those arising from Scott domains. First, we study quantitative variants, based on program distances, of sensible equational theories for the λ-calculus, like those arising from Böhm trees and from the contextual preorder. Then, we introduce applicative distances capturing higher-order Scott topologies, including reflexive objects like the D_∞ model. Finally, we provide a quantitative insight on the well-known connection between the Böhm tree of a λ-term and its Taylor expansion, by showing that the latter can be presented as an isometric transformation.

Cite As Get BibTex

Valentin Maestracci and Paolo Pistone. The Lambda Calculus Is Quantifiable. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 34:1-34:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.CSL.2025.34

Author Details

Valentin Maestracci
  • I2M, Université d'Aix-Marseille, France
Paolo Pistone
  • LIP, Université Claude Bernard Lyon 1, France

Funding

  • Pistone, Paolo: Research has been funded by the French project ANR-23-CPJ1-0054-01.

References

  1. Roberto M. Amadio and Pierre-Louis Curien. Domains and Lambda-Calculi. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1998. Google Scholar
  2. Victor Arrial, Giulio Guerrieri, and Delia Kesner. Genericity through stratification. In Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '24, New York, NY, USA, 2024. Association for Computing Machinery. URL: https://doi.org/10.1145/3661814.3662113.
  3. Hassen Aydi, Mujahid Abbas, and Calogero Vetro. Partial Hausdorff metric and Nadler’s fixed point theorem on partial metric spaces. Topology and its Applications, 159(14):3234-3242, 2012. URL: https://doi.org/10.1016/j.topol.2012.06.012.
  4. Davide Barbarossa and Giulio Manzonetto. Taylor subsumes Scott, Berry, Kahn and Plotkin. Proc. ACM Program. Lang., 4(POPL), December 2019. URL: https://doi.org/10.1145/3371069.
  5. Hendrik Pieter Barendregt. The lambda calculus - its syntax and semantics, volume 103 of Studies in logic and the foundations of mathematics. North-Holland, 1985. Google Scholar
  6. Antonio Bucciarelli, Thomas Ehrhard, and Giulio Manzonetto. Not enough points is enough. In Jacques Duparc and Thomas A. Henzinger, editors, Computer Science Logic, pages 298-312, Berlin, Heidelberg, 2007. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-540-74915-8_24.
  7. Antonio Bucciarelli, Delia Kesner, and Daniel Ventura. Non-idempotent intersection types for the lambda-calculus. Logic Journal of the IGPL, 25(4):431-464, 2017. URL: https://doi.org/10.1093/jigpal/jzx018.
  8. Michael Bukatin, Ralph Kopperman, Steve Matthews, and Homeira Pajoohesh. Partial metric spaces. American Mathematical Monthly, 116:708-718, October 2009. URL: http://www.jstor.org/stable/40391197, URL: https://doi.org/10.4169/193009709X460831.
  9. Michael A. Bukatin and Joshua S. Scott. Towards computing distances between programs via Scott domains. In Sergei Adian and Anil Nerode, editors, Logical Foundations of Computer Science, pages 33-43, Berlin, Heidelberg, 1997. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/3-540-63045-7_4.
  10. Maria Manuel Clementino and Dirk Hofmann. Exponentiation in V-categories. Topology and its Applications, 153(16):3113-3128, 2006. Special Issue: Aspects of Contemporary Topology. URL: https://doi.org/10.1016/j.topol.2005.01.038.
  11. Raphaëlle Crubillé and Ugo Dal Lago. Metric Reasoning About Lambda-Terms: The General Case. In Hongseok Yang, editor, Programming Languages and Systems - 26th European Symposium on Programming, ESOP 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, volume 10201 of Lecture Notes in Computer Science, pages 341-367, Berlin, Heidelberg, 2017. Springer. URL: https://doi.org/10.1007/978-3-662-54434-1_13.
  12. Fredrik Dahlqvist and Renato Neves. An Internal Language for Categories Enriched over Generalised Metric Spaces. In Florin Manea and Alex Simpson, editors, 30th EACSL Annual Conference on Computer Science Logic (CSL 2022), volume 216 of Leibniz International Proceedings in Informatics (LIPIcs), pages 16:1-16:18, Dagstuhl, Germany, 2022. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CSL.2022.16.
  13. Ugo Dal Lago and Francesco Gavazzo. Differential logical relations part II: increments and derivatives. In Gennaro Cordasco, Luisa Gargano, and Adele A. Rescigno, editors, Proceedings of the 21st Italian Conference on Theoretical Computer Science, Ischia, Italy, September 14-16, 2020, volume 2756 of CEUR Workshop Proceedings, pages 101-114. CEUR-WS.org, 2020. URL: http://ceur-ws.org/Vol-2756/paper_10.pdf.
  14. Ugo Dal Lago, Francesco Gavazzo, and Akira Yoshimizu. Differential logical relations, part I: the simply-typed case. In 46th International Colloquium on Automata, Languages, and Programming, ICALP 2019, July 9-12, 2019, Patras, Greece, pages 111:1-111:14, 2019. URL: https://doi.org/10.4230/LIPIcs.ICALP.2019.111.
  15. Ugo Dal Lago, Furio Honsell, Marina Lenisa, and Paolo Pistone. On Quantitative Algebraic Higher-Order Theories. In Amy P. Felty, editor, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022), volume 228 of Leibniz International Proceedings in Informatics (LIPIcs), pages 4:1-4:18, Dagstuhl, Germany, 2022. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.FSCD.2022.4.
  16. Ugo Dal Lago, Naohiko Hoshino, and Paolo Pistone. On the Lattice of Program Metrics. In Marco Gaboardi and Femke van Raamsdonk, editors, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023), volume 260 of Leibniz International Proceedings in Informatics (LIPIcs), pages 20:1-20:19, Dagstuhl, Germany, 2023. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.FSCD.2023.20.
  17. Arthur Azevedo de Amorim, Marco Gaboardi, Justin Hsu, Shin-ya Katsumata, and Ikram Cherigui. A semantic account of metric preservation. In Giuseppe Castagna and Andrew D. Gordon, editors, Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, POPL 2017, pages 545-556, New York, NY, USA, 2017. ACM. URL: https://doi.org/10.1145/3009837.3009890.
  18. Thomas Ehrhard and Laurent Regnier. The differential lambda-calculus. Theoretical Computer Science, 309:1-41, 2003. URL: https://doi.org/10.1016/S0304-3975(03)00392-X.
  19. Thomas Ehrhard and Laurent Regnier. Böhm Trees, Krivine’s Machine and the Taylor Expansion of Lambda-Terms. In Arnold Beckmann, Ulrich Berger, Benedikt Löwe, and John V. Tucker, editors, Logical Approaches to Computational Barriers, pages 186-197, Berlin, Heidelberg, 2006. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/11780342_20.
  20. Thomas Ehrhard and Laurent Regnier. Uniformity and the Taylor expansion of ordinary lambda-terms. Theor. Comput. Sci., 403(2-3):347-372, 2008. URL: https://doi.org/10.1016/j.tcs.2008.06.001.
  21. Thomas Erker, Martín Hötzel Escardó, and Klaus Keimel. The way-below relation of function spaces over semantic domains. Topology and its Applications, 89(1):61-74, 1998. Domain Theory. URL: https://doi.org/10.1016/S0166-8641(97)00226-5.
  22. Martín Hötzel Escardó. PCF extended with real numbers. Theor. Comput. Sci., 162(1):79-115, 1996. URL: https://doi.org/10.1016/0304-3975(95)00250-2.
  23. Martín Hötzen Escardó. A metric model of PCF. Unpublished note presented at the Workshop on Realizability Semantics and Applications, June 1999. Available at the author’s webpage., 1999. Google Scholar
  24. M.H. Escardo and R. Heckmann. Topologies on spaces of continuous functions. Topology Proceedings, 26(2):545-564, 2001-2002. Google Scholar
  25. Francesco Gavazzo. Quantitative behavioural reasoning for higher-order effectful programs: Applicative distances. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '18, pages 452-461, New York, NY, USA, 2018. URL: https://doi.org/10.1145/3209108.3209149.
  26. Xun Ge and Shou Lin. Completions of partial metric spaces. Topology and its Applications, 182:16-23, 2015. URL: https://doi.org/10.1016/j.topol.2014.12.013.
  27. Guillaume Geoffroy and Paolo Pistone. A partial metric semantics of higher-order types and approximate program transformations. In Computer Science Logic 2021 (CSL 2021), volume 183 of LIPIcs-Leibniz International Proceedings in Informatics, pages 35:1-35:18, 2021. URL: https://doi.org/10.4230/LIPIcs.CSL.2021.23.
  28. Dirk Hofmann and Isar Stubbe. Topology from enrichment: the curious case of partial metrics. Cahiers de Topologie et Géométrie DIfférentielle Catégorique, LIX, 4:307-353, 2018. Google Scholar
  29. Gunther Jäger and T. M. G. Ahsanullah. Characterization of quantale-valued metric spaces and quantale-valued partial metric spaces by convergence. Applied General Topology, 19(1):129-144, 2018. Google Scholar
  30. Richard Kennaway, Jan Willem Klop, M. Ronan Sleep, and Fer-Jan de Vries. Infinitary lambda calculus. Theor. Comput. Sci., 175(1):93-125, 1997. URL: https://doi.org/10.1016/S0304-3975(96)00171-5.
  31. Giulio Manzonetto. Models and theories of lambda calculus. PhD thesis, Paris Diderot University, France, 2008. URL: https://tel.archives-ouvertes.fr/tel-00715207.
  32. Radu Mardare, Prakash Panangaden, and Gordon Plotkin. Quantitative algebraic reasoning. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2016). IEEE Computer Society, 2016. Google Scholar
  33. Damiano Mazza. Non-linearity as the metric completion of linearity. In Masahito Hasegawa, editor, Typed Lambda Calculi and Applications, pages 3-14, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-642-38946-7_3.
  34. Volodymyr Mykhaylyuk and Vadym Myronyk. Metrizability of partial metric spaces. Topology and its Applications, 308:107949, 2022. URL: https://doi.org/10.1016/j.topol.2021.107949.
  35. S.J. O'Neill. Partial metrics, valuations and domain theory. Annals of the New York Academy of Sciences, 806:304-315, 1996. Google Scholar
  36. Paolo Pistone. On generalized metric spaces for the simply typed lambda-calculus. In 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021, pages 1-14. IEEE, 2021. URL: https://doi.org/10.1109/LICS52264.2021.9470696.
  37. Jason Reed and Benjamin C. Pierce. Distance makes the types grow stronger: a calculus for differential privacy. In Paul Hudak and Stephanie Weirich, editors, Proceeding of the 15th ACM SIGPLAN international conference on Functional programming, ICFP 2010, Baltimore, Maryland, USA, September 27-29, 2010, pages 157-168. ACM, 2010. URL: https://doi.org/10.1145/1863543.1863568.
  38. Salvador Romaguera, Pedro Tirado, and Óscar Valero. Complete partial metric spaces have partially metrizable computational models. Int. J. Comput. Math., 89(3):284-290, 2012. URL: https://doi.org/10.1080/00207160.2011.559229.
  39. M. P. Schellekens. The correspondence between partial metrics and semivaluations. Theoretical Computer Science, 315(1):135-149, May 2004. URL: https://doi.org/10.1016/j.tcs.2003.11.016.
  40. Michel P. Schellekens. A characterization of partial metrizability: domains are quantifiable. Theor. Comput. Sci., 305(1-3):409-432, 2003. Topology in Computer Science. URL: https://doi.org/10.1016/S0304-3975(02)00705-3.
  41. Michael B. Smyth. The constructive maximal point space and partial metrizability. Ann. Pure Appl. Log., 137(1-3):360-379, 2006. URL: https://doi.org/10.1016/j.apal.2005.05.032.
  42. Pawel Waszkiewicz. Distance and measurement in domain theory. Electronic Notes in Theoretical Computer Science, 45, 2001. URL: https://doi.org/10.1016/S1571-0661(04)80975-7.
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