Abstract
Cartesian differential categories are categories equipped with a differential combinator which axiomatizes the directional derivative. Important models of Cartesian differential categories include classical differential calculus of smooth functions and categorical models of the differential \(\lambda \)-calculus. However, Cartesian differential categories cannot account for other interesting notions of differentiation such as the calculus of finite differences or the Boolean differential calculus. On the other hand, change action models have been shown to capture these examples as well as more “exotic” examples of differentiation. However, change action models are very general and do not share the nice properties of a Cartesian differential category. In this paper, we introduce Cartesian difference categories as a bridge between Cartesian differential categories and change action models. We show that every Cartesian differential category is a Cartesian difference category, and how certain well-behaved change action models are Cartesian difference categories. In particular, Cartesian difference categories model both the differential calculus of smooth functions and the calculus of finite differences. Furthermore, every Cartesian difference category comes equipped with a tangent bundle monad whose Kleisli category is again a Cartesian difference category.
The second author is financially supported by Kellogg College, the Oxford-Google Deep Mind Graduate Scholarship, and the Clarendon Fund.
Chapter PDF
Similar content being viewed by others
Keywords
References
Alvarez-Picallo, M., Eyers-Taylor, A., Jones, M.P., Ong, C.H.L.: Fixing incremental computation. In: European Symposium on Programming. pp. 525–552. Springer (2019)
Alvarez-Picallo, M., Ong, C.H.L.: Change actions: models of generalised differentiation. In: International Conference on Foundations of Software Science and Computation Structures. pp. 45–61. Springer (2019)
Blute, R.F., Cockett, J.R.B., Seely, R.A.G.: Differential categories. Mathematical structures in computer science 16(06), 1049–1083 (2006)
Blute, R.F., Cockett, J.R.B., Seely, R.A.G.: Cartesian differential categories. Theory and Applications of Categories 22(23), 622–672 (2009)
Bradet-Legris, J., Reid, H.: Differential forms in non-linear cartesian differential categories (2018), Foundational Methods in Computer Science
Cai, Y., Giarrusso, P.G., Rendel, T., Ostermann, K.: A theory of changes for higher-order languages: Incrementalizing \(\lambda \)-calculi by static differentiation. In: ACM SIGPLAN Notices. vol. 49, pp. 145–155. ACM (2014)
Cockett, J.R.B., Cruttwell, G.S.H.: Differential structure, tangent structure, and sdg. Applied Categorical Structures 22(2), 331–417 (2014)
Cockett, J., Cruttwell, G.: Connections in tangent categories. Theory and Applications of Categories 32(26), 835–888 (2017)
Cruttwell, G.S.: Cartesian differential categories revisited. Mathematical Structures in Computer Science 27(1), 70–91 (2017)
Ehrhard, T., Regnier, L.: The differential lambda-calculus. Theoretical Computer Science 309(1), 1–41 (2003)
Ehrhard, T.: An introduction to differential linear logic: proof-nets, models and antiderivatives. Mathematical Structures in Computer Science 28(7), 995–1060 (2018)
Kelly, R., Pearlmutter, B.A., Siskind, J.M.: Evolving the incremental \(\{\)\(\backslash \)lambda\(\}\) calculus into a model of forward automatic differentiation (ad). arXiv preprint arXiv:1611.03429 (2016)
Kock, A.: Synthetic differential geometry, vol. 333. Cambridge University Press (2006)
Manzonetto, G.: What is a categorical model of the differential and the resource \(\lambda \)-calculi? Mathematical Structures in Computer Science 22(3), 451–520 (2012)
Manzyuk, O.: Tangent bundles in differential lambda-categories. arXiv preprint arXiv:1202.0411 (2012)
Richardson, C.H.: An introduction to the calculus of finite differences. Van Nostrand (1954)
Sprunger, D., Jacobs, B.: The differential calculus of causal functions. arXiv preprint arXiv:1904.10611 (2019)
Sprunger, D., Katsumata, S.y.: Differentiable causal computations via delayed trace. In: 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). pp. 1–12. IEEE (2019)
Steinbach, B., Posthoff, C.: Boolean differential calculus. In: Logic Functions and Equations, pp. 75–103. Springer (2009)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
© 2020 The Author(s)
About this paper
Cite this paper
Alvarez-Picallo, M., Lemay, JS.P. (2020). Cartesian Difference Categories. In: Goubault-Larrecq, J., König, B. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2020. Lecture Notes in Computer Science(), vol 12077. Springer, Cham. https://doi.org/10.1007/978-3-030-45231-5_4
Download citation
DOI: https://doi.org/10.1007/978-3-030-45231-5_4
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-45230-8
Online ISBN: 978-3-030-45231-5
eBook Packages: Mathematics and StatisticsMathematics and Statistics (R0)