Coherence in monoidal track categories
我们引入同伦的方法重写的基础上更高的维度类别证明的一致性结果的代数结构的类别。我们将（对称）幺半范畴的连贯性问题表示为迹范畴的非球面性问题，并利用多道生理记录仪上的重写方法来解决，将其推广到更一般的连贯性问题，即迹范畴中的三维字问题，包括辫状幺半范畴的情况.
2010-12-01 math.CT
Rewriting Graphically with Symmetric Traced Monoidal Categories
我们研究的超图，我们称之为接口线性超图的变体，其目的是创建一个健全的和完整的图形语言的对称跟踪幺半范畴类（STMCs）适合图重写。特别是，我们感兴趣的是重写的分类设置与笛卡尔结构，如数字电路。这些与以前的语言不兼容，其中使用紧凑的封闭或Frobenius结构来构造迹，因为将这些与笛卡儿积结合可能导致退化图。相反，我们必须考虑将跟踪构造为原子操作的方法。有界线性超图是一种正则超图，其中每个顶点都是一条边的源和目标，并带有一条额外的有界边。自由生成的STMC的态射被解释为接口的线性超图，直到同构（健全性）。此外，任何线性超图都是唯一STMC态射的表示，直到范畴的方程理论（完全性）。这建立了接口线性超图作为一个合适的组合语言STMC。然后，我们将展示如何将粘合剂类别的理论应用到我们的图形语言中，这意味着广泛的STMCs的等式属性可以指定为图形重写系统。数字电路的图形语言作为一个案例研究。
2021-03-19 math.CT
Rewriting Modulo Traced Comonoid Structure
University of Birmingham（伯明翰大学）
本文提出了一种基于迹余幺半群结构的图重写方法，用于描述具有延迟和反馈的顺序电路等式理论。
2026-01-01 cs.LO math.CT
Open Graphs and Monoidal Theories
弦图是推理物理过程、逻辑电路、张量网络和许多其他组成结构的强大工具。这些图的显著特征是边不需要连接到两端的顶点，并且这些未连接的端部可以被解释为图的输入和输出。在本文中，我们给出了一个具体的结构字符串图使用一种特殊类型的图称为开图。虽然开图的范畴本身不是粘合剂，我们引入了选择性粘合函子的概念，并表明这样的函子嵌入开图的范畴到类型图的环境粘合剂范畴。使用这个函子，开图的范畴继承了类型图的范畴的“足够的粘附性”来执行双推出（DPO）图重写。我们的理论的一个突出特点是，它确保重写系统是“类型安全”的意义上，重写尊重的输入和输出。这种形式主义使我们能够安全地编码计算模型的有趣结构，例如评估动态，具有简洁，明确的重写规则，而图形表示吸收了许多繁琐的细节。虽然拓扑形式主义存在的弦图，我们的建设是谨慎的，有限的，并享有可判定的算法组成和重写。我们还展示了如何开图可以参数化的图形签名，类似于monoidal签名的Joyal和街，定义类型的顶点的图形语言和约束，它们可以如何连接。利用类型开图，我们可以构造自由对称幺半范畴、PROPs和更一般的monoidal理论。因此，开图为我们提供了一个在幺半范畴中进行机械化推理的工具。
2010-11-18 cs.LO math.CT
Categorical E-Graphs for Lambda Calculi
University of Birmingham（伯明翰大学）；Kyoto University and Huawei Central Software Institute（京都大学和华为中央软件研究所）
针对 e-graphs 缺乏变量绑定支持的问题，本文基于范畴论框架扩展至闭对称幺半范畴，利用层次超图实现绑定，并提出双推重写机制，证明其与项重写的等价性。
2026-06-26 cs.LO math.CT
Rewriting techniques for relative coherence
该研究拓展代数结构相干性的重写证明方法，覆盖部分相干性与笛卡尔结构两类情形，构建抽象及项重写系统层面的重写技术与定理，可推导幺半范畴等的相干定理。
2025-07-23 math.CT
Rewriting modulo in diagrammatic algebras and application to categorification
Max Planck Institute for Mathematics（马克斯·普朗克数学研究所）
该研究发展了适用于高阶线性结构的模重写理论，将其应用于证明与奇Khovanov同调相关的超2范畴的基猜想，为非专家提供了重写理论导论。
2026-08-24 math.CT math.GT math.QA
Rewriting in higher dimensional linear categories and application to the affine oriented Brauer category
本文介绍了线性幺半范畴范畴的重写理论。这些范畴是我们将定义为线性（n，p）范畴的一个特例。我们还将定义线性（n，p）-多道图，线性适应的n-多道图，目前线性（n - 1，p）-范畴。然后，我们专注于线性（3，2）-多道图给出线性幺半范畴的介绍。最后我们给出了这个理论在线性（3，2）-多道生理记录图中的应用，利用van Ostroom定义的重写性质：递减性，用一种新的方法证明了AOB范畴上的一个基定理。
2016-03-01 math.CT math.RT
Rewriting modulo isotopies in Khovanov-Lauda-Rouquier's categorification of quantum groups
利用代数重写方法研究了量子群的Khovanov-Lauda- Rouquier候选$2$ -分类的表示.我们使用的计算方法的基础上重写模的枢轴结构的合痕公理计算一族的线性基的所有向量空间的$2$ -细胞在这个$2$ -范畴。我们表明，这些基地对应于Khovanov和劳达的约束生成集，证明了非退化的图解演算。这意味着这个$2$ -范畴是Lusztig的幂等整数量子群$\bf{U}_{q}(\mathfrak{g})$的一个范畴，它与一个可对称化的单缀Kac-Moody代数$\mathfrak{g}$相关联。
2019-07-23 math.CT math.QA math.RT
Coherent confluence modulo relations and double groupoids
一个n-范畴的连贯表示是由生成元、关系和关系之间的关系表示的。合流和终止重写系统产生连贯的表示，其关系之间的关系定义的临界分支的合流图。本文介绍了一个程序来计算一致的表示时，重写关系定义模一组公理。我们的一致性结果是使用的结构，丰富的n-范畴的双广群，其水平细胞表示重写路径，垂直细胞表示的同余产生的公理和正方形细胞表示一致性细胞引起的图的汇合模。我们说明我们的结构重写系统模交换关系的交换幺半群，合痕关系的枢纽幺半范畴范畴，和逆关系的群体。
2021-10-04 math.CT
A Critical Pair Enumeration Algorithm for String Diagram Rewriting
Johns Hopkins University（约翰霍普金斯大学）；University of Washington（华盛顿大学）；University of Technology of Compiègne（贡比涅技术大学）；Universidad Nacional de Córdoba（科尔多瓦国立大学）；Tallinn University of Technology（塔林理工大学）；University of São Paulo（圣保罗大学）；National Institute of Informatics（日本国立情报学研究所）；Ochanomizu University（御茶水女子大学）
本文提出了一种用于字符串图重写的自动化关键对枚举算法，适用于无弗罗贝尼乌斯结构的对称张量范畴。
2026-03-10 cs.DS math.CT
Dynamic Tracing: a graphical language for rewriting protocols
本研究将Set_*范畴的追踪幺半结构中的隐式转换过程显式化，推广到更多追踪Kleisli范畴并给出推测性追踪算子，为图重写计算提供形式化图形语法。
2023-05-01 cs.LO math.CT math.LO
Pictures of Processes: Automated Graph Rewriting for Monoidal Categories and Applications to Quantum Computing
这项工作是关于图形语言，它们如何被表示，以及它们反过来可以用来表示什么。更具体地说，它侧重于字符串图的表示和应用。字符串图用于表示一组进程，用“盒子”表示，带有多个（类型化的）输入和输出，用“线”表示。如果我们允许将输入和输出连接在一起，我们就可以直观地表示过程的复杂组合，形式化为幺半范畴中的态射。[...]本论文的第一个主要贡献是介绍了一个离散版本的字符串图称为字符串图。字符串图形成了一个部分粘合类别，因此可以使用双推出图重写来操纵它们。此外，我们展示了如何字符串图模重写系统可以用来构建免费的对称跟踪和紧凑的闭范畴monoidal签名。第二个贡献是图形语言在量子信息论中的应用。我们使用的混合物的图解和代数技术证明一个新的分类结果强互补的可观。[...]我们还介绍了一个图形语言的多体纠缠，并说明了一个简单的图形公理，区分两个最大纠缠的三方量子比特状态：GHZ和W。[...]第三个贡献是作者开发的两个软件工具的描述，以实现这里描述的大部分理论内容。第一个工具是Quantity，这是一个桌面应用程序，用于构建字符串图和图形理论，以及可视化地执行自动图形重写。第二个是QuantoCoSy，它使用一种称为猜想合成的程序来执行完全自动化的模型驱动理论创建。
2012-03-22 cs.AI math.CT quant-ph
Confluence of algebraic rewriting systems
代数结构上的收敛重写系统给出了解决判定问题、证明一致性结果和计算同调不变量的方法。这些方法是基于高维扩展的临界分支引理，证明了当地的汇合的临界分支。代数结构（如群或线性代数）上的重写系统的局部收敛性分析由于底层的代数公理而变得复杂。本文介绍了代数测谎模的结构，形式化的代数重写系统的规则和固有的代数公理之间的相互作用，我们展示了一个关键的分支引理代数测谎。我们推导出一个临界分支引理重写系统的代数模型，其公理指定的收敛模重写系统。我们说明了我们的建设字符串，线性和组重写系统。
2021-11-05 math.CT
ViCAR: Visualizing Categories with Automated Rewriting in Coq
ViCAR 是一个 Coq 库，提供幺半范畴定义、一致性验证、引理策略及字符串图可视化，支持图形化推理与自动重写。
2025-09-25 cs.PL math.CT
String Diagram Rewrite Theory I: Rewriting with Frobenius Structure
弦图是一种强大而直观的图形语法，起源于对对称monoidal范畴的研究。在过去的几年中，它们已经在各种计算结构的建模中得到应用，在计算机科学、物理学、控制理论、语言学和生物学等领域。在许多这样的提议中，所描述的系统的转换被建模为图的重写规则。这些发展需要弦图重写的数学基础：尽管术语的重写理论是很好理解的，但弦图的二维性质带来了额外的挑战。这项工作系统化和扩展了一系列最近的会议论文奠定了这样的基础。作为第一步，我们专注于重写系统的情况下，具有Frobenius代数的弦图解理论。这种情况普遍存在于各种方法中：例如，在线性动力系统的代数语义中，弗罗贝纽斯结构模拟电路的布线;在分类量子力学中，它们模拟相互作用的量子可观测量。我们的工作介绍了一个组合的解释弦图重写模Frobenius结构，在双推出超图重写。此外，我们证明了这种解释是健全的和完整的。在最后一部分中，我们还看到，该方法可以推广到模型重写模多个Frobenius结构。作为概念的证明，我们展示了如何从这些结果中得出一个终止策略的相互作用双代数，一个重要的重写理论在量子电路和信号流图的研究。
2022-02-03 cs.LO math.CT
Coherence without unique normal forms
范畴所携带的协变结构的相干定理传统上依赖于结构的底层项重写系统是终止的和汇合的。虽然在许多情况下都是如此，但这并不是一致性问题本身所固有的特征。这一点可以通过迭代幺半范畴范畴的理论来证明，它模拟了迭代的闭路空间，并且有一个相干定理，但不能是融合的。我们开发了一个框架来表达一致性问题的术语重写系统配备了一个二维的一致性。在这个框架内，我们提供了一般的解决方案，两个相关的一致性定理：确定是否有一个决策程序的交换性的图在所得到的结构和确定充分条件，确保"所有的图表交换“。由此产生的一致性定理既不依赖于底层重写系统的终止，也不依赖于底层重写系统的汇合。我们将这一理论应用于迭代幺半范畴范畴，得到了它们的凝聚定理的一个新的概念性证明。
2007-05-30 math.CT
From Gs-monoidal to Oplax Cartesian Categories: Constructions and Functorial Completeness
本文扩展 gs-monoidal 范畴为带箭头预序的 oplax cartesian 范畴，刻画其 Kleisli 与 span 构造，并证明 Yoneda 嵌入及函子完备性定理。
2023-09-29 cs.LO math.CT
Super rewriting theory and nondegeneracy of odd categorified sl(2)
本文将高维重写理论推广到超范畴，建立幺半超范畴与2-超范畴的重写工具，并借此证明量子 sl(2) 奇范畴化的非退化猜想，进而给出奇2-范畴上 dg-结构的分类。
2021-01-30 math.CT math.QA math.RT
Hypergraph Categories
超图范畴已经被重新发现了至少五次，有各种各样的名称，包括得到很好支持的紧致闭范畴、dgs-幺半范畴和地牢范畴。也许它们不断被重新发明的原因是双重的：有许多应用-包括自动机、数据库、电路、线性关系、图重写和信念传播-但标准定义是如此复杂和华丽，以至于很难在文献中找到。实际上，超图范畴，粗略地说，是一个“对称的幺半范畴范畴，其中每个对象都具有一个特殊的交换Frobenius幺半群的结构，满足一定的相干条件”。幸运的是，这种描述可以简化很多：超图范畴只是一个“cosan代数”。本文的目标是删除惊吓引号，使前面的陈述准确。我们证明了两个主要定理。第一个是超图范畴的凝聚定理，即每一个超图范畴都等价于一个无对象超图范畴。其次，我们证明了无对象超图范畴范畴等价于余生成代数范畴。
2019-01-18 cs.LO math.CT
!-Graphs with Trivial Overlap are Context-Free
弦图是在对称monoidal范畴中推理复合结构的有力工具。通过将字符串图表示为图形，等式推理可以通过双推出重写自动完成。!-图同时给了我们表示和证明这些图的整个族的性质的手段。同时！-图为令人惊讶的强大定理提供了优雅的证明，但对它们定义的图形语言的形式属性知之甚少。本文采取的第一步，在这些语言的特点表明，一个重要的子类！-图--其重复结构仅平凡地重叠的那些图--可以使用（上下文无关的）顶点替换语法来编码。
2015-04-10 cs.FL cs.LO math.CT
$A_{\infty}$-structures in monoidal DG categories and strong homotopy unitality
本文在任意幺半DG范畴中借助无界扭曲复形定义A∞代数、余代数、模与余模，引入强同伦幺性，构造自由-遗忘同伦伴随及导出范畴，并证明A∞代数与余代数的同伦伴随给出导出模-余模等价，应用于A∞单子与增强正合单子。
2023-11-29 math.AG math.AT math.CT
Quantomatic: A Proof Assistant for Diagrammatic Reasoning
Monoidal代数结构由可以具有多个输出以及多个输入的操作组成，其在许多领域中具有应用，包括范畴代数、程序设计语言语义、表示论、代数量子信息和量子群。字符串图提供了一种方便的图形语法，用于正式推理这种结构，同时避免了基于术语的方法的许多技术挑战。Quantification是一个工具，支持使用字符串图（半）自动构造等式证明。我们简要地概述了Quantity的重写引擎的理论基础，然后给出了一个概述的核心功能和架构，并给出了一个简单的例子项目，计算交换双代数的范式。
2015-10-13 cs.LO cs.MS math.CT
