paperbot · PL 论文追踪

全部论文 待读 收藏

P2 LNL polycategories and doctrines of linear logic

LNL polycategory 与线性逻辑的 doctrine
LMCS vol.Volume 19, Issue 22023匹配度 2/10 · 该论文属于纯范畴论与线性逻辑的形式语义研究,不涉及静态分析、LLM/Agent、浮点程序分析或贝叶斯程序分析,与用户当前核心研究方向无直接关联。虽然属于 PL 理论基础,但缺乏工程实现与 AI 交叉,因此匹配度较低。引用 2 inbox
Michael Shulman
crossref: 2026-09-10

AI 速览

一句话:引入 LNL polycategory 与 LNL doctrine,统一刻画含指数的经典线性逻辑及其多种范畴结构。

论文研究如何统一抽象带指数(exponentials)的经典线性逻辑的判定结构。作者定义 LNL polycategory,它能表示 LNL 伴随、线性指数余单子、LNL multicategory、IL-索引范畴、带 storage 的线性分配范畴、交换/强单子、CBPV 结构、极化演算模型、Freyd 范畴、skew multicategory,以及普通笛卡尔/对称/平面 multicategory、monoidal 范畴、对称 polycategory、线性分配与 *-autonomous 范畴等。为统一研究这些结构,作者引入 LNL doctrine,将各类结构视为该 doctrine 的代数。进一步证明 LNL doctrine 的自由代数可由相继式演算呈现,且 doctrine 的态射诱导其代数 2-范畴之间的伴随。

问题
如何在同一范畴与证明论语境下,统一刻画经典线性逻辑(尤其是带指数)所对应的多种判定结构和模型?
方法
定义 LNL polycategory 来抽象判定结构,并引入 LNL doctrine,把各类结构识别为该 doctrine 的代数;用相继式演算呈现自由代数,并研究 doctrine 态射与代数 2-范畴。
评估
通过范畴论构造与理论证明进行评估:展示大量已知结构均可纳入该框架,证明自由代数可由相继式演算呈现,且每个 doctrine 态射诱导其代数 2-范畴之间的伴随。
原文摘要(Abstract)

We define and study LNL polycategories, which abstract the judgmental structure of classical linear logic with exponentials. Many existing structures can be represented as LNL polycategories, including LNL adjunctions, linear exponential comonads, LNL multicategories, IL-indexed categories, linearly distributive categories with storage, commutative and strong monads, CBPV-structures, models of polarized calculi, Freyd-categories, and skew multicategories, as well as ordinary cartesian, symmetric, and planar multicategories and monoidal categories, symmetric polycategories, and linearly distributive and *-autonomous categories. To study such classes of structures uniformly, we define a notion of LNL doctrine, such that each of these classes of structures can be identified with the algebras for some such doctrine. We show that free algebras for LNL doctrines can be presented by a sequent calculus, and that every morphism of doctrines induces an adjunction between their 2-categories of algebras.

链接与引用

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

BibTeX
@article{paperbot2226,
  title = {LNL polycategories and doctrines of linear logic},
  author = {Michael Shulman},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 19, Issue 2},
  year = {2023},
  doi = {10.46298/lmcs-19(2:1)2023}
}