<figure><img src="image_1.png" /></figure>

HAL
open science

# Combining fixpoint and differentiation theory

Zeinab Galal, Jean-Simon Pacaud Lemay

► To cite this version:

Zeinab Galal, Jean-Simon Pacaud Lemay. Combining fixpoint and differentiation theory. LICS 2024 - 39th Annual ACM/IEEE Symposium on Logic in Computer Science, Jul 2024, Tallinn, Estonia. pp.1-14, 10.1145/3661814.3662108 . hal-04834931

HAL Id: hal-04834931

https://inria.hal.science/hal-04834931v1

Submitted on 12 Dec 2024

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_2.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Combining fixpoint and differentiation theory

Zeinab Galal

University of Bologna

Italy

Inria Sophia Antipolis

France

Jean-Simon Pacaud Lemay

Macquarie University

Australia

## ABSTRACT

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

## CCS CONCEPTS

* Theory of computation → Categorical semantics; * Mathematics of computing → Differential calculus.

## KEYWORDS

Categorical semantics, Cartesian differential categories, fixpoint operators

### ACM Reference Format:

Zeinab Galal and Jean-Simon Pacaud Lemay. 2024. Combining fixpoint and differentiation theory. In *39th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS '24)*, July 8–11, 2024, Tallinn, Estonia. ACM, New York, NY, USA, 16 pages. https://doi.org/10.1145/3661814.3662108

# 1 INTRODUCTION

Fixpoint theory has many applications for establishing the existence and uniqueness of solutions for systems of differential and integral equations. Dually, using the information provided by derivatives to approximate more efficiently fixpoints is a key tool in numerical analysis, data-flow analysis, automatic differentiation, enumerative combinatorics, formal language theory, etc. A well-known example is the Newton-Raphson method for fast approximation of roots or fixpoints of differentiable functions. Starting from an initial point, the main idea is to compute the next iteration by using the tangent line. It is a powerful technique as the convergence rate is

quadratic: at each iteration, the number of accurately computed digits doubles. Many other standard optimization methods are based on generalizations or variants of the Newton-Raphson method.

From the viewpoint of programming languages, fixpoints are a key feature as they allow for the presence of loops and defining programs via recursion or iteration. Incorporating recursive features into differential programming languages has seen increasing interest in recent years [1, 17, 51] and there is already a rich literature on implicit automatic differentiation to perform automatic differentiation efficiently on functions defined implicitly by fixpoint equations [3, 5, 33].

While the categorical semantics of differentiation and fixpoints are now well-established lines of research, one aspect that has not yet been studied in full detail is the interaction between them from a semantical viewpoint. The objective of this paper is to develop a denotational framework to combine fixpoints with derivatives by axiomatizing the notion of Cartesian differential categories with a fixpoint operator. This axiomatization provides a guideline to introducing differentials to $\lambda$-calculi with fixpoint operators such as PCF [54] and the $\lambda$-Y-calculus [60].

Cartesian differential categories (Definition 2.1) were introduced by Blute, Cockett, and Seely in [8], and provide the categorical foundations of multivariable differential calculus. Cartesian closed differential categories (Section 6) provide the categorical semantics of the differential $\lambda$-calculus, introduced by Ehrhard and Regnier [9, 20, 50]. Cartesian (closed) differential categories have been quite successful in formalizing various notions related to differentiation, and have also found numerous applications in both mathematics and computer science. Moreover, Cartesian differential categories belong to a larger story of categorical foundations of differentiation, which include differential categories [7], coherent differential categories [21], reverse differential categories [13], differential restriction categories [12], and tangent categories [11].

In this paper, we show how to combine the differential operator in a Cartesian differential category with various categorical notions of fixpoint operators [6, 35, 36, 38, 57] such as parametrized fixpoint operators (Definition 3.2) and Conway operators (Definition 4.2). As such, to this end, we introduce Cartesian differential fixpoint categories (Definition 3.3), which are Cartesian differential categories equipped with a parametrized fixpoint operator which satisfies what we call the differential-fixpoint rule (6) describing the derivative of the parametrized fixpoint.

To help understand the differential-fixpoint rule, let us provide some intuition using ordinary calculus. Consider the smooth function $f: \mathbb{R} \times \mathbb{R} \to \mathbb{R}$ defined as $f(x, y) := 1 - x^2y$. Then the function $g: \mathbb{R} \to \mathbb{R}$ defined as $g(x) := \frac{1}{1+x^2}$ is a solution of the fixpoint or implicit equation

$$g(x) = f(x, g(x)). \qquad (1)$$

<footnote>Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from permissions@acm.org.</footnote>

<footnote>LICS '24, July 8–11, 2024, Tallinn, Estonia</footnote>

<footnote>© 2024 Copyright held by the owner/author(s). Publication rights licensed to ACM.</footnote>

<footnote>ACM ISBN 979-8-4007-0660-8/24/07...$15.00</footnote>

<footnote>https://doi.org/10.1145/3661814.3662108</footnote>
If we differentiate both sides, using the chain rule on the right-hand side, we obtain:

$$g'(x) = \frac{\partial f}{\partial x}(x, g(x)) + \frac{\partial f}{\partial y}(x, g(x)) \cdot g'(x) \quad (2)$$

Provided that $\frac{\partial f}{\partial y}(x, g(x)) \neq 1$, we may rewrite (2) as:

$$g'(x) = \left(1 - \frac{\partial f}{\partial y}(x, g(x))\right)^{-1} \frac{\partial f}{\partial x}(x, g(x)) = \frac{-2x}{(1 + x^2)^2}$$

relating the derivative of $f$ with the derivative of its fixpoint. This is the basis of many iteration schemes to compute or approximate the derivative of a fixpoint such as the Newton-Raphson method. If we combine the equations (1) and (2), we obtain that the function $T(g) : \mathbb{R} \times \mathbb{R} \to \mathbb{R} \times \mathbb{R}$ defined as $T(g)(x, a) = (g(x), g'(x) \cdot a)$ is a fixpoint for the function $T(f) : \mathbb{R} \times \mathbb{R} \times \mathbb{R} \times \mathbb{R} \to \mathbb{R} \times \mathbb{R}$ defined as:

$$T(f)(x, y, a, b) = (f(x, y), \frac{\partial f}{\partial x}(x, y) \cdot a + \frac{\partial f}{\partial y}(x, y) \cdot b). \quad (3)$$

This $T$ operation is called the *tangent bundle functor* (Definition 2.2), and can be defined in any Cartesian differential category (it corresponds to the tangent bundle in algebraic geometry and to the Jacobian vector product in forward differentiation). Therefore, computing the derivative of the fixpoint of $f$ is equivalent to computing the fixpoint of $T(f)$, and this is the property we axiomatize for Cartesian differential categories.

**Outline:** Section 2 is a background section where we review Cartesian differential categories. In Section 3, we study the compatibility relation between parametrized fixpoint operators and differential combiners, and introduce Cartesian differential fixpoint categories. In Section 4, we consider the case of Conway operators, and prove an equivalence between various axioms relating derivatives and fixpoints. In Section 5, we study the relation between fixpoints and linearity. In Section 6, we consider the Cartesian closed setting. In Section 7, we provide many examples of Cartesian differential fixpoint categories. In Section 8, we provide an application by extending the Newton-Raphson optimization method to our setting. We conclude in Section 9 with a discussion about future work.

**Related works:** In [19, Theorem 5.29], Ehrhard proves a compatibility relation in a cpo-enriched setting between the least fixpoint operator (in the coKleisli category) and the tangent bundle functor of a Scott coherent differential category. In [59], Sprunger and Katsumata construct Cartesian differential categories with delayed trace operators, which are related to trace operators but no longer assume the fixpoint axiom.

**Conventions:** We assume the reader is familiar with basic notions of category theory such as categories, functors, products, etc. An arbitrary category will be denoted by $\mathbb{C}$, with arbitrary objects denoted by capital letters $A, B, X, Y$, etc. and maps by minuscule letters $f, g, h$, etc. Hom-sets are denoted as $\mathbb{C}(A, B)$, arbitrary maps as $f : A \to B$, identity maps as $1_A : A \to A$, and we use the standard notation $\circ$ and convention for composition (unlike in other Cartesian differential papers which use diagrammatic order).

## 2 CARTESIAN DIFFERENTIAL CATEGORIES

In this background section, we review Cartesian differential categories. For a more in-depth introduction, we refer the reader to [8, 14, 32, 46, 48].

The underlying structure of a Cartesian differential category is that of a *Cartesian left additive category*, which can be described as a category with finite products which is skew-enriched over the category of commutative monoids [32]. More explicitly, a **left additive category** [8, Definition 1.1.1] is a category $\mathbb{C}$ such that each hom-set $\mathbb{C}(A, B)$ is a commutative monoid (written additively), so we have zero maps $0$ and can take the sum of maps $f+g$, however only pre-composition preserves the additive structure, that is,

$$(f+g) \circ x = f \circ x + g \circ x \quad \text{and} \quad 0 \circ x = 0.$$

Maps $f$ which do preserve the additive structure, that is,

$$f \circ (x + y) = f \circ x + f \circ y \quad \text{and} \quad f \circ 0 = 0,$$

are called **additive** maps [8, Definition 1.1.1]. Then a Cartesian left additive category is a left additive category with finite products which is compatible with the additive structure. For a category $\mathbb{C}$ with finite products, we denote the product by $\times$, the projection maps as $\pi_j : A_1 \times \dots \times A_n \to A_j$, the pairing operation by $\langle - , \dots , - \rangle$, the canonical diagonal map by $\Delta_A = \langle 1_A, 1_A \rangle : A \to A \times A$ and the terminal object by $\tau$. Then a **Cartesian left additive category** [8, Definition 1.2.1] is a left additive category $\mathbb{C}$ which has finite products and such that all the projection maps are additive.

A Cartesian differential category is a Cartesian left additive category equipped with a differential combinator, which is an operator which sends maps to their derivative. In this paper, it is important to note that we follow the now more widely used convention used for Cartesian differential categories which flips the convention used in [8], so that the linear argument of the derivative is in the second argument rather than in the first.

**Definition 2.1.** A Cartesian differential category [8, Definition 2.1.1] is a Cartesian left additive category $\mathbb{C}$ equipped with a **differential combinator** $\mathbf{D}$, which is a family of functions indexed by pairs of objects in $\mathbb{C}$:

$$\mathbf{D} : \mathbb{C}(A, B) \to \mathbb{C}(A \times A, B) \qquad \frac{f : A \to B}{\mathbf{D}[f] : A \times A \to B}$$

such that the seven following axioms hold:

$$[\mathbf{D}.1] \quad \mathbf{D}[0] = 0 \text{ and for all } f, g : A \to B,$$

$$\mathbf{D}[f + g] = \mathbf{D}[f] + \mathbf{D}[g]$$

$$[\mathbf{D}.2] \quad \text{for all } f : A \to B \text{ and } x, y, z : C \to A,$$

$$\mathbf{D}[f] \circ \langle x, 0 \rangle = 0 \quad \text{and}$$

$$\mathbf{D}[f] \circ \langle x, y + z \rangle = (\mathbf{D}[f] \circ \langle x, y \rangle) + (\mathbf{D}[f] \circ \langle x, z \rangle)$$

$$[\mathbf{D}.3] \quad \mathbf{D}[1_A] = \pi_2 \text{ and for } j \in \{1, 2\},$$

$$\mathbf{D}[\pi_j] = \pi_j \circ \pi_2 : (A_1 \times A_2) \times (A_1 \times A_2) \to A_j$$

$$[\mathbf{D}.4] \quad \text{for all } f_i : A \to B_i,$$

$$\mathbf{D}[\langle f_1, \dots, f_n \rangle] = \langle \mathbf{D}[f_1], \dots, \mathbf{D}[f_n] \rangle$$

$$[\mathbf{D}.5] \quad \text{for all } f : A \to B, g : B \to C,$$

$$\mathbf{D}[g \circ f] = \mathbf{D}[g] \circ \langle f \circ \pi_1, \mathbf{D}[f] \rangle$$
$$[\text{CD.6}] \quad \text{for all } f : A \to B \text{ and } x, y, z : C \to A, \\ \mathbf{D}[\mathbf{D}[f]] \circ \langle x, y, 0, z \rangle = \mathbf{D}[f] \circ \langle x, z \rangle$$

$$[\text{CD.7}] \quad \text{for all } f : A \to B \text{ and } x, y, z : C \to A, \\ \mathbf{D}[\mathbf{D}[f]] \circ \langle x, y, z, 0 \rangle = \mathbf{D}[\mathbf{D}[f]] \circ \langle x, z, y, 0 \rangle$$

For a map $f : A \to B$, the map $\mathbf{D}[f] : A \times A \to B$ is called the **derivative** of $f$.

The axioms of a differential combinator are analogues of the basic properties of the total derivative from multivariable differential calculus. The axioms say that: (1) the derivative of a sum is the sum of the derivatives, (2) derivatives are additive in their second argument, (3) the derivative of identity maps and projections are projections, (4) the derivative of a pairing is the pairing of the derivatives, (5) the chain rule for the derivative of a composition, (6) the derivative is linear in its second argument, and lastly (7) is the symmetry of the partial derivatives. The term linear refers to the canonical notion of linearity in a Cartesian differential category, which we discuss in Section 5. There is a sound and complete term calculus for Cartesian differential categories [8, Section 4], which is useful for intuition and proofs. So we write:

$$\mathbf{D}[f](a, b) := \frac{\mathrm{d}f(x)}{\mathrm{d}x}(a) \cdot b$$

In particular, the chain rule axiom is expressed as:

$$\frac{\mathrm{d}g(f(x))}{\mathrm{d}x}(a) \cdot b = \frac{\mathrm{d}g(y)}{\mathrm{d}y}(f(a)) \cdot \left( \frac{\mathrm{d}f(x)}{\mathrm{d}x}(a) \cdot b \right)$$

Arguably, the canonical example of a Cartesian differential category is the category of real smooth functions, whose differential combinator is given by the standard differentiation of smooth functions [14, Example 2.10]. In Section 6, we will discuss Cartesian closed differential categories, which are particularly important since they provide the categorical semantics of the differential λ-calculus [9] – though closed structure does not play a crucial role for the story of this paper. In Section 7, we provide other examples of Cartesian differential categories. For more examples of Cartesian differential categories, we refer the reader to see [14, 32].

In a Cartesian differential category, the differential combinator induces a functor called the tangent bundle functor. This functor plays an important role in the story of this paper since, as we will see in Section 3, it fits very naturally with fixpoint operators. The name comes from the fact that every Cartesian differential category is a tangent category [11, Proposition 4.7], and so this functor corresponds to the classical tangent bundle functor for Euclidean spaces.

**Definition 2.2.** For a Cartesian differential category $\mathcal{C}$, the tangent bundle functor [46, Proposition 1] is the endofunctor $\mathbf{T}: \mathcal{C} \to \mathcal{C}$ defined on objects as $\mathbf{T}(A) = A \times A$ and on maps as $\mathbf{T}(f) = \langle f \circ \pi_1, \mathbf{D}[f] \rangle$, which in the term calculus is expressed as:

$$\mathbf{T}(f)(a, b) = \left( f(a), \frac{\mathrm{d}f(x)}{\mathrm{d}x}(a) \cdot b \right)$$

Properties that the tangent bundle functor satisfies can be found in [46, Lemma 2]. It is worthwhile to point out that the tangent bundle preserves composition if and only if the chain rule of the differential combinator holds. In fact, the chain rule can be reformulated in terms of the tangent functor bundle as: $\mathbf{D}[g \circ f] = \mathbf{D}[g] \circ \mathbf{T}(f)$.

# 3 COMBINING FIXPOINTS AND DERIVATIVES

In this section, we combine differential combators and parametrized fixpoint operators by studying their compatibility in an arbitrary Cartesian differential category, and then introduce the notion of a Cartesian differential fixpoint category. For a more in-depth introduction to categorical interpretations of fixpoint operators, we refer the reader to [6, 35, 36, 57].

Let us begin by explaining why for a Cartesian differential category, one must consider a parametrized fixpoint operator rather than simply a basic fixpoint operator. Recall that in a category with a terminal object, a **point** of an object $X$ is a map from the terminal object to $X$, so $p : \top \to X$. Then a **fixpoint operator** [57, Definition 2.1] is an operator fix which for every endomorphism $f : X \to X$ associates a point fix($f$) : $\top \to X$ such

$$f \circ \text{fix}(f) = \text{fix}(f)$$

meaning that fix($f$) is a fixpoint of $f$. Unfortunately, this kind of fixpoint operator is in a certain sense incompatible with differential combators. This is because, in a Cartesian differential category, the derivative of a point $p : \top \to X$ is always zero, $\mathbf{D}[p] = 0$. Therefore:

**LEMMA 3.1.** In a Cartesian differential category with a fixpoint operator, for every map $f : X \to X$, $\mathbf{D}[\text{fix}(f)] = 0$.

For a Cartesian differential category, one must instead consider parametrized fixpoint operators, which axiomatize the notion of fixpoints for maps in context. For a map of type $A \times X \to X$, the parameter $A$ is viewed as representing the context of the term, then taking the parametrized fixpoint gives a map of type $A \to X$. Parametrized fixpoint operators are axiomatized by two axioms: the fixpoint axiom and by naturality in the context argument.

**Definition 3.2.** For a category $\mathcal{C}$ with finite products, a parametrized fixpoint operator [57, Definition 2.2] is a family of functions fix indexed by pairs of objects in $\mathcal{C}$,

$$\text{fix}_A^X : \mathcal{C}(A \times X, X) \to \mathcal{C}(A, X) \qquad \frac{f : A \times X \to X}{\text{fix}_A^X(f) : A \to X}$$

such that the following axioms hold:

1. **Parametrized fixpoint axiom:** for all maps $f : A \times X \to X$:

$$f \circ \langle 1_A, \text{fix}_A^X(f) \rangle = \text{fix}_A^X(f)$$

2. **Naturality axiom:** for all maps $g : A \to B$ and $f : B \times X \to X$:

$$\text{fix}_B^X(f) \circ g = \text{fix}_A^X(f \circ (g \times 1_X))$$

For a map $f : A \times X \to X$, the map fix_A^X($f$) : $A \to X$ is called the **parametrized fixpoint** of $f$.

Since we will be working with term calculus notation for Cartesian differential categories, we shall use the following term calculus notation to write the parametrized fixpoint operator:

$$\text{fix}_A^X(f)(a) = \mu x.f(a, x)$$

where the variable $x$ is bound. The notation $\mu$ here is for an arbitrary fixpoint operator and not necessarily the least fixpoint operator. For example, the parametrized fixpoint axiom, which says that fix_A^X($f$) is a fixpoint of $f$ in context $A$, is expressed as:

$$f(a, \mu x.f(a, x)) = \mu x.f(a, x). \qquad (4)$$
A well-known example of a category with a parametrized fixpoint operator is the category of Scott domains and Scott continuous functions [35, Example 7.1.2], whose parametrized fixpoint operator is given by the standard Kleene iteration formula. In Section 6, we will discuss parametrized fixpoint operators in Cartesian closed categories. In Section 7, we provide other examples of parametrized fixpoint operators. For more examples of parametrized fixpoint operators, we refer the reader to see [35, 36].

So how should a differential combinator and parametrized fix-point operator interact? In particular, what should the derivative of a parametrized fixpoint be? Consider the following computation using the parametrized fixpoint axiom and the chain rule:

$$ \begin{aligned} & \frac{d\mu x.f(u, x)}{du}(a) \cdot b = \frac{df(u, \mu x.f(u, x))}{du}(a) \cdot b \\ & = \frac{df(u, v)}{d(u, v)}(a, \mu x.f(a, x)) \cdot (b, \frac{d\mu x.f(u, x)}{du}(a) \cdot b) \end{aligned} \quad (5) $$

From (4) and (5), we see that the pair

$$ (\mu x.f(a, x), \frac{d\mu x.f(u, x)}{du}(a) \cdot b) $$

is a parametrized fixpoint of $T(f)(a, x, b, y)$ in the x and y variables, that is:

$$ \begin{aligned} T(f)(a, \mu x.f(a, x), b, \frac{d\mu x.f(u, x)}{du}(a) \cdot b) \\ = (\mu x.f(a, x), \frac{d\mu x.f(u, x)}{du}(a) \cdot b) \end{aligned} $$

Thus, our compatibility relation between a parametrized fixpoint operator and differential combinator is asking that the derivative of the parametrized fixpoint be equal to the second component of the nested fixpoint:

$$ \mu(x, y).(f(a, x), \frac{df(u, v)}{d(u, v)}(a, x) \cdot (b, y)). $$

In other words, the derivative of the parametrized fixpoint is the second component of the parametrized fixpoint of the tangent bundle, up to a rearranging of variables. To make certain that this indeed makes sense, let us check that the types work correctly. So starting with a map $f: A \times X \to X$, taking its parametrized fixpoint gives us $\text{fix}_A^X(f): A \to X$, and so its derivative is of type $\text{D}[\text{fix}_A^X(f)]: A \times A \to X$. On the other hand, applying the tangent bundle functor gives us $T(f): A \times X \times A \times X \to X \times X$. For this to be of the correct type to apply the parametrized fixpoint operator, we must swap the middle two terms. So let

$$ c = \langle \pi_1, \pi_3, \pi_2, \pi_4 \rangle : A \times B \times C \times D \to A \times C \times B \times D $$

be the canonical isomorphism which swaps the middle two terms. Then pre-composing by $c$ gives us $T(f) \circ c: A \times A \times X \times X \to X \times X$. So we may take its parametrized fixpoint to get a map of type $\text{fix}_{A \times A}^{X \times X}(T(f) \circ c): A \times A \to X \times X$. Lastly, we post-compose by the second projection to finally get

$$ \pi_2 \circ \text{fix}_{A \times A}^{X \times X}(T(f) \circ c): A \times A \to X. $$

When these two maps are equal (Figure 1), we call this the differential-fixpoint rule and use it as our axiom for the definition of a Cartesian differential fixpoint category.

**Definition 3.3.** A parametrized fixpoint operator for a Cartesian differential category satisfies the **differential-fixpoint rule** if for every map $f: A \times X \to X$, the following equality holds:

$$ \mathbf{D}[\text{fix}_A^X(f)] = \pi_2 \circ \text{fix}_{\text{TA}}^{\text{TX}}(T(f) \circ c) \quad (6) $$

which in the term calculus is expressed as follows:

$$ \frac{d\mu x.f(u, x)}{du}(a) \cdot b = \pi_2(\mu(x, y).(f(a, x), \frac{df(u, v)}{d(u, v)}(a, x) \cdot (b, y))) $$

A Cartesian differential fixpoint category is a Cartesian differential category with a parametrized fixpoint operator which satisfies the differential-fixpoint rule.

We can also ask how the tangent bundle functor and the parametrized fixpoint operator interact. From the differential-fixpoint rule, by definition we have that:

$$ T(\text{fix}_A^X(f)) = \langle \text{fix}_A^X(f) \circ \pi_1, \pi_2 \circ \text{fix}_{\text{TA}}^{\text{TX}}(T(f) \circ c) \rangle $$

However, since the first component of $\text{fix}_{\text{TA}}^{\text{TX}}(T(f) \circ c)$ is not necessarily $\text{fix}_A^X(f) \circ \pi_1$, we may not have that $T(\text{fix}_A^X(f))$ is equal to $\text{fix}_{\text{TA}}^{\text{TX}}(T(f) \circ c)$. When these two are equal, we call this the tangent-fixpoint rule.

**Definition 3.4.** A parametrized fixpoint operator for a Cartesian differential category satisfies the **tangent-fixpoint rule** if for every map $f: A \times X \to X$, the following equality holds:

$$ T(\text{fix}_A^X(f)) = \text{fix}_{\text{TA}}^{\text{TX}}(T(f) \circ c) \quad (7) $$

which in the term calculus is expressed as follows:

$$ \begin{aligned} & (\mu x.f(a, x), \frac{d\mu x.f(u, x)}{du}(a) \cdot b) \\ & = \mu(x, y).(f(a, x), \frac{df(u, v)}{d(u, v)}(a, x) \cdot (b, y)) \end{aligned} $$

It means that the Cartesian functor $(T, c)$ is a morphism of categories with parametrized fixpoint operator (Definition 1.3 in [6] in the coCartesian setting).

It is straightforward to see that the tangent-fixpoint rule implies the differential-fixpoint rule:

**LEMMA 3.5.** A parametrized fixpoint operator which satisfies the tangent-fixpoint rule also satisfies the differential-fixpoint rule.

**PROOF.** By definition, note that $\pi_2 \circ T(f) = \mathbf{D}(f)$. Therefore, post-composing both sides of (7) by the second projection $\pi_2$ results precisely in (6). □

Therefore, a Cartesian differential category with a parametrized fixpoint operator which satisfies the tangent-fixpoint rule is a Cartesian differential fixpoint category. While we do not have an example of a Cartesian differential category with fixpoint operator where the differential-fixpoint rule holds but not the tangent-fixpoint rule, there is no reason to assume that the converse is necessarily true. The reason for choosing the differential-fixpoint rule over the tangent-fixpoint rule as an axiom for Cartesian differential fixpoint categories comes from the fact that it is the differential combinator which is central in the definition of Cartesian differential categories rather than the tangent bundle functor. When asking for compatibility regarding a structure or property on a Cartesian differential
<figure><img src="image_3.png" /><figcaption>Figure 1: Differential-fixpoint rule</figcaption></figure>

category, it is more natural to ask what the derivatives of the necessary structural or property maps are. The tangent-fixpoint rule is more natural when considering a Cartesian differential category instead as a tangent category [11], and will be the central axiom for the notion of a tangent category with a parametrized fixpoint operator (which is future work, see Section 9). That being said, we show that for *Conway* fixpoint operators these two rules are equivalent.

## 4 CONWAY OPERATORS AND DERIVATIVES

Fixpoint operators are closely related to the notion of trace operators. In particular, to give a trace operator for products corresponds to providing a special kind of parametrized fixpoint operator called a *Conway* operator. In this section, we study the compatibility between differential combinators and *Conway* operators (and trace operators), and introduce the notion of a traced Cartesian differential category. For a more in-depth introduction to *Conway* operators and trace operators, we refer the reader to [35, 36, 38].

**Definition 4.1.** For a category $\mathbb{C}$ with finite products, a **trace operator** [38, Section 2] is a family of functions $\text{Tr}$ indexed by triples of objects in $\mathbb{C}$,

$$ \text{Tr}_{A,B}^{X} : \mathbb{C}(A \times X, B \times X) \to \mathbb{C}(A, B) \qquad \frac{f : A \times X \to B \times X}{\text{Tr}_{A,B}^{X}(f) : A \to X} $$

which satisfy the axioms found in [35, Definition 2.1].

As mentioned, for a category with finite products, giving a trace operator is equivalent to giving a special kind of parametrized fixpoint operator called a *Conway* operator. We provide here the axiomatization of a *Conway* operator as found in [35], in terms of dinaturality and Bekić's axiom. Equivalent axiomatizations can be found in [36, 57].

**Definition 4.2.** For a category $\mathbb{C}$ with finite products, a **Conway operator** [35, Theorem 3.1] is a parametrized fixpoint operator fix which also satisfies:

1. **Dinaturality axiom:** for all maps $f : A \times X \to Y$ and $g : Y \to X$

$$ \text{fix}_A^X(g \circ f) = g \circ \text{fix}_A^Y(f \circ (1_A \times g)) $$

which in the term calculus is expressed as:

$$ \mu x.g(f(x, a)) = g(\mu x.f(x, g(a))) $$

2. **Bekić's axiom:** for all maps $f : A \times X \times Y \to X$ and $g : A \times X \times Y \to Y$ the following equality holds:

$$ \text{fix}_A^{X \times Y}((f,g)) = \langle l, \text{fix}_A^Y(g \circ (1_A \times l \times 1_Y) \circ (\Delta_A \times 1_Y)) \rangle $$

where $l := \text{fix}_A^X(f \circ ((1_{A \times X} \times \text{fix}_{A \times X}^Y(g)) \circ \Delta_{A \times X})) : A \to X$. In the term calculus, it is expressed as:

$$ \mu(x, y) (f(a, x, y), g(a, x, y)) = (\mu x.f(a, x, \mu y.g(a, x, y)), \mu y.g(a, \mu x.f(a, x, \mu y.g(a, x, y)), y)) $$

While the right-hand side of Bekić's axiom's expression seems more complex, it is extremely useful in practice. The idea is that Bekić's axiom can be understood as a form of Gaussian elimination: solving a system of nested fixpoint equations with multiple variables is reduced to solving fixpoint equations with one variable at a time. As such, Bekić's axiom will be key in the proofs of this section. Most known fixpoint operators are *Conway* but it is possible to construct fixpoint operators that satisfy all of the axioms but one of the axioms in Definitions 3.2 and 4.2 [23].

For a category with finite products, there is a bijective correspondence between trace operators and *Conway* operators [35, Theorem 3.1]. To go from a *Conway* operator to a trace operator, first recall that by the universal property of the product, a map of type $f : A \times X \to B \times X$ is a tuple of maps $f = \langle f_1, f_2 \rangle$ where $f_1 = \pi_1 \circ f : A \times X \to B$ and $f_2 = \pi_2 \circ f : A \times X \to X$. Then starting with a *Conway* operator fix, define the trace operator Tr on a map $f = \langle f_1, f_2 \rangle : A \times X \to B \times X$ as the following composite:

$$ \text{Tr}_{A,B}^{X}(f)(a) = f_1(\langle 1_A, \text{fix}_A^{X}(f_2) \rangle) $$

which in the term calculus is expressed as:

$$ \text{Tr}_{A,B}^{X}((f_1, f_2)) (a) = f_1(a, \mu x.f_2(a, x)). $$

On the other hand, starting from a trace operator Tr, define the *Conway* operator fix on a map $f : A \times X \to X$ as follows:

$$ \text{fix}_A^X(f) = \text{Tr}_{A,X}^X((f, f)) $$

As such, a category with finite products and a *Conway* operator is a **traced (Cartesian) monoidal category** [38]. So we define:

**Definition 4.3.** A **traced Cartesian differential category** is a Cartesian differential fixpoint category whose parametrized fixpoint operator is a *Conway* operator.

We wish to show that for a *Conway* operator, the differential-fixpoint rule is equivalent to the tangent-fixpoint rule. To do so, it will be useful to consider yet another equivalent rule that even more precisely describes the derivative of the parametrized fixpoint. Notice that when we applied the chain rule to $\frac{d\mu x.f(u,x)}{du}(a) \cdot b$ above, we in fact showed that it was a parametrized fixed point for

$$ \frac{df(u, v)}{du(u, v)} (a, \mu x.f(a, x)) \cdot (b, -). $$

We may then ask that it instead be the parametrized fixpoint.
**Definition 4.4.** A parametrized fixpoint operator for a Cartesian differential category satisfies the **strong differential-fixpoint rule** if for every map $f: A \times X \to X$, the following equality holds:

$$ \mathbf{D}[\mathbf{fix}_A^X(f)] = \mathbf{fix}_{A \times A}^X(\mathbf{D}[f] \circ \langle \pi_1, \mathbf{fix}_A^X(f) \circ \pi_1, \pi_2, \pi_3 \rangle) \quad (8) $$

which in the term calculus is expressed as follows:

$$ \frac{d\mu x.f(u, x)}{du}(a) \cdot b = \mu y. \frac{d f(u, v)}{d(u, v)}(a, \mu x.f(a, x)) \cdot (b, y) $$

We should explain why we chose the differential-fixpoint rule as the axiom for Cartesian differential fixpoint categories instead of the strong differential-fixpoint rule. While the strong differential-fixpoint rule only involves the differential combinator, notice that $\mathbf{fix}_A^X(f)$ appears on both sides of (8). Thus, while both the differential combinator and the tangent bundle functor are used in the differential-fixpoint rule, it is slightly more natural. With all that said, we will show that for a Conway operator, thanks to Bekić's axiom, all three of these rules are equivalent.

**PROPOSITION 4.5.** For a Conway operator fix of a Cartesian differential category, the following are equivalent:

(i) fix satisfies the differential-fixpoint rule;

(ii) fix satisfies the tangent-fixpoint rule;

(iii) fix satisfies the strong differential-fixpoint rule.

**PROOF.** The key to this proof is Bekić's axiom. Before we try to prove the equivalence of these three rules, let us first compute a useful identity using the term calculus. Assuming we have a Conway operator (and not assuming any of the three rules), consider any map $f: A \times X \to X$. To simplify using Bekić's axiom, let $z = (a, b)$, and define

$$ h(z, x, y) = f(a, x) \quad \text{and} \quad k(z, x, y) = \frac{df(u, v)}{d(u, v)}(a, x) \cdot (b, y). $$

Then using Bekić's axiom, we compute that:

$$ \begin{aligned} & \mu(x, y). (h(z, x, y), k(z, x, y)) \\ & = (\mu x.h(z, x, \mu y.k(z, x, y)), \mu y.k(z, \mu x.h(z, x, \mu y.k(z, x, y)), y)) \end{aligned} $$

So we have the equality:

$$ \begin{aligned} & \mu(x, y). (f(a, x), \frac{df(u, v)}{d(u, v)}(a, x) \cdot (b, y)) \\ & = (\mu x.f(a, x), \mu y. \frac{df(u, v)}{d(u, v)}(a, \mu x.f(a, x)) \cdot (b, y)) \end{aligned} \quad (9) $$

Using this identity, we can now prove the desired equivalence. We will prove (ii) ⇒ (i) ⇒ (iii) ⇒ (ii). Now (ii) ⇒ (i) is just Lemma 3.5. For (i) ⇒ (iii), using (9), we can easily expand out the differential-fixpoint rule as:

$$ \begin{aligned} & \frac{d\mu x.f(u, x)}{du}(a) \cdot b \\ & = \pi_2(\mu(x, y).f(a, x), \frac{df(u, v)}{d(u, v)}(a, x) \cdot (b, y))) \\ & = \pi_2(\mu x.f(a, x), \mu y.\frac{df(u, v)}{d(u, v)}(a, \mu x.f(a, x)) \cdot (b, y)) \\ & = \mu y.\frac{df(u, v)}{d(u, v)}(a, \mu x.f(a, x)) \cdot (b, y) \end{aligned} $$

So the strong differential-fixpoint rule holds. For (iii) ⇒ (ii), applying the strong differential-fixpoint rule to (9) gives us that:

$$ \begin{aligned} & \mu(x, y). (f(a, x), \frac{df(u, v)}{d(u, v)}(a, x) \cdot (b, y)) \\ & = (\mu x.f(a, x), \mu y. \frac{df(u, v)}{d(u, v)}(a, \mu x.f(a, x)) \cdot (b, y)) \\ & = \mu(x, y). (f(a, x), \frac{d\mu x.f(u, x)}{du}(a) \cdot b) \end{aligned} $$

So the tangent-fixpoint rule holds. So we conclude that for a Conway operator, the three rules are equivalent. □

Therefore, for a traced Cartesian differential category, its Conway operator satisfies the differential-fixpoint rule, the tangent-fixpoint rule, and the strong differential-fixpoint rule. Since a Conway operator is equivalent to a trace operator, there is yet another equivalent rule involving the trace operator. Unfortunately, there does not appear to be a nice formula for describing the derivative of the trace. Instead, the trace operator behaves quite nicely with the tangent bundle functor. Now for a map $f: A \times X \to B \times X$, we have that

$$ \mathbf{T}(\mathbf{Tr}_{A,B}^X(f)) : A \times A \to B \times B. $$

On the other hand, first applying the tangent functor gives $\mathbf{T}(f) : A \times X \times A \times X \to B \times X \times B \times X$. Before we can take its trace, we must post- and pre-compose by $c$ to get $c \circ \mathbf{T}(f) \circ c : A \times A \times X \times X \to B \times B \times X \times X$. Then taking the trace we finally get a map of type

$$ \mathbf{Tr}_{A \times A, B \times B}^{X \times X}(c \circ \mathbf{T}(f) \circ c) : A \times A \to B \times B. $$

Asking that these maps be equal is equivalent to the other rules.

**PROPOSITION 4.6.** A Cartesian differential category with a Conway operator is a traced Cartesian differential category if and only if for the induced trace operator $\mathbf{Tr}$ and for every map $f: A \times X \to B \times X$, the following equality holds:

$$ \mathbf{T}(\mathbf{Tr}_{A,B}^X(f)) = \mathbf{Tr}_{TA,TB}^{TX}(c \circ \mathbf{T}(f) \circ c) \quad (10) $$

which means that $(T, c)$ is a traced monoidal functor ([38]) where the monoidal product is cartesian.

**PROOF.** For the ⇒ direction, let $f = \langle f_1, f_2 \rangle$. Let us first put $c \circ \mathbf{T}(f) \circ c$ into a pair so that we can take its trace. By [46, Lemma 2.9(iv)], recall that $\mathbf{T}(\langle h, k \rangle) = c \circ \langle \mathbf{T}(h), \mathbf{T}(k) \rangle$. From this it is straightforward to compute that

$$ c \circ \mathbf{T}(f) \circ c = \langle \mathbf{T}(f_1) \circ c, \mathbf{T}(f_2) \circ c \rangle. $$

Then, using the tangent-fixpoint rule, we compute that:

$$ \begin{aligned} \mathbf{Tr}_{TA,TB}^{TX}(c \circ \mathbf{T}(f) \circ c) &= \mathbf{Tr}_{TA,TB}^{TX}(\langle \mathbf{T}(f_1) \circ c, \mathbf{T}(f_2) \circ c \rangle) \\ &= \mathbf{T}(f_1) \circ c \circ \langle 1_{A \times A}, \mathbf{fix}_{TA}^{TX}(\mathbf{T}(f_2) \circ c) \rangle \\ &= \mathbf{T}(f_1) \circ c \circ \langle \mathbf{T}(1_A), \mathbf{T}(\mathbf{fix}_A^X(f_2)) \rangle \\ &= \mathbf{T}(f_1) \circ \mathbf{T}(\langle 1_A, \mathbf{fix}_A^X(f_1) \rangle) \\ &= \mathbf{T}(f_1 \circ \langle 1_A, \mathbf{fix}_A^X(f_2) \rangle) \\ &= \mathbf{T}(\mathbf{Tr}_{A,B}^X(\langle f_1, f_2 \rangle)) = \mathbf{T}(\mathbf{Tr}_{A,B}^X(f)) \end{aligned} $$
So (10) holds as desired. For the $\Leftarrow$ direction, we will show that (10) implies the tangent-fixpoint rule. So for $f: A \times X \to X$, we get:

$$ 
\begin{align*}
\mathbf{T}(\mathbf{fix}_A^X(f)) &= \mathbf{T}(\mathbf{Tr}_{A,X}^X(\langle f, f \rangle)) \\
&= \mathbf{Tr}_{TA,TX}^{\mathbf{TX}}(c \circ \mathbf{T}(\langle f, f \rangle) \circ c) \\
&= \mathbf{Tr}_{TA,TX}^{\mathbf{TX}}(\langle \mathbf{T}(f), \mathbf{T}(f) \rangle \circ c) \\
&= \mathbf{Tr}_{TA,TX}^{\mathbf{TX}}(\langle \mathbf{T}(f) \circ c, \mathbf{T}(f) \circ c \rangle) \\
&= \mathbf{fix}_{TA}^{\mathbf{TX}}(\mathbf{T}(f) \circ c)
\end{align*}
$$

So the tangent-fixpoint rule holds. Then by Proposition 4.5, it follows that we have a traced Cartesian differential category. □

# 5 FIXPOINTS AND LINEARITY

An important notion in a Cartesian differential category is the concept of *linearity*. In particular, linear maps are those whose derivatives are simply themselves evaluated in the second argument. The term linear is justified since in many models, linear in the Cartesian differential category sense corresponds to being linear in the classical algebraic sense.

**Definition 5.1.** In a Cartesian differential category, a map $f: A \to B$ is **linear** [8, Definition 2.1.1] if $\mathrm{D}[f] = f \circ \pi_2$, which in the term calculus is expressed as:

$$ \frac{df(x)}{dx}(a) \cdot b = f(b) $$

For a Cartesian differential category $\mathbb{C}$, its subcategory of linear maps will be denoted as $\mathrm{LIN}[\mathbb{C}]$.

Properties of linear maps can be found in [14, Lemma 2.6], such as the fact that they are closed under composition, sum, and product structure. In particular, every linear map is also additive [14, Lemma 2.6.(i)]. From this, it follows that $\mathrm{LIN}[\mathbb{C}]$ has finite biproducts [8, Corollary 2.2.3]. It is important to note that although linear maps and additive maps often coincide, in an arbitrary Cartesian differential category not every additive map is necessarily linear.

We now consider how linearity interacts with parametrized fixpoint operators. The first natural thing to ask is that the linear maps be the strict maps. Indeed, an important concept for fixpoint operators is the notion of *uniformity*, which is used to characterize fixpoint operators uniquely without relying on order-theoretic arguments. The uniformity axiom is then relative to a subcategory of strict maps.

**Definition 5.2.** In a category $\mathbb{C}$ with finite products and equipped with a parametrized fixpoint operator fix, a map $h: X \to Y$ is **strict** [36, Definition 4.4] if for every $f: A \times X \to X$ and $g: A \times Y \to Y$, if the equality on the left holds, then the equality on the right holds:

$$ h \circ f = g \circ (1_A \times h) \Rightarrow h \circ \mathbf{fix}_A^X(f) = \mathbf{fix}_A^Y(g). $$

which in the term calculus is expressed as:

$$ h(f(a, x)) = g(a, h(x)) \Rightarrow h(\mu x.f(a, x)) = \mu y.g(a, y). $$

**Definition 5.3.** Let $\mathbb{C}$ and $\mathbb{S}$ be categories with finite products, and $J: \mathbb{S} \to \mathbb{C}$ be a bijective-on-objects and strict product preserving functor. Then a parametrized fixpoint operator on $\mathbb{C}$ is **J-uniform** [57, Definition 2.8] if for every map $h$ in $\mathbb{S}$, $J(h)$ is strict in $\mathbb{C}$.

Therefore, $\mathbb{S}$ is understood as a suitable subcategory of strict maps of $\mathbb{C}$. For categories of domain-like structures, the strict maps are usually the ones which preserve bottom elements. In categorical models of Linear Logic with fixpoints, the strict maps of interests are the maps of the base monoidal category. For Cartesian differential categories, it is natural to ask that the linear maps be strict. This can also be expressed in terms of the uniformity axiom by considering the canonical inclusion functor $J: \mathrm{LIN}[\mathbb{C}] \to \mathbb{C}$. Therefore, we may ask that the parametrized fixpoint operator be J-uniform, which we call being *linearly uniform*. Explicitly:

**Definition 5.4.** A parametrized fixpoint operator on a Cartesian differential category is **linearly uniform** if every linear map is strict.

In Section 7.5, we will use the uniformity axiom to make use of a theorem by Plotkin and Simpson [57] so that we can prove the necessary compatibility results between differential combinators and parametrized fixpoint operator in coKleisli categories of comonads satisfying some conditions on bifree algebras.

Linearity also behaves quite nicely with Conway operators. An important first observation is that for a Conway operator, the parametrized fixpoint of a linear map is again linear.

**LEMMA 5.5.** In a traced Cartesian differential category, if a map $f: A \times X \to X$ is linear, then $\mathbf{fix}_A^X(f): A \to X$ is also linear.

**PROOF.** We prove this using the term calculus. Using the strong differential-fixpoint rule and the fact that $f$ is linear, we compute:

$$ \frac{d\mu x.f(u, x)}{du}(a) \cdot b = \mu y. \frac{df(u, v)}{d(u, v)}(a, \mu x.f(a, x)) \cdot (b, y) = \mu y.f(b, y) $$
and we conclude that $\mathbf{fix}_A^X(f)$ is also linear. □

Therefore, if $\mathbb{C}$ is a traced Cartesian differential category with Conway operator fix, then fix is also a Conway operator on $\mathrm{LIN}[\mathbb{C}]$. This in turn means that $\mathrm{LIN}[\mathbb{C}]$ also inherits the trace operator. However, for a category with finite biproducts, to give a trace operator is equivalent to giving a repetition operator [56, Proposition 6.11]. So for a traced Cartesian differential category, its Conway operator induces a repetition operator on its subcategory of linear maps.

**Definition 5.6.** For a category $\mathbb{C}$ with finite biproducts, a **repetition operator** [56, Proposition 6.11] is a family of functions $(-)^*$ indexed by objects in $\mathbb{C}$,

$$ (-)^*_{X}: \mathbb{C}(X, X) \to \mathbb{C}(X, X) \qquad \frac{f: X \to X}{f^*: X \to X} $$

such that the following equalities hold for all $f, g: X \to X$:

1. **Fixpoint axiom:** $f^* = 1_X + f \circ f^*$

2. **Addition axiom:** $(f+g)^* = (f^* \circ g)^* \circ f^*$

3. **Dinaturality axiom:** $(f \circ g)^* \circ f = f \circ (g \circ f)^*$

**COROLLARY 5.7.** For a traced Cartesian differential category $\mathbb{C}$, $\mathrm{LIN}[\mathbb{C}]$ has a repetition operator defined as $f^* = \mathbf{fix}_X^X(\pi_1 + f \circ \pi_2)$, which in the term calculus is expressed as follows:

$$ f^*(a) = \mu x. (a + f(x)). \qquad (11) $$
On the other hand, we can also consider linearity in a certain argument. For the story of this paper, we are particularly interested in maps which are linear in their second argument.

**Definition 5.8.** In a Cartesian differential category, a map $f: A \times X \to B$ is **linear in its second argument** [14, Definition 4.5] (or simply linear in $X$ when there is no confusion) if

$$D[f] \circ \langle a, x, 0, y \rangle = f \circ \langle a, y \rangle$$

which in the term calculus is expressed as:

$$\frac{df(u, v)}{d(u, v)}(a, x) \cdot (0, y) = f(a, y).$$

In particular, [CD.6] is precisely the statement that for any map $f: A \to B$, its derivative $D[f]: A \times A \to B$ is linear in its second argument $A$. Similarly, for a map $f: A_1 \times \dots \times A_n \to B$, we can also define what it means to be linear in its $j$-th argument $A_j$ [32, Definition 2.6]. Now, taking the parametrized fixpoint in a linear argument results in zero. This makes sense since a map $f: A \times X \to X$ which is linear in $X$ is also additive in $X$. In particular, $f(a, 0) = 0$. Thus $0$ is a parametrized fixpoint. It is important to note that $f: A \times X \to X$ being linear in $X$ is quite different from $f$ being linear. Thus the following lemma does not clash with the previous one.

**LEMMA 5.9.** In a traced Cartesian differential category, if a map $f: A \times X \to X$ is linear in $X$ then $\text{fix}_A^X(f) = 0$.

**PROOF.** We use the term calculus again. The key axiom here is [CD.2], which recall says that evaluating a derivative at zero in its second argument is zero. Therefore, using the strong differential-fixpoint rule, we compute that $\mu y.f(a, y)$ is equal to

$$\mu y. \frac{df(u, v)}{d(u, v)} (a, \mu x.f(a, x)) \cdot (0, y) = \frac{d\mu x.f(u, x)}{du} (a) \cdot 0 = 0 \quad \square$$

# 6 CLOSED SETTING

Let us now consider the case when the underlying category is Cartesian closed. This is an important case since Cartesian closed differential categories (also sometimes called differential $\lambda$-categories) provide the categorical semantics of the differential $\lambda$-calculus. For a more in-depth introduction to Cartesian closed differential categories and the differential $\lambda$-calculus, we refer the reader to [9, 10, 14, 20, 50].

For a Cartesian closed category, we denote the internal hom by $A \Rightarrow B$, the evaluation map by $\text{eval}_{A,B}: (A \Rightarrow B) \times A \to B$, and for a map $f: C \times A \to B$, we denote its currying by $\lambda(f): C \to A \Rightarrow B$, which recall is the unique map such that $\text{eval}_{A,B} \circ (\lambda(f) \times 1_A) = f$. As explained in [10, Lemma 4.10], there are two equivalent ways of expressing compatibility between the closed structure and the differential combinator: one in terms of the Curry operator and one in terms of the evaluation map. In terms of the latter, a Cartesian closed differential category [10, Section 4.6] is a Cartesian differential category which is Cartesian closed such that every evaluation map is linear in their internal hom argument (which by our convention means they are linear in their first argument). Another equivalent way of axiomatizing Cartesian closed differential categories is via an axiom which says that the derivative of a Curry is the Curry of the partial derivative [14, Definition 6.2]. Every model

of the differential $\lambda$-calculus 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].

On the other hand, in a Cartesian closed category, fixpoint operators can be internalized with the notion of fixpoint combinator:

**Definition 6.1.** For a Cartesian closed category $\mathcal{C}$, a fixpoint combinator is a family of maps $\{\mathcal{Y}_X : X \Rightarrow X \to X\}_X$ indexed by the objects of $\mathcal{C}$, satisfying the following axiom for all $X$:

$$\mathcal{Y}_X = \text{eval} \circ \langle 1_{X \Rightarrow X}, \mathcal{Y}_X \rangle.$$

The equivalence between parametrized fixpoint operators and fixpoint combinators in the Cartesian closed setting works as follows: starting with a parametrized fixpoint operator fix, for every object $X$, define the map $\mathcal{Y}_X : X \Rightarrow X \to X$ as the parametrized fixpoint of the evaluation map $\text{eval}_{X,X} : (X \Rightarrow X) \times X \to X$, that is,

$$\mathcal{Y}_X := \text{fix}_{X \Rightarrow X}^X (\text{eval}_{X,X}).$$

For the other direction, for every $f: A \times X \to X$, its parametrized fixpoint can be expressed in terms of $\mathcal{Y}_X$ as:

$$\text{fix}_A^X(f) = \mathcal{Y}_X \circ \lambda(f). \qquad (12)$$

From this identity, we can express the differential-fixpoint rule and the others in terms of $\mathcal{Y}$. In particular, we highlight that (14) is the analogue of the equation Ehrhard computes in the coKleisli category of a coherent differential category which is Scott [19, Theorem 5.29].

**PROPOSITION 6.2.** In a Cartesian closed differential category with a parametrized fixpoint fix,

(i) fix satisfies the differential-fixpoint rule if and only if the following equality holds:

$$D[\mathcal{Y}_X] = \pi_2 \circ \mathcal{Y}_{\text{TX}} \circ \lambda (\text{T}(\text{eval}_{X,X}) \circ c) \qquad (13)$$

(ii) fix satisfies the tangent-fixpoint rule if and only if the following equality holds:

$$\text{T}(\mathcal{Y}_X) = \mathcal{Y}_{\text{TX}} \circ \lambda (\text{T}(\text{eval}_{X,X}) \circ c) \qquad (14)$$

(iii) fix satisfies the strong differential-fixpoint rule if and only if the following equality holds:

$$D[\mathcal{Y}_X] = \text{fix}_X \circ \lambda (D[\text{eval}] \circ \langle \pi_1, \mathcal{Y}_X \circ \pi_1, \pi_2, \pi_3 \rangle) \qquad (15)$$

**PROOF.** Let us prove (i). For the $\Rightarrow$ direction, by setting $f = \text{eval}_{X,X}$ in (6), and then using (12), we get that:

$$\begin{align*}
D[\mathcal{Y}_X] &= D[\text{fix}_{X \Rightarrow X}^X (\text{eval}_{X,X})] \\
&= \pi_2 \circ \text{fix}_{\text{TX} \Rightarrow \text{TX}}^{\text{TX}} (\text{T}(\text{eval}_{X,X}) \circ c) \\
&= \pi_2 \circ \mathcal{Y}_{\text{TX}} \circ \lambda (\text{T}(\text{eval}_{X,X}) \circ c)
\end{align*}$$

For the $\Leftarrow$ direction, first recall that $\lambda(g) \circ h = \lambda(g \circ (h \times 1))$. We also have that $\text{T}$ is a strong Cartesian monoidal functor [46, Lemma 2.9(v)]

$$c \circ (\text{T}(f) \times \text{T}(g)) = \text{T}(f \times g) \circ c.$$

From these identities, it follows that

$$\lambda (\text{T}(f) \circ c) \circ \text{T}(g) = \lambda (\text{T}(f \circ (g \times 1)) \circ c).$$
Using this and (12), we compute that:

$$
\begin{align*}
\mathbf{D}[\text{fix}_A^X(f)] &= \mathbf{D}[\mathcal{Y}_X \circ \lambda(f)] \\
&= \mathbf{D}[\mathcal{Y}_X] \circ \mathbf{T}(\lambda(f)) \\
&= \pi_2 \circ \mathcal{Y}_{\mathbf{T}X} \circ \lambda(\mathbf{T}(\text{eval}_{X,X}) \circ c) \circ \mathbf{T}(\lambda(f)) \\
&= \pi_2 \circ \mathcal{Y}_{\mathbf{T}X} \circ \lambda(\mathbf{T}(\text{eval}_{X,X} \circ (\lambda(f) \times 1)) \circ c) \\
&= \pi_2 \circ \mathcal{Y}_{\mathbf{T}X} \circ \lambda(\mathbf{T}(f) \circ c) \\
&= \pi_2 \circ \text{fix}_{\mathbf{T}A}^{\text{TX}}(\mathbf{T}(f) \circ c)
\end{align*}
$$

So the differential-fixpoint rule holds as desired. One can prove (ii) and (iii) using similar computations. □

7 EXAMPLES

7.1 Categories with finite biproducts

Any category $\mathbb{C}$ with finite biproducts is a Cartesian differential category where the differential combinator is given by pre-composition with the second projection: $\mathbf{D}[f] = f \circ \pi_2$ [14, Example 2.10]. If $\mathbb{C}$ comes equipped with a parametrized fixpoint operator such that the projection maps are strict (Definition 5.2), then the differential-fixpoint rule holds, and so $\mathbb{C}$ is a Cartesian differential fixpoint category. On the other hand, any Conway operator on $\mathbb{C}$ can easily be seen to satisfy the strong differential-fixpoint rule. Therefore, any category with finite biproducts which is equipped with a Conway operator (or equivalently a trace operator or a repetition operator) is a traced Cartesian differential category.

7.2 Categories of (weighted) relations

The category Rel whose objects are sets and morphisms are binary
relations between them is one of the most basic models of linear
logic, with many other models arising as refinements of it. The
operation mapping a set A to the set of finite multisets over A,

$$
!A := \{m : A \to \mathbb{N} \mid m \text{ has finite support}\}
$$

can be equipped with a comonad structure on **Rel**. The induced co-
Kleisli category **Rel**! is a Cartesian differential category [9, Section
5.1] and also has a canonical Conway operator [34, Proposition 3].

Binary relations over sets can be generalized to weighted re-
lations over a continuous semi-ring [43]. A continuous semi-ring
is a semi-ring ($\mathbb{S}$, $\leq$, $0$, $+$, $1$, $\cdot$) which is also a cpo, whose zero ele-
ment $0$ is the bottom, and both the addition and multiplication are
continuous. For a continuous semi-ring $\mathbb{S}$, the category $\mathbf{Rel}^\mathbb{S}$ has
objects sets and maps from $A$ to $B$ are functions $R : A \times B \to \mathbb{S}$.
The composite of $R : A \times B \to \mathbb{S}$ and $S : B \times C \to \mathbb{S}$ is the function
$S \circ R : A \times C \to \mathbb{S}$ given by

$$
(S \circ R)(a, c) = \sum_{b \in B} R(a, b) \cdot S(b, c)
$$

where the sum on the right is well defined by the cpo structure of
$\mathbb{S}$. The finite multiset construction also induces a comonad on $\mathbf{Rel}^\mathbb{S}$
and the corresponding co-Kleisli category is a Cartesian differential
category. The derivative of a weighted relation $R : !A \times B \to \mathbb{S}$ is
$\mathbf{D}[R] : !A \times !A \times B \to \mathbb{S}$:

$$
(m, n, b) \mapsto \begin{cases} R(m+n, b) & \text{if } n = [a] \text{ for some } a \in A \\ 0 & \text{otherwise} \end{cases}
$$

The co-Kleisli category $\mathbf{Rel}_!^\mathbb{S}$ also has a Conway operator obtained via Kleene iteration. For a weighted relation $R : !A \times !X \times X \to \mathbb{S}$, its least fixpoint is fix $R : !A \times X \to \mathbb{S}$ inductively defined as fix $R := \bigvee_{n \in \mathbb{N}} \text{fix}_n R$, where for $m \in !A$, we define

$$
\text{fix}_0 R(m) = 0 \quad \text{fix}_{n+1} R(m) = R(m, \text{fix}_n R(m))
$$

with composition in this expression being taken in the co-Kleisli
category. The fixpoint operator defined above satisfies the univer-
sal property of being the unique parametrized fixpoint operator
that is uniform with respect to linear morphisms, which here cor-
respond precisely to the morphisms of Rel<sup>S</sup>. This uniform Con-
way operator and the differential combinator verify the (strong)
differential-fixpoint rule, and therefore Rel<sub>!S</sub> is a traced Cartesian
closed differential category, and moreover the Conway operator is
linearly uniform. This is true because this example is an instance of
a more general statement concerning fixpoint operators obtained
via bifree algebras of comonads [57] – which we discuss in Section
7.5 below. When taking the Boolean semi-ring B = {t, f}, we get
back the relational model, Rel<sub>!S</sub><sup>B</sup> = Rel<sub>!S</sub>.

7.3 Formal Power Series

For a continuous semi-ring $\mathbb{S}$, we may consider the full subcategory of $\mathbf{Rel}_!^\mathbb{S}$ whose objects are the finite sets. This subcategory of finite sets is again a traced Cartesian differential category and is equivalent to the Lawvere theory of formal power series over $\mathbb{S}$. We obtain a traced Cartesian differential category of formal power series over any continuous semi-ring. Even though this is a subcategory of the previous example, since formal power series over continuous semi-rings are used in many areas of computer science, it is worthwhile to spell out some details.

For a continuous semi-ring $\mathbb{S}$, let $\mathbf{PW}^\mathbb{S}$ be the category whose objects are the natural numbers $n \in \mathbb{N}$ and where a map $p : n \to m$ is an $m$-tuple of power series in $n$-variables:

$$
p = (p_1(x_1, \dots, x_n), \dots, p_m(x_1, \dots, x_n)).
$$

Since coefficients are over a continuous semi-ring, the composition
of power series is well-defined. Now for $n \in \mathbb{N}$, define the set $\underline{n}$ as
$\{1, \dots, n\}$. Then the full subcategory $\mathbf{Rel}_!^\mathbb{S}$ with objects restricted to
finite sets of the form $\underline{n} \times \underline{m} \to \mathbb{S}$ in $\mathbf{Rel}_!^\mathbb{S}$ corresponds to the tuple of power
series $p = (p_1(\underline{x}), \dots, p_m(\underline{x}))$ where for $1 \le j \le m$:

$$
p_j(x_1, \dots, x_n) = \sum_{(k_1, \dots, k_n) \in \mathbb{S}^n} R(k_1, \dots, k_n, j) \cdot x_1^{k_1} \dots x_n^{k_n}
$$

Therefore, it follows that PW<sup>S</sup> is a traced Cartesian differential
category. In particular, the least fixpoint in the weighted relational
model corresponds to the least fixpoint for power series over contin-
uous semi-rings first described in [55]. On the other hand, for a map
p : n → 1, which is just a power series in n variables p(x<sub>1</sub>, . . . , x<sub>n</sub>),
applying the differential combinator to it results in the sum of its
partial derivatives:

$$
\mathbf{D}[p](\vec{x}, \vec{a}) = \sum_{i=1}^{n} \frac{\partial p(\vec{x})}{\partial x_i} \cdot a_i
$$
This corresponds to the notation $Dp|_{\vec{x}}(\vec{a})$ in papers such as [25]. By [CD.4], for a tuple $p = (p_1(\vec{x}), \dots, p_m(\vec{x}))$, its derivative is

$$D[p] = (D[p_1](\vec{x}, \vec{a}), \dots, D[p_m](\vec{x}, \vec{a})).$$

## 7.4 Quantale-enriched profunctors

Another possible generalization of the notion of relations is given by the notion of quantale enriched profunctors [39, 61]. A quantale $\mathbb{Q}$ is a complete lattice that is symmetric monoidal closed such that the tensor distributes over arbitrary suprema. Quantales are idempotent semi-rings with join $\lor$ as additive structure and tensor $\otimes$ as multiplicative structure. Instead of having sets as objects, we can consider richer structures given by the notion of quantale enriched categories: for a quantale $\mathbb{Q}$, a $\mathbb{Q}$-category $A$ consists of a set of objects $Ob(A)$ and for all objects $a, b$ an object $A(a, b)$ in $\mathbb{Q}$ together with composition $A(a, b) \otimes A(b, c) \le A(a, c)$ and identity inequalities $1 \le A(a, a)$ in $\mathbb{Q}$. For example, a $\mathbb{Q}$-category for the Lawvere quantale $\mathbb{R}_+ \cup \{\infty\}$ corresponds to the notion of generalized metric space [44].

For $\mathbb{Q}$-categories $A, B$, a $\mathbb{Q}$-profunctor $R: A \to B$ (also called distributors or bimodules) from $A$ to $B$ is a function $R: Ob(A) \times Ob(B) \to B$ with biaction inequalities for all $a, a' \in Ob(A), b, b' \in Ob(B)$:

$$A(a, a') \otimes R(a, b) \otimes B(b', b) \leq R(a', b').$$

There is an analogous free exponential construction mapping a $\mathbb{Q}$-category $A$ to the $\mathbb{Q}$-category $!A$ whose set of objects is the set of finite sequences $\vec{a} = \langle a_1, \dots, a_n \rangle$ of objects of $A$ and for $\vec{a} = \langle a_1, \dots, a_n \rangle$ and $\vec{b} = \langle b_1, \dots, b_m \rangle$, the hom-object is given by

$$!A(\vec{a}, \vec{b}) = \left\{ \begin{array}{ll} \bigvee & \otimes A(a_i, b_{\sigma i}) \quad \text{if } n = m \\ \sigma:n \le n & 1 \le i \le n \\ \perp & \text{otherwise} \end{array} \right.$$

The induced co-Kleisli category has a differential combinator, where the derivative of a $\mathbb{Q}$-profunctor $R: !A \to B$ generalizes the one in the discrete case for weighted relations:

$$((a_1, \dots, a_n), (a'_1, \dots, a'_m), b) \mapsto \left\{ \begin{array}{ll} R((a_1, \dots, a_n, a'_1), b) & \text{if } m=1 \\ \perp & \text{otherwise} \end{array} \right.$$

The induced co-Kleisli category also has a fixpoint operator mapping a $\mathbb{Q}$-profunctor $R: !A \otimes !X \to X$ to fix $R: !A \to X$ obtained by Kleene iteration as $\lor_{n \in \mathbb{N}} \text{fix}_n R$ with $\text{fix}_0 R = \perp$ and

$$\text{fix}_{n+1} R(\vec{a}, x) = \bigvee_{\substack{\vec{y}=(y_1, \dots, y_n) \in !X \\ \vec{a}_0, \dots, \vec{a}_n \in !A}} R(\vec{a}_0, \vec{y}, x) \otimes \bigotimes_{1 \le i \le n} \text{fix}_n R(\vec{a}_i, y_i)$$

So we get a Cartesian differential fixpoint category, which is again an instance of the bifree algebras story in the next section.

## 7.5 Fixpoints from bifree algebras

Recall that for an endofunctor $F: \mathbb{C} \to \mathbb{C}$, a bifree $F$-algebra [57, Section 5] is an initial $F$-algebra $(A, f: FA \to A)$ such that the inverse of $f$ is a final $F$-coalgebra $(A, f^{-1}: A \to FA)$. A result by Simpson and Plotkin allows one to construct a parametrized fixpoint operator in the co-Kleisli category of a comonad whose underlying endofunctor has suitable bifree algebras [57]. We proceed to show that if the co-Kleisli category is also a Cartesian differential category, then it is also a Cartesian differential fixpoint category.

**THEOREM 7.1.** [57, Proposition 6.5 & Theorem 3] Let $\mathbb{C}$ be a category with finite products equipped with a comonad $(F, \delta, \varepsilon)$. Let $J: \mathbb{C} \to \mathbb{C}_F$ be the free functor induced by the comonadic adjunction.

(1) If for all objects $A$ in $\mathbb{C}$, the endofunctors $F(A \times -)$ have a bifree algebra, then $\mathbb{C}_F$ has a unique uniform (with respect to $J$) parametrized fixpoint operator.

(2) If for all objects $A$ in $\mathbb{C}$, the endofunctors $F(A \times F(A \times -))$ and $F(A \times - \times -)$ have a bifree algebra, then $\mathbb{C}_F$ has a unique uniform (with respect to $J$) Conway fixpoint operator.

We give a sketch of how the parametrized fixpoint operator is constructed via bifree algebras. Assume that for all $A$ in $\mathbb{C}$, the endofunctor $F(A \times -)$ has a bifree algebra $w_A: F(A \times \Phi_A) \to \Phi_A$ which we can view as a map $A \times \Phi_A \to \Phi_A$ in the co-Kleisli category $\mathbb{C}_F$. As explained in [57, Section 6], for all $A$ in $\mathbb{C}$, there exists a unique map $t_A: A \to \Phi_A$ in $\mathbb{C}_F$ such that

$$w_A \circ (1_A \times t_A) \circ \Delta_A = t_A.$$

Moreover, for all $f: A \times X \to X$ in $\mathbb{C}_F$, there exists a unique map $u_f: \Phi_A \to X$ in $\mathbb{C}$ such that

$$J(u_f) \circ w_A = f \circ J(1_A \times u_f).$$

Then, for a map $f: A \times X \to X$ in $\mathbb{C}_F$, its parametrized fixpoint is defined as the following composite:

$$\text{fix}_A^X(f) := A \xrightarrow{t_A} \Phi_A \xrightarrow{J(u_f)} X.$$

Now suppose that $\mathbb{C}_F$ is also a Cartesian differential category, such that for all maps $f$ in $\mathbb{C}$, $J(f)$ is linear in $\mathbb{C}_F$. We will now show that the parametrized fixpoint operator defined above satisfies the tangent-fixpoint rule.

To do so, the key to this proof is that if $k$ is linear, then $T(k) = k \times k$ [46, Lemma 2.(iii)]. In particular, for all $g$ in $\mathbb{C}$, we have that $T(J(g)) = J(g) \times J(g)$. Now, to help with notation, define $e: \Phi_{A \times A} \to \Phi_A \times \Phi_A$ as $e := u_{T(w_A) \circ c}$, that is, the unique map such that

$$J(e) \circ w_{A \times A} = T(w_A) \circ c \circ (1_{A \times A} \times J(e)).$$

Then, for $f: A \times X \to X \in \mathbb{C}_F$, we compute that (note $J$ also preserves products strictly):

$$\begin{align*} T(f) \circ c \circ (1_{A \times A} \times J((u_f \times u_f) \circ e)) & \\ &= T(f) \circ c \circ (1_A \times 1_A \times J(u_f) \times J(u_f)) \circ (1_{A \times A} \times J(e)) \\ &= T(f) \circ (1_A \times J(u_f) \times 1_A \times J(u_f)) \circ c \circ (1_{A \times A} \times J(e)) \\ &= T(f) \circ (J(1_A \times u_f) \times J(1_A \times u_f)) \circ c \circ (1_{A \times A} \times J(e)) \\ &= T(f) \circ T(J(1_A \times u_f)) \circ c \circ (1_{A \times A} \times J(e)) \\ &= T(J(u_f)) \circ T(w_A) \circ c \circ (1_{A \times A} \times J(e)) \\ &= (J(u_f) \times J(u_f)) \circ J(e) \circ w_{A \times A} \\ &= J((u_f \times u_f) \circ e) \circ w_{A \times A} \end{align*}$$

By uniqueness, it follows that $u_{T(f) \circ c} = (u_f \times u_f) \circ e$. Dually, since $w_{A \times A}^{-1}$ is a final coalgebra, there is a unique map $p: \Phi_A \times \Phi_A \to \Phi_{A \times A}$ in $\mathbb{C}$ such that

$$J(p) \circ T(w_A) \circ c = w_{A \times A} \circ (1_{A \times A} \times J(p))$$

and also such that $J(p) \circ T(t_A) = t_{A \times A}$, which by uniqueness implies that $e \circ p = 1_{\Phi_A \times \Phi_A}$. Using these identities, we can finally compute
that:

$$
\begin{align*}
\mathbf{fix}_{\mathrm{TA}}^{\mathrm{TX}}(\mathbf{T}(f) \circ c) &= J(u_{\mathrm{T}(f) \circ c}) \circ t_{A \times A} \\
&= J((uf \times uf) \circ e) \circ J(p) \circ \mathbf{T}(t_A) \\
&= (J(uf) \times J(uf)) \circ J(e) \circ J(p) \circ \mathbf{T}(t_A) \\
&= (J(uf) \times J(uf)) \circ \mathbf{T}(t_A) \\
&= \mathbf{T}(J(uf) \circ t_A) = \mathbf{T}(\mathbf{fix}_A^X(f))
\end{align*}
$$

We conclude that the tangent-fixpoint rule holds and that therefore $\mathbb{C}_F$ is a Cartesian differential fixpoint category. This construction subsumes both the example of weighted relations (Section 7.2) and the example of quantale profunctors (Section 7.4) since the free exponential comonad in both examples has the required bifree algebras obtained via enrichment arguments. Both categories of weighted relations and $\mathbb{Q}$- profunctors are cpo-algebraically compact [28–30, 58]: it means that every endofunctor that is cpo-enriched has a bifree algebra and one can verify that the endofunctor of the free exponential comonad in both cases is a cpo-enriched functor. For the weighted relational model, Laird computes these bifree algebras explicitly using nested finite multisets in [42].

7.6 Fixpoint operators from fixpoint objects

A standard construction to obtain fixpoint operators in a Cartesian closed category is via cpo-enrichment. A category $\mathbb{C}$ is $\omega$-cpo enriched if each hom-set $\mathbb{C}$ is an $\omega$-cpo and composition $\mathbb{C}(A, B) \times \mathbb{C}(B, C) \to \mathbb{C}(A, C)$ is Scott-continuous. If in addition, the evaluation and pairing are monotonous, each hom-set $\mathbb{C}(A, B)$ has a bottom element 0 and for all $f$, we have $0 \circ f = 0$ and eval $\circ$ $\langle 0, f \rangle = 0$, it was shown by Berry [4] that the category has a least parametrized fixpoint operator. For each $X$, we can construct a fixpoint combinator morphism $\mathcal{Y}_X : X \Rightarrow X \to X$ as the supremum $\mathcal{Y}_X = \bigvee_n \mathcal{Y}_X^n$ where

$$
\mathcal{Y}_X^0 = 0 \quad \text{and} \quad \mathcal{Y}_X^{n+1} = \text{eval}_{X,X} \circ \langle 1_X \Rightarrow X, \mathcal{Y}_X^n \rangle.
$$

Explicitly, the parametrized fixpoint operator is defined as in (12). Now, if $\mathbb{C}$ is a Cartesian differential category and the cpo bottom elements $0$ coincide with the zero of the additive structure, then we can show that this parametrized fixpoint operator satisfies the tangent-fixpoint rule, or equivalently $\mathcal{Y}_X$ satisfies (14). We omit the proof as it follows the same reasoning as done by Ehrhard in [20, Theorem 5.29] in coherent differential categories with a Scott fixpoint [19]. The known models of (coherent) PCF typically have reflexive objects (retractions ($X \Rightarrow X \triangleleft X$) which provide models of untyped $\lambda$-calculs and are particular cases of fixpoint objects. We prove below that the tangent fixpoint axiom holds for Cartesian closed categories where fixpoint objects induce a fixpoint operator by Lawvere's theorem [45].

THEOREM 7.2. [45, Section 1] In a Cartesian closed category $\mathbb{C}$, if there is a morphism $r: X \to X \Rightarrow X$ such that for every morphism $q: A \to X \Rightarrow X$, there exists a morphism $u: A \to X$ such that $q$ can be factored as $q = r \circ u$, then every morphism $f: A \times X \to X$ has a parametrized fixpoint $\text{fix}_A^X(f): A \to X$.

The construction works as follows: for $f: A \times X \to X$, we first
define the map $p: A \times X \to X$ as

$$
p := f \circ (1_A \times \text{eval}) \circ (1_A \times r \times 1_X) \circ (1_A \times \Delta_X).
$$

Now let $u: A \to X$ be a map factoring $\lambda(p) : A \to X \Rightarrow X$ as $\lambda(p) = r \circ u$. Then the parametrized fixpoint is defined as follows:

$$
\mathbf{fix}_A^X(f) = A \xrightarrow{u} X \xrightarrow{\Delta_X} X \times X \xrightarrow{r \times 1_X} X \Rightarrow X \times X \xrightarrow{\text{eval}_{X,X}} X
$$

To prove the differential-fixpoint rule, we need to impose stronger
conditions. So we assume that for every object X, there is a map
$r_X : X \to X \Rightarrow X$ such that for every map $q : A \to X \Rightarrow X$,
there is a unique morphism $u : A \to X$ such that $q = r_X \circ u$. This
stronger assumption holds automatically for the retraction case
with reflexive objects. We also need the choice of fixpoint objects
to be compatible with the differential structure, so we assume that
for all X,

$$
r_{\mathrm{TX}} = (\pi_1 \Rightarrow 1_{\mathrm{TX}}) \circ \mathrm{T}(r_X).
$$

Moreover, since $\pi_1 \circ \langle 1_X, 0 \rangle = 1_X$, we have that

$$
\mathbf{T}(r_X) = (\langle 1_X, 0 \rangle \Rightarrow \mathbf{1}_{\mathbf{T}X}) \circ r_{\mathbf{T}X}.
$$

Now for a map $f: A \times X \to X$, define $s: TA \times TX \to TX$ as the
following composite:

$$
s := \mathbf{T}f \circ c \circ (1_{\mathcal{TA}} \times \mathrm{eval}) \circ (1_{\mathcal{TA}} \times r_{\mathcal{TX}} \times 1_{\mathcal{TX}}) \circ (1_{\mathcal{TA}} \times \Delta_{\mathcal{TX}}).
$$

Now let $w: \mathcal{TA} \to \mathcal{TX}$ be the unique map such that $r_{\mathcal{TX}} \circ w = \lambda(s)$.
Note that $\mathcal{T}(\Delta_X) = c \circ \Delta_{\mathcal{TX}}$ so we obtain:

$$
\mathbf{fix}_{\mathrm{TA}}^{\mathrm{TX}}(\mathbf{T}(f) \circ c) = \mathrm{eval}_{\mathrm{TX},\mathrm{TX}} \circ (r_{\mathrm{TX}} \times 1_{\mathrm{TX}}) \circ \Delta_{\mathrm{TX}} \circ w
$$

On the other hand, to work out $\mathbf{T}(\mathbf{fix}_A^X(f))$, we use some identities that hold in a Cartesian closed tangent category [31, Section 5.2], so in particular hold in a Cartesian closed differential category. We first have that

$$
\mathbf{T}(\mathrm{eval}_{X,Y}) \circ c = \mathrm{eval}_{TX,TY} \circ ((\pi_1 \Rightarrow 1_{TY}) \times 1_{TX})
$$

which allows us to first compute that $\mathbf{T}(p) \circ c$ is equal to

$$
\begin{align*}
\mathbf{T}(f \circ (1_A \times \text{eval}) \circ (1_A \times r_X \times 1_X) \circ (1_A \times \Delta_X)) \circ c \\
&= \mathbf{T}(f) \circ c \circ (1_{TA} \times \text{eval}) \circ (1_{TA} \times r_{TX} \times 1_{TX}) \circ (1_{TA} \times \Delta_{TX}) = s
\end{align*}
$$

Therefore, $w$ is the unique morphism such that $r_{\mathcal{TX}} \circ w = \lambda(\mathbf{T}(p) \circ c)$.
Moreover, for a map $g: A \times B \to C$, we have that

$$
\mathbf{T}(\lambda(g)) = (\langle 1_B, 0 \rangle \Rightarrow \mathbf{1}_{TC}) \circ \lambda(\mathbf{T}(g) \circ c)
$$

We then compute that:

$$
\begin{align*}
r_{\mathrm{TX}} \circ \mathbf{T}(u) &= (\pi_1 \Rightarrow 1_{\mathrm{TX}}) \circ \mathbf{T}(r_X) \circ \mathbf{T}(u) \\
&= (\pi_1 \Rightarrow 1_{\mathrm{TX}}) \circ \mathbf{T}(\lambda(p)) \\
&= (\pi_1 \Rightarrow 1_{\mathrm{TX}}) \circ (\langle 1_X, 0 \rangle \Rightarrow 1_{\mathrm{TX}}) \circ \lambda(\mathbf{T}(p) \circ c) \\
&= \lambda(\mathbf{T}(p) \circ c)
\end{align*}
$$

By uniqueness, it then follows that $\mathbf{T}(u) = w$, so we may finally
compute that:

$$
\begin{align*}
\mathbf{T}(\mathbf{fix}_A^X(f)) &= \mathbf{T}(\mathrm{eval}) \circ \mathbf{T}(r_X \times 1_X) \circ \mathbf{T}(\Delta_X) \circ \mathbf{T}(u) \\
&= \mathbf{T}(\mathrm{eval}) \circ \mathbf{T}(r_X \times 1_X) \circ c \circ \Delta_{\mathrm{T}(X)} \circ w \\
&= \mathbf{T}(\mathrm{eval}) \circ c \circ (\mathbf{T}(r_X) \times 1_{\mathrm{TX}}) \circ \Delta_{\mathrm{TX}} \circ w \\
&= \mathrm{eval} \circ ((\pi_1 \Rightarrow 1_{\mathrm{TX}}) \times 1_{\mathrm{TX}}) \circ (\mathbf{T}(r_X) \times 1_{\mathrm{TX}}) \circ \Delta_{\mathrm{TX}} \circ w \\
&= \mathrm{eval} \circ (r_{\mathrm{TX}} \times 1_{\mathrm{TX}}) \circ \Delta_{\mathrm{TX}} \circ w \\
&= \mathbf{fix}_A^X(\mathbf{T}(f)) \circ c
\end{align*}
$$

So the tangent-fixpoint rule holds as desired. Note that the uniqueness requirement can be weakened if we assume that the factoring morphisms for $r_X$ and $r_{\mathcal{T}(X)}$ are chosen in a uniform way.
# 8 NEWTON-RAPHSON ITERATION SCHEME

Newton-Raphson iteration has been extended to Kleene algebras or more generally power series over semi-rings [25, 26, 37, 41] where systems of equations in this setting can represent context-free grammars, data-flow equations, authorization problems, datalog queries etc. Newton iteration always converges for power series over $\omega$-continuous semi-rings and if we restrict to idempotent semi-rings, then it was shown to converge after a finite number of steps [25]. Similar ideas were also developed for enumerative combinatorics to compute efficiently large combinatorial structures that are defined via fixpoint equations [16, 52, 53]. In the combinatorial setting, the series always have positive coefficients corresponding to the number of structures of a given size and it also leads to a Newton iteration scheme that is always convergent.

Since combinatorial species are first order terms of a Cartesian differential fixpoint (bi)category [27] and power series over a continuous semi-ring are a subcategory of the weighted relational model, we were motivated to develop a general Newton-Raphson approximation scheme for Cartesian differential fixpoint categories which we present below. While the following construction works for the more general setting of Cartesian differential categories, we chose to present it in the Cartesian closed framework to emphasize the viewpoint of optimization procedures as higher order operators.

## 8.1 Newton approximants

We start by recalling the standard Newton-Raphson iteration method to find or approximate fixpoints for real-valued functions. For a differentiable function $f: \mathbb{R} \to \mathbb{R}$ verifying $f'(a) \neq 1$ for all $a \in \mathbb{R}$, we consider a sequence of Newton approximants $\{z_n\}_{n \in \omega}$ with $z_0 \in \mathbb{R}$ an initial chosen value and for each $n, z_{n+1} := N(f)(z_n)$ where $N(f): \mathbb{R} \to \mathbb{R}$ is defined as

$$N(f): a \mapsto a + \frac{1}{1 - f'(a)} \cdot (f(a) - a).$$

The sequence $\{z_n\}_{n \in \omega}$ may not converge or may not converge to a fixpoint of $f$ but under suitable conditions on $f$, it converges to a fixpoint and the convergence rate is quadratic. Note first that the quotient $\frac{1}{1-f'(a)} = 1+f'(a)+(f'(a))^2+...$ is a solution of the fixpoint equation

$$\frac{1}{1 - f'(a)} = 1 + f'(a) \cdot \frac{1}{1 - f'(a)}$$

which corresponds exactly to the repetition operator fixpoint equation 5.6. The general idea of Newton-Raphson iteration in our setting is to accelerate the computation of the non-linear fixpoint operator in the Cartesian (closed) category combining derivatives with the induced linear repetition operator in the category $LIN[C]$ (11).

While we remain in a setting where everything is non-negative, we want to perform truncated subtractions: for example, in the semiring of non-negative extended reals $\mathbb{R}^\infty_{\ge 0} = ([0, \infty], \ge, \times, 1, +, 0)$, the truncated subtraction operation $a \ominus b$ corresponds to $\min\{0, a-b\}$. For a general Cartesian closed differential fixpoint category $\mathbb{C}$, we know that it is enriched over commutative monoids and we can equip each hom-set $\mathbb{C}(A, B)$ with the natural order relation induced by addition:

$$\forall f, g: A \to B, g \le f \quad \Leftrightarrow \quad \exists h: A \to B, g+h = f.$$

We assume that for every $f$ in $\mathbb{C}(A, B)$, the maps $f + (-)$ and $(-) + f$ have right adjoints for the $\ge$ ordering. Explicitly, for each $f, g, h$ in $\mathbb{C}(a, b)$, there exist maps $f \ominus g$ and $f \ominus h$ such that

$$h \ge f \ominus g \Leftrightarrow g+h \ge f \Leftrightarrow g \ge f \ominus h.$$

It implies the following identities for all $f, g, h$ in $\mathbb{C}(a, b)$ and for every additive map $k: b \to c$:

$$f \ominus (g+h) = (f \ominus g) \ominus h \quad (16)$$

$$f \ge (f+g) \ominus g \quad (17)$$

$$f \le (f \ominus g) + g \text{ and if } f \ge g, \text{ then } f = (f \ominus g) + g \quad (18)$$

$$f \ominus g \le (f \ominus h) + (h \ominus g) \quad (19)$$

$$k \circ (f \ominus g) \ge (k \circ f) \ominus (k \circ g) \quad (20)$$

Since for $f: A \to A$ in $\mathbb{C}$, $D[f]: A \times A \to A$ is linear in its second argument, it implies that for any point $\tau \xrightarrow{a} A$,

$$D_a[f] := D[f] \circ (a \times 1_A) : A \to A$$

is a morphism in $LIN[C]$. Therefore, $(D_a[f])^* : A \to A$ verifies the fixpoint equation

$$(D_a[f])^* \cdot b = b + D_a[f] \cdot ((D_a[f])^* \cdot b).$$

We can now define a map $N: A \Rightarrow A \Rightarrow A \Rightarrow A$ corresponding to Newton-Raphson iteration as follows:

$$f \mapsto \lambda a.(a + (D_a[f])^* \cdot (f(a) \ominus a))$$

To define an analogue of Newton iteration in the parametrized Cartesian case, we recall first the notion of partial derivative. For a map $f: A \times B \to C$, we can obtain its partial derivative [14, Definition 6.2] from the total derivative $D[f]: A \times B \times A \times B \to C$ by precomposing with 0 morphisms:

$$D_1[f] := D[f] \circ (1_A \times 1_B \times (1_A, 0)) : A \times B \times A \to C$$

$$D_2[f] := D[f] \circ (1_A \times 1_B \times (0, 1_B)) : A \times B \times B \to C$$

In term calculus, we write the partial derivatives as:

$$\frac{df(x, b)}{dx}(a) \cdot c = \frac{df(x, y)}{d(x, y)}(a, b) \cdot (c, 0)$$

$$\frac{df(a, y)}{dy}(b) \cdot c = \frac{df(x, y)}{d(x, y)}(a, b) \cdot (0, c)$$

We can also define higher order derivatives by taking the partial derivative of the total derivative. For $f: A \to B$, we define the $n$-th derivative as $f^{(n)} := (D_1)^n[f]: A \times A^n \to B$, it is non-linear in its first argument and multi-linear in its last $n$ arguments. In the term calculus, we write this as:

$$f^{(n)}(a, (b, \dots, b)) = \frac{d^n f(x)}{dx^n}(a) \cdot (b, \dots, b)$$

In the parametrized Cartesian case, we define an operator

$$N: \mathbb{C}(A \times X, X) \to \mathbb{C}(A \times X, X)$$

mapping a morphism $f: A \times X \to X$ to the morphism

$$(a, x) \mapsto x + \left( \frac{df(a, v)}{dv}(x) \right)^* \cdot (f(a, x) \ominus x)$$
To perform Newton iteration, we assume that $\mathbb{C}$ is a Taylor category [18, 19, 22, 40], which means that each map $f: A \to B$ is equal to its Taylor expansion:

$$f(a+b) = \sum_n \frac{1}{n!} \frac{d^n f(x)}{dx^n} (a) \cdot (b, \dots, b) \quad (21)$$

or equivalently for $b \le a$

$$f(a) = \sum_n \frac{1}{n!} \frac{d^n f(x)}{dx^n} (b) \cdot (a \ominus b, \dots, a \ominus b) \quad (22)$$

Assume that the fixpoint combinator $\mathcal{Y}: A \Rightarrow A \to A$ in $\mathbb{C}$ is obtained by Scott iteration as the supremum $\mathcal{Y} = \bigvee_n \mathcal{Y}_n$ with

$$\mathcal{Y}_0 = 0 \quad \text{and} \quad \mathcal{Y}_{n+1} = \text{eval}_{A,A} \circ \langle 1_{A \Rightarrow A}, \mathcal{Y}_n \rangle$$

where $\mathbb{C}$ is assumed to be $\omega$-cpo enriched. We assume here that the $\omega$-cpo enrichment is compatible with the additive structure: 0 is the bottom element and addition commutes with suprema of $\omega$-chains.

Since the fixpoint operator we consider is the least fixpoint operator, it implies that the induced linear repetition operator (Corollary 5.7) satisfies the following induction axiom [24] for all $h, j, k \in \text{LIN}(\mathbb{C})(A, A)$:

$$h + j \circ k \le k \Rightarrow j^* \circ h \le k. \quad (23)$$

We can deduce it from the explicit computation of $j^* = \text{fix}_A^A(\pi_1 + j \circ \pi_2)$ (Corollary 5.7) which is equal to $\bigvee_n j^*k$ with

$$j^{*0} := 0 \quad \text{and} \quad j^{*k+1} := 1_X + j \circ j^{*k}.$$

We define a family of morphism $\mathcal{Z}_n : A \Rightarrow A \to A$ corresponding to the Newton approximants:

$$\mathcal{Z}_0 = 0 \quad \text{and} \quad \mathcal{Z}_{n+1} = \text{eval} \circ \langle \mathcal{N}, \mathcal{Z}_n \rangle.$$

**LEMMA 8.1.** For all $n$, the following inequalities hold:

$$\mathcal{Y}_n \le \mathcal{Z}_n \le \mathcal{Y} \quad \text{and} \quad \mathcal{Z}_n \le \text{eval} \circ \langle 1, \mathcal{Z}_n \rangle \le \mathcal{Z}_{n+1}$$

**PROOF.** For a fixed $f: A \to A$, to simplify the notation, we write $z_n := \mathcal{Z}_n(f)$, $y_n := \mathcal{Y}_n(f)$, and $y := \mathcal{Y}(f)$,

* We have $z_0 = 0 \le f(0)$ and we assume that for some $n$, $z_n \le f(z_n)$. Since $z_{n+1}$ is equal to

$$\mathcal{N}(f)(z_n) = z_n + (\mathbf{D}_{z_n}[f])^* \cdot (f(z_n) \ominus z_n)$$

we apply the Taylor formula (21) by setting $a := z_n$ and $b := (\mathbf{D}_{z_n}[f])^* \cdot (f(z_n) \ominus z_n)$, and obtain

$$f(z_{n+1}) = f(a+b) \ge f(a) + \mathbf{D}_a[f] \cdot b = z_{n+1}$$

where the last inequality is obtained from unfolding the repetition operator in the expression of $b$ and using the induction hypothesis to obtain that $f(z_n) = (f(z_n) \ominus z_n)+z_n$ by (18).

* Using again the fixpoint axiom for the repetition operator and the fact that $z_n \le f(z_n)$, we obtain that $z_{n+1}$ is equal to

$$f(z_n) + (\mathbf{D}_{z_n}[f]) \cdot (\mathbf{D}_{z_n}[f])^* \cdot (f(z_n) \ominus x_n) \ge f(z_n).$$

* We show that for all $n, y_n \le z_n$. The base case is trivial, and if we assume that $y_n \le z_n$ for some $n$, then we have:

$$y_{n+1} = f(y_n) \le f(z_n) \le z_{n+1}$$

where the last two inequalities were proved above.

* The base case $z_0 = 0 \le y$ is trivial, we want to show that if for some $n, z_n \le y$, then $z_{n+1} \le y$. We show that for all $k \in \mathcal{N}$,

$$z_n + (\mathbf{D}_{z_n}[f])^{*k} \cdot (f(z_n) \ominus z_n) \le f^{k+1}(z_n) \le y$$

which will imply the desired result by taking the supremum over $k$. For $k = 0$, the inequality follows from $f(z_n) \ge z_n$. For the inductive step, we use the Taylor formula to obtain

$$\begin{aligned} f^{k+2}(z_n) &\ge f(z_n + (\mathbf{D}_{z_n}[f])^{*k} \cdot (f(z_n) \ominus z_n)) \\ &\ge f(z_n) + (\mathbf{D}_{z_n}[f]) \cdot (\mathbf{D}_{z_n}[f])^{*k} \cdot (f(z_n) \ominus z_n)) \\ &= z_n + (\mathbf{D}_{z_n}[f])^{*k+1} \cdot (f(z_n) \ominus z_n) \quad \square \end{aligned}$$

As a corollary of Lemma 8.1, we obtain that the Newton chain converges and approximates the least fixpoint from below as desired.

## 8.2 Taylor metric and convergence rate

To measure the convergence rate of Newton iteration, we use a metric induced by the Taylor expansion which can be defined in any Taylor category [47, 49]. We define a family of operators on homsets $\mathcal{M}_n : \mathbb{C}(A, B) \to \mathbb{C}(A, B)$ mapping a morphism $f: A \to B$ to its $n$-th Taylor monomial by evaluating the $n$-th derivative at 0:

$$\mathcal{M}_n(f)(a) := \frac{d^n f(x)}{d^n x}(0) \cdot (a, \dots, a)$$

This family of operators induces a pseudo-metric (the separation axiom does not necessarily hold) on each homset $d: \mathbb{C}(A, B) \times \mathbb{C}(A, B) \to \mathbb{C}(A, B)$ given by

$$(f, g) \mapsto \begin{cases} 2^{-k} & \text{where } k = \inf\{n \in \mathbb{N} \mid \mathcal{M}_n(f) \ne \mathcal{M}_n(g)\} \\ 0 & \text{if for all } k \in \mathbb{N}, \mathcal{M}_k(f) = \mathcal{M}_k(g) \end{cases}$$

similar to the Arnold-Nivat metric for $\lambda$-terms with truncations [2]. In a Cartesian differential category, $d(f, g) = 2^{-k}$ also corresponds to the intuition $f(x) - g(x) = o(x^k)$ in analysis and we use this canonical distance for convergence analysis of optimization in our setting. The stronger triangle inequality holds for the Taylor pseudo-metric:

$$d(f, h) \le \max\{d(f, g), d(g, h)\}.$$

If $\mathbb{C}$ is a Taylor category [18, 19, 22, 40], then the separation axiom holds and we obtain an ultra-metric [47, 49].

For the convergence rate of Newton's method, we assume further that for $f: A \times X \to X$, $f(0, 0) = 0$ and that the second partial derivative of $f$ is nilpotent in its linear argument, meaning that there exists $p \ge 1$ such that for all $a, z, b$:

$$\left( \frac{df(a, v)}{dv}(z) \right)^p \cdot b = 0.$$

similarly to [52, 53] where they require the Jacobian matrix to be nilpotent. For an additive map $h: X \to X$, if $h$ is nilpotent, then for all $k: Y \to X$, we have

$$k \le h^* \circ (k \ominus (h \circ k)). \quad (24)$$

To simplify the notation, we write again $y := \text{fix}(f) : A \to X$, $z_n := \mathcal{Z}_n(f) : A \to X$, $z_{n+1} := \mathcal{Z}_{n+1}(f) : A \to X$ and

$$(\mathbf{D}_{z_n}[f](a)) \cdot b := \frac{df(a, v)}{dv}(z_n(a)) \cdot b.$$
Using (16), we obtain that $y(a) \ominus z_{n+1}(a)$ is equal to

$$(y(a) \ominus z_n(a)) \ominus ((D_{z_n}[f](a))^* \cdot (f(a, z_n(a)) \ominus z_n(a))$$

and by (24), it is less than or equal to

$$(D_{z_n}[f](a))^* \cdot ((y(a) \ominus z_n(a)) \ominus (D_{z_n}[f](a)) \cdot (y(a) \ominus z_n(a)) \ominus ((D_{z_n}[f](a))^* \cdot (f(a, z_n(a)) \ominus z_n(a))$$

which, by (20) and (16), is in turn is less than or equal to

$$(D_{z_n}[f](a))^* \cdot (((y(a) \ominus z_n(a)) \ominus (f(a, z_n(a)) \ominus z_n(a)) \ominus (D_{z_n}[f](a)) \cdot (y(a) \ominus z_n(a))$$

using (16) and (19), it is less than or equal to

$$(D_{z_n}[f](a))^* \cdot (y(a) \ominus (f(a, z_n(a)) + (D_{z_n}[f](a)) \cdot (y(a) \ominus z_n(a))$$

Lastly, since $y(a) = f(a, y(a))$ and $z_n \le y$, we can apply the Taylor formula (22) and obtain that:

$$y(a) = f(a, z_n(a)) + (D_{z_n}[f](a)) \cdot (y(a) \ominus z_n(a)) + \sum_{k \ge 2} \frac{1}{k!} \frac{d^k f(a, v)}{dv^k} (z_n(a)) \cdot (y(a) \ominus z_n(a))^k$$

Using (17), we conclude that $y(a) \ominus z_{n+1}(a)$ is less than or equal to

$$(D_{z_n}[f](a))^* \cdot \left( \sum_{k \ge 2} \frac{1}{k!} \frac{d^k f(a, v)}{dv^k} (z_n(a)) \cdot (y(a) \ominus z_n(a))^k \right)$$

We now state the main theorem of this section:

### THEOREM 8.2.

(1) The family of Newton approximants {$\mathbb{Z}_n$}$_{n \in \omega}$ is an $\omega$-chain and its supremum $\mathcal{Z} := \bigvee_n \mathbb{Z}_n$ verifies $\mathcal{Z} = \mathcal{Y}$ and for all $n$, $\mathbb{Z}_n \le \mathcal{Y}$, which means that the Newton approximants converge to the least fixpoint from below.

(2) If we consider the canonical distance induced by the Taylor monomials, for $f: A \times X \to X$, assuming that $f(0, 0) = 0$ and that the second partial derivative of $f$ is nilpotent in its linear argument, then the convergence rate is quadratic<fnref n="1" />, for all $n$:

$$d(\mathbb{Z}_{n+1}(f), \mathcal{Y}(f)) \le (d(\mathbb{Z}_n(f), \mathcal{Y}(f)))^2.$$

## 9 CONCLUSION AND FUTURE WORK

In this paper, we provided a categorical framework for combining the theory of differentiation and the theory of fixpoints. We introduced the notion of Cartesian differential fixpoint categories (Section 3), and studied the case of Conway operators (Section 4), the relation between linearity and fixpoints (Section 5), and the closed setting (Section 6). We showed how many well-known examples are Cartesian differential fixpoint categories, such as weighted relations (Section 7.2), quantales profunctors (Section 7.4), models induced by bifree algebras (Section 7.5), and those induced by fixpoint objects (Section 7.6). We also showed how the Newton-Raphson scheme can be applied in our framework (Section 8). We conclude with a brief discussion on potential future work and directions that build on the story of this paper.

Since the tangent bundle functor played such a crucial role, the first natural direction to take is to study tangent categories [11] with fixpoint operators, where the defining axiom will be the tangent-fixpoint rule (10). Moreover, (10) should also be considered as an axiom for tangent categories with trace operators in the general monoidal setting.

There are also cofree Cartesian differential categories which are built via the Faà di Bruno construction [15, 32]. We aim to study parametrized fixpoint operators in these cofree models or understand how the Faà di Bruno construction can be used to build new examples of Cartesian differential fixpoint categories.

Cartesian reverse differential categories [13] provide the categorical foundations of reverse differentiation, an important tool for automatic differentiation. Since fixpoints are also an important tool for automatic differentiation [51], it would be worthwhile to understand the compatibility relation between parametrized fixpoint operators and reverse differential combinators.

Many optimization schemes are based on refinements of the Newton-Raphson method. We would like to extend our construction to other iterative methods and study their application to approximate solutions of differential equations in our setting.

There are also many cases where we can only obtain fixpoints defined on a restricted domain which are used when we are interested in local minima or maxima and not global solutions. We therefore aim to develop a theory of fixpoints for differential restriction category [12] which would allow us to capture local implicit function theorems that are more used in practice.

## ACKNOWLEDGMENTS

We thank the anonymous reviewers for their detailed feedback which helped improve the paper. We are also grateful to Masahito Hasegawa for discussions on Conway fixpoint operators. The first author is partially supported by the MUR FARE project "CAFFEINE" (Compositional and Effectful Program Distances). The second author is funded by an ARC DECRA (DE230100303) and an AFOSR Research Grant (FA9550-24-1-0008).

<footnote n="1">¹In the works on Newton's method for power series over $\omega$-continuous semi-rings (e.g. [41]), the terminology of exponential convergence is sometimes used as the number of accurately computed monomials of the power series doubles at each iteration. This is equivalent to quadratic convergence for the Taylor metric.</footnote>
## REFERENCES

[1] Martín Abadi and Gordon D Plotkin. 2019. A simple differentiable programming language. *Proceedings of the ACM on Programming Languages* 4, POPL (2019), 1–28.

[2] André Arnold and Maurice Nivat. 1980. The metric space of infinite trees. *Algebraic and topological properties*. *Fundamenta Informaticae* 3, 4 (1980), 445–475.

[3] B. M. Bell and James V Burke. 2008. Algorithmic differentiation of implicit functions and optimal values. In *Advances in Automatic Differentiation*. Springer, Springer Berlin, Heidelberg, 67–77.

[4] G. Berry. 1979. *Modeles completement adéquats et stables des lambda-calculs typés*. Ph. D. Dissertation. Éditeur inconnu.

[5] M. Blondel, Q. Berthet, M. Cuturi, R. Frostig, S. Hoyer, F. Llinares-López, F. Pedregosa, and J.-P. Vert. 2022. Efficient and modular implicit differentiation. *Advances in neural information processing systems* 35 (2022), 5230–5242.

[6] S. L. Bloom and Z. Ésik. 1993. *Iteration theories*. Springer Berlin, Heidelberg.

[7] R.F. Blute, J.R.B. Cockett, and R.A.G. Seely. 2006. Differential Categories. *Mathematical Structures in Computer Science* 16, 06 (2006), 1049–1083.

[8] R. F. Blute, J. R. B. Cockett, and R. A. G. Seely. 2009. Cartesian Differential Categories. *Theory and Applications of Categories* 22, 23 (2009), 622–672.

[9] A. Bucciarelli, T. Ehrhard, and G. Manzonetto. 2010. Categorical models for simply typed resource calculi. *Electronic Notes in Theoretical Computer Science* 265 (2010), 213–230.

[10] J.R.B. Cockett and J. Gallagher. 2019. Categorical models of the differential λ-calculus. *Mathematical Structures in Computer Science* 29, 10 (2019), 1513–1555.

[11] J. R. B. Cockett and G. S. H. Cruttwell. 2014. Differential structure, tangent structure, and SDG. *Applied Categorical Structures* 22 (2014), 331–417.

[12] J. R. B. Cockett, G. S. H. Cruttwell, and J. D. Gallagher. 2011. Differential restriction categories. *Theory and Applications of Categories* 25, 21 (2011), 537–613.

[13] J. R. B. Cockett, G. S. H. Cruttwell, J. D. Gallagher, J.-S. P. Lemay, B. Mac Adam, G. Plotkin, and D. Pronk. 2020. Reverse Derivative Categories. *LIPIcs* 152, CSL 2020 (2020), 18:1–18:16.

[14] J. R. B. Cockett and J.-S. P. Lemay. 2022. Linearizing Combinators. *Theory and Applications of Categories* 38, 13 (2022), 374–431.

[15] J. R. B. Cockett and R. A. G. Seely. 2011. The Faa di Bruno construction. *Theory and Applications of Categories* 25, 15 (2011), 394–425.

[16] H Décoste, G Labelle, and P Leroux. 1982. Une approche combinatoriale pour l'itération de Newton-Raphson. *Advances in Applied Mathematics* 3, 4 (1982), 407–416.

[17] Pietro Di Gianantonio, Abbas Edalat, and Ran Gutin. 2023. A language for evaluating derivatives of functionals using automatic differentiation. In *Proceedings of the 39th Conference on the Mathematical Foundations of Programming Semantics*, MFPS XXXIX. *Electronic Notes in Theoretical Informatics and Computer Science* 3, 1–19.

[18] Thomas Ehrhard. 2018. An introduction to differential linear logic: proof-nets, models and antiderivatives. *Mathematical Structures in Computer Science* 28, 7 (2018), 995–1060.

[19] T. Ehrhard. 2023. A coherent differential PCF. *Logical Methods in Computer Science* Volume 19, Issue 4 (2023), 7:1–7:88. https://doi.org/10.46298/lmcs-19(4:7)2023

[20] T. Ehrhard and L. Regnier. 2003. The differential lambda-calculus. *Theoretical Computer Science* 309, 1 (2003), 1–41.

[21] T. Ehrhard and A. Walch. 2023. Cartesian coherent differential categories. In *2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)*. IEEE, 1–13.

[22] T. Ehrhard and A. Walch. 2023. Coherent Taylor expansion as a bimonad. (2023).

[23] Zoltán Ésik. 1988. Independence of the equational axioms for iteration theories. *J. Comput. System Sci.* 36, 1 (1988), 66–76.

[24] Z. Ésik and W. Kuich. 2004. Inductive *-semirings. *Theoretical Computer Science* 324, 1 (2004), 3–33.

[25] J. Esparza, S. Kiefer, and M. Luttenberger. 2010. Newtonian program analysis. *Journal of the ACM (JACM)* 57, 6 (2010), 1–47.

[26] Javier Esparza, Michael Luttenberger, and Maximilian Schlund. 2015. Fp solve: A generic solver for fixpoint equations over semirings. *International Journal of Foundations of Computer Science* 26, 07 (2015), 805–825.

[27] Marcelo Fiore, Nicola Gambino, Martin Hyland, and Glynn Winskel. 2008. The cartesian closed bicategory of generalised species of structures. *Journal of the London Mathematical Society* 77, 1 (2008), 203–220.

[28] M. P. Fiore. 2004. *Axiomatic domain theory in categories of partial maps*. Vol. 14. Cambridge University Press, Cambridge, UK.

[29] P. J. Freyd. 1992. Remarks on algebraically compact categories. In *Applications of Categories in Computer Science: Proceedings of the London Mathematical Society Symposium, Durham 1991*, Vol. 177. Cambridge University Press, Cambridge, UK, 95.

[30] P. J. Freyd. 2006. Algebraically complete categories. In *Category Theory: Proceedings of the International Conference held in Como, Italy, July 22–28, 1990*. Springer, Springer Berlin, Heidelberg, 95–104.

[31] J. Gallagher. 2018. *The differential λ-calculus: syntax and semantics for differential geometry*. Ph. D. Dissertation. Phd thesis, University of Calgary.

[32] R. Garner and J.-S. P. Lemay. 2021. Cartesian differential categories as skew enriched categories. *Applied Categorical Structures* 29, 6 (2021), 1099–1150.

[33] J. C. Gilbert. 1992. Automatic differentiation and iterative processes. *Optimization methods and software* 1, 1 (1992), 13–21.

[34] C. Grellois and P.-A. Melliès. 2015. An infinitary model of linear logic. In *Foundations of Software Science and Computation Structures: 18th International Conference, FOSSACS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015, Proceedings 18*. Springer, Springer Berlin, Heidelberg, 41–55.

[35] M. Hasegawa. 1997. Recursion from cyclic sharing: traced monoidal categories and models of cyclic lambda calculi. In *Typed Lambda Calculi and Applications*. Springer, Berlin, Heidelberg, 196–213. https://doi.org/10.1007/3-540-62688-3_37

[36] M. Hasegawa. 2004. The uniformity principle on traced monoidal categories. *Publications of the Research Institute for Mathematical Sciences* 40, 3 (2004), 991–1014. https://doi.org/10.1016/S1571-0661(04)80563-2

[37] M. W. Hopkins and Dexter C. Kozen. 1999. Parikh's theorem in commutative Kleene algebra. In *Proceedings, 14th Symposium on Logic in Computer Science (Cat. No. PR00158)*. IEEE, IEEE Computer Society, Massachusetts Ave., NW Washington, DC United State, 394–401.

[38] A. Joyal, R. Street, and D. Verity. 1996. Traced monoidal categories. *Mathematical proceedings of the cambridge philosophical society* 119, 3 (1996), 447–468.

[39] G. M. Kelly. 1982. *Basic concepts of enriched category theory*. Vol. 64. CUP Archive, Cambridge, UK.

[40] M. Kerjean and J.-S. P. Lemay. 2023. Taylor Expansion as a Monad in Models of DiLL. In *2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)*. IEEE, Boston, MA, USA, 1–13. https://doi.org/10.1109/LICS56636.2023.10175753

[41] S. Kiefer, M. Luttenberger, and J. Esparza. 2007. On the convergence of Newton's method for monotone systems of polynomial equations. In *Proceedings of the thirty-ninth annual ACM symposium on Theory of computing*. Association for Computing Machinery, New York, NY, United States, 217–226.

[42] J. Laird. 2016. Fixed points in quantitative semantics. In *Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science*. IEEE, Boston, MA, USA, 347–356.

[43] J. Laird, G. Manzonetto, G. McCusker, and M. Pagani. 2013. Weighted relational models of typed lambda-calculi. In *2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science*. IEEE, Boston, MA, USA, 301–310.

[44] F. W. Lawvere. 1973. Metric spaces, generalized logic, and closed categories. *Rendiconti del seminario matematico e fisico di Milano* 43 (1973), 135–166.

[45] W. Lawvere. 1969. Diagonal arguments and cartesian closed categories. In *Category Theory, Homology Theory and their Applications II: Proceedings of the Conference held at the Seattle Research Center of the Battelle Memorial Institute, June 24–July 19, 1968 Volume Two*. Springer, Springer Berlin, Heidelberg, 134–145.

[46] J.-S. P. Lemay. 2021. Exponential functions in cartesian differential categories. *Applied Categorical Structures* 29 (2021), 95–140.

[47] J.-S. P. Lemay. 2023. A Taylor Series Metric for Cartesian Differential Categories. (2023). International Workshop on Quantitative Logical methods.

[48] J.-S. P. Lemay. 2023. Cartesian Differential Kleisli Categories. *Electronic Notes in Theoretical Informatics and Computer Science* Volume 3 - Proceedings of MFPS XXXIX (2023), 1–19. https://doi.org/10.46298/entics.12278

[49] J.-S. P. Lemay. 2024. An Ultrametric for Cartesian Differential Categories for Taylor Series Convergence. (2024). To appear in the proceedings of the 40th Conference on Mathematical Foundations of Programming Semantics, MFPS XL.

[50] G. Manzonetto. 2012. What is a Categorical Model of the Differential and the Resource λ-Calculi? *Mathematical Structures in Computer Science* 22, 3 (2012), 451–520.

[51] D. Mazza and M. Pagani. 2021. Automatic differentiation in PCF. *Proceedings of the ACM on Programming Languages* 5, POPL (2021), 1–27.

[52] C. Pivoteau. 2008. *Génération aléatoire de structures combinatoires: méthode de Boltzmann effective*. Ph. D. Dissertation. Université Paris.

[53] C. Pivoteau, B. Salvy, and M. Soria. 2012. Algorithms for combinatorial structures: Well-founded systems and Newton iterations. *Journal of Combinatorial Theory, Series A* 119, 8 (2012), 1711–1773.

[54] G. D. Plotkin. 1977. LCF considered as a programming language. *Theoretical computer science* 5, 3 (1977), 223–255.

[55] G. Rozenberg and A. Salomaa. 2012. *Handbook of Formal Languages: Volume 3 Beyond Words*. Springer Berlin, Heidelberg.

[56] P. Selinger. 2010. A survey of graphical languages for monoidal categories. In *New Structures for Physics*. Springer Berlin, Heidelberg, 289–355. https://doi.org/10.1007/978-3-642-12821-9_4

[57] A. Simpson and G. Plotkin. 2000. Complete axioms for categorical fixed-point operators. In *Proceedings Fifteenth Annual IEEE Symposium on Logic in Computer Science (Cat. No. 99CB36332)*. IEEE, Boston, MA, USA, 30–41.

[58] Michael B Smyth and Gordon D Plotkin. 1982. The category-theoretic solution of recursive domain equations. *SIAM J. Comput.* 11, 4 (1982), 761–783.

[59] D. Sprunger and S. Katsumata. 2019. Differentiable causal computations via delayed trace. In *2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)*. IEEE, Boston, MA, USA, 1–12. https://doi.org/10.1109/LICS.2019.
8785670

[60] R. Statman. 2002. On the lambda Y calculus. In *Proceedings 17th Annual IEEE Symposium on Logic in Computer Science*. IEEE, Boston, MA, USA, 159–166.

[61] Isar Stubbe. 2004. Categorical structures enriched in a quantaloid: Categories, distributors and functors. *Theory and Applications of Categories* 14 (10 2004).