# Jacobians and Gradients
for Cartesian Differential Categories

Jean-Simon Pacaud Lemay 111Author’s website:
https://sites.google.com/view/jspl-personal-webpage/home The author would like
to thank Jonathan Gallagher for useful discussions. The author is financially
supported by a Natural Science and Engineering Research Council of Canada
(NSERC) Postdoctoral Fellowship (PDF) - Award #: 456414649Mathematics and
Computer Science Department
Mount Allison University
Sackville, New Brunswick, Canada<EMAIL_ADDRESS>
###### Abstract

Cartesian differential categories come equipped with a differential combinator
that formalizes the directional derivative from multivariable calculus.
Cartesian differential categories provide a categorical semantics of the
differential $\lambda$-calculus and have also found applications in causal
computation, incremental computation, game theory, differentiable programming,
and machine learning. There has recently been a desire to provide a
(coordinate-free) characterization of Jacobians and gradients in Cartesian
differential categories. One’s first attempt might be to consider Cartesian
differential categories which are Cartesian closed, such as models of the
differential $\lambda$-calculus, and then take the curry of the derivative.
Unfortunately, this approach excludes numerous important examples of Cartesian
differential categories such as the category of real smooth functions. In this
paper, we introduce linearly closed Cartesian differential categories, which
are Cartesian differential categories that have an internal hom of linear
maps, a bilinear evaluation map, and the ability to curry maps which are
linear in their second argument. As such, the Jacobian of a map is defined as
the curry of its derivative. Many well-known examples of Cartesian
differential categories are linearly closed, such as, in particular, the
category of real smooth functions. We also explain how a Cartesian closed
differential category is linearly closed if and only if a certain linear
idempotent on the internal hom splits. To define the gradient of a map, one
must be able to define the transpose of the Jacobian, which can be done in a
Cartesian reverse differential category. Thus, we define the gradient of a map
to be the curry of its reverse derivative and show this equals the transpose
of its Jacobian. We also explain how a linearly closed Cartesian reverse
differential category is precisely a linearly closed Cartesian differential
category with an appropriate notion of transpose.

##  1 Introduction

Cartesian differential categories, introduced by Blute, Cockett, and Seely in
[6], come equipped with a differential combinator $\mathsf{D}$ which provides
a categorical axiomatization of the directional derivative from multivariable
calculus, and so for every map $A\xrightarrow{f}B$ produces its derivative
$A\times A\xrightarrow{\mathsf{D}[f]}B$. There is no shortage of examples of
Cartesian differential categories in the literature, but arguably the most
important example is $\mathsf{SMOOTH}$, the category of Euclidean spaces
$\mathbb{R}^{n}$ and real smooth functions between them, where the
differential combinator, in this case, is precisely the classical directional
derivative. Another important class of examples are the Cartesian closed
differential categories [10, 9, 20], which provide a categorical semantics of
Ehrhard and Regnier’s differential $\lambda$-calculus [15]. Cartesian (closed)
differential categories have found numerous applications in computer science
such as being picked up by Katsumata and Sprunger in their work on causal
computations [22], by Abadi and Plotkin in their work on differentiable
programming languages [2], by Alvarez-Picallo and Ong in their work on
incremental computation [3], and by Laird, Manzonetto, and McCusker in their
work in game theory [18]. Most recently, Cartesian (closed) differential
categories have also found usage in machine learning with the introduction of
Cartesian _reverse_ differential categories [11, 13], which have been shown to
be a suitable setting for reverse gradient descent by Cruttwell, Gavranović,
Ghani, Wilson, and Zanasi in [14, 24].

An important concept in differential calculus is the Jacobian matrix. Recall
that for a smooth function $\mathbb{R}^{n}\xrightarrow{F=\langle
f_{\\_}1,\ldots,f_{\\_}n\rangle}\mathbb{R}^{m}$, its Jacobian matrix at point
$\vec{x}\in\mathbb{R}^{n}$ is given by the $n\times m$ matrix
$\mathbf{J}(F)(\vec{x})$ whose coordinates are the partial derivatives of
$f_{\\_}i$ evaluated at $\vec{x}$. The $\mathbb{R}$-linear function associated
with the Jacobian matrix at $\vec{x}$ is called the total derivative of $F$,
and evaluating this linear function at $\vec{y}$ results in the derivative
$\mathsf{D}[F](\vec{x},\vec{y})$. Thus, the Jacobian of $F$ can be interpreted
as a map
$\mathbb{R}^{n}\xrightarrow{\mathbf{J}(F)}\mathsf{LIN}(\mathbb{R}^{n},\mathbb{R}^{m})$,
where the codomain is the vector spaces of $\mathbb{R}$-linear functions from
$\mathbb{R}^{n}$ to $\mathbb{R}^{m}$, and can therefore be understood as sort
of curry
$\mathbb{R}^{n}\times\mathbb{R}^{n}\xrightarrow{\mathsf{D}[F]}\mathbb{R}^{m}$.
Interpreting the Jacobian in this manner shows how the Jacobian is a special
case of both the Fréchet derivative and the Gateaux derivative. For a smooth
function $\mathbb{R}^{n}\xrightarrow{f}\mathbb{R}$, its gradient at
$\vec{x}\in\mathbb{R}^{n}$ is the transpose of its Jacobian at $\vec{x}$,
$\nabla(f)(\vec{x})=\mathbf{J}(F)(\vec{x})^{\mathsf{T}}\in\mathbb{R}^{n}$.
Since $\mathsf{LIN}(\mathbb{R},\mathbb{R}^{n})\cong\mathbb{R}^{n}$, the
gradient can therefore be interpreted as a map
$\mathbb{R}^{n}\xrightarrow{\nabla(f)}\mathsf{LIN}(\mathbb{R},\mathbb{R}^{n})$.

The notions of Jacobians and gradients have yet to be formally defined in a
Cartesian differential category. Such concepts would be highly desirable,
specifically if one wishes to formalize machine learning algorithms in
Cartesian differential categories. This need for Jacobians and gradients is
expressed by Katsumata and Sprunger, who state the following in the conclusion
of their paper [22]: “Though we would like to say our abstract treatment of
differentiation can be used directly by machine learning practitioners, it
appears this is not the case yet. The derivative of a morphism in a Cartesian
differential category is not the same as having an explicit Jacobian or
gradient. A gradient can be recovered from this morphism by applying it to all
the basis vectors, but when there are millions of parameters in a machine
learning model, this idea is computationally disastrous. We think that by
adding some structure to Cartesian differential categories, such as a
designated closed subcategory, we could give a theoretical treatment allowing
for more explicit representation of Jacobians.” This highlights a clear need
for axiomatizing (coordinate-free) Jacobians and gradients in the context of
Cartesian differential categories.

Based on the above discussion, and as suggested by Katsumata and Sprunger,
one’s first attempt might be to consider defining Jacobians in a Cartesian
closed differential category and define the Jacobian of a map
$A\xrightarrow{f}B$ as the curry of its derivative $A\times
A\xrightarrow{\mathsf{D}[f]}B$, so
$A\xrightarrow{\lambda\left(\mathsf{D}[f]\right)}[A,B]$. While this is a very
reasonable and promising idea that enables one to one can get quite far in
extracting the main properties of the Jacobian, there is a flaw. The Cartesian
closed differential category approach would exclude numerous examples of
Cartesian differential categories, specifically those wfith a “finite-
dimensional flavour” and many machine learning-related models. In particular,
$\mathsf{SMOOTH}$ is not Cartesian closed since, intuitively, the set of
smooth functions from $\mathbb{R}^{n}$ to $\mathbb{R}^{m}$ is not a finite-
dimensional $\mathbb{R}$-vector space and therefore not isomorphic to a
Euclidean space $\mathbb{R}^{k}$. Thus another approach is required. Luckily,
the codomain of the Jacobian is $\mathsf{LIN}(\mathbb{R}^{n},\mathbb{R}^{m})$,
which is isomorphic to $\mathbb{R}^{nm}$, and so can therefore be interpreted
as an object in $\mathsf{SMOOTH}$. We may generalize this idea in numerous
Cartesian differential categories since there is a notion of linearity based
on the differential combinator (which often coincides with the notion of
linearity from linear algebra). Thus, one needs the notion of internal
_linear_ homs.

In this paper, we introduce the notion of a linearly closed Cartesian
differential category, which is a Cartesian differential category with
internal linear hom $\mathcal{L}(A,B)$ (which can be interpreted as an object
which represents the set of linear maps from $A$ to $B$), a bilinear
evaluation map $\mathcal{L}(A,B)\times A\xrightarrow{\epsilon_{\\_}\ell}B$,
and the ability to curry maps which are linear in their second argument. Many
analogues of the basic Cartesian closed properties hold for the linearly
closed setting. One of the axioms of the differential combinator states
precisely that for any map $A\xrightarrow{f}B$, its derivative $A\times
A\xrightarrow{\mathsf{D}[f]}B$ is linear in its second argument. Therefore,
the Jacobian of $f$ is defined as the curry of $\mathsf{D}[f]$,
$A\xrightarrow{\mathbf{J}(f):=\lambda_{\\_}\ell(\mathsf{D}[f])}\mathcal{L}(A,B)$,
and numerous of the basic properties of the Jacobian from classical calculus
hold. Many important examples of Cartesian differential categories are
linearly closed, such as any differential Lawvere theory like
$\mathsf{SMOOTH}$ or the Lawvere theory of polynomials over a commutative
semiring, and also the coKleisli category of a differential category which is
symmetric monoidal closed [5]. We also explain how a Cartesian closed
differential category is linearly closed if and only if a certain linear
idempotent on the internal hom splits. Therefore, a certain idempotent
completion of a Cartesian closed differential category results in a linearly
closed Cartesian differential category. Lastly, to define the gradient of a
map, one requires the ability to take the transpose (or dagger) of linear
maps. This can be achieved in a linearly closed Cartesian reverse differential
category, which we explain is precisely a linear closed Cartesian differential
category equipped with linear transpose maps
$\mathcal{L}(A,B)\xrightarrow{\tau}\mathcal{L}(B,A)$. Therefore, the gradient
of a map $A\xrightarrow{f}B$ is defined by taking the curry of its reverse
derivative $A\times B\xrightarrow{\mathsf{R}[f]}A$, which is linear in its
second argument,
$A\xrightarrow{\nabla(f):=\lambda_{\\_}\ell(\mathsf{R}[f])}\mathcal{L}(B,A)$,
which we show is equal to the transpose of its Jacobian, so
$\nabla(f)=\tau\circ\mathbf{J}(f)$. In future works, the notions of Jacobians
and gradient will be particularly useful when generalizing and applying
automatic differentiation and machine learning algorithms, such as back-
propagation or (reverse) gradient descent, in the setting of a Cartesian
(reverse) differential category. In fact, internal linear homs are a key
concept in Vákár’s recent work on automatic differentiation [23].

##  2 Background: Cartesian Differential Categories and Linear Maps

In this background section, we review Cartesian (closed) differential
categories and linear maps, as well as providing examples and a term logic
notation that will help with intuition. For a more in-depth introduction to
Cartesian differential categories, we refer the reader to [6, 12].

The underlying structure of a Cartesian differential category is that of a
Cartesian left additive category, which in particular allows one to have zero
maps and sums of maps, while also allowing for maps that do not preserve said
sums or zeros. Maps that do preserve the additive structure are called
_additive_ maps. It is important to note that we do not assume that our
Cartesian left additive categories necessarily have negatives, which allows
for examples from computer science. For a category with (chosen) finite
products we denote the (chosen) binary product as $\times$, with projection
maps $A\times B\xrightarrow{\pi_{\\_}0}A$ and ${A\times
B\xrightarrow{\pi_{\\_}1}B}$ and pairing object $\langle-,-\rangle$, and the
(chosen) terminal object as $\top$.

###### Definition 2.1

A left additive category [6, Definition 1.1.1] is a category $\mathbb{X}$ such
that each hom-set $\mathbb{X}(A,B)$ is a commutative monoid with addition
$\mathbb{X}(A,B)\times\mathbb{X}(A,B)\xrightarrow{+}\mathbb{X}(A,B)$,
$(f,g)\mapsto f+g$, and zero $0\in\mathbb{X}(A,B)$, and such that pre-
composition preserves the additive structure: $(f+g)\circ a=f\circ a+g\circ a$
and $0\circ a=0$. A map $A\xrightarrow{f}B$ is said to be additive [6,
Definition 1.1.1] if post-composition by $f$ preserves the additive structure:
$f\circ(a+b)=f\circ a+g\circ b$ and $f\circ 0=0$. A Cartesian left additive
category [6, Definition 1.2.1] is a left additive category $\mathbb{X}$ which
has finite products and such that all the projection maps $A\times
B\xrightarrow{\pi_{\\_}0}A$ and ${A\times B\xrightarrow{\pi_{\\_}1}B}$ are
additive.222We note that the definition of a Cartesian left additive category
presented here is not precisely that given in [6, Definition 1.2.1], but it is
indeed equivalent, as explained in [12].

Cartesian differential categories are Cartesian left additive categories that
come equipped with a differential combinator, whose axioms capture the basic
properties of the directional derivative from multivariable differential
calculus. In the following definition, it is important to note that we follow
the convention used in more recent work on Cartesian differential categories
which flips the convention used in [6], so that the linear argument of the
derivative is in the second argument rather than in the first.

###### Definition 2.2

A Cartesian differential category [6, Definition 2.1.1] is a Cartesian left
additive category $\mathbb{X}$ equipped with a differential combinator
$\mathsf{D}$, which is a family of operators
$\mathbb{X}(A,B)\xrightarrow{\mathsf{D}}\mathbb{X}(A\times A,B)$, where for a
map $A\xrightarrow{f}B$, the resulting map $A\times
A\xrightarrow{\mathsf{D}[f]}B$ is called the derivative of $f$, and such that:

  1. [CD.1]

$\mathsf{D}[f+g]=\mathsf{D}[f]+\mathsf{D}[g]$ and $\mathsf{D}[0]=0$

  2. [CD.2]

${\mathsf{D}[f]\\!\circ\\!\langle
a,b+c\rangle\\!=\\!\mathsf{D}[f]\\!\circ\\!\langle
a,b\rangle\\!+\\!\mathsf{D}[f]\\!\circ\\!\langle a,c\rangle}$ and
$\mathsf{D}[f]\circ\langle a,0\rangle=0$

  3. [CD.3]

$\mathsf{D}[1_{\\_}A]=\pi_{\\_}1$ and
$\mathsf{D}[\pi_{\\_}j]=\pi_{\\_}j\circ\pi_{\\_}1$

  4. [CD.4]

$\mathsf{D}[\left\langle
f,g\right\rangle]=\left\langle\mathsf{D}[f],\mathsf{D}[g]\right\rangle$

  5. [CD.5]

$\mathsf{D}[g\circ f]=\mathsf{D}[g]\circ\langle
f\circ\pi_{\\_}0,\mathsf{D}[f]\rangle$

  6. [CD.6]

$\mathsf{D}\left[\mathsf{D}[f]\right]\circ\left\langle\langle
a,b\rangle,\langle 0,c\rangle\right\rangle=\mathsf{D}[f]\circ\langle
a,c\rangle$

  7. [CD.7]

${\mathsf{D}\left[\mathsf{D}[f]\right]\circ\left\langle\langle
a,b\rangle,\langle
c,0\rangle\right\rangle=\mathsf{D}\left[\mathsf{D}[f]\right]\circ\left\langle\langle
a,c\rangle,\langle b,0\rangle\right\rangle}$

To help with the intuition, it is useful to use the term logic of Cartesian
differential categories as introduced in [6, Section 4], which expresses the
differential combinator as:
$\mathsf{D}[f](a,b):=\frac{\mathsf{d}f(x)}{\mathsf{d}x}(a)\cdot b$. [CD.1]
says that the derivative of a sum is equal to the sum of the derivatives,
$\frac{\mathsf{d}f(x)+g(x)}{\mathsf{d}x}(a)\cdot
b=\frac{\mathsf{d}f(x)}{\mathsf{d}x}(a)\cdot
b+\frac{\mathsf{d}g(x)}{\mathsf{d}x}(a)\cdot b$, and that the derivative of
zero maps is zero, $\frac{\mathsf{d}0}{\mathsf{d}x}(a)\cdot b=0$. [CD.2] says
that derivatives are additive in their second argument, so that
$\frac{\mathsf{d}f(x)}{\mathsf{d}x}(a)\cdot(b+c)=\frac{\mathsf{d}f(x)}{\mathsf{d}x}(a)\cdot
b+\frac{\mathsf{d}f(x)}{\mathsf{d}x}(a)\cdot c$ and
$\frac{\mathsf{d}f(x)}{\mathsf{d}x}(a)\cdot 0=0$. [CD.3] tells us what the
derivatives of identity maps and projections maps are, so that
$\frac{\mathsf{d}x}{\mathsf{d}x}(a)\cdot b=b$ and
$\frac{\mathsf{d}\pi_{\\_}i(x_{\\_}0,x_{\\_}1)}{\mathsf{d}(x_{\\_}0,x_{\\_}1)}(a_{\\_}0,a_{\\_}1)\cdot(b_{\\_}0,b_{\\_}1)=b_{\\_}i$.
[CD.4] says the derivative of a pairing of maps is equal to the pairing of the
derivatives, $\frac{\mathsf{d}\langle f(x),g(x)\rangle}{\mathsf{d}x}(a)\cdot
b=\left\langle\frac{\mathsf{d}f(x)}{\mathsf{d}x}(a)\cdot
b,\frac{\mathsf{d}g(x)}{\mathsf{d}x}(a)\cdot b\right\rangle$. [CD.5] is the
chain rule which tells us what the derivative of a composition of functions
is, so $\frac{\mathsf{d}g\left(f(x)\right)}{\mathsf{d}x}(a)\cdot
b=\frac{\mathsf{d}g(y)}{\mathsf{d}y}(f(a))\cdot\left(\frac{\mathsf{d}f(x)}{\mathsf{d}x}(a)\cdot
b\right)$. The last two axioms [CD.6] and [CD.7] may look somewhat mysterious
but essentially they capture properties of partial differentiation. Indeed, in
any Cartesian differential category, one can define partial differentiation by
inserting zeros in the total differential [6, Section 4.5], which in the term
logic is written respectively as:
$\frac{\mathsf{d}f(x,b)}{\mathsf{d}x}(a)\cdot
c:=\frac{\mathsf{d}f(x,y)}{\mathsf{d}\langle x,y\rangle}(a,b)\cdot(c,0)$ and
$\frac{\mathsf{d}f(a,y)}{\mathsf{d}y}(b)\cdot
c:=\frac{\mathsf{d}f(x,y)}{\mathsf{d}\langle x,y\rangle}(a,b)\cdot(0,c)$.
Thus, [CD.6] tells us what the partial derivative in the second argument of a
derivative is, $\frac{\mathsf{d}\frac{\mathsf{d}f(x)}{\mathsf{d}x}(a)\cdot
z}{\mathsf{d}z}(b)\cdot c=\frac{\mathsf{d}f(x)}{\mathsf{d}x}(a)\cdot c$, while
[CD.7] captures the symmetry of the partial derivatives,
$\frac{\mathsf{d}\frac{\mathsf{d}f(x)}{\mathsf{d}x}(y)\cdot
b}{\mathsf{d}(y)}(a)\cdot
c=\frac{\mathsf{d}\frac{\mathsf{d}f(y)}{\mathsf{d}y}(x)\cdot
c}{\mathsf{d}(x)}(a)\cdot b$. We note that partial derivatives are also
differential combinators for the simple slice categories [6, Corollary 4.5.2],
and the total derivative is equal to the sum of the partial derivatives [6,
Lemma 4.5.1], that is, $\frac{\mathsf{d}f(x,y)}{\mathsf{d}\langle
x,y\rangle}(a,b)\cdot(c,d)=\frac{\mathsf{d}f(x,b)}{\mathsf{d}x}(a)\cdot
c+\frac{\mathsf{d}f(a,y)}{\mathsf{d}y}(b)\cdot d$. More discussion on the
differential combinator axioms can be found in [6, Remark 2.1.3].

Here are now our main examples of Cartesian differential categories (see [12]
for a list of more examples of Cartesian differential categories):

###### Example 2.3

Let $R$ be a commutative ring and let $R\text{-}\mathsf{MOD}$ be the category
of $R$-modules and $R$-linear maps between them. $R\text{-}\mathsf{MOD}$ is a
Cartesian differential category where for an $R$-linear map
$M\xrightarrow{f}N$, its derivative $M\times M\xrightarrow{\mathsf{D}[f]}N$ is
defined as $\mathsf{D}[f](x,y)=f(y)$. More generally, every category with
finite biproducts is a Cartesian differential category where
${\mathsf{D}[f]=f\circ\pi_{\\_}1}$.

###### Example 2.4

Let $\mathbb{R}$ be the set of real numbers. Define $\mathsf{SMOOTH}$ as the
category whose objects are the Euclidean real vector spaces $\mathbb{R}^{n}$
and whose maps are the real smooth functions
${\mathbb{R}^{n}\xrightarrow{F}\mathbb{R}^{m}}$ between them.
$\mathsf{SMOOTH}$ is a Cartesian differential category where the differential
combinator is defined as the directional derivative of a smooth function.
Recall that a smooth function $\mathbb{R}^{n}\xrightarrow{F}\mathbb{R}^{m}$ is
in fact a tuple $F=\langle f_{\\_}1,\ldots,f_{\\_}m\rangle$ of smooth
functions $\mathbb{R}^{n}\xrightarrow{f_{\\_}i}\mathbb{R}$. Then using the
convention that $\vec{x}\in\mathbb{R}^{n}$ are column vectors, the derivative
$\mathbb{R}^{n}\times\mathbb{R}^{n}\xrightarrow{\mathsf{D}[F]}\mathbb{R}^{m}$
is defined as multiplying the Jacobian matrix of $F$ at the first argument
$\vec{x}$, which is an $m\times n$ matrix $\mathbf{J}(F)(\vec{x})$, with the
second argument $\vec{y}$, seen as an $n\times 1$ matrix:

${\small\mathsf{D}[F](\vec{x},\vec{y}):=\mathbf{J}(F)(\vec{x})\vec{y}=\begin{bmatrix}\frac{\partial
f_{\\_}1}{\partial x_{\\_}1}(\vec{x})&\frac{\partial f_{\\_}1}{\partial
x_{\\_}2}(\vec{x})&\ldots&\frac{\partial f_{\\_}1}{\partial
x_{\\_}n}(\vec{x})\\\ \frac{\partial f_{\\_}2}{\partial
x_{\\_}1}(\vec{x})&\frac{\partial f_{\\_}2}{\partial
x_{\\_}2}(\vec{x})&\ldots&\frac{\partial f_{\\_}2}{\partial
x_{\\_}n}(\vec{x})\\\ \vdots&\vdots&\vdots&\vdots\\\ \frac{\partial
f_{\\_}m}{\partial x_{\\_}1}(\vec{x})&\frac{\partial f_{\\_}m}{\partial
x_{\\_}2}(\vec{x})&\ldots&\frac{\partial f_{\\_}m}{\partial
x_{\\_}n}(\vec{x})\end{bmatrix}\begin{bmatrix}y_{\\_}1\\\ y_{\\_}2\\\
\vdots\\\
y_{\\_}n\end{bmatrix}=\begin{bmatrix}\sum\limits^{n}_{\\_}{i=1}\frac{\partial
f_{\\_}1}{\partial x_{\\_}i}(\vec{x})y_{\\_}i\\\ \vdots\\\
\sum\limits^{n}_{\\_}{i=1}\frac{\partial f_{\\_}m}{\partial
x_{\\_}i}(\vec{x})y_{\\_}i\end{bmatrix}}$

When $m=1$, for a smooth function $\mathbb{R}^{n}\xrightarrow{f}\mathbb{R}$,
$\mathsf{D}[f](\vec{x},\vec{y})$ is precisely the directional derivative of
$f$ at point $\vec{x}$ and along the vector $\vec{y}$.

###### Example 2.5

An important source of examples of Cartesian differential categories is the
coKleisli categories of differential categories [5]. Very briefly (and leaving
out most of the details), a differential category [5, Definition 2.4] is a
symmetric monoidal category (with tensor product $\otimes$ and unit $k$) with
a comonad $\oc$ which comes equipped with a deriving transformation $\oc
A\otimes A\xrightarrow{\mathsf{d}}A$ satisfying certain coherences which
capture the basic algebraic properties of differentiation [4, Definition 7].
Examples of differential categories can be found in [4, Section 9]. By [6,
Proposition 3.2.1], when a differential category has finite products, the
coKleisli category of $\oc$ is a Cartesian differential category where the
differential combinator is defined using the deriving transformation.

An important class of maps in a Cartesian differential category are the linear
maps and maps which are linear in certain arguments. Essentially, a map is
linear in an argument if when differentiating with respect to that argument
(and keeping the other arguments constant), one gets back the starting map.

###### Definition 2.6

In a Cartesian differential category $\mathbb{X}$ with differential combinator
$\mathsf{D}$:

  1. (i)

A map $A\xrightarrow{f}B$ is linear [6, Definition 2.2.1] if
$\mathsf{D}[f]\circ\langle a,b\rangle=f\circ b$ (i.e.
$\frac{\mathsf{d}f(x)}{\mathsf{d}x}(a)\cdot b=f(b)$);

  2. (ii)

A map $A\times B\xrightarrow{f}C$ is linear in its first argument if $f$ is
linear with respect to the partial derivative in its first argument, that is,
$\mathsf{D}[f]\circ\left\langle\langle a,b\rangle,\langle
c,0\rangle\right\rangle=f\circ\langle c,b\rangle$ (i.e.
${\frac{\mathsf{d}f(x,b)}{\mathsf{d}x}(a)\cdot c=f(c,b)}$);

  3. (iii)

A map $A\times B\xrightarrow{f}C$ is linear in its second argument if $f$ is
linear with respect to the partial derivative in its second argument, that is,
$\mathsf{D}[f]\circ\left\langle\langle a,b\rangle,\langle
0,d\rangle\right\rangle=f\circ\langle a,d\rangle$ (i.e.
$\frac{\mathsf{d}f(a,y)}{\mathsf{d}y}(b)\cdot d=f(a,d)$);

  4. (iv)

A map $A\times B\xrightarrow{f}C$ is bilinear if it is linear in its first
argument and linear in its second argument, or equivalently if
$\mathsf{D}[f]\circ\left\langle\langle a,b\rangle,\langle
c,d\rangle\right\rangle=f\circ\langle a,d\rangle+f\circ\langle c,b\rangle$
(i.e.
${\frac{\mathsf{d}f(x,y)}{\mathsf{d}(x,y)}(a,b)\cdot(c,d)=f(a,d)+f(c,b)}$).

Define the subcategory of linear maps $\mathsf{Lin}[\mathbb{X}]$ to be the
category whose objects are the same as $\mathbb{X}$ and whose maps are linear
in $\mathbb{X}$, and let $\mathsf{U}:\mathsf{Lin}[\mathbb{X}]\to\mathbb{X}$ be
the obvious inclusion functor.

By [CD.6], for any map $f$, its derivative $\mathsf{D}[f]$ is linear in its
second argument, while by [CD.3], identity maps and projections are linear. In
fact, by [6, Lemma 2.2.2], linear maps are also closed under composition,
addition, and pairings, which implies that $\mathsf{Lin}[\mathbb{X}]$ is a
Cartesian left additive category with the same structure as $\mathbb{X}$.
Furthermore, every linear map is also additive (though the converse is not
always true), and as a result, the finite product structure of $\mathbb{X}$
becomes a finite biproduct structure in $\mathsf{Lin}[\mathbb{X}]$, where in
particular, the injection maps are defined as
$A\xrightarrow{\iota_{\\_}0:=\langle 1_{\\_}A,0\rangle}A\times B$ and
$B\xrightarrow{\iota_{\\_}1:=\langle 0,1_{\\_}B\rangle}A\times B$.

###### Example 2.7

In $R\text{-}\mathsf{MOD}$, every $R$-linear map is linear in the Cartesian
differential sense, so we have that
$\mathsf{Lin}[R\text{-}\mathsf{MOD}]=R\text{-}\mathsf{MOD}$. On the other
hand, $M\times M^{\prime}\xrightarrow{f}N$ is linear in its first argument
(resp. second argument) if and only if $f(x,y)=f(x,0)$ (resp.
$f(x,y)=f(0,y)$). Therefore, the only maps which are bilinear in the Cartesian
differential sense are the zero maps. The same story holds true for any
category with finite biproducts.

###### Example 2.8

In $\mathsf{SMOOTH}$, a smooth function
$\mathbb{R}^{n}\xrightarrow{F}\mathbb{R}^{m}$ is linear in the Cartesian
differential sense if and only if it is $\mathbb{R}$-linear in the classical
sense, that is, $F(s\vec{x}+t\vec{y})=sF(\vec{x})+tF(\vec{y})$ for all
$s,t\in\mathbb{R}$ and $\vec{x},\vec{y}\in\mathbb{R}^{n}$. So
$\mathsf{Lin}[\mathsf{SMOOTH}]$ is the category of $\mathbb{R}$-linear maps
between the $\mathbb{R}$-vector spaces $\mathbb{R}^{n}$. Similarly, a smooth
function $\mathbb{R}^{n}\times\mathbb{R}^{k}\xrightarrow{G}\mathbb{R}^{m}$ is
linear in its first argument (resp. second argument) if and only if it is
$\mathbb{R}$-linear in its first argument $\mathbb{R}^{n}$ (resp. second
argument $\mathbb{R}^{k}$), that is,
$G(s\vec{x}+t\vec{y},\vec{z})=sG(\vec{x},\vec{z})+tG(\vec{y},\vec{z})$ (resp.
$G(\vec{z},s\vec{x}+t\vec{y})=sG(\vec{z},\vec{x})+tG(\vec{z},\vec{x})$). Thus,
$\mathbb{R}^{n}\times\mathbb{R}^{k}\xrightarrow{G}\mathbb{R}^{m}$ is bilinear
if and only if it is $\mathbb{R}$-bilinear.

We conclude this section by reviewing Cartesian closed differential categories
(also sometimes called differential $\lambda$-categories [9, 20]). As the name
suggests, these are Cartesian differential categories whose underlying
category is also Cartesian closed and such that the differential combinator is
compatible with the curry operator. For a Cartesian closed category, we denote
the internal hom by $[A,B]$, the evaluation map by $[A,B]\times
A\xrightarrow{\epsilon}B$, and for a map $A\times B\xrightarrow{f}C$, its
curry is denoted $A\xrightarrow{\lambda(f)}[B,C]$.

###### Definition 2.9

A Cartesian closed differential category [10, Section 4.6] is a Cartesian
differential category which is also a Cartesian closed category such that all
evaluation maps $[A,B]\times A\xrightarrow{\epsilon}B$ are linear in their
first argument (note that this implies that
$\lambda(f+g)=\lambda(f)+\lambda(g)$ and $\lambda(0)=0$).

Here are now some examples of Cartesian closed differential categories.

###### Example 2.10

Every model of the differential $\lambda$-calculus [15] induces a Cartesian
closed differential category [10, Theorem 4.3], and conversely, every
Cartesian closed differential category induces a model of the differential
$\lambda$-calculus [9, Theorem 4.12].

###### Example 2.11

$R\text{-}\mathsf{MOD}$ and $\mathsf{SMOOTH}$ are not Cartesian closed
differential categories since neither is Cartesian closed.

###### Example 2.12

A differential storage category [4, Definition 10] is a differential category
with finite products and Seely isomorphisms, that is, $!(A\times B)\cong\oc
A\otimes\oc B$ and $\oc\top\cong k$ are isomorphisms. By [7, Theorem 4.4.2],
for a differential storage category whose base category is also symmetric
monoidal closed (with internal homs denoted by $A\multimap B$), the coKleisli
category is a Cartesian closed differential category where $[A,B]=\oc
A\multimap B$. Examples can be found in [9, Section 5].

###### Example 2.13

The category of convenient vector spaces and smooth functions between them is
a Cartesian closed differential category [21, Example 2.4.2]. For a detailed
introduction to convenient vector spaces, see [17]. Briefly, a convenient
vector space is a locally convex vector space $E$ such that for every smooth
function $\mathbb{R}\xrightarrow{c}E$, called a smooth curve, there exists
another smooth curve $\mathbb{R}\xrightarrow{\overline{c}}E$ such that
$\overline{c}^{\prime}=c$. If $E$ and $F$ are convenient vector spaces, then a
smooth function is a function $E\xrightarrow{f}F$ which preserves smooth
curves, that is, if $c$ is a smooth curve of $E$, then $f\circ c$ is a smooth
curve of $F$. Let $\mathsf{CON}$ be the category of convenient vector spaces
and smooth functions between them. $\mathsf{CON}$ is a Cartesian closed
differential category where the internal hom is given by
$[E,F]=\\{E\xrightarrow{f}F|~{}\text{$f$ is smooth}\\}$, which is indeed a
convenient vector space, and for a smooth function $E\xrightarrow{f}F$, its
derivative $E\times E\xrightarrow{\mathsf{D}[f]}F$ is defined as
$\mathsf{D}[f](x,y):=\lim\limits_{\\_}{t\to 0}\frac{f(x+ty)-f(x)}{t}$, where
$t\in\mathbb{R}$. Note that while $\mathsf{SMOOTH}$ is not Cartesian closed,
$\mathsf{SMOOTH}$ is a sub-Cartesian differential category of $\mathsf{CON}$.
Furthermore, $\mathsf{CON}$ is also the coKleisli category of a differential
storage category [8].

##  3 Linearly Closed Cartesian Differential Categories and Jacobians

In this section, we introduce the main contribution of this paper: linearly
closed Cartesian differential categories, which are the appropriate setting
for defining Jacobians (in the Fréchet/Gateaux derivative sense) in the
context of Cartesian differential categories.

###### Definition 3.1

A linearly closed Cartesian differential category is a Cartesian differential
category such that for each pair of objects $A$ and $B$, there is an object
$\mathcal{L}(A,B)$, called the internal linear hom, and a bilinear map
$\mathcal{L}(A,B)\times A\xrightarrow{\epsilon_{\\_}\ell}B$, called the
evaluation map, such that for every map $A\times B\xrightarrow{f}C$ which is
linear in its second argument, there exists a unique map
${A\xrightarrow{\lambda_{\\_}\ell(f)}\mathcal{L}(B,C)}$, called the linear
curry of $f$, such that $f=A\times B\xrightarrow{\lambda_{\\_}\ell(f)\times
1_{\\_}B}\mathcal{L}(B,C)\times B\xrightarrow{\varepsilon_{\\_}\ell}C$.

It is worth highlighting the major differences between being linearly closed
and Cartesian closed. (1) $\mathcal{L}(A,B)$ should be interpreted as the
internal version of $\mathsf{Lin}[\mathbb{X}](A,B)$, the linear maps from $A$
to $B$, while $[A,B]$ is the internal version of $\mathbb{X}(A,B)$, all maps
from $A$ to $B$. (2) The evaluation map $\mathcal{L}(A,B)\times
A\xrightarrow{\epsilon_{\\_}\ell}B$ is bilinear, while $[A,B]\times
A\xrightarrow{\epsilon}B$ is only linear in its first argument. The difference
here is due to the fact that linear maps are additive, while an arbitrary map
may not be. (3) In a linearly closed setting, we are only able to curry linear
arguments. (4) It is possible to be linearly closed and not Cartesian closed,
and vice versa. We stress that being linearly closed does not imply that
$\mathsf{Lin}[\mathbb{X}]$ is Cartesian closed. However, if a Cartesian
differential category $\mathbb{X}$ has a monoidal representation in the sense
of [7, Section 3.2], then we conjecture that being linearly closed is
equivalent to $\mathsf{Lin}[\mathbb{X}]$ being monoidal closed (this approach
has been studied by Gallagher and MacAdam [16], and we note that both
$\mathsf{SMOOTH}$ and $\mathsf{CON}$ have monoidal representation).

Now recall that [CD.6] says that for any map $f$, $\mathsf{D}[f]$ is linear in
its second argument. Therefore, the Jacobian of $f$ is defined as the linear
curry of its derivative:

###### Definition 3.2

In a linearly closed Cartesian differential category, the Jacobian of a map
$A\xrightarrow{f}B$ is the map $A\xrightarrow{\mathbf{J}(f)}\mathcal{L}(A,B)$
defined as the linear curry of $A\times A\xrightarrow{\mathsf{D}[f]}B$, that
is, $\mathbf{J}(f):=\lambda_{\\_}\ell(\mathsf{D}[f])$.

Here are now some examples of linearly closed Cartesian differential
categories and Jacobians:

###### Example 3.3

$R\text{-}\mathsf{MOD}$ is not a linearly closed Cartesian differential
category since the only bilinear maps are zero maps. The same is true for any
category with finite biproducts.

###### Example 3.4

$\mathsf{SMOOTH}$ is a linearly closed Cartesian differential category where
the internal linear hom is
$\mathcal{L}(\mathbb{R}^{n},\mathbb{R}^{m})=\mathbb{R}^{nm}$ and the
evaluation map
${\mathbb{R}^{nm}\times\mathbb{R}^{n}\xrightarrow{\epsilon_{\\_}\ell}\mathbb{R}^{m}}$
is defined as laying out the first argument, which is a column vector of size
$nm$, into a matrix of size $m\times n$ and then multiplying by the second
argument, seen as a matrix of size $n\times 1$:

${\small\epsilon_{\\_}\ell\left(\vec{x},\vec{y}\right):=\begin{bmatrix}x_{\\_}1&x_{\\_}2&\ldots&x_{\\_}n\\\
x_{\\_}{n+1}&x_{\\_}{n+2}&\ldots&x_{\\_}{2n}\\\ \vdots&\vdots&\vdots&\vdots\\\
x_{\\_}{(m-1)n+1}&x_{\\_}{(m-1)n+2}&\ldots&x_{\\_}{mn}\end{bmatrix}\begin{bmatrix}y_{\\_}1\\\
y_{\\_}2\\\ \vdots\\\
y_{\\_}n\end{bmatrix}=\begin{bmatrix}\sum\limits^{n}_{\\_}{i=1}x_{\\_}{i}y_{\\_}i\\\
\vdots\\\ \sum\limits^{n}_{\\_}{i=1}x_{\\_}{(m-1)n+i}y_{\\_}i\end{bmatrix}}$

When $m=1$, the evaluation map is given by the dot product of vectors
$\epsilon_{\\_}\ell(\vec{x},\vec{y})=\vec{x}\cdot\vec{y}=\sum\limits^{n}_{\\_}{i=1}x_{\\_}{i}y_{\\_}i$.
To define the linear curry, let $e_{\\_}i\in\mathbb{R}^{n}$ be the canonical
basis vectors, $e_{\\_}i=[0,\ldots,0,1,0,\ldots,0]^{\mathsf{T}}$. Then for a
smooth function $\mathbb{R}^{n}\times\mathbb{R}^{k}\xrightarrow{G=\langle
g_{\\_}1,\ldots,g_{\\_}m\rangle}\mathbb{R}^{m}$, which is linear in its second
argument, define $\mathbb{R}^{n}\xrightarrow{\lambda(G)}\mathbb{R}^{km}$ as
$\lambda(G)(\vec{x})=[g_{\\_}1(\vec{x},e_{\\_}1),\ldots,g_{\\_}1(\vec{x},e_{\\_}k),g_{\\_}2(\vec{x},e_{\\_}1),\ldots,g_{\\_}m(\vec{x},e_{\\_}k)]^{\mathsf{T}}$.
For a smooth function ${\mathbb{R}^{n}\xrightarrow{F=\langle
f_{\\_}1,\ldots,f_{\\_}m\rangle}\mathbb{R}^{m}}$, taking
$\mathbf{J}(F)(\vec{x})=\lambda_{\\_}\ell(\mathsf{D}[F])(\vec{x})$ results
precisely in the Jacobain matrix of $F$ at $\vec{x}$ interpreted as column
vector of size $nm$, $\mathbf{J}(F)(\vec{x})=[\frac{\partial
f_{\\_}1}{\partial x_{\\_}1}(\vec{x}),\ldots,\frac{\partial f_{\\_}1}{\partial
x_{\\_}n}(\vec{x}),\frac{\partial f_{\\_}2}{\partial
x_{\\_}1}(\vec{x}),\ldots,\frac{\partial f_{\\_}m}{\partial
x_{\\_}n}(\vec{x})]^{\mathsf{T}}$, which when post-composed in the evaluation
map results in laying it out back into an $m\times n$ matrix.

###### Example 3.5

For a differential category with finite products, if the base category is
symmetric monoidal closed, then the coKleisli category will be a linearly
closed differential category where the internal linear hom is given by
$\mathcal{L}(A,B):=A\multimap B$. For a coKleisli map $\oc A\xrightarrow{f}B$,
its Jacobian $\oc A\xrightarrow{\mathbf{J}(f)}A\multimap B$ is define as the
curry in the base symmetric monoidal category of the composite $\oc A\otimes
A\xrightarrow{d}\oc A\xrightarrow{f}B$. Note that unlike in the Cartesian
closed case, we do not need to assume the presence of Seely isomorphisms for
the linearly closed case. That said, it can be shown that the coKleisli
category of a differential storage category is linearly closed if and only if
the base category is symmetric monoidal closed. Furthermore, this internal
linear hom captures the notion of linear types in Vákár’s work on automatic
differentiation [23].

###### Example 3.6

$\mathsf{CON}$ is a linearly closed Cartesian differential category where the
internal linear hom is $\mathcal{L}(E,F)=\\{E\xrightarrow{f}F|~{}\text{$f$ is
smooth and $\mathbb{R}$-linear}\\}\subset[E,F]$, and the evaluation map
$\mathcal{L}(E,F)\times E\xrightarrow{\epsilon_{\\_}\ell}F$ is defined in the
obvious way, $\epsilon_{\\_}\ell(f,x)=f(x)$. A smooth function $E\times
E^{\prime}\xrightarrow{g}F$ is linear in its second argument if and only if
$g$ is $\mathbb{R}$-linear in its second argument. So if $g$ is linear in its
second argument, then
$E\xrightarrow{\lambda_{\\_}\ell(g)}\mathcal{L}(E^{\prime},F)$ is defined as
$\lambda_{\\_}\ell(g)(x)(y)=g(x,y)$. For a smooth function
$E\xrightarrow{f}F$, its Jacobian
$E\xrightarrow{\mathbf{J}(f)}\mathcal{L}(E,F)$ is defined as
$\mathbf{J}(f)(x)(y)=\mathsf{D}[f](x,y)$.

Being linearly closed shares many similar looking properties to being
Cartesian closed. In term logic notation, we write
$\lambda_{\\_}\ell(f)(a)=\lambda_{\\_}\ell y.f(a,y)$ and
$\epsilon_{\\_}\ell(g,a)=g(a)$, and $\left(\lambda_{\\_}\ell
y.f(a,y)\right)(b)=f(a,b)$, and so $\mathbf{J}(f)(a)=\lambda_{\\_}\ell
y.\frac{\mathsf{d}f(x)}{\mathsf{d}x}(a)\cdot y$.

###### Proposition 3.7

Let $\mathbb{X}$ be a linearly closed Cartesian differential category.

  1. 1.

$\lambda_{\\_}\ell(f+g)=\lambda_{\\_}\ell(f)+\lambda_{\\_}\ell(g)$ and
$\lambda_{\\_}\ell(0)=0$.

  2. 2.

$\mathsf{D}[\lambda_{\\_}\ell(f)]=\lambda_{\\_}\ell\left(\mathsf{D}[f]\circ\left\langle\langle\pi_{\\_}0\circ\pi_{\\_}0,0\rangle,\langle\pi_{\\_}1\circ\pi_{\\_}0,\pi_{\\_}1\rangle\right\rangle\right)$
(i.e. $\frac{\mathsf{d}\lambda_{\\_}\ell y.f(x,y)}{\mathsf{d}x}(a)\cdot
b=\lambda_{\\_}\ell y.\frac{\mathsf{d}f(x,y)}{\mathsf{d}x}(a)\cdot c$).

  3. 3.

There is a functor
$\mathsf{LIN}[\mathbb{X}]^{op}\times\mathsf{LIN}[\mathbb{X}]\xrightarrow{\mathcal{L}}\mathsf{LIN}[\mathbb{X}]$
which maps a pair of object to the internal linear hom $\mathcal{L}(A,B)$, and
sends a pair of linear maps $A\xrightarrow{f}B$ and $X\xrightarrow{g}Y$ to the
linear map $\mathcal{L}(B,X)\xrightarrow{\mathcal{L}(f,g)}\mathcal{L}(A,Y)$
defined as the linear curry of $\mathcal{L}(B,X)\times A\xrightarrow{1\times
f}\mathcal{L}(B,X)\times B\xrightarrow{\epsilon_{\\_}\ell}X\xrightarrow{g}Y$.

  4. 4.

There are natural isomorphisms: (i) $\mathcal{L}(A,B\times
C)\cong\mathcal{L}(A,B)\times\mathcal{L}(A,C)$, (ii)
$\mathcal{L}(A,C)\times\mathcal{L}(B,C)\cong\mathcal{L}(A\times B,C)$, (iii)
$\mathcal{L}(A,\top)\cong\top\cong\mathcal{L}(\top,A)$, and (iv)
$\mathcal{L}\left(A,\mathcal{L}(B,C)\right)\cong\mathcal{L}\left(B,\mathcal{L}(A,C)\right)$.

######  Proof 3.1.

(Sketch) The computations for (1) and (2) are essentially the same as those in
[10, Lemma 4.10]. The proofs that $\mathcal{L}$ is a functor,
$\mathcal{L}(A,\top)\cong\top$, $\mathcal{L}(A,B\times
C)\cong\mathcal{L}(A,B)\times\mathcal{L}(A,C)$, and
$\mathcal{L}\left(A,\mathcal{L}(B,C)\right)\cong\mathcal{L}\left(B,\mathcal{L}(A,C)\right)$
are essentially the same as in the Cartesian closed case. On the other hand,
$\top\cong\mathcal{L}(\top,A)$ and
$\mathcal{L}(A,C)\times\mathcal{L}(B,C)\cong\mathcal{L}(A\times B,C)$
intuitively follow from the fact that $\top$ is an initial object and $\times$
is a coproduct in $\mathsf{LIN}[\mathbb{X}]$. In other words, the only linear
map of type $\top\to A$ is $0$, while a linear map of type $A\times B\to C$ is
actually a pair of linear maps $A\to C$ and $B\to C$.

We conjecture that being linearly closed induces a non-unital closed category
structure on $\mathsf{LIN}[\mathbb{X}]$. The non-unital part comes from the
fact that there may not be an object $R$ such that $A\cong\mathcal{L}(R,A)$
for all objects $A$. While both $\mathsf{SMOOTH}$ and $\mathsf{CON}$ have such
an object, namely $R=\mathbb{R}$, if we take $\mathsf{SMOOTH}_{\\_}{even}$ the
subcategory of Euclidean spaces of even dimension, then
$\mathsf{SMOOTH}_{\\_}{even}$ is still a linearly closed Cartesian
differential category, but does not have a unit. In future work, it will be of
interest to study linearly closed Cartesian differential categories with both
a unit and monoidal representation. Furthermore, note that in the Cartesian
closed setting we have that $[A,[B,C]]\cong[A\times B,C]$, but in the linearly
closed setting, $\mathcal{L}\left(A,\mathcal{L}(B,C)\right)$ represents the
bilinear maps $A\times B\to C$, which is different from
$\mathcal{L}\left(A\times B,C\right)$, which represents the linear maps
$A\times B\to C$, and so
$\mathcal{L}\left(A,\mathcal{L}(B,C)\right)\ncong\mathcal{L}\left(A\times
B,C\right)$.

Next we turn our attention to properties of the Jacobian. In particular, we
provide analogues of three basic classical identities: (1)
$\mathbf{J}(F+G)(\vec{x})=\mathbf{J}(F)(\vec{x})+\mathbf{J}(G)(\vec{x})$, (2)
if $F$ is $\mathbb{R}$-linear with associated matrix $A$ (i.e.
$F(\vec{x})=A\vec{x}$) then $\mathbf{J}(F)(\vec{x})=A$, and (3)
$\mathbf{J}(G\circ
F)(\vec{x})=\mathbf{J}(G)(F(\vec{x}))\mathbf{J}(F)(\vec{x})$. The first
identity is easy to generalize, while the latter two requires defining some
extra maps. For a linear map $A\xrightarrow{f}B$, let
$\top\xrightarrow{p_{\\_}f}\mathcal{L}(A,B)$ be the linear curry of the
composite $\top\times A\xrightarrow{\pi_{\\_}1}A\xrightarrow{f}B$, so in term
logic notation $p_{\\_}f=\lambda_{\\_}\ell x.f(x)$. Next, define the map
${\mathcal{L}(B,C)\times\mathcal{L}(A,B)\xrightarrow{\odot}\mathcal{L}(A,C)}$
as the linear curry of the composite
${\mathcal{L}(B,C)\times\mathcal{L}(A,B)\times
A\xrightarrow{1_{\\_}{\mathcal{L}(B,C)}\times\varepsilon_{\\_}\ell}\mathcal{L}(B,C)\times
B\xrightarrow{\varepsilon_{\\_}\ell}C}$, and note that $\odot$ captures
composition of linear maps, which we write in term logic notation as $g\odot
f=\lambda_{\\_}\ell x.g(f(x))$. We leave it to the reader to check for
themselves that in $\mathsf{SMOOTH}$, if
${\mathbb{R}^{n}\xrightarrow{F}\mathbb{R}^{m}}$ is an $\mathbb{R}$-linear map
with associated $n\times m$ matrix $A$, then $p_{\\_}F$ is precisely $A$ in
column vector form, while composition of $\mathbb{R}$-linear maps corresponds
to matrix multiplication, and so $\odot$ plays the role of matrix
multiplication.

######  Proposition 3.2.

In a linearly closed Cartesian differential category:

  1. (i)

$\mathbf{J}(f+g)=\mathbf{J}(f)+\mathbf{J}(g)$ and $\mathbf{J}(0)=0$ (i.e.
$\mathbf{J}(f+g)(a)=\mathbf{J}(f)(a)+\mathbf{J}(g)(a)$ and
$\mathbf{J}(0)(a)=0$).

  2. (ii)

If $A\xrightarrow{f}B$ is linear, then $\mathbf{J}(f)=p_{\\_}f\circ 0$ (i.e.
$\mathbf{J}(f)(a)=\lambda_{\\_}\ell x.f(x)$).

  3. (iii)

$\mathbf{J}(g\circ f)=\odot\circ\langle\mathbf{J}(g)\circ
f,\mathbf{J}(f)\rangle$ (i.e. $\mathbf{J}(g\circ
f)(a)=\mathbf{J}(g)(f(a))\odot\mathbf{J}(f)(a)$)

######  Proof 3.3.

(Sketch) The first identity follows immediately from [CD.1] and Proposition
3.7.(1). For the second identity, if $f$ is linear then using the term logic
we compute: $\mathbf{J}(f)(a)=\lambda_{\\_}\ell
y.\frac{\mathsf{d}f(x)}{\mathsf{d}x}(a)\cdot y=\lambda_{\\_}\ell y.f(y)$.
Lastly for the third identity, we use the chain rule [CD.5] to compute:
$\mathbf{J}(g\circ f)(a)=\lambda_{\\_}\ell
y.\frac{\mathsf{d}g(f(x))}{\mathsf{d}x}(a)\cdot y=\lambda_{\\_}\ell
y.\frac{\mathsf{d}g(z)}{\mathsf{d}z}(f(a))\cdot\left(\frac{\mathsf{d}f(x)}{\mathsf{d}x}(a)\cdot
y\right)=\lambda_{\\_}\ell
y.\mathbf{J}(g)(f(a))\left(\mathbf{J}(f)(a)(y)\right)=\mathbf{J}(g)(f(a))\odot\mathbf{J}(f)(a)$.

We conjecture that it is possible to provide an equivalent alternative
axiomatization of a linearly closed Cartesian differential category as a
Cartesian left additive category equipped with $\mathcal{L}(-,-)$,
$\varepsilon_{\\_}\ell$, and $\mathbf{J}$, where one would define the
differential combinator as
$\mathsf{D}[-]=\varepsilon_{\\_}\ell\circ(\mathbf{J}(-)\times 1)$. While this
is definitely of interest, it does require a bit of work to properly set up
everything. As such, this will be a story for another time.

We finish this section by providing necessary and sufficient conditions for
when a Cartesian closed differential category is also linearly closed, and
then explaining how every Cartesian closed differential category embeds into a
linearly closed Cartesian differential category via splitting linear
idempotents. We start with the definition of linear idempotents splitting
linearly (which is a special case of [10, Section 4.5]):

######  Definition 3.4.

In a Cartesian differential category, a linear split idempotent is an
idempotent $A\xrightarrow{e}A$ which is linear and such that there are linear
maps $A\xrightarrow{r}B$ and $B\xrightarrow{s}A$ such that $s\circ r=e$ and
$r\circ s=1_{\\_}B$. A linear idempotent complete Cartesian differential
category is a Cartesian differential category such that all linear idempotents
are linear split idempotents.

The key idea is that we will define a linear idempotent on the internal hom
$[A,B]$ which linearly splits via the internal linear hom $\mathcal{L}(A,B)$.
To define this idempotent, we will require the notion of partial linearization
[12, Proposition 5.5]. So for a map $A\times B\xrightarrow{f}C$, its
linearization in context $A$ is the map $A\times
B\xrightarrow{\mathsf{L}^{A}[f]}C$ defined as
$\mathsf{L}^{A}[f]:=\mathsf{D}[f]\circ\langle\langle\pi_{\\_}0,0\rangle,\langle
0,\pi_{\\_}1\rangle\rangle$, i.e.
$\mathsf{L}^{A}[f](a,b)=\frac{\mathsf{d}f(a,y)}{\mathsf{d}y}(0)\cdot b$. The
map $\mathsf{L}^{A}[f]$ is now linear in its second argument. So in a
Cartesian closed differential category, define
${[A,B]\xrightarrow{\ell}[A,B]}$ as the linear curry of the partial
linearization of the evaluation map ${[A,B]\times
A\xrightarrow{\mathsf{L}^{[A,B]}\left[\epsilon\right]}B}$, that is,
$\ell=\lambda_{\\_}\ell\left(\mathsf{L}^{[A,B]}\left[\epsilon\right]\right)$.
In term logic notation, we have that $\ell(f)=\lambda_{\\_}\ell
y.\frac{\mathsf{d}f(x)}{\mathsf{d}x}(0)\cdot y$, and so $\ell$ is understood
as mapping an arbitrary map $f$ to its linearization [12, Proposition 3.6]. As
such, it follows that $\ell$ is a linear idempotent.

######  Proposition 3.5.

A Cartesian closed differential category is linearly closed if and only if
$[A,B]\xrightarrow{\ell}[A,B]$ is a linear split idempotent.

######  Proof 3.6.

(Sketch) Suppose that our Cartesian closed differential category is also
linearly closed. As explained above, $\ell$ is already idempotent and linear.
So it remains to construct a linear splitting of $\ell$. First consider the
curry of the evaluation map for the linear closed structure,
$\mathcal{L}(A,B)\xrightarrow{\lambda(\epsilon_{\\_}\ell)}[A,B]$, which is
linear since $\epsilon_{\\_}\ell$ was linear in its first argument. Next,
consider the linear curry of the partial linearization of the evaluation map
for the Cartesian closed structure,
$[A,B]\xrightarrow{\lambda_{\\_}\ell\left(\mathsf{L}^{[A,B]}[\epsilon]\right)}\mathcal{L}(A,B)$,
which is also linear since $\mathsf{L}^{[A,B]}[\epsilon]$ is linear in its
first argument. Then it follows that
$\lambda_{\\_}\ell\left(\mathsf{L}^{[A,B]}[\epsilon]\right)\circ\lambda(\epsilon_{\\_}\ell)=1_{\\_}{\mathcal{L}(A,B)}$
and
$\lambda(\epsilon_{\\_}\ell)\circ\lambda_{\\_}\ell\left(\mathsf{L}^{[A,B]}[\epsilon]\right)=\ell$.
So $\ell$ is a linear split idempotent. Conversely, suppose that
$[A,B]\xrightarrow{\ell}[A,B]$ is a linear split idempotent via
$[A,B]\xrightarrow{r}\mathcal{L}(A,B)$ and
$\mathcal{L}(A,B)\xrightarrow{s}[A,B]$. Then the internal linear hom is given
by the object of the splitting $\mathcal{L}(A,B)$, while the evaluation map is
defined as the composite $\epsilon_{\\_}\ell:=\mathcal{L}(A,B)\times
A\xrightarrow{s\times 1_{\\_}A}[A,B]\times
A\xrightarrow{\mathsf{L}^{[A,B]}[\epsilon]}B$, which is bilinear since
$\mathsf{L}^{[A,B]}[\epsilon]$ is bilinear and $s$ is linear. The linear curry
of a map $A\times B\xrightarrow{f}C$ which is linear in its second argument is
defined as the composite
$\lambda_{\\_}\ell(f):=A\xrightarrow{\lambda(f)}[A,B]\xrightarrow{r}\mathcal{L}(A,B)$.
So our Cartesian closed differential category is linearly closed.

In a Cartesian closed differential category which is also linearly closed, for
a map $A\times B\xrightarrow{f}C$ which is linear in its second argument, its
curry $A\xrightarrow{\lambda(f)}[B,C]$ factors through its linear curry
$A\xrightarrow{\lambda_{\\_}\ell(f)}\mathcal{L}(B,C)$ in the sense that
$\lambda(f)=A\xrightarrow{\lambda_{\\_}\ell(f)}\mathcal{L}(B,C)\xrightarrow{s}[A,B]$.
It is also worth pointing out that while it is true that $[A,B]\times
A\xrightarrow{\mathsf{L}^{[A,B]}\left[\epsilon\right]}B$ is bilinear and that
if $A\times B\xrightarrow{f}C$ is linear in its second argument then we also
have that $f=\mathsf{L}^{[B,C]}\left[\epsilon\right]\circ(\lambda(f)\times
1_{\\_}B)$, this does not give a linearly closed structure since $\lambda(f)$
may fail the uniqueness requirement (i.e.
$\mathsf{L}^{[A,B]}\left[\epsilon\right]$ is not monic in its first argument).
For example, we have that
$\mathsf{L}^{[A,B]}\left[\epsilon\right]=\mathsf{L}^{[A,B]}\left[\epsilon\right]\circ(\ell\times
1_{\\_}A)$ but $\ell\neq 1_{\\_}{[A,B]}$.

Given any Cartesian differential category, we may build its linear idempotent
completion in the obvious way. For a Cartesian differential category
$\mathbb{X}$, let $\mathsf{LS}[\mathbb{X}]$ be the category whose objects are
pairs $(A,A\xrightarrow{e}A)$ consisting of an object $A$ and a linear
idempotent $e$ of $\mathbb{X}$ and whose maps
$(A,e)\xrightarrow{f}(B,e^{\prime})$ are maps $A\xrightarrow{f}B$ $\mathbb{X}$
such that $f\circ e=e^{\prime}\circ f$. By [12, Proposition 4.7, Corollary
4.1], $\mathsf{LS}[\mathbb{X}]$ is a Cartesian differential category where the
differential combinator is defined as in $\mathbb{X}$, and
$\mathsf{LS}[\mathbb{X}]$ is also linear idempotent complete. Furthermore, if
$\mathbb{X}$ was a Cartesian closed differential category, then
$\mathsf{LS}[\mathbb{X}]$ is also a Cartesian closed differential category.
Therefore, putting all of this together, we obtain the following:

######  Proposition 3.7.

If $\mathbb{X}$ is a Cartesian closed differential category, then
$\mathsf{LS}[\mathbb{X}]$ is a linearly closed Cartesian closed differential
category.

##  4 Cartesian Reverse Differential Categories and Gradients

In most of the standard conventions of calculus, the gradient of a scalar-
valued smooth function is the transpose of its Jacobian. In this section, we
explain how Cartesian reverse differential categories are the appropriate
setting in which to define gradients and transposes. We briefly review
Cartesian reverse differential categories and invite readers to see the full
story in the original paper [11].

######  Definition 4.1.

A Cartesian reverse differential category is a Cartesian left additive
category $\mathbb{X}$ equipped with a reverse differential combinator
$\mathsf{R}$, which is a family of operators
$\mathbb{X}(A,B)\xrightarrow{\mathsf{R}}\mathbb{X}(A\times B,A)$, where for a
map $A\xrightarrow{f}B$, the resulting map $A\times
B\xrightarrow{\mathsf{R}[f]}A$ is called the reverse derivative of $f$, and
such that the seven axioms found in [11, Definition 13] hold.

######  Example 4.2.

$\mathsf{SMOOTH}$ is a Cartesian reverse differential category where for a
smooth function of type $\mathbb{R}^{n}\xrightarrow{F}\mathbb{R}^{m}$,
$F=\langle f_{\\_}1,\ldots,f_{\\_}m\rangle$, its reverse derivative
$\mathbb{R}^{n}\times\mathbb{R}^{m}\xrightarrow{\mathsf{R}[F]}\mathbb{R}^{n}$
is defined by multiplying the transpose of the Jacobian matrix of $F$ at the
first argument $\vec{x}$, which is an $n\times m$ matrix
$\mathbf{J}(F)(\vec{x})^{\mathsf{T}}$, with the second argument $\vec{y}$,
viewed as an $m\times 1$ matrix:

${\small\mathsf{R}[F](\vec{x},\vec{y}):=\mathbf{J}(F)(\vec{x})^{\mathsf{T}}\vec{y}=\begin{bmatrix}\frac{\partial
f_{\\_}1}{\partial x_{\\_}1}(\vec{x})&\frac{\partial f_{\\_}2}{\partial
x_{\\_}1}(\vec{x})&\ldots&\frac{\partial f_{\\_}m}{\partial
x_{\\_}1}(\vec{x})\\\ \frac{\partial f_{\\_}1}{\partial
x_{\\_}2}(\vec{x})&\frac{\partial f_{\\_}2}{\partial
x_{\\_}2}(\vec{x})&\ldots&\frac{\partial f_{\\_}m}{\partial
x_{\\_}2}(\vec{x})\\\ \vdots&\vdots&\vdots&\vdots\\\ \frac{\partial
f_{\\_}1}{\partial x_{\\_}n}(\vec{x})&\frac{\partial f_{\\_}2}{\partial
x_{\\_}n}(\vec{x})&\ldots&\frac{\partial f_{\\_}m}{\partial
x_{\\_}n}(\vec{x})\end{bmatrix}\begin{bmatrix}y_{\\_}1\\\ y_{\\_}2\\\
\vdots\\\
y_{\\_}m\end{bmatrix}=\begin{bmatrix}\sum\limits^{m}_{\\_}{j=1}\frac{\partial
f_{\\_}j}{\partial x_{\\_}1}(\vec{x})y_{\\_}j\\\ \vdots\\\
\sum\limits^{m}_{\\_}{j=1}\frac{\partial f_{\\_}j}{\partial
x_{\\_}n}(\vec{x})y_{\\_}j\end{bmatrix}}$

When $m=1$, for a smooth function $\mathbb{R}^{n}\xrightarrow{f}\mathbb{R}$,
recall that its gradient at $\vec{x}\in\mathbb{R}^{n}$ is defined as
$\nabla(f)(\vec{x})=\mathbf{J}(F)(\vec{x})^{\mathsf{T}}=[\frac{\partial
f}{\partial x_{\\_}1}(\vec{x}),\ldots,\frac{\partial f_{\\_}1}{\partial
x_{\\_}n}(\vec{x})]^{\mathsf{T}}$. So its reverse derivative
$\mathbb{R}^{n}\times\mathbb{R}\xrightarrow{\mathsf{R}[f]}\mathbb{R}^{n}$ is
given by multiplying its gradient at $\vec{x}$ with the scalar in the second
argument, $\mathsf{R}[f](\vec{x},y)=\nabla(f)(\vec{x})y$.

Every Cartesian reverse differential category is also a Cartesian differential
category [11, Theorem 16], where the differential combinator $\mathsf{D}$ is
induced by the reverse differential combinator $\mathsf{R}$. Explicitly, for a
map $A\xrightarrow{f}B$, note that its second order reverse derivative is of
type $(A\times B)\times
A\xrightarrow{\mathsf{R}\left[\mathsf{R}[f]\right]}A\times B$. Then the
derivative of $f$ is defined as the composite $\mathsf{D}[f]:=A\times
A\xrightarrow{\langle 1_{\\_}A,0\rangle\times 1_{\\_}A}(A\times B)\times
A\xrightarrow{\mathsf{R}\left[\mathsf{R}[f]\right]}A\times
B\xrightarrow{\pi_{\\_}1}B$. Conversely, every Cartesian differential category
with a contextual linear dagger [11, Definition 39] is a Cartesian reverse
differential category [11, Theorem 41]. Very briefly, a contextual linear
dagger amounts to an operator $(-)^{\dagger[-]}$ which sends every map
$A\times B\xrightarrow{f}C$ which is linear in its second argument to a map
$A\times C\xrightarrow{f^{\dagger[A]}}B$ which is again linear in its second
argument, and such that $(-)^{\dagger[A]}$ makes the category of maps which
are linear in context $A$ into a $\dagger$-category with finite
$\dagger$-biproducts. Then the reverse derivative of a map $A\xrightarrow{f}B$
is defined by the taking the dagger in context of its derivative, that is,
$\mathsf{R}[f]:=A\times B\xrightarrow{\mathsf{D}[f]^{\dagger[A]}}B$.
Furthermore, these constructions are inverses of each other [11, Theorem 42].

In a Cartesian reverse differential category, for any map $f$, its reverse
derivative $\mathsf{R}[f]$ is linear in its second argument. Therefore we
define the gradient of $f$ as the linear curry of its reverse derivative:

######  Definition 4.3.

A linearly closed Cartesian reverse differential category is a Cartesian
reverse differential category whose induced Cartesian differential structure
is linearly closed. In a linearly closed Cartesian reverse differential
category, the gradient of a map $A\xrightarrow{f}B$ is the map
$A\xrightarrow{\nabla(f)}\mathcal{L}(B,A)$ defined as the linear curry of
$A\times B\xrightarrow{\mathsf{R}[f]}A$, that is,
$\nabla(f):=\lambda_{\\_}\ell(\mathsf{R}[f])$.

Let us explain why this is the correct definition of the gradient by proving
that it is the transpose of the Jacobian. To do so, we first need the notion
of a transpose operator:

######  Definition 4.4.

A linearly closed Cartesian differential category has a linear transpose if
for every pair of objects $A$ and $B$, there is a linear map
$\mathcal{L}(A,B)\xrightarrow{\tau}\mathcal{L}(B,A)$ such that (i)
$\tau\circ\tau=1$, (ii) $\tau\circ p_{\\_}{1_{\\_}A}=p_{\\_}{1_{\\_}A}$ and
$\tau\circ p_{\\_}{\pi_{\\_}j}=\tau\circ p_{\\_}{\iota_{\\_}j}$, and (iii)
$\tau\circ\odot=\odot\circ\langle\tau\circ\pi_{\\_}1,\tau\circ\pi_{\\_}0\rangle$.

As we will see below, it turns out that in the linearly closed setting, having
a linear transpose is equivalent to having a contextual linear dagger (and so
also to having a reverse differential combinator). Therefore, the linear
transpose axioms are analogues of the fact that in a Cartesian reverse
differential category, $\mathsf{Lin}[\mathbb{X}]$ is a $\dagger$-category with
$\dagger$-biproducts [11, Proposition 24], and so $\tau(f)=f^{\dagger}$.
Explicitly, (i) captures the fact $\dagger$ is an involution
${f^{\dagger}}^{\dagger}=f$, (ii) captures the fact that $\dagger$ maps
identities to identities, $1^{\dagger}=1$, and projections to injections,
$\pi_{\\_}j^{\dagger}=\iota_{\\_}j$, while (iii) tells us that $\dagger$ is
contravariant, $(g\circ f)^{\dagger}=f^{\dagger}\circ g^{\dagger}$. In
$\mathsf{SMOOTH}$, if ${\mathbb{R}^{n}\xrightarrow{F}\mathbb{R}^{m}}$ is an
$\mathbb{R}$-linear map with associated $n\times m$ matrix $A$, then
$F^{\dagger}$ is the $\mathbb{R}$-linear map given by the transpose matrix
$A^{\mathsf{T}}$, and so $\tau$ does indeed plays the role of the matrix
transpose operation.

######  Proposition 4.5.

A linearly closed Cartesian reverse differential category is precisely a
linearly closed Cartesian differential category equipped with a linear
transpose. Furthermore:

  1. (i)

$f^{\dagger[A]}=\varepsilon_{\\_}\ell^{\dagger[\mathcal{L}(A,B)]}\circ(\lambda_{\\_}\ell(f)\times
1)$.

  2. (ii)

$\lambda_{\\_}\ell(f^{\dagger[A]})=\tau\circ\lambda_{\\_}\ell(f)$.

  3. (iii)

$\nabla(f)=\tau\circ\mathbf{J}(f)$.

  4. (iv)

$\nabla(f+g)=\nabla(f)+\nabla(g)$ and $\nabla(0)=0$.

  5. (v)

If $f$ is linear then $\nabla(f)=p_{\\_}{f^{\dagger}}\circ 0$.

  6. (vi)

$\nabla(g\circ f)=\odot\circ\langle\nabla(f),\nabla(g)\circ f\rangle$.

######  Proof 4.6.

(Sketch) Starting with a linearly closed Cartesian reverse differential
category, first consider the contextual linear dagger of the evaluation map
$\mathcal{L}(A,B)\times
B\xrightarrow{\varepsilon_{\\_}\ell^{\dagger[\mathcal{L}(A,B)]}}A$, and define
the transpose map as its linear curry
$\mathcal{L}(A,B)\xrightarrow{\tau=\lambda_{\\_}\ell\left(\varepsilon_{\\_}\ell^{\dagger[\mathcal{L}(A,B)]}\right)}\mathcal{L}(B,A)$.
Then $\tau$ is a linear transpose since, as explained above, the linear
transpose axioms will follow from the fact that $\mathsf{Lin}[\mathbb{X}]$ is
a $\dagger$-category with $\dagger$-biproducts. Conversely, starting with a
linearly closed Cartesian differential category with a linear transpose
$\tau$, it suffices to construct a contextual linear dagger. For a map
$A\times B\xrightarrow{f}C$ which is linear in its second argument, we define
its dagger as $f^{\dagger[A]}:=A\times C\xrightarrow{\lambda(f)\times
1_{\\_}C}\mathcal{L}(B,C)\times C\xrightarrow{\tau\times
1_{\\_}C}\mathcal{L}(C,B)\times C\xrightarrow{\varepsilon_{\\_}\ell}B$. So we
obtain a linearly closed Cartesian reverse differential category. Next, (i)
follows from the fact that the contextual linear dagger preserves modification
to the context, and so:
$f^{\dagger[A]}=\left(\varepsilon_{\\_}\ell\circ(\lambda_{\\_}\ell(f)\times
1)\right)^{\dagger[A]}=\varepsilon_{\\_}\ell^{\dagger[\mathcal{L}(A,B)]}\circ(\lambda_{\\_}\ell(f)\times
1)$. Then (ii) is simply the linear curry of (i). For (iii), using (ii) and
$\mathsf{R}[f]=\mathsf{D}[f]^{\dagger[A]}$, we compute that
$\nabla(f)=\lambda_{\\_}\ell(\mathsf{R}[f])=\lambda_{\\_}\ell(\mathsf{D}[f]^{\dagger[A]})=\tau\circ\lambda_{\\_}\ell(\mathsf{D}[f])=\tau\circ\mathbf{J}(f)$.
The remaining three identities are simply the transpose versions of the three
identities from Proposition 3.2 and the linear transpose axioms (and that if
$A\xrightarrow{f}B$ is linear then $\tau\circ p_{\\_}f=p_{\\_}{f^{\dagger}}$,
which is a special case of (ii)).

We conjecture that an equivalent alternative axiomatization of a linearly
closed Cartesian reverse differential category can be given in terms of a
Cartesian left additive category equipped with $\mathcal{L}(-,-)$,
$\varepsilon_{\\_}\ell$, $\nabla$, and $\tau$, where one would define the
reverse differential combinator as
$\mathsf{R}[-]=\varepsilon_{\\_}\ell\circ(\nabla(-)\times 1)$. In other future
work, it should also be possible to generalize other important notions from
classical differential calculus such as the divergence, the curl, the
Laplacian, and the Hessian. In fact, recall that the Hessian matrix is defined
as the Jacobian matrix of the gradient. Therefore, the Hessian can be defined
in a linearly closed Cartesian reverse differential category as
$A\xrightarrow{\mathbf{H}(f):=\mathbf{J}(\nabla(f))}\mathcal{L}\left(A,\mathcal{L}(B,A)\right)$.

## References

  * [1]
  * [2] M. Abadi & G. D. Plotkin (2019): _A simple differentiable programming language_.  Proceedings of the ACM on Programming Languages 4(POPL), pp. 1–28, 10.1145/3190508.3190551.
  * [3] M. Alvarez-Picallo & C.-H. L. Ong (2019): _Change actions: models of generalised differentiation_.  In: International Conference on Foundations of Software Science and Computation Structures, Springer, pp. 45–61, 10.1007/3-540-10286-8.
  * [4] R. F. Blute, J. R. B. Cockett, J.-S. P. Lemay & R. A. G. Seely (2020): _Differential Categories Revisited_.  Applied Categorical Structures 28, pp. 171–235, 10.1007/s10485-019-09572-y.
  * [5] R. F. Blute, J. R. B. Cockett & R. A. G. Seely (2006): _Differential categories_.  Mathematical structures in computer science 16(06), pp. 1049–1083, 10.1017/S0960129506005676.
  * [6] R. F. Blute, J. R. B. Cockett & R. A. G. Seely (2009): _Cartesian differential categories_.  Theory and Applications of Categories 22(23), pp. 622–672.
  * [7] R. F. Blute, J. R. B. Cockett & R. A. G. Seely (2015): _Cartesian differential storage categories_.  Theory and Applications of Categories 30(18), pp. 620–686.
  * [8] R. F. Blute, T. Ehrhard & C. Tasson (2012): _A convenient differential category_.  Cahiers de Topologie et Géométrie Différentielle Catégoriques LIII, pp. 211–232.
  * [9] A. Bucciarelli, T. Ehrhard & G. Manzonetto (2010): _Categorical models for simply typed resource calculi_.  Electronic Notes in Theoretical Computer Science 265, pp. 213–230, 10.1016/j.entcs.2010.08.013.
  * [10] J. D. Cockett, J. R. B.; Gallagher (2019): _Categorical models of the differential $\lambda$-calculus_.  Mathematical Structures in Computer Science, 10.1017/S0960129519000070.
  * [11] J. R. B. Cockett, G. S. H. Cruttwell, J. D. Gallagher, J.-S. P. Lemay, B. MacAdam, G. Plotkin & D. Pronk (2020): _Reverse Derivative Categories_.  LIPIcs 152(CSL 2020), pp. 18:1–18:16, 10.4230/LIPIcs.CSL.2020.18.
  * [12] J. R. B. Cockett & J.-S. P. Lemay (2022): _Linearizing Combinators_.  Theory and Applications of Categories 38(13), pp. 374–431.
  * [13] G. Cruttwell, J. Gallagher & D. Pronk (2020): _Categorical semantics of a simple differential programming language_.  In: Proceedings of Applied Category Theory 2020.
  * [14] G. Cruttwell, B. Gavranović, N. Ghani, P. Wilson & F. Zanasi (2022): _Categorical Foundations of Gradient-Based Learning_.  In: Programming Languages and Systems, Springer International Publishing, pp. 1–28, 10.1007/978-3-030-99336-81.
  * [15] T. Ehrhard & L. Regnier (2003): _The differential lambda-calculus_.  Theoretical Computer Science 309(1), pp. 1–41, 10.1016/S0304-3975(03)00392-X.
  * [16] J. Gallagher & B. MacAdam: _Discussions on Cartesian differential categories with linear homs._ Unpublished.
  * [17] A. Kriegl & P. W. Michor (1997): _The convenient setting of global analysis_.  53, American Mathematical Soc., 10.1090/surv/053/06.
  * [18] J. Laird, G. Manzonetto & G. McCusker (2013): _Constructing differential categories and deconstructing categories of games_.  Information and Computation 222, pp. 247–264, 10.1016/j.ic.2012.10.015.
  * [19] J.-S. P. Lemay (2018): _A Tangent Category Alternative to the Faa Di Bruno Construction_.  Theory and Applications of Categories 33(35), pp. 1072–1110.
  * [20] G. Manzonetto (2012): _What is a categorical model of the differential and the resource $\lambda$-calculi?_ Mathematical Structures in Computer Science 22(3), 10.1017/S0960129511000594.
  * [21] O. Manzyuk (2012): _Tangent bundles in differential lambda-categories_.  arXiv preprint arXiv:1202.0411.
  * [22] D. Sprunger & S. Katsumata (2019): _Differentiable causal computations via delayed trace_.  In: 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), IEEE, pp. 1–12, 10.1109/LICS.2019.8785670.
  * [23] M. Vákár (2021): _CHAD: Combinatory Homomorphic Automatic Differentiation_.  arXiv preprint arXiv:2103.15776.
  * [24] P. Wilson & F. Zanasi (2020): _Reverse Derivative Ascent: A Categorical Approach to Learning Boolean Circuits_.  In: Proceedings of Applied Category Theory 2020, 10.4204/EPTCS.333.17.