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