paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Template games and differential linear logic

模板博弈与微分线性逻辑
LICS 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)2019匹配度 1/10 · 该论文属于纯逻辑/形式语义理论,研究微分线性逻辑的博弈语义及其与同伦论的联系,与用户的 PL↔AI、LLM/Agent、浮点程序分析、贝叶斯程序分析等方向没有直接交集;仅可视为 PL 理论基础,但缺乏与静态分析、LLM 或工程落地的关联。引用 13 inbox
Paul-Andre Mellies
crossref: 2026-09-12

AI 速览

一句话:首次为经典形式的微分线性逻辑建立博弈语义,并揭示其与同伦论的意外联系。

该论文研究微分线性逻辑(DiLL)的语义模型,特别是为其经典形式构造博弈语义,这是博弈语义中长期未决的问题。作者将其此前的乘法加性线性逻辑(MALL)模板博弈模型扩展到含指数模态的情形,指数模态由自由对称幺半范畴的标准构造 Sym 导出。构造过程中,作者与 Fiore、Gambino、Hyland 和 Winskel 十年前提出的广义物种(generalised species)模型进行了细致比较。结果不仅首次给出了 DiLL 经典形式的博弈语义,解决了旧开问题,还意外揭示出线性逻辑与同伦理论之间富有前景的收敛。

问题
微分线性逻辑的经典形式长期缺乏博弈语义;已有模板博弈模型仅覆盖乘法加性线性逻辑(MALL),尚未处理指数模态。
方法
作者利用自由对称幺半范畴的标准构造 Sym 引入指数模态,将模板博弈模型扩展到 DiLL,并与广义物种模型进行范畴式比较。
评估
这是一项理论构造与范畴比较工作;论文证明新模型给出 DiLL 经典形式的首个博弈语义,解决旧开问题,并揭示线性逻辑与同伦论之间的联系。
原文摘要(Abstract)

We extend our recent template game model of multiplicative additive linear logic (MALL) with an exponential modality of linear logic (LL) derived from the standard categorical construction Sym of the free symmetric monoidal category. We obtain in this way the first game semantics of differential linear logic (DiLL) in its classical form. The construction of the model relies on a careful and healthy comparison with the model of generalised species designed ten years ago by Fiore, Gambino, Hyland and Winskel. Besides the resolution of an old open problem of game semantics, the study reveals an unexpected and promising convergence between linear logic and homotopy theory.

链接与引用

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

BibTeX
@inproceedings{paperbot5016,
  title = {Template games and differential linear logic},
  author = {Paul-Andre Mellies},
  booktitle = {LICS},
  year = {2019},
  doi = {10.1109/lics.2019.8785830}
}