Document Open Access Logo

Böhm and Taylor for All!

Authors Aloÿs Dufour, Damiano Mazza

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2024.29.pdf
  • Filesize: 0.74 MB
  • 20 pages

Document Identifiers

Author Details

Aloÿs Dufour
  • Université Sorbonne Paris Nord, LIPN, CNRS, Villetaneuse, France
Damiano Mazza
  • CNRS, LIPN, Université Sorbonne Paris Nord, Villetaneuse, France

Acknowledgements

The authors wish to thank Michele Pagani, who pointed out Lemma 23.

Cite AsGet BibTex

Aloÿs Dufour and Damiano Mazza. Böhm and Taylor for All!. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 29:1-29:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.FSCD.2024.29

Abstract

Böhm approximations, used in the definition of Böhm trees, are a staple of the semantics of the lambda-calculus. Introduced more recently by Ehrhard and Regnier, Taylor approximations provide a quantitative account of the behavior of programs and are well-known to be connected to intersection types. The key relation between these two notions of approximations is a commutation theorem, roughly stating that Taylor approximations of Böhm trees are the same as Böhm trees of Taylor approximations. Böhm and Taylor approximations are available for several variants or extensions of the lambda-calculus and, in some cases, commutation theorems are known. In this paper, we define Böhm and Taylor approximations and prove the commutation theorem in a very general setting. We also introduce (non-idempotent) intersection types at this level of generality. From this, we show how the commutation theorem and intersection types may be applied to any calculus embedding in a sufficiently nice way into our general calculus. All known Böhm-Taylor commutation theorems, as well as new ones, follow by this uniform construction.

Subject Classification

ACM Subject Classification
  • Theory of computation → Linear logic
  • Theory of computation → Denotational semantics
  • Theory of computation → Operational semantics
  • Theory of computation → Lambda calculus
  • Theory of computation → Process calculi
Keywords
  • Linear logic
  • Differential linear logic
  • Taylor expansion of lambda-terms
  • Böhm trees
  • Process calculi

Metrics

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

References

  1. Beniamino Accattoli. Exponentials as substitutions and the cost of cut elimination in linear logic. Log. Methods Comput. Sci., 19(4), 2023. Google Scholar
  2. Davide Barbarossa. Resource approximation for the λμ-calculus. In Proceedings of LICS, pages 27:1-27:12, 2022. Google Scholar
  3. Davide Barbarossa and Giulio Manzonetto. Taylor subsumes Scott, Berry, Kahn and Plotkin. Proc. ACM Program. Lang., 4(POPL):1:1-1:23, 2020. Google Scholar
  4. 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. Elsevier, 1977. Google Scholar
  5. Henk 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. Henk Barendregt, Mario Coppo, and Mariangiola Dezani-Ciancaglini. A filter lambda model and the completeness of type assignment. J. Symb. Log., 48(4):931-940, 1983. Google Scholar
  7. Gérard Boudol. The lambda-calculus with multiplicities (abstract). In Proceedings of CONCUR, volume 715 of Lecture Notes in Computer Science, pages 1-6. Springer, 1993. Google Scholar
  8. Antonio Bucciarelli, Delia Kesner, Alejandro Ríos, and Andrés Viso. The bang calculus revisited. Inf. Comput., 293:105047, 2023. Google Scholar
  9. Alberto Carraro, Thomas Ehrhard, and Antonino Salibra. The stack calculus. In Proceedings of LSFA, volume 113 of EPTCS, pages 93-108, 2012. Google Scholar
  10. Jules Chouquet and Christine Tasson. Taylor expansion for call-by-push-value. In Proceedings of CSL, volume 152 of LIPIcs, pages 16:1-16:16, 2020. Google Scholar
  11. Mario Coppo and Mariangiola Dezani-Ciancaglini. An extension of the basic functionality theory for the λ-calculus. Notre Dame J. Formal Log., 21(4):685-693, 1980. Google Scholar
  12. Ugo Dal Lago, Marc de Visme, Damiano Mazza, and Akira Yoshimizu. Intersection types and runtime errors in the pi-calculus. Proceedings of the ACM on Programming Languages, 3(POPL:7), 2019. Google Scholar
  13. Vincent Danos and Laurent Regnier. The structure of multiplicatives. Arch. Math. Log., 28(3):181-203, 1989. Google Scholar
  14. Daniel de Carvalho. Sémantiques de la logique linéaire et temps de calcul. Ph.D. thesis, Université de la Méditerranée-Aix-Marseille 2, 2007. Google Scholar
  15. Daniel de Carvalho. Execution time of λ-terms via denotational semantics and intersection types. Math. Struct. Comput. Sci., 28(7):1169-1203, 2018. Google Scholar
  16. Thomas Ehrhard. On Köthe sequence spaces and linear logic. Math. Struct. Comput. Sci., 12(5):579-623, 2002. Google Scholar
  17. Thomas Ehrhard. Finiteness spaces. Math. Struct. Comput. Sci., 15(4):615-646, 2005. Google Scholar
  18. Thomas Ehrhard. Collapsing non-idempotent intersection types. In Proceedings of CSL, volume 16 of LIPIcs, pages 259-273, 2012. Google Scholar
  19. Thomas Ehrhard. Call-by-push-value from a linear logic point of view. In Proceedings of ESOP, volume 9632 of Lecture Notes in Computer Science, pages 202-228, 2016. Google Scholar
  20. Thomas Ehrhard. An introduction to differential linear logic: proof-nets, models and antiderivatives. Math. Struct. Comput. Sci., 28(7):995-1060, 2018. Google Scholar
  21. Thomas Ehrhard and Giulio Guerrieri. The bang calculus: an untyped lambda-calculus generalizing call-by-name and call-by-value. In Proceedings of PPDP, pages 174-187, 2016. Google Scholar
  22. Thomas Ehrhard and Olivier Laurent. Acyclic solos and differential interaction nets. Log. Methods Comput. Sci., 6(3), 2010. Google Scholar
  23. Thomas Ehrhard and Laurent Regnier. Böhm trees, Krivine’s machine and the Taylor expansion of lambda-terms. In Proceedings of CiE 2006, volume 3988 of Lecture Notes in Computer Science, pages 186-197, 2006. Google Scholar
  24. Thomas Ehrhard and Laurent Regnier. Differential interaction nets. Theor. Comput. Sci., 364(2):166-195, 2006. Google Scholar
  25. Thomas Ehrhard and Laurent Regnier. Uniformity and the Taylor expansion of ordinary lambda-terms. Theor. Comput. Sci., 403(2-3):347-372, 2008. Google Scholar
  26. Philippa Gardner. Discovering needed reductions using type theory. In Proceedings of TACS, pages 555-574, 1994. Google Scholar
  27. Jean-Yves Girard. Linear logic. Theor. Comput. Sci., 50:1-102, 1987. Google Scholar
  28. Kohei Honda and Olivier Laurent. An exact correspondence between a typed pi-calculus and polarised proof-nets. Theor. Comput. Sci., 411(22-24):2223-2238, 2010. Google Scholar
  29. Axel Kerinec, Giulio Manzonetto, and Michele Pagani. Revisiting call-by-value Böhm trees in light of their Taylor expansion. Log. Methods Comput. Sci., 16(3), 2020. Google Scholar
  30. Paul Blain Levy. Call-By-Push-Value: A Functional/Imperative Synthesis, volume 2 of Semantics Structures in Computation. Springer, 2004. Google Scholar
  31. Damiano Mazza. The true concurrency of differential interaction nets. Math. Struct. Comput. Sci., 28(7):1097-1125, 2018. Google Scholar
  32. Damiano Mazza, Luc Pellissier, and Pierre Vial. Polyadic approximations, fibrations and intersection types. Proceedings of the ACM on Programming Languages, 2(POPL:6), 2018. Google Scholar
  33. Michele Pagani and Paolo Tranquilli. The conservation theorem for differential nets. Math. Struct. Comput. Sci., 27(6):939-992, 2017. Google Scholar
  34. Paolo Tranquilli. Confluence of pure differential nets with promotion. In Proceedings of CSL, volume 5771 of Lecture Notes in Computer Science, pages 500-514, 2009. Google Scholar
  35. Takeshi Tsukada, Kazuyuki Asada, and C.-H. Luke Ong. Generalised species of rigid resource terms. In Proceedings of LICS, pages 1-12, 2017. Google Scholar
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
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact