A foundational theory of compositional categorical rewriting theory is presented, based on a collection of fibration-like properties that collectively induce and structure intrinsically the large collection of lemmata used in the proofs of theorems such as concurrency and associativity. The resulting highly generic proofs of these theorems are given; it is noteworthy that the proof of the concurrency theorem takes only a few lines and, while that of associativity remains somewhat longer, it would be unreadably long if written directly in terms of the basic lemmata. In addition to improving, or even enabling, the readability of human-written proofs, we anticipate that this more generic and modular style of writing proofs should organize and inform the production of formalized proofs in a proof assistant such as Coq or Isabelle. A curated list of known instances of our framework is used to conclude the paper with a detailed discussion of the conditions under which the Double Pushout and Sesqui-Pushout semantics of graph transformation are compositional.

翻译：本文提出了一种组合范畴重写理论的基础理论，该理论基于一组类似纤维化的性质，这些性质共同作用并在内部结构化地引入了大量引理，这些引理用于证明诸如并发性和结合性等定理。文中给出了这些定理的高度通用化证明；值得注意的是，并发性定理的证明仅需数行，而结合性定理的证明虽然稍长，但若直接基于基本引理书写则会冗长到难以阅读。除了提升甚至实现人类可读证明的可读性外，我们预期这种更通用、更模块化的证明风格将组织和指导在Coq或Isabelle等证明助手中生成形式化证明的过程。本文通过列举已知的框架实例，详细讨论了双推图与半推图语义在图变换中具有组合性的条件，以此作为总结。