Document Open Access Logo

Coderelictions for Free Exponential Modalities

Author Jean-Simon Pacaud Lemay

PDF
Thumbnail PDF

File

LIPIcs.CALCO.2021.19.pdf
  • Filesize: 0.81 MB
  • 21 pages

Document Identifiers

Author Details

Jean-Simon Pacaud Lemay
  • Mathematics and Computer Science Department, Mount Allison University, Sackville, Canada

Funding

  • Lemay, Jean-Simon Pacaud: The author is financially supported by a NSERC Postdoctoral Fellowship (PDF) - Award #: 456414649

Acknowledgements

The author would like to thank the anonymous referees for their comments and suggestions which helped improve this paper, as well as Robert A. G. Seely, Paul-André Melliès, Rory Lucyshyn-Wright for useful discussions, support of this project, and editorial comments.

Cite As Get BibTex

Jean-Simon Pacaud Lemay. Coderelictions for Free Exponential Modalities. In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 19:1-19:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021) https://doi.org/10.4230/LIPIcs.CALCO.2021.19

Abstract

In a categorical model of the multiplicative and exponential fragments of intuitionistic linear logic (MELL), the exponential modality is interpreted as a comonad ! such that each cofree !-coalgebra !A comes equipped with a natural cocommutative comonoid structure. An important case is when ! is a free exponential modality so that !A is the cofree cocommutative comonoid over A. A categorical model of MELL with a free exponential modality is called a Lafont category. A categorical model of differential linear logic is called a differential category, where the differential structure can equivalently be described by a deriving transformation !A⊗A →{𝖽_A} !A or a codereliction A →{η_A} !A. Blute, Lucyshyn-Wright, and O'Neill showed that every Lafont category with finite biproducts is a differential category. However, from a differential linear logic perspective, Blute, Lucyshyn-Wright, and O'Neill’s approach is not the usual one since the result was stated in the dual setting and the proof is in terms of the deriving transformation 𝖽. In differential linear logic, it is often the codereliction η that is preferred and that plays a more prominent role. In this paper, we provide an alternative proof that every Lafont category (with finite biproducts) is a differential category, where we construct the codereliction η using the couniversal property of the cofree cocommtuative comonoid !A and show that η is unique. To achieve this, we introduce the notion of an infinitesimal augmentation k⊕A →{𝖧_A} !(k ⊕ A), which in particular is a !-coalgebra and a comonoid morphism, and show that infinitesimal augmentations are in bijective correspondence to coderelictions (and deriving transformations). As such, infinitesimal augmentations provide a new equivalent axiomatization for differential categories in terms of more commonly known concepts. For a free exponential modality, its infinitesimal augmentation is easy to construct and allows one to clearly see the differential structure of a Lafont category, regardless of the construction of !A.

Subject Classification

ACM Subject Classification
  • Theory of computation → Categorical semantics
  • Theory of computation → Linear logic
Keywords
  • Differential Categories
  • Coderelictions
  • Differential Linear Logic
  • Free Exponential Modalities
  • Lafont Categories
  • Infinitesimal Augmentations

Metrics

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

References

  1. M. Barr. Coalgebras over a commutative ring. Journal of Algebra, 32(3):600-610, 1974. Google Scholar
  2. G.M. Bierman. What is a categorical model of intuitionistic linear logic? In International Conference on Typed Lambda Calculi and Applications, pages 78-93. Springer, 1995. Google Scholar
  3. R. F. Blute, J. R. B. Cockett, J.-S. P. Lemay, and R. A. G. Seely. Differential categories revisited. Applied Categorical Structures, 28:171-235, 2020. URL: https://doi.org/10.1007/s10485-019-09572-y.
  4. R. F. Blute, J. R. B. Cockett, and R. A. G. Seely. Cartesian differential storage categories. Theory and Applications of Categories, 30(18):620-686, 2015. Google Scholar
  5. R. F Blute, R. B. B. Lucyshyn-Wright, and K O'Neill. Derivations in codifferential categories. Cahiers de Topologie et Géométrie Différentielle Catégoriques, 57:243-280, 2016. Google Scholar
  6. R. F. Blute, Blute, J. R. B. Cockett, and R. A. G. Seely. Differential categories. Mathematical structures in computer science, 16(6):1049-1083, 2006. Google Scholar
  7. R. F. Blute, Blute, J. R. B. Cockett, and R. A. G. Seely. Cartesian differential categories. Theory and Applications of Categories, 22(23):622-672, 2009. Google Scholar
  8. J. Clift and D. Murfet. Cofree coalgebras and differential linear logic. Mathematical Structures in Computer Science, 30(4):416-457, 2020. URL: https://doi.org/10.1017/S0960129520000134.
  9. J. R. B. Cockett and G. S. H. Cruttwell. Differential structure, tangent structure, and SDG. Applied Categorical Structures, 22(2):331-417, 2014. Google Scholar
  10. J.R. B. Cockett, J.-S. P. Lemay, and R. B. B. Lucyshyn-Wright. Tangent Categories from the Coalgebras of Differential Categories. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020), volume 152 of Leibniz International Proceedings in Informatics (LIPIcs), pages 17:1-17:17, Dagstuhl, Germany, 2020. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: https://doi.org/10.4230/LIPIcs.CSL.2020.17.
  11. R. Crubillé, T. Ehrhard, M. Pagani, and C. Tasson. The free exponential modality of probabilistic coherence spaces. In International Conference on Foundations of Software Science and Computation Structures, pages 20-35. Springer, 2017. Google Scholar
  12. T. Ehrhard. An introduction to differential linear logic: proof-nets, models and antiderivatives. Mathematical Structures in Computer Science, 28:995-1060, 2018. Google Scholar
  13. T. Ehrhard and L. Regnier. The differential lambda-calculus. Theoretical Computer Science, 309(1):1-41, 2003. Google Scholar
  14. T. Ehrhard and L. Regnier. Differential interaction nets. Theoretical Computer Science, 364(2):166-195, 2006. Google Scholar
  15. M.P. Fiore. Differential structure in models of multiplicative biadditive intuitionistic linear logic. In International Conference on Typed Lambda Calculi and Applications, pages 163-177. Springer, 2007. Google Scholar
  16. J.-Y. Girard. Linear logic. Theoretical computer science, 50(1):1-101, 1987. Google Scholar
  17. J.-Y. Girard and Y. Lafont. Linear logic and lazy computation. In International Joint Conference on Theory and Practice of Software Development, pages 52-66. Springer, 1987. Google Scholar
  18. M. Hyland and A. Schalk. Glueing and orthogonality for models of linear logic. Theoretical computer science, 294(1-2):183-231, 2003. Google Scholar
  19. Y. Lafont. Logiques, catégories et machines. PhD thesis, PhD thesis, Université Paris 7, 1988. Google Scholar
  20. J. Laird. Weighted models for higher-order computation. Information and Computation, 275:104645, 2020. Google Scholar
  21. J. Laird, G. Manzonetto, and G. McCusker. Constructing differential categories and deconstructing categories of games. Information and Computation, 222:247-264, 2013. Google Scholar
  22. J. Laird, G. Manzonetto, G. McCusker, and M. Pagani. Weighted relational models of typed lambda-calculi. In Proceedings of the 2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science, pages 301-310. IEEE Computer Society, 2013. Google Scholar
  23. S. Lang. Algebra, revised 3rd ed. Graduate Texts in Mathematics, 211, 2002. Google Scholar
  24. J.-S. P. Lemay. Lifting Coalgebra Modalities and MELL Model Structure to Eilenberg-Moore Categories. Logical Methods in Computer Science, Volume 15, Issue 4, November 2019. URL: https://doi.org/10.23638/LMCS-15(4:8)2019.
  25. P.-A. Melliès. Categorical models of linear logic revisited. HAL preprint, hal-00154229, 2003. Google Scholar
  26. P.-A. Melliès. Categorical semantics of linear logic. Panoramas et syntheses, 27:15-215, 2009. Google Scholar
  27. P.-A. Melliès, N. Tabareau, and C. Tasson. An explicit formula for the free exponential modality of linear logic. Mathematical Structures in Computer Science, pages 1-34, 2017. Google Scholar
  28. D. Murfet. On Sweedler’s cofree cocommutative coalgebra. Journal of Pure and Applied Algebra, 219(12):5289-5304, 2015. Google Scholar
  29. A. Schalk. What is a categorical model of linear logic? Manuscript, available from http://www.cs.man.ac.uk/ schalk/notes/llmodel.pdf, 2004. Google Scholar
  30. R. A. G. Seely. Linear logic, *-autonomous categories and cofree coalgebras. In Categories in Computer Science and Logic (1987), pages 371-382. American Mathematical Society, 1989. Google Scholar
  31. S. Slavnov. On banach spaces of sequences and free linear logic exponential modality. Mathematical Structures in Computer Science, 29(2):215-242, 2019. URL: https://doi.org/10.1017/S0960129517000251.
  32. M. E. Sweedler. Hopf algebras. mathematical lecture note series, 1969. 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 About DROPS Imprint Privacy Contact