Document Open Access Logo

Unifying Graded Linear Logic and Differential Operators

Authors Flavien Breuvart, Marie Kerjean, Simon Mirwasser

PDF
Thumbnail PDF

File

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

Document Identifiers

Author Details

Flavien Breuvart
  • LIPN, USPN, Villetaneuse, France
Marie Kerjean
  • CNRS, LIPN, USPN, Villetaneuse, France
Simon Mirwasser
  • LIPN, USPN, Villetaneuse, France

Funding

  • Breuvart, Flavien: Supported by the project ANR-18-CE25-0001.
  • Kerjean, Marie: Supported by the projects ANR-20-CE48-0002 and ANR-20-CE48-0014.

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 Get BibTex

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
  • Graded Logic

Metrics

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

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. Google Scholar
  2. Rick Blute, Robin Cockett, and Robert Seely. Differential categories. Mathematical Structures in Computer Science, 16(6), 2006. Google Scholar
  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. Google Scholar
  4. Siegfried Bosch. Algebra. Springer-Lehrbuch. Springer, 2009. Google Scholar
  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. Google Scholar
  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. Google Scholar
  7. Aloïs Brunel, Damiano Mazza, and Michele Pagani. Backpropagation in the Simply Typed Lambda-calculus with Linear Negation. Principles of Programming Languages, 2020. Google Scholar
  8. Y. Dabrowski and M. Kerjean. Models of Linear Logic based on the Schwartz epsilon product. Theory and Applications of Categories, 2020. Google Scholar
  9. Ugo Dal Lago and Martin Hofmann. Bounded linear logic, revisited. In Typed Lambda Calculi and Applications (TLCA). Springer Berlin Heidelberg, 2009. Google Scholar
  10. Thomas Ehrhard. On Köthe Sequence Spaces and Linear Logic. Mathematical Structures in Computer Science, 12(5), 2002. Google Scholar
  11. Thomas Ehrhard. Finiteness spaces. Mathematical Structures in Computer Science, 15(4), 2005. Google Scholar
  12. Thomas Ehrhard. An introduction to differential linear logic: proof-nets, models and antiderivatives. Mathematical Structures in Computer Science, 28(7), 2018. Google Scholar
  13. Thomas Ehrhard and Antonio Bucciarelli. On phase semantics and denotational semantics: the exponentials. Annals of Pure and Applied Logic, 109(3), 2001. Google Scholar
  14. Thomas Ehrhard and Laurent Regnier. Differential interaction nets. Theoretical Computer Science, 364(2), 2006. Google Scholar
  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. Google Scholar
  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. Google Scholar
  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. Google Scholar
  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. Google Scholar
  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. Google Scholar
  20. Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50(1), 1987. Google Scholar
  21. Jean-Yves Girard. Normal functors, power series and λ-calculus. Annals of Pure and Applied Logic, 1988. Google Scholar
  22. Jean-Yves Girard, Andre Scedrov, and Philip Scott. Bounded linear logic. Theoretical Computer Science, 9, August 1991. Google Scholar
  23. Lars Hormander. Linear partial differential operators. Springer Berlin, 1963. Google Scholar
  24. Hans Jarchow. Locally convex spaces. B. G. Teubner Stuttgart, 1981. Mathematical Textbooks. Google Scholar
  25. Marie Kerjean. A logical account for linear partial differential equations. In Logic in Computer Science (LICS), Proceedings. Association for Computing Machinery, 2018. Google Scholar
  26. Marie Kerjean and Jean-Simon Pacaud Lemay. Taylor Expansion as a Monad in Models of Dill, 2023. preprint. Google Scholar
  27. O. Laurent. Etude de la polarisation en logique. Thèse de Doctorat, Université Aix-Marseille II, March 2002. Google Scholar
  28. Jean-Simon Pacaud Lemay and Jean-Baptiste Vienney. Graded differential categories and graded differential linear logic, 2023. preprint. Google Scholar
  29. Paul-André Melliès. Parametric monads and enriched adjunctions, 2012. preprint. Google Scholar
  30. Michele Pagani. The cut-elimination theorem for differential nets with promotion. In International Conference on Typed Lambda Calculus and Applications, 2009. Google Scholar
  31. L. Schwartz. Théorie des distributions. Publications de l'Institut de Mathématique de l'Université de Strasbourg, No. IX-X. Hermann, Paris, 1966. Google Scholar
  32. James Wallbridge. Jets and differential linear logic. Mathematical Structures in Computer Science, 30(8), 2020. URL: https://doi.org/10.1017/S0960129520000249.
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 About DROPS Imprint Privacy Contact