[TYPES] Announcement of paper on differential categories

[Robert Seely]

Differential categories

by  R.F. Blute, J.R.B. Cockett and R.A.G. Seely

   This paper is available at                              
      http://www.math.mcgill.ca/rags/difftl/difftl.ps.gz   

Abstract

Following work of Ehrhard and Regnier, we introduce the notion of a
differential category: an additive symmetric monoidal category with a comonad
(a "coalgebra modality") and a differential combinator, satisfying a number of
coherence conditions. In such a category, one should imagine the morphisms in
the base category as being linear maps and the morphisms in the coKleisli
category as being smooth (infinitely differentiable). Although such categories
do not necessarily arise from models of linear logic, one should think of this
as replacing the usual dichotomy of linear vs. stable maps established for
coherence spaces.

After establishing the basic axioms, we give a number of examples. The most
important example arises from a general construction, a comonad on the category
of vector spaces. This comonad and associated differential operators fully
capture the usual notion of derivatives of smooth maps. Finally, we derive
additional properties of differential categories in certain special cases,
especially when the differential comonad is a storage modality, as in linear
logic. In particular, we introduce the notion of categorical model of the
differential calculus, and show that it captures the not-necessarily-closed
fragment of Ehrhard-Regnier differential lambda-calculus.

It is important to note that differential categories in our sense are
strictly more general than the Ehrhard-Regnier structures. For example,
by developing them without monoidal closed structure, we capture various
"standard models" of differentiation which do not have these properties
(principly our examples over vector spaces).

Type theorists should notice that although the emphasis of the paper is
on the categorical semantics, the category theory is presented in a way
that makes the underlying type theory very transparent; the analogy with
linear logic is naturally striking, as it provides one of the intuitions, 
although our models are not necessarily models of linear logic.

-- 
<rags at math.mcgill.ca>
<www.math.mcgill.ca/rags>