Differential linear categories provide the categorical semantics of the multiplicative and exponential fragments of Differential Linear Logic. Briefly, a differential linear category is a symmetric monoidal category that is enriched over commutative monoids (called additive enrichment) and has a monoidal coalgebra modality that is equipped with a codereliction. The codereliction is what captures the ability of differentiating non-linear proofs via linearization in Differential Linear Logic. The additive enrichment plays an important role since it allows one to express the famous Leibniz rule. However, the axioms of a codereliction can be expressed without any sums or zeros. Therefore, it is natural to ask if one can consider a possible non-additive enriched version of differential linear categories. In this paper, we show that even if a codereliction can technically be defined in a non-additive setting, it nevertheless induces an additive enrichment via bialgebra convolution. Thus, we obtain a novel characterization of a differential linear category as a symmetric monoidal category with a monoidal bialgebra modality equipped with a codereliction. Moreover, we also show that coderelictions are, in fact, unique. We also introduce monoidal Hopf coalgebra modalities and discuss how antipodes relate to enrichment over Abelian groups.

In this paper, we explain how the abstract notion of a differential bundle in a tangent category provides a new way of thinking about the category of modules over a commutative ring and its opposite category. MacAdam previously showed that differential bundles in the tangent category of smooth manifolds are precisely smooth vector bundles. Here we provide characterizations of differential bundles in the tangent categories of commutative rings and (affine) schemes. For commutative rings, the category of differential bundles over a commutative ring is equivalent to the category of modules over that ring. For affine schemes, the category of differential bundles over the Spec of a commutative ring is equivalent to the opposite category of modules over said ring. Finally, for schemes, the category of differential bundles over a scheme is equivalent to the opposite category of quasi-coherent sheaves of modules over that scheme.

In a differential category and in Differential Linear Logic, the exponential conjunction ! admits structural maps, characterizing quantitative operations and symmetric co-structural maps, characterizing differentiation. In this paper, we introduce the notion of a Laplace distributor, which is an extra structural map which distributes the linear negation operation (_)^∗ over ! and transforms the co-structural rules into the structural rules. Laplace distributors are directly inspired by the well-known Laplace transform, which is all-important in numerical analysis. In the star-autonomous setting, a Laplace distributor induces a natural transformation from ! to the exponential disjunction ?, which we then call a Laplace transformation. According to its semantics, we show that Laplace distributors correspond precisely to the notion of a generalized exponential function e^x on the monoidal unit. We also show that many well-known and important examples have a Laplace distributor/transformation, including (weighted) relations, finiteness spaces, Köthe spaces, and convenient vector spaces.

Interactions between derivatives and fixpoints have many important applications in both computer science and mathematics. In this paper, we provide a categorical framework to combine fixpoints with derivatives by studying Cartesian differential categories with a fixpoint operator. We introduce an additional axiom relating the derivative of a fixpoint with the fixpoint of the derivative. We show how the standard examples of Cartesian differential categories where we can compute fixpoints provide canonical models of this notion. We also consider when the fixpoint operator is a Conway operator, or when the underlying category is closed. As an application, we show how this framework is a suitable setting to formalize the Newton-Raphson optimization for fast approximation of fixpoints and extend it to higher order languages.

Differential Linear Logic (DiLL) adds to Linear Logic (LL) a symmetrization of three out of the four exponential rules, which allows the expression of a natural notion of differentiation. In this paper, we introduce a codigging inference rule for DiLL and study the categorical semantics of DiLL with codigging using differential categories. The addition of codigging makes the rules of DiLL completely symmetrical. We will explain how codigging is interpreted thanks to the exponential function ex, and in certain cases by the convolutional exponential. In a setting with codigging, every proof is equal to its Taylor series, which implies that every model of DiLL with codigging is quantitative. We provide examples of codigging in relational models, as well as models related to game logic and quantum programming. We also construct a graded model of DiLL with codigging in which the indices witness exponential growth. Codigging makes the exponential of-course connective ! in LL into a monad, where the monad axioms enforce Taylor expansion. As such, codigging opens the door to monadic reformulations of quantitative features in programming languages, as well as further categorical generalizations.

Abstract Cartesian reverse differential categories (CRDCs) are a recently defined structure which categorically model the reverse differentiation operations used in supervised learning. Here, we define a related structure called a monoidal reverse differential category, prove important results about its relationship to CRDCs, and provide examples of both structures, including examples coming from models of quantum computation.

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.

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 of a more discrete nature such as the calculus of finite differences. On the other hand, change action models have been shown to capture these examples as well as more "exotic" examples of differentiation. But change action models are very general and do not share the nice properties of Cartesian differential categories. 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 reverse derivative is a fundamental operation in machine learning and automatic differentiation. This paper gives a direct axiomatization of a category with a reverse derivative operation, in a similar style to that given by Cartesian differential categories for a forward derivative. Intriguingly, a category with a reverse derivative also has a forward derivative, but the converse is not true. In fact, we show explicitly what a forward derivative is missing: a reverse derivative is equivalent to a forward derivative with a dagger structure on its subcategory of linear maps. Furthermore, we show that these linear maps form an additively enriched category with dagger biproducts.

Following the pattern from linear logic, the coKleisli category of a differential category is a Cartesian differential category. What then is the coEilenberg-Moore category of a differential category? The answer is a tangent category! A key example arises from the opposite of the category of Abelian groups with the free exponential modality. The coEilenberg-Moore category, in this case, is the opposite of the category of commutative rings. That the latter is a tangent category captures a fundamental aspect of both algebraic geometry and Synthetic Differential Geometry. The general result applies when there are no negatives and thus encompasses examples arising from combinatorics and computer science. This is an extended version of a conference paper for CSL2020.

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.

Abstract Differential categories axiomatize the basics of differentiation and provide categorical models of differential linear logic. A differential category is said to have antiderivatives if a natural transformation , which all differential categories have, is a natural isomorphism. Differential categories with antiderivatives come equipped with a canonical integration operator such that generalizations of the Fundamental Theorems of Calculus hold. In this paper, we show that Blute, Ehrhard, and Tasson's differential category of convenient vector spaces has antiderivatives. To help prove this result, we show that a differential linear category – which is a differential category with a monoidal coalgebra modality – has antiderivatives if and only if one can integrate over the monoidal unit and such that the Fundamental Theorems of Calculus hold. We also show that generalizations of the relational model (which are biproduct completions of complete semirings) are also differential linear categories with antiderivatives.

Abstract Linear Logic was introduced as the computational counterpart of the algebraic notion of linearity. Differential Linear Logic refines Linear Logic with a proof-theoretical interpretation of the geometrical process of differentiation. In this article, we construct a polarized model of Differential Linear Logic satisfying computational constraints such as an interpretation for higher-order functions, as well as constraints inherited from physics such as a continuous interpretation for spaces. This extends what was done previously by Kerjean for first order Differential Linear Logic without promotion. Concretely, we follow the previous idea of interpreting the exponential of Differential Linear Logic as a space of higher-order distributions with compact-support, which is constructed as an inductive limit of spaces of distributions on Euclidean spaces. We prove that this exponential is endowed with a co-monadic like structure, with the notable exception that it is functorial only on isomorphisms. Interestingly, as previously argued by Ehrhard, this still allows the interpretation of differential linear logic without promotion.

Differential categories are now an established abstract setting for differentiation. However, not much attention has been given to the process which is inverse to differentiation: integration. This paper presents the parallel development for integration by axiomatizing an integral transformation, sA: !A → !A ⊗ A, in a symmetric monoidal category with a coalgebra modality. When integration is combined with differentiation, the two fundamental theorems of calculus are expected to hold (in a suitable sense): a differential category with integration which satisfies these two theorems is called a calculus category. Modifying an approach to antiderivatives by T. Ehrhard, we define having antiderivatives as the demand that a certain natural transformation, K: !A → !A, is invertible. We observe that a differential category having antiderivatives, in this sense, is always a calculus category. When the coalgebra modality is monoidal, it is natural to demand an extra coherence between integration and the coalgebra modality. In the presence of this extra coherence, we show that a calculus category with a monoidal coalgebra modality has its integral transformation given by antiderivatives and, thus, that the integral structure is uniquely determined by the differential structure. The paper finishes by providing a suite of separating examples. Examples of differential categories, integral categories and calculus categories based on both monoidal and (mere) coalgebra modalities are presented. In addition, differential categories which are not integral categories are discussed and vice versa.