---
abstract: 'We prove that the semantics of intuitionistic linear logic in vector spaces which uses cofree coalgebras to model the exponential is a model of differential linear logic. Thus, in this semantics, proof denotations have natural derivatives. We give several examples of these derivatives.'
author:
- 'James Clift, Daniel Murfet'
title: Cofree coalgebras and differential linear logic
---

ł[|]{}

Introduction
============

The idea of taking derivatives of programs is an old one [@paige §2] with many manifestations, including automatic differentiation of algorithms computing real-valued functions [@autodiff] and incremental computation [@incdiff]. However, these approaches are limited to restricted classes of computations, and it is only recently with the development of the differential $\lambda$-calculus by Ehrhard-Regnier [@difflambda] and its refinement differential linear logic [@blutecs; @ehrhard-survey] that derivatives have been defined for general higher-order programs. As with ordinary calculus, the aim of these theories is to assign to a program $P$ another program $\partial P$ (the derivative) which computes the change in the output of $P$ resulting from an infinitesimal change to its input. Here we give ourselves arbitrary $\mathbb{C}$-linear combinations of programs (meaning $\lambda$-terms or proofs in linear logic) as a starting point so that “small” changes to the input make sense.

This paper is about the semantics of differential linear logic, following [@blutecs]. The aim is to explain how the natural semantics of intuitionistic linear logic in vector spaces [@hyland; @murfet_ll] is already a model of differential linear logic. The key point is that tangent vectors and derivatives appear as soon as we introduce cofree coalgebras to model the exponential, which shows that the differential structure is intrinsic to the algebra of linear logic.

To see this, let ${\llbracket - \rrbracket}$ denote semantics in vector spaces and suppose we are given a proof $\pi$ in linear logic computing a function from inputs of type $A$ to outputs of type $B$: $$\varwidth{.9\textwidth}\centering\leavevmode
\AxiomC{$\pi$}
\noLine\UnaryInfC{$\vdots$}
\def\extraVskip{5pt}
\noLine\UnaryInfC{${!} A \vdash B$\,.}
\DisplayProof\endvarwidth$$ The space of inputs to ${\llbracket \pi \rrbracket}$ is ${\llbracket A \rrbracket}$, and a small change in the input starting from $P \in {\llbracket A \rrbracket}$ is a tangent vector $\nu$ at $P$, viewing ${\llbracket A \rrbracket}$ as a smooth manifold or a scheme. This is equivalent to the data of a linear map @C+2pc[ (\[\]/\^2)\^\* & [A ]{} ]{} where $\mathbb{C}[\varepsilon]/\varepsilon^2$ is the ring of dual numbers (this bijection is reviewed in Appendix \[section:tangent\_vectors\]). If ${\llbracket {!} A \rrbracket}$ is the universal cocommutative counital coalgebra mapping to ${\llbracket A \rrbracket}$ then there is a unique lifting of this linear map to a morphism of coalgebras \[eq:toucan\] @C+2pc[ (\[\]/\^2)\^\* & [ A ]{}. ]{} Similarly the linear map ${\llbracket \pi \rrbracket}: {\llbracket {!} A \rrbracket} {\longrightarrow}{\llbracket B \rrbracket}$ lifts to a morphism of coalgebras ${\llbracket {!} A \rrbracket} {\longrightarrow}{\llbracket {!} B \rrbracket}$ which may be composed with to give a morphism of coalgebras \[eq:toucan2\] @C+2pc[ (\[\]/\^2)\^\* & [ A ]{} & [ B ]{} ]{} which, in turn, defines a tangent vector at the point ${\llbracket \pi \rrbracket}\ket{\emptyset}_P \in {\llbracket B \rrbracket}$, where $\ket{\emptyset}_P$ is the point of ${\llbracket {!} A \rrbracket}$ corresponding to $P$. The tangent vector gives the infinitesimal variation of the output of $\pi$ on the input $P$, when the input is varied in the direction of $\nu$.

The formal statement is that for any algebraically closed field $k$ of characteristic zero the semantics of intuitionistic linear logic in $k$-vector spaces defined using cofree coalgebras is model of differential linear logic (Theorem \[main\_theorem\]). We refer to this as the *Sweedler semantics*, since the explicit description of this universal coalgebra is due to him [@sweedler; @murfet_ll]. The proof is elementary and we make no claim here to technical novelty; the link between the symmetric coalgebra and differential calculus is well-known. Perhaps our main contribution is to give several detailed examples showing how to compute these derivatives. We do this with the aim of reinforcing the fact that differentiating programs, even higher-order ones, is a natural thing to do.\
We conclude this introduction with a sketch of one such example and a comparison of our work to other semantics of differential linear logic. To elaborate a little more on the notation: for any type $A$ of linear logic (which for us has only connectives $\otimes, \multimap, !$) there is a vector space ${\llbracket A \rrbracket}$, and for any proof $\pi$ of $A \vdash B$ there is a linear map ${\llbracket \pi \rrbracket}: {\llbracket A \rrbracket} {\longrightarrow}{\llbracket B \rrbracket}$. In particular every proof $\xi$ of type $A$ has a denotation ${\llbracket \xi \rrbracket} \in {\llbracket A \rrbracket}$, and the promotion of $\xi$ has for its denotation a vector $\ket{\emptyset}_{{\llbracket \xi \rrbracket}} \in {\llbracket !A \rrbracket}$, see [@murfet_ll §5.3].

For any binary sequence $S \in \{0,1\}^*$ there is an encoding of $S$ as a proof $\underline{S}$ of type $$\textbf{bint}_A = {!}(A \multimap A) \multimap \big({!}(A \multimap A) \multimap (A \multimap A)\big)\,.$$ Repetition of sequences can be encoded as a proof $$\varwidth{.9\textwidth}\centering\leavevmode
\AxiomC{${\underline{\mathrm{repeat}}}$}
\noLine\UnaryInfC{$\vdots$}
\def\extraVskip{5pt}
\noLine\UnaryInfC{${!} \textbf{bint}_A \vdash \textbf{bint}_A$\,.}
\RightLabel{\scriptsize $\multimap R$}
\DisplayProof\endvarwidth$$ The denotation is a linear map ${\llbracket  {!}\textbf{bint}_A  \rrbracket} {\longrightarrow}{\llbracket  \textbf{bint}_A  \rrbracket}$ sending $\ket{\emptyset}_{{\llbracket \underline{S} \rrbracket}}$ to ${\llbracket \underline{SS} \rrbracket}$. The derivative of ${\underline{\mathrm{repeat}}}$ according to the theory of differential linear logic is another a proof $$\varwidth{.9\textwidth}\centering\leavevmode
\AxiomC{$\partial\, {\underline{\mathrm{repeat}}}$}
\noLine\UnaryInfC{$\vdots$}
\def\extraVskip{5pt}
\noLine\UnaryInfC{${!} \textbf{bint}_A, \textbf{bint}_A \vdash \textbf{bint}_A$\,}
\RightLabel{\scriptsize $\multimap R$}
\DisplayProof\endvarwidth$$ which can be derived from ${\underline{\mathrm{repeat}}}$ by new deduction rules called codereliction, cocontraction and coweakening (see Section \[section:coder\]). We prove in Section \[section:bint\] that the denotation of this derivative in the Sweedler semantics is the linear map $$\begin{gathered}
{\llbracket \partial\, {\underline{\mathrm{repeat}}} \rrbracket}: {\llbracket  {!}\textbf{bint}_A  \rrbracket} \otimes {\llbracket  \textbf{bint}_A \rrbracket} {\longrightarrow}{\llbracket  \textbf{bint}_A  \rrbracket}\,,\\
\ket{\emptyset}_{{\llbracket \underline{S} \rrbracket}} \otimes {\llbracket \underline{T} \rrbracket} \longmapsto {\llbracket \underline{ST} \rrbracket} + {\llbracket \underline{TS} \rrbracket}\end{gathered}$$ whose value on the tensor $\ket{\emptyset}_{{\llbracket \underline{S} \rrbracket}} \otimes {\llbracket \underline{T} \rrbracket}$ we interpret as the derivative of the repeat program at the sequence $S$ in the direction of the sequence $T$. This can be justified informally by the following calculation using an infinitesimal $\varepsilon$ $$\begin{aligned}
(S + \varepsilon T)( S + \varepsilon T) = SS + \varepsilon( ST + TS ) + \varepsilon^2 TT,\end{aligned}$$ which says that varying the sequence infinitesimally from $S$ in the direction of $T$ causes a variation of the repetition in the direction of $ST + TS$.\
The Sweedler semantics is far from the first semantics of differential linear logic: basic examples include the categories of sets and relations [@blutecs §2.5.1] and suplattices [@blutecs §2.5.2]. The motivating examples using topological spaces and differentiable functions are the Köthe and finiteness space semantics of Ehrhard [@ehrhard-kothe; @ehrhard-finiteness] and the semantics of Blute-Ehrhard-Tasson [@blutecon] based on the theory of convenient vector spaces [@frolicher]. These papers explain that the geometric “avatar” of the exponential connective of linear logic is the functor sending a space $X$ to the space of distributions on $X$ (for a precise statement, see Remark \[remark:distr\]). This remarkable analogy between logic and geometry deserves further study. One obstacle is that it seems difficult to compute examples of denotations and their derivatives in the convenient vector space setting of [@blutecon]. For example the coproduct [@blutecon p.12] is defined by extension to a Mackey closure, and is rather implicit.

Conceptually the Sweedler semantics is similar to these examples in that the exponential is modelled by a space of distributions (with finite support) but it is purely algebraic and there are simple explicit formulas for all the structure maps. Moreover in the algebraic approach the differential structure emerges naturally from the exponential structure, rather than being “baked in”. The downside is that the smoothness of proof denotations in our semantics is obscured; in particular, in the case $k = \mathbb{C}$ some extra work is required to see the relation between our differential structure and the derivatives in the usual sense.\
For background material on linear logic and its semantics see [@girard_llogic; @girard_prooftypes; @mellies]. The formal theory of coalgebras is simpler over algebraically closed fields, which explains why we use $k = \mathbb{C}$ in our examples, but this is not really important: one could work over $k = \mathbb{R}$ by taking $\mathbb{C}$-points into account in the explicit description of the cofree coalgebra.\
*Acknowledgements.* Thanks to Kazushige Terui, who stimulated this project by asking if the cofree coalgebra gave a model of differential linear logic.

Main Theorem
============

Let $k$ be an algebraically closed field of characteristic zero and ${\mathcal{V}}$ the category of $k$-vector spaces. This is a model of intuitionistic linear logic, as observed in [@hyland p.5] and developed in detail in [@murfet_ll]. Our notation is as in [@murfet_coalg] and [@murfet_ll §5], see Appendix \[section:background\] for a review.

For a vector space $V$ we denote by ${!} V$ the universal cocommutative counital coalgebra mapping to $V$, with $d: {!} V {\longrightarrow}V$ the universal map. The map $V \mapsto {!} V$ extends to a comonad on ${\mathcal{V}}$ with natural transformation $\delta: {!} {\longrightarrow}{!} {!}$. The coproduct and counit are respectively denoted $\Delta: {!} V {\longrightarrow}{!} V \otimes {!} V$ and $w: {!} V {\longrightarrow}k$. Given vector spaces $V,W$ we write $\sigma_{V,W}: V \otimes W {\longrightarrow}W \otimes V$ for the swap map $\sigma_{V,W}(x \otimes y) = y \otimes x$.

By [@blutecs Proposition 2.6] to equip ${\mathcal{V}}$ with the coalgebra modality $({!}, \delta, d, \Delta, w)$ as a differential category, we need to define a deriving transformation [@blutecs Definition 2.5].

A *deriving transformation* for $({\mathcal{V}}, {!}, \delta, d, \Delta, w)$ is a family of morphisms $$D_V: {!} V \otimes V {\longrightarrow}{!} V$$ natural in $V$, satisfying the following properties for all $V$:

-   $w \circ D = 0$, that is, @C+2pc[ V V \^-[D]{} & [!]{} V \^-[w]{} & k ]{} = 0.

-   $\Delta \circ D = (1 \otimes D) \circ (\Delta \otimes 1) + (D \otimes 1) \circ (1 \otimes \sigma) \circ (\Delta \otimes 1)$, that is, @C+2pc[ [!]{} V V \^-[D]{} & [!]{} V \^- & [!]{} V V ]{} is equal to the sum $$\begin{gathered}
    \xymatrix@C+2pc{{!} V \otimes V \ar[r]^-{\Delta \otimes 1} & {!} V \otimes {!} V \otimes V \ar[r]^-{1 \otimes D} & {!} V \otimes {!} V} \quad +\\
    \xymatrix@C+2pc{{!} V \otimes V \ar[r]^-{\Delta \otimes 1} & {!} V \otimes {!} V \otimes V \ar[r]^-{1 \otimes \sigma_{{!}V, V}}_{\cong} & {!} V \otimes V \otimes {!} V \ar[r]^-{D \otimes 1} & {!} V \otimes {!} V}\end{gathered}$$

-   $d \circ D = a \circ (w \otimes 1)$, that is, @C+2pc[ [!]{} V V \^-[D]{} & [!]{} V \^-[d]{} & V ]{} = @C+2pc[ [!]{} V V \^-[w 1]{} & k V \^-[a]{}\_- & V ]{} where $a(\lambda \otimes x) = \lambda x$.

-   $\delta \circ D = D_{{!} V} \circ (\delta \otimes D) \circ (\Delta \otimes 1)$, that is, @C+2pc[ [!]{} V V \^-[D]{} & [!]{} V \^- & [!]{}[!]{} V ]{} is equal to \[eq:D4final\] @C+2pc[ [!]{} V V \^-[1]{} & [!]{} V V V \^-[D]{} & [!]{}[!]{} V V \^-[D\_[[!]{}V]{}]{} & [!]{}[!]{} V. ]{}

We refer to [@blutecs §2.2] for an explanation of these axioms. Briefly, (D.1) says the derivative of constant maps is zero, (D.2) is the product rule, (D.3) says the derivative of a linear map is constant, and (D.4) is the chain rule. Clearly the rules specify how to commute $D$ past the structural maps $\delta, d, \Delta, w$. Here $d$ stands for the dereliction rule in linear logic, $\Delta$ for contraction and $w$ for weakening. The map $\delta$ stands for promotion, since for a linear map $\phi: {!} V {\longrightarrow}W$ the unique lifting to a morphism of coalgebras $\Phi: {!} V {\longrightarrow}{!} W$ can be obtained as the composite @C+2pc[ [!]{} V \^- & [!!]{} V \^-[[!]{} ]{} & [!]{} W. ]{}

\[defn:D\] We define the $k$-linear map $D_V: {!} V \otimes V {\longrightarrow}V$ by \[defn:DV\] D\_V( \_P ) = \_P.

See Remark \[remark:justify\] for a justification of this definition from the point of view of [@murfet_coalg].

\[main\_theorem\] $D_V$ is a deriving transformation for any vector space $V$.

We split the proof into a series of lemmas. We prefer to give the proofs without first choosing a basis of $V$, but if one is willing to do so, then the connection between these identities and the usual rules of calculus follows from writing the formula for the coproduct $\Delta$ as a kind of Taylor expansion; see for example [@seiler (B.65)].

(D.1) holds for $V$.

This is clear, since the counit $w: {!} V {\longrightarrow}V$ vanishes on $\ket{\omega_1,\ldots,\omega_t}_P$ if $t > 0$.

(D.2) holds for $V$.

Setting $\nu_0 = \nu$ we have $$\begin{aligned}
\Delta D \big( \ket{\nu_1,\ldots,\nu_s}_P \otimes \nu \big) &= \Delta \ket{\nu, \nu_1, \ldots, \nu_s }_P\\
&= \sum_{I \subseteq \{0,1,\ldots,s\}} \ket{\nu_I}_P \otimes \ket{\nu_{I^c}}_P\\
&= \sum_{0 \in I} \ket{\nu_I}_P \otimes \ket{\nu_{I^c}}_P + \sum_{0 \notin I} \ket{\nu_I}_P \otimes \ket{\nu_{I^c}}_P \\
&= \sum_{J \subseteq \{1,\ldots,s\}}\ket{\nu, \nu_J}_P \otimes \ket{\nu_{J^c}}_P + \sum_{J \subseteq \{1,\ldots,s\}} \ket{\nu_J}_P \otimes \ket{\nu, \nu_{J^c}}_P \\
&= \sum_{J \subseteq \{1,\ldots,s\}} \Big\{ D\big( \ket{\nu_J}_P \otimes \nu \big) \otimes \ket{\nu_{J^c}}_P + \ket{\nu_J}_P \otimes D\big( \ket{\nu_{J^c}}_P \otimes \nu \big) \Big\}\end{aligned}$$ as claimed, where for $I \subseteq \{0,1,\ldots,s\}$ we write $I^c$ for $\{0,\ldots,s\} \setminus I$ and for $J \subseteq \{1,\ldots,s\}$, we write $J^c$ for $\{1,\ldots,s\} \setminus J$.

(D.3) holds for $V$.

We have $$d D\big( \ket{\nu_1,\ldots,\nu_s}_P \otimes \nu \big) = d\ket{\nu,\nu_1,\ldots,\nu_s}_P = \delta_{s=0} \nu$$ while $$a( w \otimes 1 )\big( \ket{\nu_1,\ldots,\nu_s}_P \otimes \nu \big) = w\ket{\nu_1,\ldots,\nu_s}_P \cdot \nu = \delta_{s=0} \nu\,.$$

(D.4) holds for $V$.

The trivial case is, with $Q = \ket{\emptyset}_P$, $$\delta D( \ket{\emptyset}_P \otimes \nu ) = \delta\ket{\nu}_P = \big|\, \ket{\nu}_P \big\rangle_Q$$ and on the other side $$\begin{aligned}
D_{{!} V}( \delta \otimes D )( \Delta \otimes 1)( \ket{\emptyset}_P \otimes \nu ) &= D_{{!} V}( \delta \otimes D)( \ket{\emptyset}_P \otimes \ket{\emptyset}_P \otimes \nu )\\
&= D_{{!} V}( \ket{\emptyset}_Q \otimes \ket{\nu}_P )\\
&= \big|\, \ket{\nu}_P \big\rangle_Q\,.\end{aligned}$$ Now we consider the case $s > 0$. Putting $\nu_0 = \nu$ and writing ${\mathcal{P}}_T$ for the set of partitions of $T$ we have $$\delta D\big(  \ket{\nu_1,\ldots,\nu_s}_P \otimes \nu \big) = \sum_{X \in {\mathcal{P}}_{\{0,1,\ldots,s\}}} \Big| \otimes_{x \in X} \ket{\nu_{x}}_P \Big\rangle_Q$$ where for a partition $X = \{ x_1,\ldots,x_t \}$ the notation means $$\Big| \otimes_{x \in X} \ket{\nu_{x}}_P \Big\rangle_Q = \Big|\, \ket{\nu_{x_1}}_P, \ldots, \ket{\nu_{x_t}}_P \Big\rangle_Q\,.$$ See Appendix \[section:background\] for the definition of $\ket{\nu_x}$ when $x$ is a set. There is a surjective function $$\begin{gathered}
\theta: {\mathcal{P}}_{\{0,1,\ldots,s\}} {\longrightarrow}{\mathcal{P}}_{\{1,\ldots,s\}}\\
\theta( X ) = \big\{ x \setminus \{0\} \l x \in X \text{ and } x \neq \{0\} \big\}\end{gathered}$$ and given a partition $X = \{ x_1,\ldots,x_t \}$ of $\{1,\ldots,s\}$, $$\begin{aligned}
\theta^{-1}(X) &= \Big\{ \{ x_1 \cup \{0\}, x_2, \ldots, x_t \},\\
&\quad\{ x_1, x_2 \cup \{0\}, \ldots, x_t \},\\
&\quad\ldots,\\
&\quad\{ x_1, x_2, \ldots, x_{t-1}, x_t \cup \{0\} \}\\
&\quad\{ x_1, x_2, \ldots, x_t, \{0\} \} \Big\}\,.\end{aligned}$$ With this in mind we have, writing $\otimes_{x' \neq x} \ket{\nu_{x'}}_P$ for the list of $\ket{\nu_{x'}}_P$ as $x'$ ranges over elements of $X \setminus \{x\}$, that $\delta D\big(  \ket{\nu_1,\ldots,\nu_s}_P \otimes \nu \big)$ is equal to \[eq\_written72\] \_[X \_[{1,…,s}]{}]{} { \_[x X]{} | \_P, \_[x’ x]{} \_P\_Q + | \_P, \_[x X]{} \_P \_Q }. Note that when $X = \big\{ \{ 1,\ldots,s \} \big\}$ the summand is $$\Big|\, \ket{\nu,\nu_1,\ldots,\nu_s}_P \Big\rangle_Q + \Big|\, \ket{\nu}_P, \ket{\nu_1,\ldots,\nu_s}_P \Big\rangle_Q\,.$$ On the other hand, the right hand side of the (D.4) identity is $$\begin{aligned}
&D_{{!} V}(\delta \otimes D)(\Delta \otimes 1)\big(  \ket{\nu_1,\ldots,\nu_s}_P \otimes \nu \big)\\
&= \sum_{I \subseteq \{1,\ldots,s\}} D_{{!}V}(\delta \otimes D)\Big( \ket{\nu_I}_P \otimes \ket{\nu_{I^c}}_P \otimes \nu \Big)\\
&= \sum_{I \subseteq \{1,\ldots,s\}} D_{{!} V}\Big( \delta \ket{\nu_I}_P \otimes \ket{\nu, \nu_{I^c}}_P \Big)\\
&= D_{{!} V}\Big( \delta\ket{\emptyset}_P \otimes \ket{\nu, \nu_1, \ldots, \nu_s }_P \Big)\\
&\qquad + \sum_{\emptyset \subset I} \sum_{Y \in {\mathcal{P}}_I} D_{{!}V}\Big( \big| \otimes_{y \in Y} \ket{\nu_y}_P \big\rangle_Q \otimes \ket{\nu, \nu_{I^c}}_P \Big)\\
&= \Big|\, \ket{ \nu, \nu_1,\ldots,\nu_s }_P \Big\rangle_Q + \sum_{\emptyset \subset I}\sum_{Y \in {\mathcal{P}}_I}  \Big|\, \ket{\nu, \nu_{I^c}}_P\,, \otimes_{y \in Y} \ket{\nu_y}_P \Big\rangle_Q\\
&= \Big|\, \ket{ \nu, \nu_1,\ldots,\nu_s }_P \Big\rangle_Q + \sum_{Y \in {\mathcal{P}}_{\{1,\ldots,s\}}} \Big|\, \ket{\nu}_P\,, \otimes_{y \in Y} \ket{\nu_y}_P \Big\rangle_Q\\
&\qquad+ \sum_{\emptyset \subset I \subset \{1,\ldots,s\}} \sum_{Y \in {\mathcal{P}}_I} \Big|\, \ket{\nu, \nu_{I^c}}_P\,, \otimes_{y \in Y} \ket{\nu_y}_P \Big\rangle_Q\end{aligned}$$ which matches since the last sum can be rewritten as $$\sum_{\substack{X \in {\mathcal{P}}_{\{1,\ldots,s\}}\\ \text{ with } |X| > 1}} \sum_{x \in X} \Big|\, \ket{\nu, \nu_x}_P\,, \otimes_{x' \neq x} \ket{\nu_{x'}}_P \Big\rangle_Q\,.$$

${\mathcal{V}}$ is a differential category.

This follows from [@blutecs Proposition 2.6].

Codereliction, cocontraction, coweakening {#section:coder}
-----------------------------------------

An alternative formulation of the differential structure in differential linear logic is in terms of *codereliction, cocontraction* and *coweakening* maps; see [@fiore] and [@blutecon §5.1]. This has the advantage of providing an appealing symmetry to the formulation of the syntax. In this section we briefly sketch the definition of these maps in the Sweedler semantics. Throughout linear logic means intuitionistic linear logic with the connectives ${!}, \otimes, \multimap$.

First we recall the canonical commutative Hopf structure on ${!} V$ of [@sweedler §6.4]. Given vector spaces $V_1,V_2$ then (see [@sweedler Remark 2.19]) there is an isomorphism of coalgebras $$\begin{gathered}
\Psi: {!} V_1 \otimes {!} V_2 {\longrightarrow}{!} (V_1 \oplus V_2)\,,\\
\ket{\nu_1,\ldots,\nu_s}_P \otimes \ket{\omega_1,\ldots,\omega_t}_Q \longmapsto \ket{\nu_1,\ldots,\nu_s,\omega_1,\ldots,\omega_t}_{(P,Q)}\,.\end{gathered}$$ Using this and the definitions in [@sweedler], it is easy to check that the product $\nabla$ is $$\begin{gathered}
\nabla: {!} V \otimes {!} V {\longrightarrow}{!} V\,,\\
\ket{\nu_1,\ldots,\nu_s}_P \otimes \ket{\omega_1,\ldots,\omega_t}_Q \longmapsto \ket{\nu_1,\ldots,\nu_s,\omega_1,\ldots,\omega_t}_{P+Q}\,,\end{gathered}$$ while the antipode $S$ is $$\begin{gathered}
S: {!} V {\longrightarrow}{!} V\,,\\
\ket{\nu_1,\ldots,\nu_s}_P \longmapsto \ket{-\nu_1,\ldots,-\nu_s}_{-P}\end{gathered}$$ and the unit $u: k {\longrightarrow}{!} V$ is $u(1) = \ket{\emptyset}_0$. By [@sweedler Theorem 6.4.8] these maps make ${!} V$ into a commutative (and cocommutative) Hopf algebra. In the terminology of [@ehrhard-survey] the map $\nabla$ is the *cocontraction* map and $u$ is the *coweakening* map (the antipode seems not to have a formal role in differential linear logic). Finally,

The *codereliction* $\bar{d}$ is the composite $$\xymatrix@C+2pc{
V \cong V \otimes k \ar[r]^-{1 \otimes u} & V \otimes {!} V \ar[r]^-{D} & {!} V
}$$ which is given by $\nu \mapsto \ket{\nu}_0$.

Note that we can recover $D$ as $$\begin{gathered}
\xymatrix@C+2pc{
{!} V \otimes V \ar[r]^-{1 \otimes \bar{d}} & {!} V \otimes {!} V \ar[r]^-{\nabla} & {!} V
}\\
\ket{\nu_1,\ldots,\nu_s}_P \otimes \nu \mapsto \ket{\nu_1,\ldots,\nu_s}_P \otimes \ket{\nu}_0 \mapsto \ket{\nu,\nu_1,\ldots,\nu_s}_P\,.\end{gathered}$$ It seems more convenient to model differentiation syntactically using the codereliction, cocontraction and coweakening maps, rather than the deriving transformation $D$ itself. We briefly sketch how this works, following [@ehrhard-survey]. In the sequent calculus for linear logic one introduces three new deduction rules “dual” to dereliction, contraction and weakening: $$\AxiomC{$\Gamma, {!}A, \Delta \vdash B$}
\LeftLabel{(Codereliction): }
\RightLabel{\scriptsize coder}
\UnaryInfC{$\Gamma, A, \Delta \vdash B$}
\DisplayProof$$ $$\AxiomC{$\Gamma, !A, \Delta \vdash B$}
\LeftLabel{(Cocontraction): }
\RightLabel{\scriptsize coctr}
\UnaryInfC{$\Gamma, !A, !A, \Delta \vdash B$}
\DisplayProof$$ $$\AxiomC{$\Gamma, !A, \Delta \vdash B$}
\LeftLabel{(Coweakening): }
\RightLabel{\scriptsize coweak}
\UnaryInfC{$\Gamma, \Delta \vdash B$}
\DisplayProof$$ together with new cut-elimination rules [@ehrhard-survey §1.4.3].

\[defn:derivative\_proof\] Given a proof $\pi$ of ${!} A \vdash B$ in linear logic, the *derivative* $\partial \pi$ is the proof

whose denotation is, by our earlier remark, the composite @C+2pc[ [!]{} [A ]{} [A ]{} \^-[D]{} & [!]{} [A ]{} \^- & [B ]{}. ]{}

\[remark:totem\] Given $\pi$ as above we have the function [@murfet_ll Definition 5.10] \_[nl]{}: [A ]{} [B ]{}, P \_P, and for $P, \nu \in {\llbracket A \rrbracket}$ we interpret the vector D( \_P ) = \_P [B ]{} as the derivative of ${\llbracket \pi \rrbracket}_{nl}$ at the point $P$ in the direction of $\nu$. Here we implicitly identify ${\llbracket A \rrbracket}$ with the tangent space $T_P{\llbracket A \rrbracket}$ and ${\llbracket B \rrbracket}$ with the tangent space $T_{{\llbracket \pi \rrbracket}_{nl}(P)} {\llbracket B \rrbracket}$. This interpretation is justified by the following elaboration of the remarks in the Introduction.

Let $\operatorname{prom}(\pi)$ denote the proof which is the promotion of $\pi$, which has for its denotation the unique morphism of coalgebras ${\llbracket  \operatorname{prom}(\pi)  \rrbracket}: {!} {\llbracket A \rrbracket} {\longrightarrow}{!} {\llbracket B \rrbracket}$ with $d \circ {\llbracket  \operatorname{prom}(\pi)  \rrbracket} = {\llbracket \pi \rrbracket}$. Let $\Psi: (k[\varepsilon]/\varepsilon^2)^* {\longrightarrow}{!} {\llbracket A \rrbracket}$ be the morphism of coalgebras as in corresponding to the tangent vector $\nu$ at a point $P \in {\llbracket A \rrbracket}$. Then the morphism of coalgebras \[eq:prompiafterpsi\] [() ]{} : (k\[\]/\^2)\^\* [!]{} [B ]{} has the following values, writing $Q = {\llbracket \pi \rrbracket}_{nl}(P)$, we have by [@murfet_coalg Theorem 2.22] $$\begin{aligned}
{\llbracket  \operatorname{prom}(\pi)  \rrbracket}\Psi(1) &= {\llbracket  \operatorname{prom}(\pi)  \rrbracket} \ket{\emptyset}_P = \ket{\emptyset}_Q\,,\\
{\llbracket  \operatorname{prom}(\pi)  \rrbracket}\Psi(\varepsilon^*) &= {\llbracket  \operatorname{prom}(\pi)  \rrbracket} \ket{\nu}_P = \Big|\, {\llbracket \pi \rrbracket}\ket{\nu}_P \Big\rangle_Q\,.\end{aligned}$$ Under the bijection of Section \[section:tangent\_vectors\] the morphism of coalgebras therefore corresponds to the tangent vector ${\llbracket \pi \rrbracket}\ket{\nu}_P \in {\llbracket B \rrbracket}$ at $Q$.

It is easy using the formulas for $\nabla, D$ to check that the $\nabla$-rule of [@blutecs §4.3] is satisfied:

The diagram @C+2pc[ V V V \_-[D 1]{} \^-[1 ]{} & V V \^-[D]{}\
[!]{} V V \_- & [!]{} V ]{} commutes.

This, together with [@blutecs Theorem 4.12], shows that ${\mathcal{V}}$ with the comonad ${!}$ and deriving transformation $D$ is a model of the differential calculus in the sense of [@blutecs Definition 4.11].

${\mathcal{V}}$ is a categorical model of the differential calculus.

Examples {#section:examples}
========

In this section we give various examples of proofs $\pi$ and the derivatives ${\llbracket \pi \rrbracket} \circ D$ of their denotations, according to Definition \[defn:derivative\_proof\]. We recall briefly the definition of the semantics ${\llbracket - \rrbracket}$ in the category ${\mathcal{V}}$ of $k$-vector spaces from [@hyland] and [@murfet_ll §5.1, §5.3]. For a propositional variable $x$ the denotation ${\llbracket x \rrbracket}$ is any finite-dimensional vector space, and $$\begin{aligned}
{\llbracket A \multimap B \rrbracket} &= \Hom_k({\llbracket A \rrbracket},{\llbracket B \rrbracket})\,,\\
{\llbracket A \otimes B \rrbracket} &= {\llbracket A \rrbracket} \otimes {\llbracket B \rrbracket}\,,\\
{\llbracket {!}A \rrbracket} &= {!} {\llbracket A \rrbracket}\,,\end{aligned}$$ where ${!} V$ denotes the universal cocommutative counital coalgebra mapping to $V$.

The encoding of integers and binary sequences in linear logic is based on the following encoding of the composition rule.

For any formula $A$ let $C^1_A$ denote the proof

We define recursively for $n > 1$ a proof $C^n_A$ of $A, (A \multimap A)^n \vdash A$, where $(A \multimap A)^n$ denotes a sequence of $n$ copies of $A \multimap A$, to be

For $n \ge 1$ let $\comp^n_A$ denote the proof

We define $\comp^0_A$ to be the proof

If $V = {\llbracket A \rrbracket}$ and $\alpha_i \in {\llbracket A \multimap A \rrbracket} = \operatorname{End}_k(V)$ for $1 \le i \le n$ then \[order\_comp\] [\^n\_A ]{}( \_1 \_n ) = \_n \_1, while ${\llbracket \comp^0_A \rrbracket} = 1_V$.

Church numerals {#section:church}
---------------

The type of *integers on $A$* [@girard_llogic §5.3.2] is: $$\inta_A = {!}( A \multimap A ) \multimap (A \multimap A)\,.$$ For $n \ge 0$ we define the Church numeral $\underline{n}_A$ to be the proof

Generally we omit the final step, since it is irrelevant semantically. In the case $n = 0$ the ${!}(A \multimap A)$ is introduced on the left by a weakening rule.

The proof $\underline{2}_A$ (see e.g. [@murfet_ll Example 5.9]) is

From now on $A$ is fixed and we write $\underline{n}$ for $\underline{n}_A$. Let $V = {\llbracket A \rrbracket}$ so ${\llbracket A \multimap A \rrbracket} = \operatorname{End}_k(V)$. In the notation of Remark \[remark:totem\], there is a function [ ]{}\_[nl]{}: \_k(V) \_k(V).

For $n \ge 0$ and $\alpha \in \operatorname{End}_k(V)$, we have ${\llbracket \underline{n} \rrbracket}\ket{\emptyset}_\alpha = \alpha^n$ so ${\llbracket \underline{n} \rrbracket}_{nl}(\alpha) = \alpha^n$.

This is an easy exercise, see [@murfet_ll] for the case $n = 2$.

The derivative $\partial\, \underline{n}$ of Definition \[defn:derivative\_proof\] is a proof of ${!}(A \multimap A), A \multimap A \vdash A \multimap A$ and for $\alpha, \nu \in \operatorname{End}_k(V)$ the value of its denotation ${\llbracket \partial\, \underline{n} \rrbracket} = {\llbracket \underline{n} \rrbracket} \circ D$ on $\ket{\emptyset}_\alpha \otimes \nu$, that is, the derivative of $\underline{n}$ at $\alpha$ in the direction of $\nu$, is ${\llbracket \underline{n} \rrbracket} \ket{\nu}_\alpha$.

\[lemma:nderiv\] ${\llbracket \underline{n} \rrbracket}\ket{\nu}_\alpha = \sum_{i = 1}^{n} \alpha^{i-1} \nu \alpha^{n-i}$.

This may be computed using the formulas of [@murfet_ll p.19]. For example, in the case $n = 2$ the image of $\ket{\nu}_\alpha$ under ${\llbracket \underline{n} \rrbracket}$ is given by $$\begin{aligned}
\ket{\nu}_\alpha 
&\xmapsto{\makebox[1cm]{\scriptsize ctr}} \ket{\nu}_\alpha \otimes \ket{\emptyset}_\alpha + \ket{\emptyset}_\alpha \otimes \ket{\nu}_\alpha
\\&\xmapsto{\makebox[1cm]{\scriptsize $2 \times$ \text{der}} } \nu \otimes \alpha + \alpha \otimes \nu
\\&\xmapsto{\makebox[1cm]{\scriptsize $ - \circ -$} } \alpha \circ \nu + \nu \circ \alpha\,,\end{aligned}$$ as claimed.

When $k = \mathbb{C}$, $V$ is $r$-dimensional and $\varphi = {\llbracket \underline{n} \rrbracket}_{nl}$, the vector ${\llbracket \underline{n} \rrbracket}\ket{\nu}_\alpha$ agrees with the image of $\nu$ under the usual tangent map of the smooth map $\varphi$ $$\xymatrix@C+2pc{
M_r(\mathbb{C}) \cong T_\alpha \operatorname{End}_k(V) \ar[r]^-{T_\alpha \varphi} & T_{\alpha^n}\operatorname{End}_k(V) \cong M_r(\mathbb{C})\,.
}$$ This justifies in this case the interpretation of ${\llbracket \underline{n} \rrbracket}\ket{\nu}_\alpha$ as the derivative.

Binary integers {#section:bint}
---------------

The type of *binary integers on $A$* [@girard_complexity §2.5.3] is: $$\binta_A = {!}( A \multimap A) \multimap ({!}( A \multimap A) \multimap ( A \multimap A)).$$ Given a sequence $S \in \{0,1\}^*$ we define a proof $\underline{S}_A$ of $\binta_A$ as follows. Let $l \ge 0$ be the length of $S$. The proof tree for $\underline{S}_A$ matches that of the Church numeral $\underline{l}$ up to the step where we perform contractions, that is, $$\label{bint_Upto}
\varwidth{.9\textwidth}\centering\leavevmode
\AxiomC{$\comp^l_A$}
\noLine\UnaryInfC{$\vdots$}
\noLine\UnaryInfC{$(A \multimap A)^{l} \vdash A \multimap A$}
\doubleLine\RightLabel{\scriptsize $n \times$ der}
\UnaryInfC{${!}(A \multimap A)^l \vdash A \multimap A$}
\DisplayProof\endvarwidth$$ We match each copy of ${!}(A \multimap A)$ on the left with the corresponding position in $S$, and using a series of contractions we identify all copies corresponding to a position in which $0$ appears in $S$, and likewise all copies corresponding to positions with a $1$. After these contractions, there will be two copies of ${!}(A \multimap A)$ on the left (the first being by convention the remnant of all the $0$-associated copies) unless $S$ contains only $0$’s or only $1$’s. In this case we use further a weakening rule to introduce the “missing” ${!}(A \multimap A)$, giving finally the desired proof $\underline{S}_A$:

In the final right $\multimap R$ introduction rules, the second copy of ${!}(A \multimap A)$ (associated with the $1$’s in $S$) is moved across the turnstile first. If $S$ is the empty sequence, then $l = 0$ and the proof is a pair of weakenings on the left followed by the $\multimap R$ introduction rules.

For the rest of this section $A$ is fixed and we write $\underline{S}$ for $\underline{S}_A$.

The proof $\underline{001}$ is

where the colouring indicates which copies of ${!}(A \multimap A)$ are contracted. Using , [ ]{}(\_\_) = [\^3\_A ]{}(\_\_\_) = .

Generalising the calculation of Section \[section:church\] we now describe the derivatives of binary integers. The general formula computes, for $S \in \{0,1\}^*$, the linear operator $${\llbracket  \underline{S}  \rrbracket}\big( \ket{\alpha_1,\ldots,\alpha_r}_{\gamma} \otimes \ket{\beta_1,\ldots,\beta_s}_{\delta} \big) \in \operatorname{End}_k(V)\,.$$ Informally, this operator is described by inserting $\gamma$ for $0$ and $\delta$ for $1$ in (the reversal of) $S$, and then summing over all ways of replacing $r$ of the $\gamma$’s in this composite with $\alpha_i$’s, and $t$ of the $\delta$’s with $\beta_j$’s. Let $\operatorname{Inj}(P,Q)$ denote the set of injective functions $P {\longrightarrow}Q$, and write $[s] = \{1,\ldots,s\}$.

\[lemma:derivative\_bint\] Let $S = a_l a_{l-1} \cdots a_1$ with $a_i \in \{0,1\}$ be a binary sequence, and set $$N_0 = \{ j \l a_j = 0 \}\,, \qquad N_1 = \{ j \l a_j = 1 \}\,.$$ Then we have \[eq:formula\_derivative\_bint\] [ ]{}( \_ \_ ) = \_[f (\[s\],N\_0)]{} \_[g (\[r\],N\_1)]{} \^[f,g]{}\_1 \^[f,g]{}\_l, where $$\Gamma^{f,g}_i = \begin{cases}
\gamma & i \in N_0 \setminus \operatorname{Im}(f)\,,\\
\delta & i \in N_1 \setminus \operatorname{Im}(g)\,,\\
\alpha_j & \text{if } i \in \operatorname{Im}(f) \text{ and } f(j) = i\,,\\
\beta_j & \text{if } i \in \operatorname{Im}(g) \text{ and } g(j) = i\,.
\end{cases}$$ In particular this vanishes if $s > |N_0|$ or $r > |N_1|$.

This is clear, since ${\llbracket \underline{S} \rrbracket}$ applies $n = |N_0|$ coproducts to $\ket{\alpha_1,\ldots,\alpha_s}_{\gamma}$ yielding $$\sum_{\substack{J_1,\ldots,J_n\\ \text{pairwise disjoint, s.t.} \\ J_1 \cup \cdots \cup J_n = \{1,\ldots,s\}}} \ket{\alpha_{J_1}}_\gamma \otimes \cdots \otimes \ket{\alpha_{J_n}}_\gamma\,,$$ to which the dereliction operator $d^{\otimes n}$ is applied, which annihilates those tuples $(J_1,\ldots,J_n)$ where any $J_i$ contains more than one element. The resulting sum is over $f \in \operatorname{Int}([s],N_0)$ and each summand is $\gamma \otimes \cdots \otimes \alpha_{\sigma(1)} \otimes \cdots \otimes \gamma \otimes \cdots \alpha_{\sigma(s)} \otimes \cdots \otimes \gamma$ for a permutation $\sigma$. The same is true of $\ket{\beta_1,\ldots,\beta_r}_{\delta}$, and after the two resulting tensors are intertwined the final step is compose all the operators, yielding .

For $S = 001$ we have $$\begin{aligned}
{\llbracket \underline{001} \rrbracket}\big( \ket{\alpha}_\gamma \otimes \ket{\emptyset}_\delta \big) &= \delta \circ \alpha \circ \gamma + \delta \circ \gamma \circ \alpha\,,\\
{\llbracket \underline{001} \rrbracket}\big( \ket{\alpha_1,\alpha_2}_\gamma \otimes \ket{\emptyset}_\delta \big) &= \delta \circ \alpha_1 \circ \alpha_2 + \delta \circ \alpha_2 \circ \alpha_1\,,\\
{\llbracket \underline{001} \rrbracket}\big( \ket{\emptyset}_\gamma \otimes \ket{\beta}_\delta \big) &= \beta \circ \gamma \circ \gamma\,,\\
{\llbracket \underline{001} \rrbracket}\big( \ket{\alpha}_\gamma \otimes \ket{\beta}_\delta \big) &= \beta \circ \alpha \circ \gamma + \beta \circ \gamma \circ \alpha\,,\\
{\llbracket \underline{001} \rrbracket}\big( \ket{\alpha_1,\alpha_2}_\gamma \otimes \ket{\beta}_\delta \big) &= \beta \circ \alpha_1 \circ \alpha_2 + \beta \circ \alpha_2 \circ \alpha_1\,.\end{aligned}$$ and zero for all other inputs.

More interestingly we can also compute the derivatives of proofs of ${!}\binta_A \vdash \binta_A$. In what follows $A$ is fixed and $E = A \multimap A$.

The proof $\repeat$ is

which repeats a binary sequence in the sense that the cutting it against the promotion of $\underline{S}$ is equivalent under cut-elimination to $\underline{SS}$. In particular, ${\llbracket \repeat \rrbracket}\ket{\emptyset}_{{\llbracket \underline{S} \rrbracket}} = {\llbracket \underline{SS} \rrbracket}$.

Given $S, T \in \{0,1\}^*$ the derivative of $\repeat$ at $S$ in the direction of $T$ is \_[[ ]{}]{} [\_A ]{} = \_k( [!]{} \_k(V) \_k(V), \_k(V)), and as promised in the Introduction:

${\llbracket \repeat \rrbracket}\ket{{\llbracket \underline{T} \rrbracket}}_{{\llbracket \underline{S} \rrbracket}} = {\llbracket \underline{ST} \rrbracket} + {\llbracket \underline{TS} \rrbracket}$.

The value of the left-hand side on a tensor $\ket{\alpha_1,\ldots,\alpha_s}_{\gamma} \otimes \ket{\beta_1,\ldots,\beta_r}_{\delta}$ is computed by reading the proof-tree for $\repeat$ from bottom to top: $$\begin{aligned}
\ket{{\llbracket \underline{T} \rrbracket}}_{{\llbracket \underline{S} \rrbracket}} 
&\xmapsto{\makebox[1cm]{\scriptsize\text{ctr}}} \ket{{\llbracket \underline{T} \rrbracket}}_{{\llbracket \underline{S} \rrbracket}} \otimes \ket{\emptyset}_{{\llbracket \underline{S} \rrbracket}} + \ket{\emptyset}_{{\llbracket \underline{S} \rrbracket}} \otimes \ket{{\llbracket \underline{T} \rrbracket}}_{{\llbracket \underline{S} \rrbracket}}
\\&\xmapsto{\makebox[1cm]{\scriptsize$2\times$ der}} {\llbracket \underline{T} \rrbracket} \otimes {\llbracket \underline{S} \rrbracket} + {\llbracket \underline{S} \rrbracket} \otimes {\llbracket \underline{T} \rrbracket}
\\&\xmapsto{\makebox[1cm]{\scriptsize${2\times} {R \multimap}$}} \ket{\alpha_1,\ldots,\alpha_s}_{\gamma} \otimes \ket{\beta_1,\ldots,\beta_r}_{\delta} \otimes \big({\llbracket \underline{T} \rrbracket} \otimes {\llbracket \underline{S} \rrbracket} + {\llbracket \underline{S} \rrbracket} \otimes {\llbracket \underline{T} \rrbracket}\big)
\\&\xmapsto{\makebox[1cm]{\scriptsize$2\times$ ctr}} \sum_{I,J} \ket{\alpha_I}_{\gamma} \otimes \ket{\beta_J}_{\delta} \otimes \ket{\alpha_{I^c}}_{\gamma} \otimes \ket{\beta_{J^c}}_{\delta} \otimes \big( {\llbracket \underline{T} \rrbracket} \otimes {\llbracket \underline{S} \rrbracket} + {\llbracket \underline{S} \rrbracket} \otimes {\llbracket \underline{T} \rrbracket} \big)
\\&\xmapsto{\makebox[1cm]{}} \sum_{I,J} {\llbracket \underline{S} \rrbracket}\big( \ket{\alpha_I}_{\gamma} \otimes \ket{\beta_J}_{\delta} \big) \circ {\llbracket \underline{T} \rrbracket}\big( \ket{\alpha_{I^c}}_{\gamma} \otimes \ket{\beta_{J^c}}_{\delta} \big)
\\& \qquad\qquad + \sum_{I,J} {\llbracket \underline{T} \rrbracket}\big( \ket{\alpha_I}_{\gamma} \otimes \ket{\beta_J}_{\delta} \big) \circ {\llbracket \underline{S} \rrbracket}\big( \ket{\alpha_{I^c}}_{\gamma} \otimes \ket{\beta_{J^c}}_{\delta} \big)\end{aligned}$$ which agrees with ${\llbracket \underline{ST} \rrbracket} + {\llbracket \underline{TS} \rrbracket}$ on $\ket{\alpha_1,\ldots,\alpha_s}_{\gamma} \otimes \ket{\beta_1,\ldots,\beta_r}_{\delta}$ by Lemma \[lemma:derivative\_bint\].

Multiplication {#section:mult}
--------------

The multiplication of Church numerals is encoded by a proof $\mult_A$ of ${!} \inta_A, \inta_A \vdash \inta_A$, see for example [@girard_complexity §2.5.2]. To construct the proof tree it will be convenient to introduce the following intermediate proof $\gamma$, writing $E = A \multimap A$ as above:

Then ${\llbracket \gamma \rrbracket}: {!}\operatorname{End}_k(V) \otimes {!}{\llbracket \inta_A \rrbracket} \to {!}\operatorname{End}_k(V)$ is a morphism of coalgebras such that $${\llbracket \gamma \rrbracket}(t \otimes \vacu_\alpha) = \vacu_{\alpha(t)} \qquad \text{and} \qquad {\llbracket \gamma \rrbracket}(t \otimes \ket{\nu}_\alpha) = \ket{\nu(t)}_{\alpha(t)},$$ for $\alpha, \nu \in {\llbracket \inta_A \rrbracket} = \Hom_k({!}\operatorname{End}_k(V), \operatorname{End}_k(V))$ and $t \in {!} \operatorname{End}_k(V)$. The proof $\mult_A$ is

Let $l,m,n \ge 0$ be integers. We write $\mult_A(-,n)$ for the proof of ${!} \inta_A \vdash \inta_A$ obtained from the above by cutting against the proof $\underline{n}$ of $\vdash \inta_A$. The derivative of this proof at $\alpha = {\llbracket \underline{l} \rrbracket}$ in the direction of $\nu = {\llbracket \underline{m} \rrbracket}$ is the element of ${\llbracket \inta_A \rrbracket}$ given on $t \in {!} \operatorname{End}_k(V)$ by $$\begin{aligned}
{\llbracket \mult_A \rrbracket}\big(\ket{\nu}_\alpha \otimes {\llbracket \underline{n} \rrbracket}\big)(t)
= {\llbracket \underline{n} \rrbracket}\big(\ket{\nu(t)}_{\alpha(t)}\big)
= \sum_{i = 1}^{n} \alpha(t)^{i-1} \nu(t) \alpha(t)^{n-i}\end{aligned}$$ using Lemma \[lemma:nderiv\] in the last step. When $t = \vacu_x$ for $x \in \operatorname{End}_k(V)$, this evaluates to $$\sum_{i = 1}^{n} \alpha(t)^{i-1} \nu(t) \alpha(t)^{n-i} 
= \sum_{i = 1}^{n} x^{l(i-1)} x^m x^{l(n-i)} 
= n x^{l(n-1)+m}.$$ This result agrees with a more traditional calculus approach using limits: $$\begin{aligned}
&\lim_{h \to 0} \frac{{\llbracket \mult_A \rrbracket}(\vacu_{{\llbracket \underline{l} \rrbracket} + h {\llbracket \underline{m} \rrbracket}} \otimes {\llbracket n \rrbracket})\vacu_x  - {\llbracket \mult_A \rrbracket}(\vacu_{{\llbracket \underline{l} \rrbracket}} \otimes {\llbracket \underline{n} \rrbracket})\vacu_x}{h}\\
&= \lim_{h \to 0} \frac{{\llbracket \underline{n} \rrbracket}\vacu_{x^l + h x^m} - {\llbracket \underline{n} \rrbracket}\vacu_{x^l}}{h} \\
\\&= \lim_{h \to 0} \frac{(x^l + h x^m)^n - x^{ln}}{h} 
\\&= nx^{l(n-1)+m}.\end{aligned}$$ This agreement between limits and the derivatives of Definition \[defn:derivative\_proof\] holds more generally, but will be discussed elsewhere.

The cofree coalgebra {#section:background}
====================

Let $k$ be an algebraically closed field of characteristic zero and ${\mathcal{V}}$ the category of $k$-vector spaces (possibly infinite dimensional). It is straightforward to check that the universal counital cocommutative coalgebra mapping to a finite-dimensional vector space $V$ (i.e. the cofree coalgebra) is the space $\Hom_k^{\cont}(\operatorname{Sym}(V^*),k)$ of linear functionals on the symmetric algebra $\operatorname{Sym}(V^*)$ which vanish on an ideal of finite codimension [@hyland]. Using the Chinese remainder theorem one sees further that this coalgebra breaks into a sum of pieces each isomorphism to a symmetric algebra, that is, that there is an isomorphism of coalgebras \[eq:isocontnu\] \_k\^((V\^\*),k) \_[P V]{} \_P(V) where $\operatorname{Sym}_P(V)$ is the symmetric algebra with its usual coproduct structure. Following the tradition of linear logic, we denote this universal coalgebra ${!} V$. The explicit formulas for the coproduct $\Delta_V$, counit $w_V$ and universal morphism $d_V: {!} V {\longrightarrow}V$ are given in [@murfet_coalg] and [@murfet_ll §5.2]. The universality of $d_V$ means more precisely that for any cocommutative coalgebra $C$ there is an isomorphism $$\begin{gathered}
\Hom_{\operatorname{Coalg}(k)}(C, {!} V) \cong \Hom_{k}(C, V)\,,\\
\Phi \longmapsto d_V \circ \Phi\end{gathered}$$ where the left hand side denotes morphisms of $k$-coalgebras.

We use the following notation from [@murfet_coalg; @murfet_ll]: the image in the summand $\operatorname{Sym}_P(V)$ of ${!} V$ of a tensor $\nu_1 \otimes \cdots \otimes \nu_s \in V^{\otimes s}$ is denoted $$\ket{\nu_1,\ldots,\nu_s}_P = \overline{\nu_1 \otimes \cdots \otimes \nu_s} \in \operatorname{Sym}_P(V) \subseteq {!} V\,.$$ By definition $\ket{\nu_{\tau(1)}, \ldots, \nu_{\tau(s)}}_P$ is the same element of ${!} V$ for any permutation $\tau \in \mathfrak{S}_s$. The identity $1 \in \operatorname{Sym}_P(V)$ is denoted $\ket{\emptyset}_P$. Given a subset $C = \{i_1,\ldots,i_t\} \subseteq \{1,\ldots,s\}$ we write $\ket{\nu_C}_P$ for $\ket{\nu_{i_1},\ldots,\nu_{i_t}}_P$. By [@murfet_coalg Theorem 2.22] the unique morphism of coalgebras $\delta: {!} V {\longrightarrow}{!} {!} V$ lifting the identity on ${!} V$, that is, satisfying $d_{{!} V} \circ \delta = 1_{{!} V}$, is given for $P, \nu_1,\ldots,\nu_s \in V$ by the formula \_P = \_ | \_P, …, \_P \_Q where $Q = \ket{\emptyset}_P$. As a special case $\delta\ket{\emptyset}_P = \ket{\emptyset}_Q$. By construction the tuple $({!}, \delta, d, \Delta, w)$ is a coalgebra modality on ${\mathcal{V}}$ in the sense of [@blutecs Definition 2.1].

Tangent vectors {#section:tangent_vectors}
---------------

There is a well-known connection between the cofree coalgebra and tangent vectors, arising from the identification of the former with a coalgebra of distributions on $V$. We review this point of view at the end of Section \[section:residues\]. But first we recall the approach to this connection of [@murfet_ll Appendix B] which emphasises the ring of dual numbers $k[\varepsilon]/(\varepsilon^2)$. In algebraic geometry this ring represents tangent vectors, in the sense that there is a bijection between morphisms of $k$-schemes $\operatorname{Spec}(k[\varepsilon]/\varepsilon^2) {\longrightarrow}X$ and pairs $(P, \nu)$ consisting of a closed point $P \in X$ and a tangent vector $\nu \in T_P X = ({\mathfrak{m}}/{\mathfrak{m}}^2)^*$ where ${\mathfrak{m}} \subseteq {\mathcal{O}}_{X,P}$ is the maximal ideal.

When $X = \operatorname{Spec}(\operatorname{Sym}(V^*))$ for a finite-dimensional vector space $V$, the closed points of $X$ are in bijection with vectors in $V$, and the tangent space $T_P X$ is canonically isomorphic to $V$. Hence a morphism $\Phi: \operatorname{Spec}(k[\varepsilon]/(\varepsilon^2)) {\longrightarrow}X$ is determined by two vectors $P, \nu \in V$. This data is naturally associated with the element $$\ket{\nu}_P \in {!} V$$ as follows. Let ${\mathcal{T}} = (k[\varepsilon]/(\varepsilon^2))^*$ with its natural coalgebra structure. Then $$\begin{aligned}
\Hom_{\operatorname{Sch}/k}\!\big(\operatorname{Spec}(k[\varepsilon]/(\varepsilon^2)), X\big) &\cong \Hom_{\operatorname{Alg}(k)}\!\big(\operatorname{Sym}(V^*), k[\varepsilon]/(\varepsilon^2)\big)\\
&\cong \Hom_{k}(V^*, k[\varepsilon]/(\varepsilon^2))\\
&\cong \Hom_{k}({\mathcal{T}}, V)\\
&\cong \Hom_{\operatorname{Coalg}(k)}({\mathcal{T}}, {!} V)\,.\end{aligned}$$ Under these bijections the scheme morphism $\Phi$ corresponds to the linear map : V\^\* k\[\]/(\^2), (f) = f(P) 1 + \_( f )|\_[x=P]{} and to the morphism of coalgebras \[eq:app\_psiman\] : [!]{} V, ( 1 ) = \_P, ( \^\* ) = \_P. This justifies the identification of $\ket{\nu}_P \in {!} V$ with the tangent vector $\nu$ at $P \in X$.

Under the isomorphism the element $\ket{\nu}_P$ corresponds to the functional taking the derivative of a function $f \in \operatorname{Sym}(V^*)$ in the direction $\nu$ at $P$. One way to talk about such distributions for arbitrary fields is the framework of local cohomology and residues, which we now recall from [@murfet_coalg].

Local cohomology and residues {#section:residues}
-----------------------------

For a finite-dimensional vector space $V$ of dimension $n$ with $R = \operatorname{Sym}(V^*)$, one proves using local duality [@murfet_coalg Theorem 2.6] that there is an isomorphism \[eq:otherbangV\] \_[P V]{} H\^[n]{}\_[P]{}(R, \^n\_[R/k]{}) \_k\^((V\^\*),k) , where $H^n_P$ denotes local cohomology at $P$ [@residuesduality]. This isomorphism is defined by sending a class $\tau$ in the local cohomology at $P$ to the functional $f \mapsto \Res_P(f \tau)$ where $\Res_P$ denotes a generalised residue and $f \tau$ the action by $R$ on local cohomology. The connection between and is given by an isomorphism $H^{n}_{P}(R, \Omega^n_{R/k}) \cong \operatorname{Sym}_P(V)$ identifying the identity $\ket{\emptyset}_P$ in $\operatorname{Sym}_P(V)$ with the class of the meromorphic differential form [@murfet_coalg Definition 2.9] H\^[n]{}\_[P]{}(R, \^n\_[R/k]{}). It is easy to see that $$\label{eq:residue_differentiates}
\Res_P\Big( f \ket{\nu}_P \Big) = \partial_{\nu}( f )|_{x = P}\,,$$ and more generally that [@murfet_coalg Lemma 2.13] $$\label{eq:residue_differentiates2}
\Res_P\Big( f \ket{\nu_1,\ldots,\nu_s}_P \Big) = \partial_{\nu_1} \cdots \partial_{\nu_s}( f )|_{x = P}\,.$$ Thus we may identify elements of ${!} V$ with functionals on the space of polynomial functions, given by taking derivatives at points of $V$.

When $k = \mathbb{C}$ with $V = \mathbb{C} \nu$ and $z = \nu^*$ the generator of $R = \mathbb{C}[z]$, this is nothing but the Cauchy integral formula since we have \_P = , \_P = and the Cauchy formula says $$f'(P) = \frac{1}{2 \pi i} \oint_\gamma \frac{f(z)}{(z-P)^2} {\operatorname{d}\!{z}}\,.$$

\[remark:distr\] When $k = \mathbb{R}$ this agrees with the analytic theory of distributions, since by [@friedlander Theorem 3.2.1] the $\mathbb{C}$-vector space of distributions on the real manifold $V$ supported at a point $P$ is spanned by the functions $$f \longmapsto \partial_{\nu_1} \cdots \partial_{\nu_s}(f)|_{x=P}$$ as $s \ge 0$ and $\nu_1,\ldots,\nu_s$ varies over all sequences in $V$. So in this case we can identify the coalgebra ${!} V \otimes_{\mathbb{R}} \mathbb{C}$ with the space of distributions on $V$ with finite support.

In the semantics of differential linear logic defined using finiteness spaces [@ehrhard-finiteness] and convenient vector spaces [@blutecon] the space ${!} V$ is a closure of the linear span of Dirac distributions (in our notation, $\ket{\emptyset}_P$) on $V$. More precisely, if $V$ is a finite-dimensional convenient vector space then ${!} V$ consists of distributions of compact support, which are obtained as limits of Dirac distributions. For example, see [@blutecs Theorem 5.7] for the limit defining the distribution $\ket{v}_0$ in our notation. There is a very similar role for Dirac distributions in the Coherent Banach space semantics of linear logic in [@girard_banach §3.2].

It is interesting to note that functional programs extended with Dirac distributions have already been considered in the literature on automatic differentiation; see [@nilsson]. For an abstract categorical theory of distributions via monads, see [@kock].

Any cocommutative coalgebra is the direct limit of finite-dimensional coalgebras, and the category of finite-dimensional cocommutative coalgebras is isomorphic to the category of zero-dimensional schemes over $k$. This is taken as the starting point of one approach to noncommutative geometry which has been influential in the study of $A_\infty$-algebras, where one posits that an arbitrary coalgebra is the coalgebra of distributions on a “noncommutative space” [@kontnc p.15], [@kontnc2; @lebruyn].

\[remark:justify\] Definition \[defn:D\] is justified as follows: adding $\nu$ to a ket, under the residue, contributes a partial derivative in the direction of $\nu$ by . Stating this in a different way, observe that there is a canonical map $\iota: V {\longrightarrow}{\mathcal{D}}(R)$ sending $\nu \in V$ to the differential operator $\partial_\nu$ and we have a $k$-linear map @C+2pc[ H\^n\_P(R, \^n\_[R/k]{}) V \^-[1 ]{} & H\^n\_P(R, \^n\_[R/k]{}) (R) \^-[a]{} & H\^n\_P(R, \^n\_[R/k]{}) ]{} where $a$ denotes the action of the ring ${\mathcal{D}}(R)$ on local cohomology [@murfet_coalg Lemma 2.7]. These maps assemble in the colimit to give .

[BHLS03]{}

R. Blute, T. Ehrhard and C. Tasson, *A convenient differential category*, arXiv preprint [\[arXiv:1006.3140\]](https://arxiv.org/abs/1006.3140), 2010.

R. Blute, J. Cockett and R. Seely, *Differential categories*, Mathematical Structures in Computer Science 16.06, pp.1049–1083, 2006.

G. Corliss, *Automatic differentiation bibliography*, in Automatic Differentiation of Algorithms: Theory, Implementation, and Application, pp. 331–353. SIAM, Philadelphia, Pennsylvania, USA, 1991. [updated on-line version](http://liinwww.ira.uka.de/bibliography/-Math/auto.diff.html).

T. Ehrhard, *On Köthe sequence spaces and linear logic*, Mathematical Structures in Computer Science 12, pp. 579–623, 2002.

[to3em]{}, *Finiteness spaces*, Mathematical Structures in Computer Science 15, pp. 615–646, 2005.

[to3em]{}, *An introduction to Differential Linear Logic: proof-nets, models and antiderivatives*, arXiv preprint [\[arXiv:1606.01642\]](https://arxiv.org/abs/1606.01642) 2016.

T. Ehrhard and O. Laurent, *Interpreting a finitary $\pi$-calculus in differential interaction nets*, International Conference on Concurrency Theory, Springer Berlin Heidelberg, 2007.

T. Ehrhard and L. Regnier, *The differential $\lambda$-calculus*, Theoretical Computer Science 309, pp. 1–41, 2003.

[to3em]{}, *Differential interaction nets*, Theoretical Computer Science 364, pp. 166–195, 2006.

M. Fiore, *Differential structure in models of multiplicative biadditive intuitionistic linear logic*, Proceedings of TLCA, pp. 163–-177, 2007.

F. Friedlander and M. Joshi, *Introduction to the Theory of Distributions*, Cambridge University Press, 1998.

A. Frolicher and A. Kriegl, *Linear spaces and differentiation theory*, Wiley, 1988.

J.-Y. Girard, *Linear Logic*, Theoretical Computer Science 50 (1), 1–102, 1987.

[to3em]{}, *Normal functors, power series and the $\lambda$-calculus* Annals of Pure and Applied Logic, 37: 129–177, 1988.

[to3em]{}, *Light linear logic*, Information and Computation 14, 1995.

[to3em]{}, *Coherent Banach spaces: a continuous denotational semantics*, Theoretical Computer Science 227.1, pp. 275–297, 1999.

J.-Y. Girard, Y. Lafont, and P. Taylor, *Proofs and Types*, Cambridge Tracts in Theoretical Computer Science 7, Cambridge University Press, 1989.

R. Hartshorne, *Residues and duality*, Lecture Notes in Mathematics, No. 20, Springer-Verlag, Berlin, 1966.

M. Hyland and A. Schalk, *Glueing and orthogonality for models of linear logic*, Theoretical Computer Science, 294: 183–231, 2003.

A. Kock, *Commutative monads as a theory of distributions*, Theory and Applications of Categories 26.4 (2012): 97–131.

M. Kontsevich and Y. Soibelman, *Notes on $A_\infty$-algebras, $A_\infty$-categories and non-commutative geometry*, In Homological mirror symmetry (pp. 1-67). Springer Berlin Heidelberg, 2008.

[to3em]{}, *Deformation theory*, in preparation, accessible [\[online\]](https://www.math.ksu.edu/~soibel/Book-vol1.ps), 2002.

L. Le Bruyn, *Noncommutative geometry and dual coalgebras*, arXiv preprint, [\[arXiv:0805.2377\]](http://arxiv.org/abs/0805.2377), 2008.

P-A. Melliès, *Categorical semantics of linear logic*, in Interactive models of computation and program behaviour, Panoramas et Synthèses $27$, Société Mathématique de France, 2009.

D. Murfet, *On Sweedler’s cofree cocommutative coalgebra*, J. Pure and Applied Algebra. 219, pp. 5289–5304 [\[arXiv:1406.5749\]](http://arxiv.org/abs/1406.5749), 2015.

[to3em]{}, *Logic and linear algebra: an introduction*, arXiv preprint, [\[arXiv:1407.2650\]](https://arxiv.org/abs/1407.2650), 2014.

H. Nilsson, *Functional automatic differentiation with [D]{}irac impulses*, In ACM SIGPLAN Notices (Vol. 38, No. 9, pp. 153-164), 2003.

R. Paige and S. Koenig, *Finite differencing of computable expressions*, ACM Transactions on Programming Languages and Systems (TOPLAS), 4(3), pp. 402–454, 1982.

G. Ramalingam and T. Reps, *A categorized bibliography on incremental computation*, In POPL, pp. 502–510. ACM, 1993.

W. Seiler, *Involution: The formal theory of differential equations and its applications in computer algebra* (Vol. 24), Springer Science & Business Media, 2009.

M. Sweedler, *Hopf Algebras*, W. A. Benjamin, New York, 1969.
