key: cord-0054950-nbuahini
authors: Alvarez-Picallo, Mario; Lemay, Jean-Simon Pacaud
title: Cartesian Difference Categories
date: 2020-04-17
journal: Foundations of Software Science and Computation Structures
DOI: 10.1007/978-3-030-45231-5_4
sha: dbdd840a970c56eded35954ecd541ed20a982285
doc_id: 54950
cord_uid: nbuahini

Cartesian differential categories are categories equipped with a differential combinator which axiomatizes the directional derivative. Important models of Cartesian differential categories include classical differential calculus of smooth functions and categorical models of the differential [Formula: see text] -calculus. However, Cartesian differential categories cannot account for other interesting notions of differentiation such as the calculus of finite differences or the Boolean differential calculus. On the other hand, change action models have been shown to capture these examples as well as more “exotic” examples of differentiation. However, change action models are very general and do not share the nice properties of a Cartesian differential category. In this paper, we introduce Cartesian difference categories as a bridge between Cartesian differential categories and change action models. We show that every Cartesian differential category is a Cartesian difference category, and how certain well-behaved change action models are Cartesian difference categories. In particular, Cartesian difference categories model both the differential calculus of smooth functions and the calculus of finite differences. Furthermore, every Cartesian difference category comes equipped with a tangent bundle monad whose Kleisli category is again a Cartesian difference category.

In the early 2000s, Ehrhard and Regnier introduced the differential λ-calculus [10] , an extension of the λ-calculus equipped with a differential combinator capable of taking the derivative of arbitrary higher-order functions. This development, based on models of linear logic equipped with a natural notion of "derivative" [11] , sparked a wave of research into categorical models of differentiation.

One of the most notable developments in the area is the introduction of Cartesian differential categories [4] by Blute, Cockett and Seely, which provide an abstract categorical axiomatization of the directional derivative from differential calculus. The relevance of Cartesian differential categories lies in their ability to model both "classical" differential calculus (with the canonical example being the category of Euclidean spaces and smooth functions between) and the differential λ-calculus (as every categorical model for it gives rise to a Cartesian differential category [14] ). However, while Cartesian differential categories have proven to be an immensely successful formalism, they have, by design, some limitations. Firstly, they cannot account for certain "exotic" notions of derivative, such as the difference operator from the calculus of finite differences [16] or the Boolean differential calculus [19] . This is because the axioms of a Cartesian differential category stipulate that derivatives should be linear in their second argument (in the same way that the directional derivative is), whereas these aforementioned discrete sorts of derivative need not be. Additionally, every Cartesian differential category is equipped with a tangent bundle monad [7, 15] whose Kleisli category can be intuitively understood as a category of generalized vector fields. This Kleisli category has an obvious differentiation operator which comes close to making it a Cartesian differential category, but again fails the requirement of being linear in its second argument.

More recently, discrete derivatives have been suggested as a semantic framework for understanding incremental computation. This led to the development of change structures [6] and change actions [2] . Change action models have been successfully used to provide a model for incrementalizing Datalog programs [1] , but have also been shown to model the calculus of finite differences as well as the Kleisli category of the tangent bundle monad of a Cartesian differential category. Change action models, however, are very general, lacking many of the nice properties of Cartesian differential categories (for example, addition in a change action model is not required to be commutative), even though they are verified in most change action models. As a consequence of this generality, the tangent bundle endofunctor in a change action model can fail to be a monad.

In this work, we introduce Cartesian difference categories (Section 4.2), whose key ingredients are an infinitesimal extension operator and a difference combinator, whose axioms are a generalization of the differential combinator axioms of a Cartesian differential category. In Section 4.3, we show that every Cartesian differential category is, in fact, a Cartesian difference category whose infinitesimal extension operator is zero, and conversely how every Cartesian difference category admits a full subcategory which is a Cartesian differential category. In Section 4.4, we show that every Cartesian difference category is a change action model, and conversely how a full subcategory of suitably well-behaved objects of a change action model is a Cartesian difference category. In Section 6, we show that every Cartesian difference category comes equipped with a monad whose Kleisli category again a Cartesian difference category. Finally, in Section 5 we provide some examples of Cartesian difference categories; notably, the calculus of finite differences and the stream calculus.

In this section, we briefly review Cartesian differential categories, so that the reader may compare Cartesian differential categories with the new notion of Cartesian difference categories which we introduce in the next section. For a full detailed introduction on Cartesian differential categories, we refer the reader to the original paper [4] .

Here we recall the definition of Cartesian left additive categories [4] -where "additive" is meant being skew enriched over commutative monoids, which in particular means that we do not assume the existence of additive inverses, i.e., "negative elements". By a Cartesian category we mean a category X with chosen finite products where we denote the binary product of objects A and B by A × B with projection maps π 0 : A × B → A and π 1 : A × B → B and pairing operation −, − , and the chosen terminal object as with unique terminal maps ! A : A → . [4] is a category X such that each hom-set X(A, B) is a commutative monoid with addition operation + : X(A, B)× X(A, B) → X(A, B) and zero element (called the zero map) 0 ∈ X(A, B), such that pre-composition preserves the additive structure:

and 0•f = 0. A map k in a left additive category is additive if post-composition by k preserves the additive structure: k • (f + g) = k • f + k • g and k • 0 = 0. A Cartesian left additive category [4] is a Cartesian category X which is also a left additive category such all projection maps π 0 : A × B → A and

We note that the definition given here of a Cartesian left additive category is slightly different from the one found in [4] , but it is indeed equivalent. By [4, Proposition 1.2.2] , an equivalent axiomatization is of a Cartesian left additive category is that of a Cartesian category where every object comes equipped with a commutative monoid structure such that the projection maps are monoid morphisms. This will be important later in Section 4.2.

Definition 2. A Cartesian differential category [4] is a Cartesian left additive category equipped with a differential combinator D of the form

verifying the following coherence conditions:

Note that here, following the more recent work on Cartesian differential categories, we've flipped the convention found in [4] , so that the linear argument is in the second argument rather than in the first argument.

We highlight that by [ 

As a Cartesian difference category is a generalization of a Cartesian differential category, we leave the discussion of the intuition of these axioms for later in Section 4.2 below. We also refer to [4, Section 4] for a term calculus which may help better understand the axioms of a Cartesian differential category. The canonical example of a Cartesian differential category is the category of real smooth functions, which we will discuss in Section 5.1. Other interesting examples of can be found throughout the literature such as categorical models of the differential λ-calculus [10, 14] , the subcategory of differential objects of a tangent category [7] , and the coKleisli category of a differential category [3, 4] .

Change actions [1, 2] have recently been proposed as a setting for reasoning about higher-order incremental computation, based on a discrete notion of differentiation. Together with Cartesian differential categories, they provide the core ideas behind Cartesian difference categories. In this section, we quickly review change actions and change action models, in particular, to highlight where some of the axioms of a Cartesian difference category come from. For more details on change actions, we invite readers to see the original paper [2] .

A ≡ (A, ΔA, ⊕ A , + A , 0 A ) consisting of two objects A and ΔA, and three maps:

such that (ΔA, + A , 0 A ) is a monoid and ⊕ A : A × ΔA → A is an action of ΔA on A, that is, the following equalities hold:

For a change action A and given a pair of maps f : C → A and g : C → ΔA,

Similarly, for maps h : C → ΔA and k : C → ΔA, define h + A k = + A • h, k . Therefore, that ⊕ A is an action of ΔA on A can be rewritten as:

The intuition behind the above definition is that the monoid ΔA is a type of possible "changes" or "updates" that might be applied to A, with the monoid structure on ΔA representing the capability to compose updates.

Change actions give rise to a notion of derivative, with a distinctly "discrete" flavour. Given change actions on objects A and B, a map f : A → B can be said to be differentiable when changes to the input (in the sense of elements of ΔA) are mapped to changes to the output (that is, elements of ΔB). In the setting of incremental computation, this is precisely what it means for f to be incrementalizable, with the derivative of f corresponding to an incremental version of f .

is a derivative of f whenever the following equalities hold:

The intuition for these axioms will be explained in more detail in Section 4.2 when we explain the axioms of a Cartesian difference category. Note that although there is nothing in the above definition guaranteeing that any given map has at most a single derivative, the chain rule does hold. As a corollary, differentiation is compositional and therefore the change actions in X form a category.

are derivatives for composable maps f and g respectively, then

Definition 5. Given a Cartesian category X, define its change actions category CAct(X) as the category whose objects are change actions in X and whose arrows

There is an obvious product-preserving forgetful functor E : CAct(X) → X sending every change action (A, ΔA, ⊕, +, 0) to its base object A and every map (f, ∂[f ]) to the underlying map f . As a setting for studying differentiation, the category CAct(X) is rather lacklustre, since there is no notion of higher derivatives, so we will instead work with change action models. Informally, a change action model consists of a rule which for every object A of X associates a change action over it, and for every map a choice of a derivative.

Cartesian category X is a productpreserving functor α : X → CAct(X) that is a section of the forgetful functor E.

For brevity, when A is an object of a change action model, we will write ΔA, ⊕ A , + A , and 0 A to refer to the components of the corresponding change action α(A). Examples of change action models can be found in [2] . In particular, we highlight that a Cartesian differential category always provides a change model action. We will generalize this result, and show in Section 4.4 that a Cartesian difference category also always provides a change action model.

In this section, we introduce Cartesian difference categories, which are generalizations of Cartesian differential categories. Examples of Cartesian difference categories can be found in Section 5.

We first introduce infinitesimal extensions, which is an operator that turns a map into an "infinitesimal" version of itself -in the sense that every map coincides with its Taylor approximation on infinitesimal elements.

is an additive map (Definition 1). In light of this, it turns out that infinitesimal extensions can equivalently be described as a class of additive maps

. Furthermore, infinitesimal extensions equipped each object with a canonical change action structure:

Proof. As mentioned earlier, that (A, + A , 0 A ) is a commutative monoid was shown in [4] . On the other hand, that ⊕ A is a change action follows from the fact that ε preserves the addition.

we note that f ⊕ A g = f + ε(g) and f + A g = f + g, and so in particular + A = +. Therefore, from now on we will omit the subscripts and simply write ⊕ and +.

For every Cartesian left additive category, there are always at least two possible infinitesimal extensions: Lemma 4. For any Cartesian left additive category X,

Setting ε(f ) = 0 defines an infinitesimal extension on X and therefore in this case,

Setting ε(f ) = f defines an infinitesimal extension on X and therefore in this case,

We note that while these examples of infinitesimal extensions may seem trivial, they are both very important as they will give rise to key examples of Cartesian difference categories.

verifying the following coherence conditions:

Before giving some intuition on the axioms [C∂.0] to [C∂.7], we first observe that one could have used change action notation to express [C∂.0], [C∂.2], and [C∂.6] which would then be written as: 

Proof. The proof is essentially the same as [7, Proposition 4.2] .

The keen eyed reader will notice that the axioms of a Cartesian difference category are very similar to the axioms of a Cartesian differential category. it may be useful to write them out using element-like notation. In element-like notation, [C∂.0] is written as:

This condition can be read as a generalization of the Kock-Lawvere axiom that characterizes the derivative in from synthetic differential geometry [13] . Broadly speaking, the Kock-Lawvere axiom states that, for any map f : R → R and any

where D is the subset of R consisting of infinitesimal elements. It is by analogy with the Kock-Lawvere axiom that we refer to ε as an "infinitesimal extension" as it can be thought of as embedding the space A into a subspace ε(A) of infinitesimal elements.

[C∂.1] states that the differential of a sum of maps is the sum of differentials, and similarly for zero maps and the infinitesimal extension of a map. [C∂.2] is the first crucial difference between a Cartesian difference category and a Cartesian differential category. In a Cartesian differential category, the differential of a map is assumed to be additive in its second argument. In a Cartesian difference category, just as derivatives for change actions, while the differential is still required to preserve zeros in its second argument, it is only additive "up to a small perturbation", that is:

tells us what the differential of the identity and projection maps are, while [C∂.4] says that the differential of a pairing of maps is the pairing of their differentials. [C∂.5] is the chain rule which expresses what the differential of a composition of maps is: 

and finally [C∂.7] is expressed as:

It is interesting to note that while [C∂.6] is different from [CD.6], its alternative version [C∂.6.a] is the same as [CD.6.a].

Here we explain how a Cartesian differential category is a Cartesian difference category where the infinitesimal extension is given by zero. Proposition 1. Every Cartesian differential category X with differential combinator D is a Cartesian difference category where the infinitesimal extension is defined as ε(f ) = 0 and the difference combinator is defined to be the differential combinator, ∂ = D. . Therefore, the differential combinator satisfies the Cartesian difference axioms and we conclude that a Cartesian differential category is a Cartesian difference category.

Conversely, one can always build a Cartesian differential category from a Cartesian difference category by considering the objects for which the infinitesimal extension is the zero map.

Proposition 2. For a Cartesian difference category X with infinitesimal extension ε and difference combinator ∂, then X 0 , the full subcategory of objects A such that ε(1 A ) = 0, is a Cartesian differential category where the differential combinator is defined to be the difference combinator, D = ∂.

Proof. First note that if ε(1 A ) = 0 and ε(1 B ) = 0, then by definition it also follows that ε(1 A×B ) = 0, and also that for the terminal object ε(1 ) = 0 by uniqueness of maps into the terminal object. Thus X 0 is closed under finite products and is therefore a Cartesian left additive category. Furthermore, we again note that since ε(f ) = 0, this implies that for maps between such objects the Cartesian difference axioms are precisely the Cartesian differential axioms. Therefore, the difference combinator is a differential combinator for this subcategory, and so X 0 is a Cartesian differential category.

In any Cartesian difference category X, the terminal object always satisfies that ε(1 ) = 0, and so therefore, X 0 is never empty. On the other hand, applying Proposition 2 to a Cartesian differential category results in the entire category. It is also important to note that the above two propositions do not imply that if a difference combinator is a differential combinator then the infinitesimal extension must be zero. In Section 5.3, we provide such an example of a Cartesian differential category that comes equipped with a non-zero infinitesimal extension such that the differential combinator is a difference combinator with respect to this non-zero infinitesimal extension.

In this section, we show how every Cartesian difference category is a particularly well-behaved change action model, and conversely how every change action model contains a Cartesian difference category. It is clear that not every change action model is a Cartesian difference category. For example, change action models do not require the addition to be commutative. On the other hand, it can be shown that every change action model contains a Cartesian difference category as a full subcategory.

Let (X, α : X → CAct(X)) be a change action model. An object A is flat whenever the following hold:

We would like to show that for any change action model (X, α), its full subcategory of flat objects, Flat α is a Cartesian difference category. Starting with the finite product structure, since α preserves finite products, it is straightforward to see that is Euclidean and if A and B are flat then so is A × B. The sum of maps f : A → B and g : A → B in Flat α is defined using the change action structure f + B g, while the zero map 0 : A → B is 0 = 0 B •! A . And so we obtain that:

Proof. Most of the Cartesian left additive structure is straightforward. However, since the addition is not required to be commutative for arbitrary change actions, we will show that the addition is commutative for Euclidean objects. Using that ⊕ B is an action, that by [F.2] we have that ⊕ B • π 1 is a derivative for ⊕ B , and [CAD.1], we obtain that:

, ⊕ B is right-injective and we conclude that f + g = g + f .

As an immediate consequence We note that for any change action model (X, α), since the terminal object is always flat, Flat α is never empty.

We use the action of the change action structure to define the infinitesimal extension. So for a map f : A → B in Flat α , define ε(f ) : A → B as follows:

Proof. We show that ε preserve the addition. Following the same idea as in the proof of Lemma 6, we obtain the following:

Then by [F.3] , it follows that ε(f + g) = ε(f )+ε(g). The remaining infinitesimal extension axioms are proven in a similar fashion. Lastly, the difference combinator for Flat α is defined in the obvious way, that is, ∂[f ] is defined as the second component of α(f ). 

An important subclass of maps in a Cartesian differential category is the subclass of linear maps [ 

Using element-like notation, the first point of the above lemma says that if f is linear then f (ε(x)) = ε(f (x)). And while all linear maps are additive, the converse is not necessarily true, see [4, Corollary 2.3.4] . However, an immediate consequence of the above lemma is that the subcategory of linear maps of a Cartesian difference category has finite biproducts.

Another interesting subclass of maps is the subclass of ε-linear maps, which are maps whose infinitesimal extension is linear.

Lemma 9. In a Cartesian difference category,

Using element-like notation, the first point of the above lemma says that if f is ε-linear then f (x + ε(y)) = f (x) + ε(f (y)). So ε-linear maps are additive on "infinitesimal" elements (i.e. those of the form ε(y)).

For a Cartesian differential category, linear maps in the Cartesian difference category sense are precisely the same as the Cartesian differential category sense [4, Definition 2.2.1], while every map is ε-linear since ε = 0.

Every Cartesian differential category is a Cartesian difference category where the infinitesimal extension is zero. As a particular example, we consider the category of real smooth functions, which as mentioned above, can be considered to be the canonical (and motivating) example of a Cartesian differential category.

Let R be the set of real numbers and let SMOOTH be the category whose objects are Euclidean spaces R n (including the point R 0 = { * }), and whose maps are smooth functions F : R n → R m . SMOOTH is a Cartesian left additive category where the product structure is given by the standard Cartesian product of Euclidean spaces and where the additive structure is defined by point-wise addition, (F + G)(x) = F (x) + G(x) and 0(x) = (0, . . . , 0) , where x ∈ R n . SMOOTH is a Cartesian differential category where the differential combinator is defined by the directional derivative of smooth functions. Explicitly, for a smooth function F : R n → R m , which is in fact a tuple of smooth functions

can also be defined in terms of the Jacobian matrix of F . Therefore SMOOTH is a Cartesian difference category with infinitesimal extesion ε = 0 and with difference combinator D. Since ε = 0, the induced action is simply x ⊕ R n y = x. Also a smooth function is linear in the Cartesian difference category sense precisely if it is R-linear in the classical sense, and every smooth function is ε-linear.

Here we explain how the difference operator from the calculus of finite differences gives an example of a Cartesian difference category but not a Cartesian differential category. This example was the main motivating example for developing Cartesian difference categories. The calculus of finite differences is captured by the category of abelian groups and arbitrary set functions between them. Let Ab be the category whose objects are abelian groups G (where we use additive notation for group structure) and where a map f : G → H is simply an arbitrary function between them (and therefore does not necessarily preserve the group structure). Ab is a Cartesian left additive category where the product structure is given by the standard Cartesian product of sets and where the additive structure is again given by point-wise addition, (f + g)(x) = f (x)+ g(x) and 0(x) = 0. Ab is a Cartesian difference category where the infinitesimal extension is simply given by the identity, that is, ε(f ) = f , and and where the difference combinator ∂ is defined as follows for a map f : G → H:

On the other hand, ∂ is not a differential combinator for Ab since it does not satisfy It is worth noting that in [5] , the goal was to drop the addition and develop a "non-additive" version of Cartesian differential categories.

In Ab, since the infinitesimal operator is given by the identity, the induced action is simply the addition, x⊕ G y = x+y. On the other hand, the linear maps in Ab are precisely the group homomorphisms. But by [C∂.0] and [C∂.2] , we get that:

So f is a group homomorphism. Conversely, if f is a group homomorphism:

So f is linear. Since ε(f ) = f , the ε-linear maps are precisely the linear maps.

Here we provide a simple example of a Cartesian difference category whose difference combinator is also a differential combinator, but where the infinitesimal extension is neither zero nor the identity. Let R be a commutative semiring and let MOD R be the category of Rmodules and R-linear maps between them. MOD R has finite biproducts and is therefore a Cartesian left additive category where every map is additive. Every r ∈ R induces an infinitesimal extension ε r defined by scalar multiplication, ε r (f )(m) = rf (m). Then MOD R is a Cartesian difference category with the infinitesimal extension ε r for any r ∈ R and difference combinator ∂ defined as:

R-linearity of f assures that [C∂.0] holds, while the remaining Cartesian difference axioms hold trivially. In fact, ∂ is also a differential combinator and therefore MOD R is also a Cartesian differential category. The induced action is given by m ⊕ M n = m + rn. By definition of ∂, every map in MOD R is linear, and by definition of ε r and R-linearity, every map is also ε-linear.

Here we show how one can extend the calculus of finite differences example to stream calculus. The differential calculus of causal functions and interesting applications have recently been studying in [17, 18] .

For a set A, let A ω denote the set of infinite sequences of elements of A, where we write [a i ] for the infinite sequence [a i ] = (a 1 , a 2 , a 3 , . . .) and a i:j for the (finite) subsequence (a i , a i+1 , . . . , a j ) . A function f : A ω → B ω is causal whenever the n-th element f ([a i ]) n of the output sequence only depends on the first n elements of [a i ], that is, f is causal if and only if whenever a 0:n = b 0:n then f ([a i ]) 0:n = f ([b i ]) 0:n . We now consider streams over abelian groups, so let Ab ω be the category whose objects are all the Abelian groups and whose morphisms are causal maps from G ω to H ω . Ab ω is a Cartesian left-additive category, where the product is given by the standard product of abelian groups and where the additive structure is lifted point-wise from the structure of Ab, that is,

) n and 0 ([a i ]) n = 0. In order to define the infinitesimal extension, we first need to define the truncation operator z. So let G be an abelian group and [a i ] ∈ G ω , then define the sequence z([a i ]) as:

The category Ab ω is a Cartesian difference category where the infinitesimal extension is given by the truncation operator, ε(f ) ([a i ]) = z (f ([a i ])), and where the difference combinator ∂ is defined as follows:

Note the similarities between the difference combinator on Ab and that on Ab ω .

The induced action is computed out to be: 

In this section, we show that the difference combinator of a Cartesian difference category induces a monad, called the tangent monad, whose Kleisli category is again a Cartesian difference category. This construction is a generalization of the tangent monad for Cartesian differential categories [7, 15] . However, the Kleisli category of the tangent monad of a Cartesian differential category is not a Cartesian differential category, but rather a Cartesian difference category.

Let X be a Cartesian difference category with infinitesimal extension ε and difference combinator ∂. Define the functor T : X → X as follows:

and define the natural transformations η : 1 X ⇒ T and μ : T 2 ⇒ T as follows:

Proof. Functoriality of T will follow from [C∂.3] and the chain rule [C∂.5]. Naturality of η and μ and the monad identities will follow from the remaining difference combinator axioms. The full lengthy brute force calculations will appear in an upcoming extended journal version of this paper.

When X is a Cartesian differential category with the difference structure arising from setting ε = 0, this tangent bundle monad coincides with the standard tangent monad corresponding to its tangent category structure [7, 15] .

Recall that the Kleisli category of the monad (T, μ, η) is defined as the category X T whose objects are the objects of X, and where a map

The identity map in X T is the monad unit η A : A → T(A), while composition of Kleisli maps f : A → T(B) and g : B → T(C) is defined as the composite μ C • T(g) • f . To distinguish between composition in X and X T , we denote Kleisli composition as g • T f = μ C • T(g) • f . If f = f 0 , f 1 and g = g 0 , g 1 , then their Kleisli composition can be explicitly computed out to be:

Kleisli maps can be understood as "generalized" vector fields. Indeed, T(A) should be thought of as the tangent bundle over A, and therefore a vector field would be a map 1, f : A → T(A), which is of course also a Kleisli map. For more details on the intuition behind this Kleisli category see [7] . We now wish to explain how the Kleisli category is again a Cartesian difference category.

We begin by exhibiting the Cartesian left additive structure of the Kleisli category. The product of objects in X T is defined as A × B with projections π T 0 : A × B → T(A) and π T 1 : A × B → T(B) defined respectively as π T 0 = π 0 , 0 and π T 1 = π 1 , 0 . The pairing of Kleisli maps f = f 0 , f 1 and g = , g 0 , g 1 is defined as f, g T = f 0 , g 0 , f 1 , g 1 . The terminal object is again and where the unique map to the terminal object is ! T A = 0. The sum of Kleisli maps f Kleisli maps f = f 0 , f 1 and g = , g 0 , g 1 is defined as f + T g = f +g = f 0 +g 0 , f 1 +g 1 , and the zero Kleisli maps is simply 0 T = 0 = 0, 0 . Therefore we conclude that the Kleisli category of the tangent monad is a Cartesian left additive category.

The infinitesimal extension ε T for the Kleisli category is defined as follows for a Kleisli map f = f 0 , f 1 :

It is interesting to point out that for an object A the induced action ⊕ T A can be computed out to be:

= π 0 , 0 + 0, π 1 = π 0 , π 1 = 1 T(A) and we stress that this is the identity of T(A) in the base category X (but not in the Kleisli category).

To define the difference combinator for the Kleisli category, first note that difference combinators by definition do not change the codomain. That is, if f : A → T(B) is a Kleisli arrow, then the type of its derivative qua Kleisli arrow should be A × A → T(B) × T(B), which coincides with the type of its derivative in X. Therefore, the difference combinator ∂ T for the Kleisli category can be defined to be the difference combinator of the base category, that is, for a Kleisli map f = f 0 , f 1 :

Proposition 6. For a Cartesian difference category X, the Kleisli category X T is a Cartesian difference category with infinitesimal extension ε T and difference combinator ∂ T .

Proof. The full lengthy brute force calculations will appear in an upcoming extended journal version of this paper. We do note that a crucial identity for this proof is that for any map f in X, the following equality holds:

This helps simplify many of the calculations for the difference combinator axioms since T(∂[f ]) appears everywhere due to the definition of Kleisli composition.

As a result, the Kleisli category of a Cartesian difference category is again a Cartesian difference category, whose infinitesimal extension is neither the identity or the zero map. This allows one to build numerous examples of interesting and exotic Cartesian difference categories, such as the Kleisli category of Cartesian differential categories (or iterating this process, taking the Kleisli category of the Kleisli category). We highlight the importance of this construction in the Cartesian differential case as it does not in general result in a Cartesian differential category. Indeed, even if ε = 0, it is always the case that ε T = 0. We conclude this section by taking a look at the linear maps and the ε T -linear maps in the Kleisli category.

, which amounts to requiring that:

Therefore a Kleisli map is linear in the Kleisli category if and only if it is the pairing of maps which are linear in the base category. On the other hand, f is ε T -linear if ε T (f ) = 0, f 0 + ε(f 1 ) is linear in the Kleisli category, which in this case amounts to requiring that f 0 + ε(f 1 ) is linear. Therefore, if f 0 is linear and f 1 is ε-linear, then f is ε T -linear.

We have presented Cartesian difference categories, which generalize Cartesian differential categories to account for more discrete definitions of derivatives while providing an additional structure that is absent in change action models. We have also exhibited important examples and shown that Cartesian difference categories arise quite naturally from considering tangent bundles in any Cartesian differential category. We claim that Cartesian difference categories can facilitate the exploration of differentiation in discrete spaces, by generalizing techniques and ideas from the study of their differential counterparts. For example, Cartesian differential categories can be extended to allow objects whose tangent space is not necessarily isomorphic to the object itself [9] . The same generalization could be applied to Cartesian difference categories -with some caveats: for example, the equation defining a linear map (Definition 10) becomes ill-typed, but the notion of ε-linear map remains meaningful.

Another relevant path to consider is developing the analogue of the "tensor" story for Cartesian difference categories. Indeed, an important source of examples of Cartesian differential categories are the coKleisli categories of a tensor differential category [3, 4] . A similar result likely holds for a hypothetical "tensor difference category", but it is not clear how these should be defined: [C∂.2] implies that derivatives in the difference sense are non-linear and therefore their interplay with the tensor structure will be much different.

A further generalization of Cartesian differential categories, categories with tangent structure [7] are defined directly in terms of a tangent bundle functor rather than requiring that every tangent bundle be trivial (that is, in a tangent category it may not be the case that TA = A × A). Some preliminary research on change actions has already shown that, when generalized in this way, change actions are precisely internal categories, but the consequences of this for change action models (and, a fortiori, Cartesian difference categories) are not understood. More recently, some work has emerged about differential equations using the language of tangent categories [8] . We believe similar techniques can be applied in a straightforward way to Cartesian difference categories, where they might be of use to give an abstract formalization of discrete dynamical systems and difference equations.

An important open question is whether Cartesian difference categories (or a similar notion) admit an internal language. It is well-known that the differential λ-calculus can be interpreted in Cartesian closed differential categories [14] . Given their similarities, we believe there will be a very similar "difference λcalculus" which could potentially have applications to automatic differentiation (change structures, a notion similar to change actions, have already been proposed as models of forward-mode automatic differentiation [12] , although work on the area seems to have stagnated).

Lastly, we should mention that there are adjunctions between the categories of Cartesian difference categories, change action models, and Cartesian differential categories given by Proposition 1, 2, 3, and 4. These adjunctions will be explored in detail in the upcoming journal version of this paper. which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

Fixing incremental computation

Change actions: models of generalised differentiation

Differential categories. Mathematical structures in computer science

Cartesian differential categories. Theory and Applications of Categories

Differential forms in non-linear cartesian differential categories

A theory of changes for higherorder languages: Incrementalizing λ-calculi by static differentiation

Differential structure, tangent structure, and sdg. Applied Categorical Structures

Connections in tangent categories. Theory and Applications of Categories

Cartesian differential categories revisited

The differential lambda-calculus

An introduction to differential linear logic: proof-nets, models and antiderivatives

Evolving the incremental {\lambda} calculus into a model of forward automatic differentiation (ad)

Synthetic differential geometry

What is a categorical model of the differential and the resource λ-calculi?

Tangent bundles in differential lambda-categories

An introduction to the calculus of finite differences. Van Nostrand

The differential calculus of causal functions

Differentiable causal computations via delayed trace

Boolean differential calculus

Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/),