Hostname: page-component-f554764f5-44mx8 Total loading time: 0 Render date: 2025-04-14T12:26:11.662Z Has data issue: false hasContentIssue false
  • English
  • Français

Coherent Taylor expansion as a bimonad

Published online by Cambridge University Press:  11 April 2025

Thomas Ehrhard  and
Aymeric Walch Open the ORCID record for Aymeric Walch [Opens in a new window]
Thomas Ehrhard
Affiliation:
Université Paris Cité, CNRS, Inria, IRIF, F-75013, Paris, France
Aymeric Walch*
Affiliation:
Université Paris Cité, CNRS, IRIF, F-75013, Paris, France
*
Corresponding author: Aymeric Walch; Email: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

We extend the recently introduced setting of coherent differentiation by taking into account not only differentiation but also Taylor expansion in categories which are not necessarily (left) additive. The main idea consists in extending summability into an infinitary functor which intuitively maps any object to the object of its countable summable families. This functor is endowed with a canonical structure of a bimonad. In a linear logical categorical setting, Taylor expansion is then axiomatized as a distributive law between this summability functor and the resource comonad (aka. exponential). This distributive law allows to extend the summability functor into a bimonad on the coKleisli category of the resource comonad: this extended functor computes the Taylor expansion of the (nonlinear) morphisms of the coKleisli category. We also show how this categorical axiomatization of Taylor expansion can be generalized to arbitrary cartesian categories, leading to a general theory of Taylor expansion formally similar to that of cartesian differential categories, although it does not require the underlying cartesian category to be left additive. We provide several examples of concrete categories that arise in denotational semantics and feature such analytic structures.

Keywords

categorical semanticsdenotational semanticslinear logicdifferential lambda calculustaylor expansioncoherent differentiation
Type
Special issue: Differential Structures
Information
Mathematical Structures in Computer Science , Volume 35 , 2025 , e9
Check for updates
Copyright
© The Author(s), 2025. Published by Cambridge University Press

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

Article purchase

Temporarily unavailable

References

Aguiar, M., Haim, M. and Franco, I. (2018). Monads on higher monoidal categories. Applied Categorical Structures 26 (3) 413–458.CrossRefGoogle Scholar
Arbib, M. A. and Manes, E. G. (1980). Partially additive categories and flow-diagram semantics. Journal of Algebra 62 (1) 203–227.CrossRefGoogle Scholar
Barbarossa, D. and Manzonetto, G. (2020). Taylor subsumes scott, berry, kahn and plotkin. Proceedings of the ACM on Programming Languages 4 (POPL) 1:1–1:23.CrossRefGoogle Scholar
Beck, J. (1969) Distributive laws. In: Seminar on Triples and Categorical Homology Theory, Eckmann, B. (ed.), Berlin, Heidelberg, Springer Berlin Heidelberg, 119–140.CrossRefGoogle Scholar
Berry, G. (1978). Stable models of typed λ-calculi. In: Automata, Languages and Programming, Ausiello, G. and Böhm, C. (ed.), Berlin, Heidelberg, Springer Berlin Heidelberg, 72–89.CrossRefGoogle Scholar
Bierman, G. M. (1995). What is a categorical model of intuitionistic linear logic?. In Dezani-Ciancaglini, M. and Plotkin, G. (ed.) Typed Lambda Calculi and Applications, Berlin, Heidelberg, Springer Berlin Heidelberg, 78–93.CrossRefGoogle Scholar
Blute, R., Cockett, R. and Seely, R. (2006). Differential categories. Mathematical Structures in Computer Science 16 (6) 1049–1083.CrossRefGoogle Scholar
Blute, R., Cockett, R. and Seely, R. (2009). Cartesian differential categories. Theory and Applications of Categories 22 622–672.Google Scholar
Blute, R., Cockett, R. and Seely, R. (2014). Cartesian differential storage categories, arXiv: Category Theory, 30.Google Scholar
Boudes, P. (2011). Non-uniform (hyper/multi)coherence spaces. Mathematical Structures in Computer Science 21 (1) 1–40.CrossRefGoogle Scholar
Bruguières, A., Lack, S. and Virelizier, A. (2011). Hopf monads on monoidal categories. Advances in Mathematics 227 (2) 745–800.CrossRefGoogle Scholar
Bucciarelli, A. and Ehrhard, T. (2001). On phase semantics and denotational semantics: the exponentials. Annals of Pure and Applied Logic 109 (3) 205–241.CrossRefGoogle Scholar
Cockett, R. and Cruttwell, G. (2014). Differential structure, tangent structure, and SDG. Applied Categorical Structures 22 (2) 331–417.CrossRefGoogle Scholar
Cockett, R., Lemay, J.-S. P. and Lucyshyn-Wright, R. B. B. (2020). Tangent categories from the coalgebras of differential categories. In: Fernández, M. and Muscholl, A.(eds.), 28th EACSL Annual Conference on Computer Science Logic (CSL 2020), Leibniz International Proceedings in Informatics (LIPIcs), Dagstuhl, Germany, vol. 152, 17:1–17:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik.Google Scholar
Cockett, R. and Seely, R. (1997). Proof theory for full intuitionistic linear logic, bilinear logic, and mix categories. Theory and Applications of Categories 3 85–131.Google Scholar
Crubillé, R., Ehrhard, T., Pagani, M. and Tasson, C. (2017). The free exponential modality of probabilistic coherence spaces. In: Esparza, J. and Murawski, A. S. (eds.), Lecture Notes in Computer Science, Foundations of Software Science and Computation Structures - 20th International Conference, FOSSACS. 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, vol. 10203, 20–35.CrossRefGoogle Scholar
Danos, V. and Ehrhard, T. (2011a). Probabilistic coherence spaces as a model of higher-order probabilistic computation. Information and Computation 209 (6) 966–991.CrossRefGoogle Scholar
Danos, V. and Ehrhard, T. (2011b). Probabilistic coherence spaces as a model of higher-order probabilistic computation. Information and Computation 209 (6) 966–991.CrossRefGoogle Scholar
Day, B. (1970). On closed categories of functors. In: Reports of the Midwest Category Seminar IV, MacLane, S., Applegate, H., Barr, M., Day, B., Dubuc, E., Phreilambud, P. A., Street, R., Tierney, M. and Swierczkowski, S. (ed.), Berlin, Heidelberg, Springer Berlin Heidelberg, 1–38.Google Scholar
Dieudonné, J. (1969). Foundations of Modern Analysis, Boston, MA, Academic Press.Google Scholar
Ehrhard, T. (2002). On köthe sequence spaces and linear logic. Mathematical Structures in Computer Science 12 (5) 579–623.CrossRefGoogle Scholar
Ehrhard, T. (2005). Finiteness spaces. Mathematical Structures in Computer Science 15 (4) 615–646,32pp.CrossRefGoogle Scholar
Ehrhard, T. (2018). An introduction to differential linear logic: Proof-nets, models and antiderivatives. Mathematical Structures in Computer Science 28 (7) 995–1060.CrossRefGoogle Scholar
Ehrhard, T. (2022). Differentials and distances in probabilistic coherence spaces. Logical Methods in Computer Science 18 (3).Google Scholar
Ehrhard, T. (2023a). A coherent differential pcf. Logical Methods in Computer Science 19 (4).Google Scholar
Ehrhard, T. (2023b). Coherent differentiation. Mathematical Structures in Computer Science 33 (4–5) 259–310.CrossRefGoogle Scholar
Ehrhard, T. and Geoffroy, G. (2022). Integration in Cones. Technical report, IRIF (UMR_8243) - Institut de Recherche en Informatique Fondamentale.Google Scholar
Ehrhard, T. and Regnier, L. (2003). The differential lambda-calculus. Theoretical Computer Science 309 (1-3) 1–41.CrossRefGoogle Scholar
Ehrhard, T. and Regnier, L. (2008). Uniformity and the taylor expansion of ordinary lambda-terms. Theoretical Computer Science 403 (2) 347–372.CrossRefGoogle Scholar
Ehrhard, T., Tasson, C. and Pagani, M. (2014). Probabilistic coherence spaces are fully abstract for probabilistic pcf. SIGPLAN Notices 49 (1) 309–320.CrossRefGoogle Scholar
Ehrhard, T. and Walch, A. (2023). Cartesian coherent differential categories. In: 2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Los Alamitos, CA, USA, IEEE Computer Society, 1–13.Google Scholar
Fraenkel, L. E. (1978). Formulae for high derivatives of composite functions. Mathematical Proceedings of the Cambridge Philosophical Society 83 (2) 159–165.CrossRefGoogle Scholar
Garner, R. and Lemay, J. (2021). Cartesian differential categories as skew enriched categories. Applied Categorical Structures 29 (6) 1099–1150. Copyright the Author(s) 2021. Version archived for private and non-commercial use with the permission of the author/s and according to publisher conditions. For further rights please contact the publisher.CrossRefGoogle Scholar
Girard, J. (1987). Linear logic. Theoretical Computer Science 50 (1) 1–102.CrossRefGoogle Scholar
Guitart, R. (1980). Tenseurs et machines. Cahiers de Topologie et Géométrie Différentielle Catégoriques 21 (1) 5–62.Google Scholar
Haghverdi, E. (2000). Unique decomposition categories, geometry of interaction and combinatory logic. Mathematical Structures in Computer Science 10 (2) 205–230.CrossRefGoogle Scholar
Hines, P. (2013). A categorical analogue of the monoid semiring construction. Mathematical Structures in Computer Science 23 (1) 55–94.CrossRefGoogle Scholar
Johnstone, P. T. (1975). Adjoint lifting theorems for categories of algebras. Bulletin of the London Mathematical Society 7 (3) 294–297.CrossRefGoogle Scholar
Keigher, W. (1975). Adjunctions and comonads in differential algebra. Pacific Journal of Mathematics 59 (1) 99–112.CrossRefGoogle Scholar
Kelly, G. M. (1974) Doctrinal adjunction. In: Category Seminar, Kelly, G. M. (ed.), Berlin, Heidelberg, Springer Berlin Heidelberg, 257–280.CrossRefGoogle Scholar
Kelly, G. M. and Street, R. (1974) Review of the elements of 2-categories. In: Category Seminar, Kelly, G. M. (ed.), Berlin, Heidelberg, Springer Berlin Heidelberg, 75–103.CrossRefGoogle Scholar
Kerjean, M. and Lemay, J.-S. P. (2023). Taylor expansion as a monad in models of DiLL. In: 2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 1–13.CrossRefGoogle Scholar
Kock, A. (1970). Monads on symmetric monoidal closed categories. Archiv der Mathematik 21 (1) 1–10.CrossRefGoogle Scholar
Kock, A. (1971). Closed categories generated by commutative monads. Journal of the Australian Mathematical Society 12 (4) 405–424.CrossRefGoogle Scholar
Kock, A. (1972). Strong functors and monoidal monads. Archiv der Mathematik 23 (1) 113–120.CrossRefGoogle Scholar
Lafont, Y. (1988). An Analysis of Example. Phd thesis, Université Paris VII.Google Scholar
Laird, J., Manzonetto, G., McCusker, G. and Pagani, M. (2013). Weighted relational models of typed lambda-calculi. In: 2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science, 301–310.CrossRefGoogle Scholar
Lamarche, F. (1992). Quantitative domains and infinitary algebras. Theoretical Computer Science 94 (1) 37–62.CrossRefGoogle Scholar
Lamarche, F. (1995). Generalizing coherent domains and hypercoherences. In: Eleventh Annual Conference on Mathematical Foundations of Programming Semantics, MFPS 1995, Tulane University, New Orleans, LA, USA, March 29 - April 1, 1995, Brookes, S. D., Main, M. G., Melton, A. and Mislove, M. W. (eds.), vol. 1, Electronic Notes in Theoretical Computer Science.Google Scholar
Lemay, J.-S. P. (2018). A tangent category alternative to the Faa di Bruno construction. Theory and Applications of Categories 33 (35) 1072–1110.Google Scholar
MacLane, S. (1971). Categories for the Working Mathematician, vol. 5, New York, Springer-Verlag, Graduate Texts in Mathematics.Google Scholar
Manes, E. G. and Arbib, M. A., eds 1986. Algebraic Approaches to Program Semantics. Springer-Verlag, Berlin, Heidelberg.CrossRefGoogle Scholar
Manzonetto, G. (2012). What is a categorical model of the differential and the resource $\lambda$ -calculi? Mathematical Structures in Computer Science 22 (3) 451–520.CrossRefGoogle Scholar
Maranda, J.-M. (1965). Formal categories. Canadian Journal of Mathematics 17 758–801.CrossRefGoogle Scholar
Melliès, P.-A. (2009). Categorical semantics of linear logic. Panoramas et Synthèses 27 1–196.Google Scholar
Melliès, P.-A., Tabareau, N. and Tasson, C. (2009). An explicit formula for the free exponential modality of linear logic. In: Automata, Languages and Programming, Albers, S., Marchetti-Spaccamela, A., Matias, Y., Nikoletseas, S. and Thomas, W. (ed.), Berlin, Heidelberg, Springer Berlin Heidelberg, 247–260.CrossRefGoogle Scholar
Mesablishvili, B. and Wisbauer, R. (2011). Bimonads and hopf monads on categories. Journal of K-Theory K-Theory and Its Applications to Algebra Geometry and Topology 7 (2) 349–388.CrossRefGoogle Scholar
Moerdijk, I. (2002). Monads on tensor categories. Journal of Pure and Applied Algebra 168 (2) 189–208. Category Theory 1999: selected papers, conference held in Coimbra in honour of the 90th birthday of Saunders Mac Lane.CrossRefGoogle Scholar
Ong, C.-H. L. (2017). Quantitative semantics of the lambda calculus: Some generalisations of the relational model. In: 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 1–12.CrossRefGoogle Scholar
Plotkin, G. (1977). Lcf considered as a programming language. Theoretical Computer Science 5 (3) 223–255.CrossRefGoogle Scholar
Power, J. and Watanabe, H. (2002). Combining a monad and a comonad. Theoretical Computer Science 280 (1) 137–62.CrossRefGoogle Scholar
Rosicky, J. (1984). Abstract tangent functors. Diagrammes 12 JR1–JR11. talk: 3.Google Scholar
Scott, D. (1976). Data types as lattices. SIAM Journal on Computing 5 (3) 522–587.CrossRefGoogle Scholar
Street, R. (1972). The formal theory of monads. Journal of Pure and Applied Algebra 2 (2) 149–168.CrossRefGoogle Scholar
Tsukada, T. and Asada, K. (2022). Linear-algebraic models of linear logic as categories of modules over $\sigma$ -semirings $*$ . In: Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS’22, New York, NY, USA, Association for Computing Machinery.Google Scholar
Van Osdol, D. H. (1971). Sheaves in Regular Categories, Berlin, Heidelberg, Springer Berlin Heidelberg, 223–239.CrossRefGoogle Scholar
Walch, A. (2022). Coherent differentiation in models of Linear Logic. Internship report, ENS de Lyon.Google Scholar
Whittlesey, E. F. (1965). Analytic functions in banach spaces. Proceedings of the American Mathematical Society 16 (5) 1077–1083.CrossRefGoogle Scholar
Wisbauer, R. (2008). Algebras versus coalgebras. Applied Categorical Structures 16 (1-2) 255–295.CrossRefGoogle Scholar