Document Open Access Logo

Approximation Theory for Distant Bang Calculus

Authors Kostia Chardonnet , Jules Chouquet , Axel Kerinec

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2026.11.pdf
  • Filesize: 0.92 MB
  • 20 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Linear logic
  • Theory of computation → Lambda calculus
  • Theory of computation → Operational semantics
Keywords
  • Lambda-calculus
  • Böhm Trees
  • Taylor expansion of lambda-terms

Metrics

Abstract

Approximation semantics capture the observable behaviour of λ-terms. Böhm Trees and Taylor Expansion are its two central paradigms, related by the Commutation Theorem. While these notions are well understood in Call-by-Name (CbN), they have only recently been developed for Call-by-Value (CbV), which motivate the search for a unified approximation framework. The Bang-calculus provides such a framework: it subsumes both CbN and CbV through linear-logic translations and enjoys robust rewriting properties. We develop the approximation semantics of dBang (the Bang-calculus with explicit substitutions and distant reductions) by introducing approximation trees in the Böhm tradition together with Taylor expansion. We establish their fundamental properties, including a commutation theorem. Via translations, our results recover the CbN and CbV cases within a single unifying framework capturing infinitary and resource-sensitive semantics.

Cite As Get BibTex

Kostia Chardonnet, Jules Chouquet, and Axel Kerinec. Approximation Theory for Distant Bang Calculus. In 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 378, pp. 11:1-11:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.FSCD.2026.11

Author Details

Kostia Chardonnet
  • Université de Lorraine, CNRS, Inria, LORIA, F-54000 Nancy, France
Jules Chouquet
  • Université d'Orléans, INSA CVL, LIFO, UR 4022, Orléans, France
Axel Kerinec
  • Université Paris Est Creteil, LACL, F-94010 Créteil, France

Funding

This work is supported by the Plan France 2030 through the PEPR integrated project EPiQ ANR-22-PETQ-0007 and the HQI platform ANR-22-PNCQ-0002; and by the European project MSCA Staff Exchanges Qcomical HORIZON-MSCA-2023-SE-01. The project is also supported by the Maison du Quantique MaQuEst.

References

  1. Beniamino Accattoli. An Abstract Factorization Theorem for Explicit Substitutions. In Ashish Tiwari, editor, 23rd International Conference on Rewriting Techniques and Applications (RTA'12), volume 15 of Leibniz International Proceedings in Informatics (LIPIcs), pages 6-21, Dagstuhl, Germany, 2012. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.RTA.2012.6.
  2. Beniamino Accattoli and Delia Kesner. The structural λ-calculus. In Anuj Dawar and Helmut Veith, editors, Computer Science Logic, pages 381-395, Berlin, Heidelberg, 2010. Springer Berlin Heidelberg. Google Scholar
  3. Beniamino Accattoli and Delia Kesner. Preservation of strong normalisation modulo permutations for the structural lambda-calculus. Logical Methods in Computer Science, Volume 8, Issue 1, March 2012. URL: https://doi.org/10.2168/lmcs-8(1:28)2012.
  4. Roberto Amadio and Pierre-Louis Curien. Domains and Lambda Calculi. CTTCS. CUP, 1998. Google Scholar
  5. Zena Ariola. Relating graph and term rewriting via böhm models. Applicable Algebra in Engineering, Communication and Computing, 7, February 1970. URL: https://doi.org/10.1007/3-540-56868-9_15.
  6. Zena M. Ariola and Stefan Blom. Skew confluence and the lambda calculus with letrec. Annals of Pure and Applied Logic, 117(1):95-168, 2002. URL: https://doi.org/10.1016/S0168-0072(01)00104-X.
  7. Victor Arrial, Giulio Guerrieri, and Delia Kesner. Quantitative inhabitation for different lambda calculi in a unifying framework. Proc. ACM Program. Lang., 7(POPL), 2023. URL: https://doi.org/10.1145/3571244.
  8. Victor Arrial, Giulio Guerrieri, and Delia Kesner. The benefits of diligence. In Christoph Benzmüller, Marijn J. H. Heule, and Renate A. Schmidt, editors, Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3-6, 2024, Proceedings, Part II, volume 14740 of Lecture Notes in Computer Science, pages 338-359. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-63501-4_18.
  9. 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.
  10. 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. URL: https://doi.org/10.1016/S0049-237X(08)71129-7.
  11. Henk Barendregt. The Lambda Calculus: Its Syntax and Semantics, volume 103 of Studies in Logic and the Foundations of Mathematics. North-Holland, Amsterdam, 1984. Google Scholar
  12. Henk Barendregt, Marko Eekelen, John Glauert, Richard Kennaway, Marinus Plasmeijer, and Michael Sleep. Term graph rewriting. In Proceedings of the Parallel Architectures and Languages Europe, pages 141-158, 1987. Google Scholar
  13. Gérard Boudol. Computational semantics of terms rewriting systems. Research Report RR-0192, INRIA, 1983. URL: https://inria.hal.science/inria-00076366.
  14. Antonio Bucciarelli, Delia Kesner, Alejandro Ríos, and Andrés Viso. The bang calculus revisited. Information and Computation, 293:105047, 2023. URL: https://doi.org/10.1016/j.ic.2023.105047.
  15. Alberto Carraro and Giulio Guerrieri. A semantical and operational account of call-by-value solvability. In Anca Muscholl, editor, Foundations of Software Science and Computation Structures, pages 103-118, Berlin, Heidelberg, 2014. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-642-54830-7_7.
  16. Alberto Carraro and Giulio Guerrieri. A semantical and operational account of call-by-value solvability. In Anca Muscholl, editor, Foundations of Software Science and Computation Structures - 17th International Conference, FOSSACS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings, volume 8412 of Lecture Notes in Computer Science, pages 103-118. Springer, 2014. URL: https://doi.org/10.1007/978-3-642-54830-7_7.
  17. Kostia Chardonnet, Jules Chouquet, and Axel Kerinec. Approximation theory for distant bang calculus, 2026. Long version with technical appendix. URL: https://arxiv.org/abs/2601.05199.
  18. 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), volume 299 of Leibniz International Proceedings in Informatics (LIPIcs), pages 29:1-29:20, Dagstuhl, Germany, 2024. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.FSCD.2024.29.
  19. Thomas Ehrhard. Collapsing non-idempotent intersection types. In Patrick Cégielski and Arnaud Durand, editors, Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL, volume 16 of Leibniz International Proceedings in Informatics (LIPIcs), pages 259-273, Dagstuhl, Germany, 2012. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CSL.2012.259.
  20. Thomas Ehrhard. Call-by-push-value from a linear logic point of view. In Peter Thiemann, editor, Programming Languages and Systems, pages 202-228, Berlin, Heidelberg, 2016. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-662-49498-1_9.
  21. 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, New York, NY, USA, 2016. Association for Computing Machinery. URL: https://doi.org/10.1145/2967973.2968608.
  22. Thomas Ehrhard and Laurent Regnier. The differential lambda-calculus. Theoretical Computer Science, 309(1):1-41, 2003. URL: https://doi.org/10.1016/S0304-3975(03)00392-X.
  23. 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.
  24. 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.
  25. Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50(1):1-101, 1987. URL: https://doi.org/10.1016/0304-3975(87)90045-4.
  26. Regnier L Girard J-Y, Lafont Y, editor. Advances in Linear Logic. London Mathematical Society Lecture Note Series. Cambridge University Press, 1995. Google Scholar
  27. Axel Kerinec. A story of lambda-calculus and approximation. Theses, Université Paris-Nord - Paris XIII, June 2023. URL: https://theses.hal.science/tel-04624826.
  28. Axel Kerinec, Giulio Manzonetto, and Michele Pagani. Revisiting call-by-value böhm trees in light of their taylor expansion. Logical Methods in Computer Science, Volume 16, Issue 3, July 2020. URL: https://doi.org/10.23638/LMCS-16(3:6)2020.
  29. Delia Kesner, Victor Arrial, and Giulio Guerrieri. Meaningfulness and Genericity in a Subsuming Framework. In Jakob Rehof, editor, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024), volume 299 of Leibniz International Proceedings in Informatics (LIPIcs), pages 1:1-1:24, Dagstuhl, Germany, 2024. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.FSCD.2024.1.
  30. Jim Laird, Giulio Manzonetto, Guy McCusker, and Michele Pagani. Weighted relational models of typed lambda-calculi. In Proceedings of the 2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '13, pages 301-310, USA, 2013. IEEE Computer Society. URL: https://doi.org/10.1109/LICS.2013.36.
  31. Paul Blain Levy. Call-by-push-value: A subsuming paradigm. In Jean-Yves Girard, editor, Typed Lambda Calculi and Applications, pages 228-243, Berlin, Heidelberg, 1999. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/3-540-48959-2_17.
  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. Lionel Vaux. Normalizing the taylor expansion of non-deterministic λ-terms, via parallel reduction of resource vectors. Log. Methods Comput. Sci., 15(3), 2019. URL: https://doi.org/10.23638/LMCS-15(3:9)2019.
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-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact