Monoidal Differential Turing Categories

Differential $\lambda$-calculus [6] is an extension of $\lambda$-calculus which enables one to treat differentiation of analytic functions purely syntactically. Just as simply typed $\lambda$-calculus is sound and complete with respect to Cartesian closed categories by the Curry-Howard-Lambek correspondence, simply typed differential $\lambda$-calculus is sound and complete with respect to Cartesian (closed) differential categories [3]. In [4], Cockett and Gallagher refined these ideas to provide a categorical semantics of the untyped differential $\lambda$-calculus, introducing the Cartesian differential Turing category with differential canonical codes. This coherently combined a Cartesian differential category with a type of category that provides a sound and complete semantics for the ordinary untyped $\lambda$-calculus: a (total) Turing category with canonical codes.

Now, an important source of examples of Cartesian differential categories comes from the categorical semantics of differential linear logic: monoidal differential categories [2]. Briefly, a monoidal differential category is a symmetric monoidal category with a comonad $!$ and a natural isomorphism $d_A:\mathrm{!}A\otimes A\to \mathrm{!}A$, called the deriving transformation, that satisfies certain coherences that capture the fundamental properties of differentiation, like the product rule and chain rule. The coKleisli category of a monoidal differential category is a Cartesian differential category [1]. It is then natural to ask what is the analogue of a monoidal differential category whose coKleisli is a Cartesian differential Turing category.

In this talk, I will introduce monoidal differential Turing categories and their analogous notion of differential canonical codes. At the heart of this definition is a distinguished object $T$, called the universal object, a family of application morphisms $\bullet :T\otimes \mathrm{!}B\to C$, and a family of functions $\lambda :\mathrm{Hom}(A\otimes \mathrm{!}B,C)\to \mathrm{Hom}(A,T)$ such that the following diagrams commute:

One should think of these diagrams as defining a weak form of currying: $\lambda$ is transposition, $\bullet$ is evaluation which is also linear in its first argument, and $T$ behaves like a uniform exponential object. We will show that the coKleisli category of a monoidal differential Turing category (with differential canonical codes) is indeed a Cartesian differential Turing category (with differential canonical codes). We will then extend these constructions to the closely-related reverse differential setting from [5].