Document Open Access Logo

Absolute Convergence and Taylor Expansion in Web Based Models of Linear Logic

Authors Christine Tasson , Aymeric Walch

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2026.29.pdf
  • Filesize: 1.32 MB
  • 23 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Linear logic
  • Theory of computation → Categorical semantics
  • Mathematics of computing → Differential calculus
Keywords
  • Categorical semantics
  • Linear Logic
  • Quantitative semantics
  • Taylor expansion

Metrics

Abstract

We provide in this paper a generic construction of web models of linear logic with partial sums. Our construction captures a wide class of orthogonality models, ranging from coherence spaces to probabilistic coherence spaces, finiteness spaces and Köthe spaces. All these models are built on the same principles, but were very heterogeneous in the specificities of their technical development. Our construction factorizes these specificities, allowing a unified treatment of further developments, such as differentiation and Taylor expansion.
The differential λ-calculus relates quantitative aspects of programs to differentiation and to Taylor expansion in models of linear logic. Recent work has generalized the axioms of Taylor expansion, so that they apply to many models that only feature partial sums. However, that work did not cover Köthe spaces and finiteness spaces. We generalize the theory of Taylor expansion to models in which coefficients can be negative, and we prove that our generic web models always satisfy this new axiomatization. Therefore, all the aforementioned models feature a Taylor expansion.

Cite As Get BibTex

Christine Tasson and Aymeric Walch. Absolute Convergence and Taylor Expansion in Web Based Models of Linear Logic. In 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 378, pp. 29:1-29:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.FSCD.2026.29

Author Details

Christine Tasson
  • Fédération ENAC ISAE-SUPAERO ONERA, Université de Toulouse, France
Aymeric Walch
  • Fédération ENAC ISAE-SUPAERO ONERA, Université de Toulouse, France

Funding

This work has been partly funded by the ANR JCJC project Species, Syntax and Semantics, ANR-20-CE48-0010.

Acknowledgements

We would like to thank Thomas Ehrhard for his helpful advices. Our notion of absolute PCR was created following one of his suggestions. We also thank our reviewers for their numerous and helpful comments.

References

  1. Jon Beck. Distributive laws. In B. Eckmann, editor, Seminar on Triples and Categorical Homology Theory, pages 119-140, Berlin, Heidelberg, 1969. Springer Berlin Heidelberg. Google Scholar
  2. R. Blute, Robin Cockett, and R. Seely. Differential categories. Mathematical Structures in Computer Science, 16:1049-1083, December 2006. URL: https://doi.org/10.1017/S0960129506005676.
  3. R. Blute, Robin Cockett, and R. Seely. Cartesian differential categories. Theory and Applications of Categories, 22:622-672, January 2009. Google Scholar
  4. Richard Blute, Thomas Ehrhard, and Christine Tasson. A convenient differential category. Cah. Topol. Géom. Différ. Catég., 53(3):211-232, 2012. Google Scholar
  5. Antonio Bucciarelli and Thomas Ehrhard. On phase semantics and denotational semantics: the exponentials. Ann. Pure Appl. Log., 109(3):205-241, 2001. URL: https://doi.org/10.1016/S0168-0072(00)00056-7.
  6. Antonio Bucciarelli, Thomas Ehrhard, and Giulio Manzonetto. Categorical models for simply typed resource calculi. Electronic Notes in Theoretical Computer Science, 265:213-230, 2010. Proceedings of the 26th Conference on the Mathematical Foundations of Programming Semantics (MFPS 2010). URL: https://doi.org/10.1016/j.entcs.2010.08.013.
  7. Kenta Cho, Bart Jacobs, Bas Westerbaan, and Abraham Westerbaan. An introduction to effectus theory. arXiv preprint arXiv:1512.05813, 2015. URL: https://arxiv.org/abs/1512.05813.
  8. Robin Cockett and G. Cruttwell. Differential Structure, Tangent Structure, and SDG. Applied Categorical Structures, 22, April 2014. URL: https://doi.org/10.1007/s10485-013-9312-0.
  9. Raphaëlle Crubillé, Thomas Ehrhard, Michele Pagani, and Christine Tasson. The Free Exponential Modality of Probabilistic Coherence Spaces. In Javier Esparza and Andrzej S. Murawski, editors, Foundations of Software Science and Computation Structures - 20th International Conference, FOSSACS 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 10203 of Lecture Notes in Computer Science, pages 20-35, 2017. URL: https://doi.org/10.1007/978-3-662-54458-7_2.
  10. Ugo Dal Lago and Thomas Leventis. On the Taylor Expansion of Probabilistic lambda-terms. In Herman Geuvers, editor, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019), volume 131 of Leibniz International Proceedings in Informatics (LIPIcs), pages 13:1-13:16, Dagstuhl, Germany, 2019. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.FSCD.2019.13.
  11. Vincent Danos and Thomas Ehrhard. Probabilistic coherence spaces as a model of higher-order probabilistic computation. Information and Computation, 209(6):966-991, 2011. URL: https://doi.org/10.1016/j.ic.2011.02.001.
  12. Thomas Ehrhard. On köthe sequence spaces and linear logic. Mathematical Structures in Computer Science, 12, January 2002. URL: https://doi.org/10.1017/S0960129502003729.
  13. Thomas Ehrhard. Finiteness spaces. Mathematical Structures in Computer Science, 15(4):615-646, July 2005. 32 pages. URL: https://doi.org/10.1017/S0960129504004645.
  14. Thomas Ehrhard. Coherent differentiation. Mathematical Structures in Computer Science, pages 1-52, 2023. URL: https://doi.org/10.1017/S0960129523000129.
  15. Thomas Ehrhard and Guillaume Geoffroy. Integration in cones. Logical Methods in Computer Science, Volume 21, Issue 1, January 2025. URL: https://doi.org/10.46298/lmcs-21(1:1)2025.
  16. 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.
  17. 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.
  18. Thomas Ehrhard and Aymeric Walch. Coherent taylor expansion as a bimonad. Mathematical Structures in Computer Science, 35:e9, 2025. URL: https://doi.org/10.1017/S0960129525000040.
  19. Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50(1):1-101, 1987. URL: https://doi.org/10.1016/0304-3975(87)90045-4.
  20. Kazimierz Glazek. A guide to the literature on semirings and their applications in mathematics and information sciences: with complete bibliography. Springer Dordrecht, 2002. URL: https://doi.org/10.1007/978-94-015-9964-1.
  21. Esfandiar Haghverdi. Unique decomposition categories, geometry of interaction and combinatory logic. Mathematical Structures in Computer Science, 10(2):205-230, 2000. URL: https://doi.org/10.1017/S0960129599003035.
  22. Peter Hines. A categorical analogue of the monoid semiring construction. Mathematical Structures in Computer Science, 23(1):55-94, 2013. URL: https://doi.org/10.1017/S0960129512000059.
  23. Martin Hyland and Andrea Schalk. Glueing and orthogonality for models of linear logic. Theoretical Computer Science, 294(1):183-231, 2003. Category Theory and Computer Science. URL: https://doi.org/10.1016/S0304-3975(01)00241-9.
  24. G. M. Kelly and Ross Street. Review of the elements of 2-categories. In Gregory M. Kelly, editor, Category Seminar, pages 75-103, Berlin, Heidelberg, 1974. Springer Berlin Heidelberg. Google Scholar
  25. Marie Kerjean and Jean-Simon Pacaud Lemay. Taylor expansion as a monad in models of DiLL. In 2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1-13, 2023. URL: https://doi.org/10.1109/LICS56636.2023.10175753.
  26. Marie Kerjean and Christine Tasson. Mackey-complete spaces and power series – a topological model of differential linear logic. Mathematical Structures in Computer Science, 28(4):472-507, 2018. URL: https://doi.org/10.1017/S0960129516000281.
  27. Marie Morgane Kerjean and Pierre-Marie Pédrot. δ is for dialectica. 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.3662106.
  28. Anders Kock. Monads on symmetric monoidal closed categories. Archiv der Mathematik, 21:1-10, January 1970. URL: https://doi.org/10.1007/BF01220868.
  29. Anders Kock. Closed categories generated by commutative monads. Journal of the Australian Mathematical Society, 12(4):405-424, 1971. URL: https://doi.org/10.1017/S1446788700010272.
  30. Anders Kock. Strong functors and monoidal monads. Archiv der Mathematik, 23:113-120, December 1972. URL: https://doi.org/10.1007/BF01304852.
  31. Yves Lafont. Logiques, catégories et machines : implantation de langages de programmation guidée par la logique catégorique. Phd thesis, Université Paris VII, January 1988. Google Scholar
  32. J. Laird. Fixed points in quantitative semantics. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, pages 347-356, New York, NY, USA, 2016. Association for Computing Machinery. URL: https://doi.org/10.1145/2933575.2934569.
  33. Jim Laird, Giulio Manzonetto, Guy McCusker, and Michele Pagani. Weighted relational models of typed lambda-calculi. In 2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science, pages 301-310, 2013. URL: https://doi.org/10.1109/LICS.2013.36.
  34. Jean-Simon Pacaud Lemay. An ultrametric for cartesian differential categories for taylor series convergence. Electronic Notes in Theoretical Informatics and Computer Science, 4, 2024. URL: https://doi.org/10.46298/ENTICS.14670.
  35. Saunders MacLane. Categories for the Working Mathematician. Springer-Verlag, New York, 1971. Graduate Texts in Mathematics, Vol. 5. Google Scholar
  36. Ernest G. Manes and Michael A. Arbib, editors. Algebraic Approaches to Program Semantics. Springer-Verlag, Berlin, Heidelberg, 1986. Google Scholar
  37. Giulio Manzonetto. What is a categorical model of the differential and the resource λ-calculi? Mathematical Structures in Computer Science, 22(3):451-520, 2012. URL: https://doi.org/10.1017/S0960129511000594.
  38. Paul-André Melliès. Categorical semantics of linear logic. Panoramas et Synthèses, 27:1-196, 2009. Google Scholar
  39. Paul-André Melliès, Nicolas Tabareau, and Christine Tasson. An explicit formula for the free exponential modality of linear logic. In Susanne Albers, Alberto Marchetti-Spaccamela, Yossi Matias, Sotiris Nikoletseas, and Wolfgang Thomas, editors, Automata, Languages and Programming, pages 247-260, Berlin, Heidelberg, 2009. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-642-02930-1_21.
  40. Bachuki Mesablishvili and Robert Wisbauer. Bimonads and hopf monads on categories. Journal of K-theory K-theory and its Applications to Algebra Geometry and Topology, 7:349-388, April 2011. URL: https://doi.org/10.1017/is010001014jkt105.
  41. Michele Pagani, Peter Selinger, and Benoît Valiron. Applying quantitative semantics to higher-order quantum computing. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, pages 647-658, New York, NY, USA, 2014. Association for Computing Machinery. URL: https://doi.org/10.1145/2535838.2535879.
  42. John Power and Hiroshi Watanabe. Combining a monad and a comonad. Theoretical Computer Science, 280(1):137-162, 2002. Coalgebraic Methods in Computer Science. URL: https://doi.org/10.1016/S0304-3975(01)00024-X.
  43. Peter Selinger. Towards a semantics for higher-order quantum computation. In Proceedings of the 2nd International Workshop on Quantum Programming Languages, TUCS General Publication, volume 33, pages 127-143, 2004. Google Scholar
  44. László Szirmay-Kalos. Higher order automatic differentiation with dual numbers. Periodica Polytechnica Electrical Engineering and Computer Science, 65, October 2020. URL: https://doi.org/10.3311/PPee.16341.
  45. Takeshi Tsukada and Kazuyuki Asada. Linear-algebraic models of linear logic as categories of modules over σ-semirings*. In Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '22, New York, NY, USA, 2022. Association for Computing Machinery. URL: https://doi.org/10.1145/3531130.3533373.
  46. Lionel Vaux. Normalizing the taylor expansion of non-deterministic λ-terms, via parallel reduction of resource vectors. Logical Methods in Computer Science, Volume 15, Issue 3, July 2019. URL: https://doi.org/10.23638/LMCS-15(3:9)2019.
  47. A. Walch. Compositional Taylor expansion in cartesian differential categories . In 2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 748-760, Los Alamitos, CA, USA, June 2025. IEEE Computer Society. URL: https://doi.org/10.1109/LICS65433.2025.00062.
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