paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Categorical models of Linear Logic with fixed points of formulas

具有公式不动点的线性逻辑的范畴模型
LICS 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)2021匹配度 2/10 · 该论文研究命题线性逻辑 μLL 的范畴语义与指称式归一化,属于纯形式语义/证明论,与用户关注的 LLM/Agent 静态分析、浮点程序分析、贝叶斯程序分析等方向无直接关联,且未涉及工程实现或工业落地。引用 0 inbox
Thomas Ehrhard, Farzad Jafarrahmani
crossref: 2026-09-12

AI 速览

一句话:为带最小/最大不动点的命题线性逻辑 μLL 建立范畴语义,给出两个模型,后者展示指称式证明归一化。

论文研究 μLL 的范畴语义。μLL 是带最小与最大不动点的命题线性逻辑,在 Baelde 的命题 μMALL 基础上加入指数。作者以 Seely 范畴及作用于其上的强函子为一般框架,给出该语言的语义解释。文中构造两个实例:第一个基于集合与关系范畴,其中最小与最大不动点被同样解释;第二个基于带完全性概念的集合(非一致完全空间)及其保持完全性的关系范畴,其中两类不动点获得不同解释。后一模型表明 μLL 具有指称式的证明归一化性质,从而以范畴语义刻画其证明论行为。

问题
如何为扩展了最小/最大不动点和指数的命题线性逻辑 μLL 提供范畴语义,并区分最小与最大不动点。
方法
基于 Seely 范畴与强函子搭建一般语义框架,并构造集合-关系模型和带完全性空间的集合-关系模型两个实例。
评估
通过两个具体模型验证框架;其中非一致完全空间模型区分最小/最大不动点,并证明 μLL 的指称式证明归一化。
原文摘要(Abstract)

We develop a categorical semantics of μLL, a version of propositional Linear Logic with least and greatest fixed points extending David Baelde's propositional μMALL with exponentials. Our general categorical setting is based on Seely categories and on strong functors acting on them. We exhibit two simple instances of this setting. In the first one, which is based on the category of sets and relations, least and greatest fixed points are interpreted in the same way. In the second one, based on a category of sets equipped with a notion of totality (non-uniform totality spaces) and relations preserving it, least and greatest fixed points have distinct interpretations. This latter model shows that μLL enjoys a denotational form of normalization of proofs.

链接与引用

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

BibTeX
@inproceedings{paperbot6207,
  title = {Categorical models of Linear Logic with fixed points of formulas},
  author = {Thomas Ehrhard and Farzad Jafarrahmani},
  booktitle = {LICS},
  year = {2021},
  doi = {10.1109/lics52264.2021.9470664}
}