Coderelictions for Free Exponential Modalities
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.
Differential Categories
Coderelictions
Differential Linear Logic
Free Exponential Modalities
Lafont Categories
Infinitesimal Augmentations
Theory of computation~Categorical semantics
Theory of computation~Linear logic
19:1-19:21
Regular Paper
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.
Jean-Simon Pacaud
Lemay
Jean-Simon Pacaud Lemay
Mathematics and Computer Science Department, Mount Allison University, Sackville, Canada
https://sites.google.com/view/jspl-personal-webpage/home
https://orcid.org/0000-0003-4124-3722
The author is financially supported by a NSERC Postdoctoral Fellowship (PDF) - Award #: 456414649
10.4230/LIPIcs.CALCO.2021.19
M. Barr. Coalgebras over a commutative ring. Journal of Algebra, 32(3):600-610, 1974.
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.
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.
https://doi.org/10.1007/s10485-019-09572-y
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.
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.
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.
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.
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.
https://doi.org/10.1017/S0960129520000134
J. R. B. Cockett and G. S. H. Cruttwell. Differential structure, tangent structure, and SDG. Applied Categorical Structures, 22(2):331-417, 2014.
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.
https://doi.org/10.4230/LIPIcs.CSL.2020.17
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.
T. Ehrhard. An introduction to differential linear logic: proof-nets, models and antiderivatives. Mathematical Structures in Computer Science, 28:995-1060, 2018.
T. Ehrhard and L. Regnier. The differential lambda-calculus. Theoretical Computer Science, 309(1):1-41, 2003.
T. Ehrhard and L. Regnier. Differential interaction nets. Theoretical Computer Science, 364(2):166-195, 2006.
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.
J.-Y. Girard. Linear logic. Theoretical computer science, 50(1):1-101, 1987.
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.
M. Hyland and A. Schalk. Glueing and orthogonality for models of linear logic. Theoretical computer science, 294(1-2):183-231, 2003.
Y. Lafont. Logiques, catégories et machines. PhD thesis, PhD thesis, Université Paris 7, 1988.
J. Laird. Weighted models for higher-order computation. Information and Computation, 275:104645, 2020.
J. Laird, G. Manzonetto, and G. McCusker. Constructing differential categories and deconstructing categories of games. Information and Computation, 222:247-264, 2013.
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.
S. Lang. Algebra, revised 3rd ed. Graduate Texts in Mathematics, 211, 2002.
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.
https://doi.org/10.23638/LMCS-15(4:8)2019
P.-A. Melliès. Categorical models of linear logic revisited. HAL preprint, hal-00154229, 2003.
P.-A. Melliès. Categorical semantics of linear logic. Panoramas et syntheses, 27:15-215, 2009.
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.
D. Murfet. On Sweedler’s cofree cocommutative coalgebra. Journal of Pure and Applied Algebra, 219(12):5289-5304, 2015.
A. Schalk. What is a categorical model of linear logic? Manuscript, available from http://www.cs.man.ac.uk/ schalk/notes/llmodel.pdf, 2004.
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.
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.
https://doi.org/10.1017/S0960129517000251
M. E. Sweedler. Hopf algebras. mathematical lecture note series, 1969.
Jean-Simon Pacaud Lemay
Creative Commons Attribution 4.0 International license
https://creativecommons.org/licenses/by/4.0/legalcode