一句话:将相干微分从线性逻辑范畴模型推广到一般笛卡尔范畴,并给出可解释微分项语言的语义框架。
本文把 Ehrhard 最近在线性逻辑范畴模型上提出的相干微分(Coherent Differentiation)推广到一般笛卡尔范畴。其核心是引入可和性(summability)结构,从而在范畴上诱导出部分左加性结构;再附加函子性与自然性条件,即可实现一套微分演算,并可用接近 Blute、Cockett 与 Seely 的笛卡尔微分范畴的形式表述。作者进一步表明,一个带有自然微分概念的简单项语言可以方便地在该类范畴中解释,从而为笛卡尔设定下的相干微分提供统一语义框架。
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.