paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Taylor expansion in linear logic is invertible

线性逻辑中的 Taylor 展开是可逆的
LMCS vol.Volume 14, Issue 42018匹配度 1/10 · 该论文属于纯线性逻辑与证明论的语义研究，讨论 MELL 证明网的 Taylor 展开与关系模型完备性，未涉及静态分析、机器学习系统、Agentic 程序、LLM 辅助形式化验证、浮点程序分析或贝叶斯程序分析等用户核心方向。引用 5 inbox
Daniel de Carvalho
形式语义
crossref: 2026-09-10

AI 速览

一句话：证明不同 MELL 证明网具有不同 Taylor 展开，并由此导出关系模型对 MELL 的完备性。

本文研究乘法指数线性逻辑（MELL）证明网的 Taylor 展开及其与关系模型完备性的关系。每个 MELL 证明网都可展开为一个 differential net，即其 Taylor 展开。作者证明该展开操作是单射的：两个不同的 MELL 证明网不可能具有相同的 Taylor 展开。作为推论，论文得到 MELL 的完备性结果：关系模型对 MELL 证明网是单射的，即两个 MELL 证明网在关系模型中相等，当且仅当它们可由 cut-elimination 公理化。该工作表明 Taylor 展开不仅能区分证明网，而且将展开这一语法操作与关系指称模型中的等式理论精确对应起来。

问题
核心问题是 Taylor 展开是否保留 MELL 证明网的区分信息，以及关系模型能否完备刻画 MELL 证明网的 cut-elimination 等价。
方法
将每个 MELL 证明网展开为其 Taylor 展开（differential net），并证明该展开映射是单射。
评估
通过理论证明完成：由 Taylor 展开的单射性推出关系模型对 MELL 证明网的单射性，即关系模型中的等式恰由 cut-elimination 公理化。
原文摘要（Abstract）

Each Multiplicative Exponential Linear Logic (MELL) proof-net can be expanded into a differential net, which is its Taylor expansion. We prove that two different MELL proof-nets have two different Taylor expansions. As a corollary, we prove a completeness result for MELL: We show that the relational model is injective for MELL proof-nets, i.e. the equality between MELL proof-nets in the relational model is exactly axiomatized by cut-elimination.

链接与引用

DOI 原文 · PDF（开放获取） ·

BibTeX 
@article{paperbot351,
  title = {Taylor expansion in linear logic is invertible},
  author = {Daniel de Carvalho},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 14, Issue 4},
  year = {2018},
  doi = {10.23638/lmcs-14(4:21)2018}
}