Cartesian Coherent Differential Categories

03/13/2023
by   Thomas Ehrhard, et al.
0

We extend to general Cartesian categories the idea of Coherent Differentiation recently introduced by Ehrhard in the setting of categorical models of Linear Logic. The first ingredient is a summability structure which induces a partial left-additive structure on the category. Additional functoriality and naturality assumptions on this summability structure implement a differential calculus which can also be presented in a formalism close to Blute, Cockett and Seely's Cartesian differential categories. We show that a simple term language equipped with a natural notion of differentiation can easily be interpreted in such a category.

READ FULL TEXT

Please sign up or login with your details

Forgot password? Click here to reset