Document Open Access Logo

Ohana Trees and Taylor Expansion for the λI-Calculus: No variable gets left behind or forgotten!

Authors Rémy Cerda , Giulio Manzonetto , Alexis Saurin

PDF HTML 5

Files

Thumbnail PDF
PDF
LIPIcs.FSCD.2025.12.pdf
  • Filesize: 1.03 MB
  • 20 pages
HTML5 Logo HTML (experimental)
LIPIcs.FSCD.2025.12.html

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Rewrite systems
  • Theory of computation → Lambda calculus
  • Theory of computation → Denotational semantics
Keywords
  • λ-calculus
  • program approximation
  • Taylor expansion
  • λI-calculus
  • persistent free variables
  • Böhm trees
  • Ohana trees

Metrics

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

Abstract

Although the λI-calculus is a natural fragment of the λ-calculus, obtained by forbidding the erasure, its equational theories did not receive much attention. The reason is that all proper denotational models studied in the literature equate all non-normalizable λI-terms, whence the associated theory is not very informative. The goal of this paper is to introduce a previously unknown theory of the λI-calculus, induced by a notion of evaluation trees that we call "Ohana trees". The Ohana tree of a λI-term is an annotated version of its Böhm tree, remembering all free variables that are hidden within its meaningless subtrees, or pushed into infinity along its infinite branches. 
We develop the associated theories of program approximation: the first approach - more classic - is based on finite trees and continuity, the second adapts Ehrhard and Regnier’s Taylor expansion. We then prove a Commutation Theorem stating that the normal form of the Taylor expansion of a λI-term coincides with the Taylor expansion of its Ohana tree. As a corollary, we obtain that the equality induced by Ohana trees is compatible with abstraction and application. We conclude by discussing the cases of Lévy-Longo and Berarducci trees, and generalizations to the full λ-calculus.

Cite As Get BibTex

Rémy Cerda, Giulio Manzonetto, and Alexis Saurin. Ohana Trees and Taylor Expansion for the λI-Calculus: No variable gets left behind or forgotten!. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 12:1-12:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.FSCD.2025.12

Author Details

Rémy Cerda
  • Université Paris Cité, CNRS, IRIF, F-75013, Paris, France
Giulio Manzonetto
  • Université Paris Cité, CNRS, IRIF, F-75013, Paris, France
Alexis Saurin
  • Université Paris Cité, CNRS, IRIF, F-75013, Paris, France
  • INRIA π³, Paris, France

Funding

  • Cerda, Rémy: Partially funded by the ANR project RECIPROG ANR-21-CE48-019.
  • Saurin, Alexis: Partially funded by the ANR project RECIPROG ANR-21-CE48-019.

Acknowledgements

We wish to thank Thomas Ehrhard, Paul-André Melliès, Lorenzo Tortora de Falco and Lionel Vaux Auclair for interesting discussions. We also thank the anonymous reviewers for the many valuable corrections they suggested.

References

  1. Sandra Alves and Mário Florido. Structural rules and algebraic properties of intersection types. In Helmut Seidl, Zhiming Liu, and Corina S. Pasareanu, editors, Theoretical Aspects of Computing - ICTAC 2022 - 19th International Colloquium, Tbilisi, Georgia, September 27-29, 2022, Proceedings, volume 13572 of Lecture Notes in Computer Science, pages 60-77. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-17715-6_6.
  2. Davide Barbarossa and Giulio Manzonetto. Taylor subsumes Scott, Berry, Kahn and Plotkin. Proceedings of the ACM on Programming Languages, 4(POPL):1-23, 2019. URL: https://doi.org/10.1145/3371069.
  3. Henk Barendregt. The type free lambda calculus. In Jon Barwise, editor, Handbook of Mathematical Logic, volume 90 of Studies in Logic and the Foundations of Mathematics, pages 1091-1132. North-Holland, Amsterdam, 1977. Google Scholar
  4. Henk Barendregt. The lambda calculus - its syntax and semantics, volume 103 of Studies in logic and the foundations of mathematics. North-Holland, 1984. Google Scholar
  5. Henk Barendregt and Giulio Manzonetto. A Lambda Calculus Satellite. College Publications, 2022. URL: https://www.collegepublications.co.uk/logic/mlf/?00035.
  6. Stefano Berardi and Ugo de'Liguoro. Non-monotonic pre-fix points and learning. Fundam. Informaticae, 150(3-4):259-280, 2017. URL: https://doi.org/10.3233/FI-2017-1470.
  7. Alessandro Berarducci. Infinite λ-calculus and non-sensible models. In Marcel Dekker, editor, Logic and Algebra, volume 180, pages 339-377, New York, 1996. Presented to the conference in honour of Roberto Magari, Pontignano 1994. Google Scholar
  8. Flavien Breuvart, Giulio Manzonetto, and Domenico Ruoppolo. Relational graph models at work. Log. Methods Comput. Sci., 14(3), 2018. URL: https://doi.org/10.23638/LMCS-14(3:2)2018.
  9. Alberto Carraro, Thomas Ehrhard, and Antonino Salibra. Exponentials with infinite multiplicities. In Anuj Dawar and Helmut Veith, editors, Computer Science Logic, 24th International Workshop, CSL 2010, 19th Annual Conference of the EACSL, Brno, Czech Republic, August 23-27, 2010. Proceedings, volume 6247 of Lecture Notes in Computer Science, pages 170-184. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-15205-4_16.
  10. Rémy Cerda. Taylor Approximation and Infinitary λ-Calculi. Phd thesis, Aix-Marseille Université, 2024. URL: https://hal.science/tel-04664728.
  11. Rémy Cerda, Giulio Manzonetto, and Alexis Saurin. Ohana trees and Taylor expansion for the λI-calculus. No variable gets left behind or forgotten!, 2025. Version of this paper with additional proofs in an appendix. URL: https://arxiv.org/abs/2505.06193.
  12. Rémy Cerda and Lionel Vaux Auclair. Finitary simulation of infinitary β-reduction via Taylor expansion, and applications. Logical Methods in Computer Science, 19, 2023. URL: https://doi.org/10.46298/lmcs-19(4:34)2023.
  13. Alonzo Church. The calculi of lambda conversion. Princeton University Press, 1941. Google Scholar
  14. Lukasz Czajka. A new coinductive confluence proof for infinitary lambda calculus. Log. Methods Comput. Sci., 16(1), 2020. URL: https://doi.org/10.23638/LMCS-16(1:31)2020.
  15. Daniel de Carvalho and Lorenzo Tortora de Falco. The relational model is injective for multiplicative exponential linear logic (without weakenings). Ann. Pure Appl. Log., 163(9):1210-1236, 2012. URL: https://doi.org/10.1016/J.APAL.2012.01.004.
  16. Daniel de Carvalho and Lorenzo Tortora de Falco. A semantic account of strong normalization in linear logic. Inf. Comput., 248:104-129, 2016. URL: https://doi.org/10.1016/J.IC.2015.12.010.
  17. Aloÿs Dufour and Damiano Mazza. Böhm and Taylor for all! In Jakob Rehof, editor, 9th International Conference on Formal Structures for Computation and Deduction, FSCD 2024, July 10-13, 2024, Tallinn, Estonia, volume 299 of LIPIcs, pages 29:1-29:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. URL: https://doi.org/10.4230/LIPICS.FSCD.2024.29.
  18. Lavinia Egidi, Furio Honsell, and Simona Ronchi Della Rocca. Operational, denotational and logical descriptions: a case study. Fundam. Informaticae, 16(1):149-169, 1992. Google Scholar
  19. Thomas Ehrhard and Laurent Regnier. The differential lambda-calculus. Theor. Comput. Sci., 309(1-3):1-41, 2003. URL: https://doi.org/10.1016/S0304-3975(03)00392-X.
  20. 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 (CiE 2006), pages 186-197, 2006. URL: https://doi.org/10.1007/11780342_20.
  21. Thomas Ehrhard and Laurent Regnier. Uniformity and the Taylor expansion of ordinary lambda-terms. Theoretical Computer Science, 403(2):347-372, 2008. URL: https://doi.org/10.1016/j.tcs.2008.06.001.
  22. Jörg Endrullis, Dimitri Hendriks, and Jan Willem Klop. Highlights in infinitary rewriting and lambda calculus. Theor. Comput. Sci., 464:48-71, 2012. URL: https://doi.org/10.1016/J.TCS.2012.08.018.
  23. Marcelo Fiore, Gordon Plotkin, and Daniele Turi. Abstract syntax and variable binding. In 14th Symposium on Logic in Computer Science, 1999. URL: https://doi.org/10.1109/lics.1999.782615.
  24. Silvia Ghilezan. Strong normalization and typability with intersection types. Notre Dame J. Formal Log., 37(1):44-52, 1996. URL: https://doi.org/10.1305/NDJFL/1040067315.
  25. Furio Honsell and Marina Lenisa. Some results on the full abstraction problem for restricted lambda calculi. In Andrzej M. Borzyszkowski and Stefan Sokolowski, editors, Mathematical Foundations of Computer Science 1993, 18th International Symposium, MFCS'93, Gdansk, Poland, August 30 - September 3, 1993, Proceedings, volume 711 of Lecture Notes in Computer Science, pages 84-104. Springer, 1993. URL: https://doi.org/10.1007/3-540-57182-5_6.
  26. J. Martin E. Hyland. A syntactic characterization of the equality in some models for the λ-calculus. Journal London Mathematical Society (2), 12(3):361-370, 1975. Google Scholar
  27. Benedetto Intrigila, Giulio Manzonetto, and Andrew Polonsky. Degrees of extensionality in the theory of Böhm trees and Sallé’s conjecture. Log. Methods Comput. Sci., 15(1), 2019. URL: https://doi.org/10.23638/LMCS-15(1:6)2019.
  28. Bart Jacobs. Semantics of lambda-I and of other substructure lambda calculi. In Marc Bezem and Jan Friso Groote, editors, Typed Lambda Calculi and Applications, International Conference on Typed Lambda Calculi and Applications, TLCA '93, Utrecht, The Netherlands, March 16-18, 1993, Proceedings, volume 664 of Lecture Notes in Computer Science, pages 195-208. Springer, 1993. URL: https://doi.org/10.1007/BFB0037107.
  29. Richard Kennaway, Jan Willem Klop, M. Ronan Sleep, and Fer-Jan de Vries. Infinitary lambda calculi and Böhm models. In Jieh Hsiang, editor, Rewriting Techniques and Applications, 6th International Conference, RTA-95, Kaiserslautern, Germany, April 5-7, 1995, Proceedings, volume 914 of Lecture Notes in Computer Science, pages 257-270. Springer, 1995. URL: https://doi.org/10.1007/3-540-59200-8_62.
  30. Jeroen Ketema, Stefan Blom, Takahito Aoto, and Jakob Grue Simonsen. Rewriting Transfinite Terms, pages 129-144. Lulu Press Inc, United States, 2009. Google Scholar
  31. Jean-Jacques Lévy. An algebraic interpretation of the λβK-calculus; and an application of a labelled λ-calculus. Theor. Comput. Sci., 2(1):97-114, 1976. URL: https://doi.org/10.1016/0304-3975(76)90009-8.
  32. Giuseppe Longo. Set-theoretical models of λ-calculus: theories, expansions, isomorphisms. Annals of Pure and Applied Logic, 24(2):153-188, 1983. URL: https://doi.org/10.1016/0168-0072(83)90030-1.
  33. Stefania Lusin and Antonino Salibra. The lattice of lambda theories. J. Log. Comput., 14(3):373-394, 2004. URL: https://doi.org/10.1093/LOGCOM/14.3.373.
  34. Giulio Manzonetto and Michele Pagani. Böhm’s Theorem for resource lambda calculus through Taylor Expansion. In C.-H. Luke Ong, editor, Typed Lambda Calculi and Applications - 10th International Conference, TLCA 2011, Novi Sad, Serbia, June 1-3, 2011. Proceedings, volume 6690 of Lecture Notes in Computer Science, pages 153-168. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-21691-6_14.
  35. Giulio Manzonetto, Andrew Polonsky, Alexis Saurin, and Jakob Grue Simonsen. The fixed point property and a technique to harness double fixed point combinators. J. Log. Comput., 29(5):831-880, 2019. URL: https://doi.org/10.1093/LOGCOM/EXZ013.
  36. Paul-André Melliès. Higher-order parity automata. In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017, pages 1-12. IEEE Computer Society, 2017. URL: https://doi.org/10.1109/LICS.2017.8005077.
  37. James Hiram Morris. Lambda calculus models of programming languages. Phd thesis, Massachusetts Institute of Technology (MIT), 1968. Google Scholar
  38. Federico Olimpieri and Lionel Vaux Auclair. On the Taylor expansion of λ-terms and the groupoid structure of their rigid approximants. Logical Methods in Computer Science, 18, 2022. URL: https://doi.org/10.46298/lmcs-18(1:1)2022.
  39. Michele Pagani and Paolo Tranquilli. Parallel reduction in resource lambda-calculus. In Zhenjiang Hu, editor, Programming Languages and Systems, 7th Asian Symposium, APLAS 2009, Seoul, Korea, December 14-16, 2009. Proceedings, volume 5904 of Lecture Notes in Computer Science, pages 226-242. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-10672-9_17.
  40. Simona Ronchi Della Rocca. Characterization theorems for a filter lambda model. Inf. Control., 54(3):201-216, 1982. URL: https://doi.org/10.1016/S0019-9958(82)80022-3.
  41. Dana S. Scott. Continuous lattices. In Lawvere, editor, Toposes, Algebraic Geometry and Logic, volume 274 of Lecture Notes in Mathematics, pages 97-136. Springer, 1972. Google Scholar
  42. Paula Severi and Fer-Jan de Vries. The infinitary lambda calculus of the infinite η-Böhm trees. Math. Struct. Comput. Sci., 27(5):681-733, 2017. URL: https://doi.org/10.1017/S096012951500033X.
  43. Terese. Term Rewriting Systems, volume 55 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2003. Google Scholar
  44. Steffen van Bakel. Complete restrictions of the intersection type discipline. Theor. Comput. Sci., 102(1):135-163, 1992. URL: https://doi.org/10.1016/0304-3975(92)90297-S.
  45. Steffen van Bakel, Franco Barbanera, Mariangiola Dezani-Ciancaglini, and Fer-Jan de Vries. Intersection types for lambda-trees. Theor. Comput. Sci., 272(1-2):3-40, 2002. URL: https://doi.org/10.1016/S0304-3975(00)00346-7.
  46. Lionel Vaux. Normalizing the Taylor expansion of non-deterministic λ-terms, via parallel reduction of resource vectors. Logical Methods in Computer Science, 15, 2019. URL: https://doi.org/10.23638/LMCS-15(3:9)2019.
  47. Christopher P. Wadsworth. The relation between computational and denotational properties for Scott’s 𝒟_∞-models of the lambda-calculus. SIAM J. Comput., 5(3):488-521, 1976. URL: https://doi.org/10.1137/0205036.
  48. Christopher P. Wadsworth. Approximate reduction and lambda calculus models. SIAM J. Comput., 7(3):337-356, 1978. URL: https://doi.org/10.1137/0207028.
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