Rocq 中基于黏性范畴论的图重写
计算机科学中的逻辑
2026-03-03 v2
摘要
我们设计了一个关于黏性范畴的 Rocq 库，使用 Hierarchy Builder (HB)。它围绕两个层次结构构建：第一个是范畴层次结构，底部为一般范畴，顶部为黏性范畴，中间包含较弱的黏性范畴变体。第二个是关于态射的层次结构（包括同构、单态射和正则单态射）。每个层次都配备多个接口以定义实例。我们覆盖了基本范畴概念，如 pullback 和 equalizer，以及黏性范畴特有的结论。通过该库，我们形式化了范畴图重写理论的两个核心定理：Church-Rosser 定理和并发定理。我们提供了多个实例，包括类型范畴、有限类型范畴、简单图范畴和预历范畴。我们详细说明了所做的实现选择，并报告了 HB 在该形式化工作中的使用情况。
引用
@article{arxiv.2509.17392,
title = {Adhesive category theory for graph rewriting in Rocq},
author = {Samuel Arsac and Russ Harmer and Damien Pous},
journal= {arXiv preprint arXiv:2509.17392},
year = {2026}
}