paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Ribbon Tensorial Logic

带状张量逻辑
LICS Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science2018匹配度 2/10 · 该论文属于证明论、范畴逻辑与拓扑语义的基础理论研究,与用户关注的静态分析、LLM/Agent、浮点程序分析和贝叶斯程序分析均无直接关联;仅在形式语义/逻辑这一大方向上与PL有较远的背景关联。引用 8 inbox
Paul-André Melliès
crossref: 2026-09-12

AI 速览

一句话:提出带状张量逻辑,将证明映射为带状缠结并证明该翻译忠实,从而给出平衡对话范畴的相干定理与拓扑博弈语义基础。

论文引入一种具有拓扑感知能力的张量逻辑变体,称为带状张量逻辑。它为每个证明关联一个带状缠结,用以追踪证明中张量否定的流动;该翻译具有函子性,其构造基于证明论中的对话范畴与纽结理论中的带状范畴之间的对应。核心结果是翻译的忠实性:两个证明在带状张量逻辑的等式理论下相等,当且仅当它们对应的带状缠结在拓扑形变下相等。这一“证明即缠结”定理可视为平衡对话范畴的相干定理,并为拓扑博弈语义提供数学基础。

问题
如何为张量逻辑的证明赋予拓扑不变量,并用它刻画证明在等式理论下的相等性?
方法
作者定义带状张量逻辑,在对话范畴与带状范畴之间建立对应,将每个证明翻译为追踪张量否定流动的带状缠结,并证明该翻译具有函子性。
评估
通过证明忠实性定理进行评估:两个证明在带状张量逻辑中等价当且仅当其带状缠结拓扑等价;该结果进一步导出平衡对话范畴的相干定理和拓扑博弈语义基础。
原文摘要(Abstract)

We introduce a topologically-aware version of tensorial logic, called ribbon tensorial logic. To every proof of the logic, we associate a ribbon tangle which tracks the flow of tensorial negations inside the proof. The translation is functorial: it is performed by exhibiting a correspondence between the notion of dialogue category in proof theory and the notion of ribbon category in knot theory. Our main result is that the translation is also faithful: two proofs are equal modulo the equational theory of ribbon tensorial logic if and only if the associated ribbon tangles are equal up to topological deformation. This "proof-as-tangle" theorem may be understood as a coherence theorem for balanced dialogue categories, and as a mathematical foundation for topological game semantics.

链接与引用

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

BibTeX
@inproceedings{paperbot4325,
  title = {Ribbon Tensorial Logic},
  author = {Paul-André Melliès},
  booktitle = {LICS},
  year = {2018},
  doi = {10.1145/3209108.3209129}
}