R.F. Blute, J.R.B. Cockett, J-S.P. Lemay, R.A.G. Seely
Abstract:
Differential categories were introduced to provide a minimal
categorical doctrine for differential linear logic. Here we revisit
the formalism and, in particular, examine the two different approaches
to defining differentiation which were introduced. The basic approach
used a deriving transformation, while a more refined approach, in the
presence of a bialgebra modality, used a codereliction. The latter
approach is particularly relevant to linear logic settings, where the
coalgebra modality is monoidal and the Seely isomorphisms give rise to
a bialgebra modality. Here, we prove that these apparently distinct
notions of differentiation, in the presence of a monoidal coalgebra
modality, are completely equivalent. Thus, for linear settings, there
is only one notion of differentiation.
The paper also presents a number of separating examples for coalgebra
modalities - which are and are not monoidal - which do and do not
support differential structure. Of particular interest is the
observation that - counter intuitively - differential algebras never
form differential categories although they do have a monoidal
coalgebra modality. On the other hand, Rota-Baxter algebras - which
are usually associated with integration - provide an example
of a differential category which has a non-monoidal coalgebra
modality.
This is an extended version of "There is only one notion of differentiation." Cockett, R., & Lemay, J-S., 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017).