Hostname: page-component-74656f9884-2dmjx Total loading time: 0 Render date: 2026-11-09T14:44:07.837Z Has data issue: false hasContentIssue false
  • English
  • Français

Cofree coalgebras and differential linear logic

Published online by Cambridge University Press:  10 June 2020

James Clift  and
Daniel Murfet Open the ORCID record for Daniel Murfet [Opens in a new window]
James Clift
Affiliation:
Department of Mathematics, University of Melbourne
Daniel Murfet*
Affiliation:
Department of Mathematics, University of Melbourne
*
*Corresponding author. Email: d.murfet@unimelb.edu.au
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the 'Save PDF' action button.

We prove that the semantics of intuitionistic linear logic in vector spaces which uses cofree coalgebras is also a model of differential linear logic, and that the Cartesian closed category of cofree coalgebras is a model of the simply typed differential λ-calculus.

Keywords

linear logicdifferential linear logicsemantics

Information

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 30 , Issue 4 , April 2020 , pp. 416 - 457
Copyright
© The Author(s) 2020. Published by Cambridge University Press

References

Blute, R., Ehrhard, T. and Tasson, C. (2010). A convenient differential category, arXiv preprint [arXiv:1006.3140].Google Scholar
Blute, R., Cockett, J. and Seely, R. (2006). Differential categories. Mathematical Structures in Computer Science 16 (06) 1049–1083.CrossRefGoogle Scholar
Blute, R., Cockett, J. and Seely, R. (2009). Cartesian differential categories. Theory and Applications of Categories 22 (23) 622–672.Google Scholar
Blute, R., Cockett, J. and Seely, R. (2015). Cartesian differential storage categories. Theory and Applications of Categories 30 620–686.Google Scholar
Borceux, F. (1994). Handbook of Categorical Algebra 2: Categories and Structures, Encyclopedia of Mathematics and Its Applications, Cambridge, Cambridge University Press.CrossRefGoogle Scholar
Bourbaki, N. (1989). Algebra I, Springer-Verlag Berlin Heidelberg.Google Scholar
Bucciarelli, A., Ehrhard, T. and Manzonetto, G. (2010). Categorical models for simply typed resource calculi. Electronic Notes in Theoretical Computer Science 265 213–230.CrossRefGoogle Scholar
Cockett, J. and Lemay, J.-S. (2019). Integral categories and calculus categories. Mathematical Structures in Computer Science 29(2) 1–66.CrossRefGoogle Scholar
Corliss, G. (1991). Automatic differentiation bibliography. In: Automatic Differentiation of Algorithms: Theory, Implementation, and Application, Philadelphia, Pennsylvania, USA, SIAM, 331–353. updated on-line version.Google Scholar
Ehrhard, T. (2002). On Köthe sequence spaces and linear logic. Mathematical Structures in Computer Science 12 579–623.CrossRefGoogle Scholar
Ehrhard, T. (2005). Finiteness spaces. Mathematical Structures in Computer Science 15 615–646.CrossRefGoogle Scholar
Ehrhard, T. (2016). An introduction to Differential Linear Logic: proof-nets, models and antiderivatives, arXiv preprint [arXiv:1606.01642].Google Scholar
Ehrhard, T. and Laurent, O. (2007). Interpreting a finitary -calculus in differential interaction nets. In: International Conference on Concurrency Theory, Berlin Heidelberg, Springer.Google Scholar
Ehrhard, T. and Regnier, L. (2003). The differential -calculus. Theoretical Computer Science 309 1–41.CrossRefGoogle Scholar
Ehrhard, T. and Regnier, L. (2006). Differential interaction nets. Theoretical Computer Science 364 166–195.CrossRefGoogle Scholar
Eisenbud, D. and Harris, J. (2000). The Geometry of Schemes, Springer Graduate Texts in Mathematics, vol. 197, New York, Springer-Verlag.Google Scholar
Fiore, M. (2007). Differential structure in models of multiplicative biadditive intuitionistic linear logic. In: Proceedings of TLCA, 163–177.CrossRefGoogle Scholar
Friedlander, F. and Joshi, M. (1998). Introduction to the Theory of Distributions, Cambridge, Cambridge University Press.Google Scholar
Frolicher, A. and Kriegl, A. (1988). Linear Spaces and Differentiation Theory, Great Britain, Wiley.Google Scholar
Girard, J.-Y. (1987). Linear logic. Theoretical Computer Science 50 (1) 1–102.CrossRefGoogle Scholar
Girard, J.-Y. (1988). Normal functors, power series and the -calculus. Annals of Pure and Applied Logic 37 129–177.CrossRefGoogle Scholar
Girard, J.-Y. (1995). Light linear logic. Information and Computation 143(2) 175–204.CrossRefGoogle Scholar
Girard, J.-Y. (1999). Coherent Banach spaces: a continuous denotational semantics. Theoretical Computer Science 227 (1) 275–297.CrossRefGoogle Scholar
Girard, J.-Y., Lafont, Y. and Taylor, P. (1989). Proofs and Types, Cambridge Tracts inTheoretical Computer Science, vol. 7, Cambridge University Press.Google Scholar
Hartshorne, R. (1966). Residues and Duality, Lecture Notes in Mathematics, vol. 20, Berlin, Springer-Verlag.Google Scholar
Hartshorne, R. (1977). Algebraic Geometry, Springer Graduate Texts in Mathematics, vol. 52, New York, Springer-Verlag.Google Scholar
Hyland, M. and Schalk, A. (2003). Glueing and orthogonality for models of linear logic. Theoretical Computer Science 294 183–231.CrossRefGoogle Scholar
Kock, A. (2012). Commutative monads as a theory of distributions. Theory and Applications of Categories 26 (4) 97–131.Google Scholar
Kontsevich, M. and Soibelman, Y. (2008). Notes on A ∞-algebras, A ∞-categories and non-commutative geometry. In: Homological Mirror Symmetry, Berlin Heidelberg, Springer, 1–67.Google Scholar
Kontsevich, M. and Soibelman, Y. (2002). Deformation theory, in preparation, accessible [online].Google Scholar
Lambek, J. and Scott, P. J. (1986). Introduction to Higher Order Categorical Logic, Cambridge Studies in AdvancedMathematics, vol. 7, Cambridge, Cambridge University Press.Google Scholar
Le Bruyn, L. (2008). Noncommutative geometry and dual coalgebras, arXiv preprint, [arXiv:0805.2377].Google Scholar
Melliès, P.-A. (2009). Categorical semantics of linear logic. In: Interactive Models of Computation and Program Behaviour, Panoramas et Synthèses vol., Société Mathématique de France.Google Scholar
Murfet, D. (2015). On Sweedler’s cofree cocommutative coalgebra. Journal of Pure and Applied Algebra 219 5289–5304. [arXiv:1406.5749].CrossRefGoogle Scholar
Murfet, D. (2014). Logic and linear algebra: an introduction, arXiv preprint, [arXiv:1407.2650].Google Scholar
Nilsson, H. (2003). Functional automatic differentiation with Dirac impulses. ACM SIGPLAN Notices 38 (9) 153–164.CrossRefGoogle Scholar
Paige, R. and Koenig, S. (1982). Finite differencing of computable expressions. ACM Transactions on Programming Languages and Systems (TOPLAS) 4 (3) 402–454.CrossRefGoogle Scholar
Ramalingam, G. and Reps, T. (1993). A categorized bibliography on incremental computation. In: POPL, ACM, 502–510.CrossRefGoogle Scholar
Seiler, W. (2009). Involution: The Formal Theory of Differential Equations and its Applications in Computer Algebra, vol. 24, Springer-Verlag Berlin Heidelberg.Google Scholar
Sweedler, M. (1969). Hopf Algebras, New York, W. A. Benjamin.Google Scholar