paperbot · PL 论文追踪

全部论文 待读 收藏

P2 A Functorial Excursion Between Algebraic Geometry and Linear Logic

代数几何与线性逻辑之间的函子式漫游
LICS Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science2022匹配度 2/10 · 论文属于代数几何与线性逻辑交叉的纯范畴语义/形式语义研究,虽与程序语言理论中的线性逻辑模型相关,但未涉及用户画像核心关注的静态分析、LLM/Agent、浮点程序分析或贝叶斯程序分析。引用 5 inbox
Paul-André Melliès
crossref: 2026-09-12dblp: 2026-09-12

AI 速览

一句话:用函子点方法为交换环上的预层(含 scheme)构造预层模范畴,并证明其构成直觉主义线性逻辑模型。

本文探讨代数几何与线性逻辑之间的深层联系。代数几何中,scheme 既有几何面,也配备拟凝聚模的对称幺半范畴。作者采用 Grothendieck 的函子点观点,把交换环范畴上的协变预层 X 视为广义空间,并在其“上方”构造预层模范畴 PshMod_X。该范畴是对称幺半闭的,因而给出直觉主义线性逻辑的一个模型;其指数模态通过以适当方式粘合环代数上的 Sweedler 对偶构造得到。这一结果将 scheme 等几何对象统一纳入线性逻辑的范畴语义框架,表明几何空间上的模范畴可系统地为线性逻辑提供模型。

问题
如何从代数几何中的 scheme 与模层出发,建立与直觉主义线性逻辑之间的范畴语义联系。
方法
使用 Grothendieck 的函子点方法,为交换环范畴上的协变预层(尤其 scheme)构造预层模范畴 PshMod_X,并通过粘合环代数上的 Sweedler 对偶构造指数模态。
评估
以范畴论构造和定理证明进行论证,说明 PshMod_X 对称幺半闭且构成直觉主义线性逻辑模型;摘要未报告实现或实验评估。
原文摘要(Abstract)

The language of Algebraic Geometry combines two complementary and dependent levels of discourse: on the geometric side, schemes define spaces of the same cohesive nature as manifolds ; on the vectorial side, every scheme X comes equipped with a symmetric monoidal category of quasicoherent modules, which may be seen as generalised vector bundles on the scheme X. In this paper, we use the functor of points approach to Algebraic Geometry developed by Grothendieck in the 1970s to establish that every covariant presheaf X on the category of commutative rings — and in particular every scheme X — comes equipped “above it” with a symmetric monoidal closed category PshModX of presheaves of modules. This category PshModX defines moreover a model of intuitionistic linear logic, whose exponential modality is obtained by glueing together in an appropriate way the Sweedler dual construction on ring algebras.

链接与引用

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

BibTeX
@inproceedings{Mellies22,
  title = {A Functorial Excursion Between Algebraic Geometry and Linear Logic},
  author = {Paul-André Melliès},
  booktitle = {LICS},
  year = {2022},
  doi = {10.1145/3531130.3532488}
}