paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Rewriting techniques for relative coherence

相对相干性的重写技术
LMCS vol.Volume 21, Issue 32025匹配度 2/10 · 该论文研究重写系统用于相对相干性证明,属于范畴论与形式语义/证明工程,虽与形式化验证有间接关联,但与用户核心关注的静态分析、LLM/Agent、浮点程序分析和贝叶斯程序分析均无直接交集。引用 0 inbox
Samuel Mimram
crossref: 2026-09-10

AI 速览

一句话:扩展基于重写的相干性证明,覆盖部分相干与笛卡尔结构,并恢复单子/对称单子范畴相干定理。

该论文研究如何用重写技术证明代数结构的相干性。已有工作表明,在合理假设下,临界对的汇合图可给出所需相干公理,如 Mac Lane 单子范畴相干定理。作者同时朝两个方向推广:一是相对相干性,即相干只对部分结构态射成立;二是笛卡尔结构,其中变量可被复制或删除。论文先在抽象重写系统中建立一般定理与重写技术,再推广到项重写系统,使其能处理相干性。作为应用,作者说明如何恢复单子范畴与对称单子范畴的相干定理。

问题
如何将基于重写与临界对汇合性的相干性证明方法,推广到只对部分结构态射成立的相对相干性,以及允许变量复制和删除的笛卡尔结构。
方法
在抽象重写系统中建立相对相干性的定理与重写技术,再将结论推广到扩展后的项重写系统,并通过单子范畴与对称单子范畴的例子展示应用。
评估
以理论证明和例子验证为主:从抽象重写到项重写给出通用框架,并说明可恢复单子范畴与对称单子范畴的经典相干定理。
原文摘要(Abstract)

A series of works has established rewriting as an essential tool in order to prove coherence properties of algebraic structures, such as MacLane's coherence theorem for monoidal categories, based on the observation that, under reasonable assumptions, confluence diagrams for critical pairs provide the required coherence axioms. We are interested here in extending this approach simultaneously in two directions. Firstly, we want to take into account situations where coherence is partial, in the sense that it only applies to a subset of the structural morphisms. Secondly, we are interested in structures which are cartesian in the sense that variables can be duplicated or erased. We develop theorems and rewriting techniques in order to achieve this, first in the setting of abstract rewriting systems, and then extend them to term rewriting systems, suitably generalized to take coherence into account. As an illustration of our results, we explain how to recover the coherence theorems for monoidal and symmetric monoidal categories.

链接与引用

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

BibTeX
@article{Mimram25,
  title = {Rewriting techniques for relative coherence},
  author = {Samuel Mimram},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 21, Issue 3},
  year = {2025},
  doi = {10.46298/lmcs-21(3:7)2025}
}