paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Cartesian Coherent Differential Categories

笛卡尔相干微分范畴
LICS 2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)2023匹配度 1/10 · 该论文属于纯范畴论/形式语义,研究相干微分在笛卡尔范畴中的推广与项语言语义,不涉及机器学习系统、Agentic 程序、静态分析、LLM、浮点程序分析或贝叶斯程序分析。引用 4 inbox
Ehrhard Thomas, Walch Aymeric
crossref: 2026-09-12dblp: 2026-09-12arxiv: 2026-09-12

AI 速览

一句话:将相干微分从线性逻辑范畴模型推广到一般笛卡尔范畴,并给出可解释微分项语言的语义框架。

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

问题
如何将线性逻辑范畴模型中的相干微分推广到一般笛卡尔范畴,并刻画其所需的结构条件?
方法
引入可和性结构以诱导部分左加性结构,并附加函子性与自然性假设,以接近笛卡尔微分范畴的形式建立微分演算。
评估
通过给出一个简单项语言及其自然微分概念在该类范畴中的解释来展示框架;属于理论构造与语义验证。
原文摘要(Abstract)

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.

链接与引用

DOI 原文 · arXiv · PDF(开放获取) · DBLP

BibTeX
@inproceedings{ThomasW23,
  title = {Cartesian Coherent Differential Categories},
  author = {Ehrhard Thomas and Walch Aymeric},
  booktitle = {LICS},
  year = {2023},
  doi = {10.1109/lics56636.2023.10175717}
}