Document

# Unifying Graded Linear Logic and Differential Operators

## File

LIPIcs.FSCD.2023.21.pdf
• Filesize: 0.75 MB
• 21 pages

## Acknowledgements

We thank the anonymous reviewers for their kind and constructive comments on the first version of the paper, which greatly contributed to its improvement.

## Cite As

Flavien Breuvart, Marie Kerjean, and Simon Mirwasser. Unifying Graded Linear Logic and Differential Operators. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 21:1-21:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.FSCD.2023.21

## Abstract

Linear Logic refines Classical Logic by taking into account the resources used during the proof and program computation. In the past decades, it has been extended to various frameworks. The most famous are indexed linear logics which can describe the resource management or the complexity analysis of a program. From another perspective, Differential Linear Logic is an extension which allows the linearization of proofs. In this article, we merge these two directions by first defining a differential version of Graded linear logic: this is made by indexing exponential connectives with a monoid of differential operators. We prove that it is equivalent to a graded version of previously defined extension of finitary differential linear logic. We give a denotational model of our logic, based on distribution theory and linear partial differential operators with constant coefficients.

## Subject Classification

##### ACM Subject Classification
• Theory of computation → Linear logic
• Mathematics of computing → Partial differential equations
• Theory of computation → Denotational semantics
##### Keywords
• Linear Logic
• Denotational Semantics
• Functional Analysis

## Metrics

• Access Statistics
• Total Accesses (updated on a weekly basis)
0

## References

1. Jean-Philippe Bernardy, Mathieu Boespflug, Ryan R. Newton, Simon Peyton Jones, and Arnaud Spiwack. Linear haskell: practical linearity in a higher-order polymorphic language. In Principles of Programming Languages 2018 (POPL 2018). ACM, January 2018.
2. Rick Blute, Robin Cockett, and Robert Seely. Differential categories. Mathematical Structures in Computer Science, 16(6), 2006.
3. Rick Blute, Thomas Ehrhard, and Christne Tasson. A convenient differential category. Les cahiers de topologie et de géométrie différentielle catégorique, 2012.
4. Siegfried Bosch. Algebra. Springer-Lehrbuch. Springer, 2009.
5. Flavien Breuvart and Michele Pagani. Modelling Coeffects in the Relational Semantics of Linear Logic. In Computer Science Logic (CSL ), Leibniz International Proceedings in Informatics (LIPIcs). Schloss Dagstuhl, 2015.
6. Aloïs Brunel, Marco Gaboardi, Damiano Mazza, and Steve Zdancewic. A core quantitative coeffect calculus. In Programming Languages and Systems. Springer Berlin Heidelberg, 2014.
7. Aloïs Brunel, Damiano Mazza, and Michele Pagani. Backpropagation in the Simply Typed Lambda-calculus with Linear Negation. Principles of Programming Languages, 2020.
8. Y. Dabrowski and M. Kerjean. Models of Linear Logic based on the Schwartz epsilon product. Theory and Applications of Categories, 2020.
9. Ugo Dal Lago and Martin Hofmann. Bounded linear logic, revisited. In Typed Lambda Calculi and Applications (TLCA). Springer Berlin Heidelberg, 2009.
10. Thomas Ehrhard. On Köthe Sequence Spaces and Linear Logic. Mathematical Structures in Computer Science, 12(5), 2002.
11. Thomas Ehrhard. Finiteness spaces. Mathematical Structures in Computer Science, 15(4), 2005.
12. Thomas Ehrhard. An introduction to differential linear logic: proof-nets, models and antiderivatives. Mathematical Structures in Computer Science, 28(7), 2018.
13. Thomas Ehrhard and Antonio Bucciarelli. On phase semantics and denotational semantics: the exponentials. Annals of Pure and Applied Logic, 109(3), 2001.
14. Thomas Ehrhard and Laurent Regnier. Differential interaction nets. Theoretical Computer Science, 364(2), 2006.
15. Yōji Fukihara and Shin-ya Katsumata. Generalized bounded linear logic and its categorical semantics. In Foundations of Software Science and Computation Structures (FoSSaCS). Springer International Publishing, 2021.
16. Marco Gaboardi, Andreas Haeberlen, Justin Hsu, Arjun Narayan, and Benjamin Pierce. Linear Dependent Types for Differential Privacy. In Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '13. ACM, 2013.
17. Marco Gaboardi, Shin-ya Katsumata, Dominic Orchard, Flavien Breuvart, and Tarmo Uustalu. Combining effects and coeffects via grading. In Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, International Conference on Functional Programming, ICFP. Association for Computing Machinery, 2016.
18. R. Gannoun, R. Hachaichi, H. Ouerdiane, and A. Rezgui. Un théorème de dualité entre espaces de fonctions holomorphes à croissance exponentielle. Journal of Functional Analysis, 171(1), 2000.
19. Dan Ghica and Alex I. Smith. Bounded linear types in a resource semiring. In Programming Languages and Systems,, European Symposium on Programming, (ESOP). Springer Berlin Heidelberg, 2014.
20. Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50(1), 1987.
21. Jean-Yves Girard. Normal functors, power series and λ-calculus. Annals of Pure and Applied Logic, 1988.
22. Jean-Yves Girard, Andre Scedrov, and Philip Scott. Bounded linear logic. Theoretical Computer Science, 9, August 1991.
23. Lars Hormander. Linear partial differential operators. Springer Berlin, 1963.
24. Hans Jarchow. Locally convex spaces. B. G. Teubner Stuttgart, 1981. Mathematical Textbooks.
25. Marie Kerjean. A logical account for linear partial differential equations. In Logic in Computer Science (LICS), Proceedings. Association for Computing Machinery, 2018.
26. Marie Kerjean and Jean-Simon Pacaud Lemay. Taylor Expansion as a Monad in Models of Dill, 2023. preprint.
27. O. Laurent. Etude de la polarisation en logique. Thèse de Doctorat, Université Aix-Marseille II, March 2002.
28. Jean-Simon Pacaud Lemay and Jean-Baptiste Vienney. Graded differential categories and graded differential linear logic, 2023. preprint.