论文标题
构图重写理论的基础
Fundamentals of Compositional Rewriting Theory
论文作者
论文摘要
构成分类重写理论的基础理论是基于类似纤维化的特性的集合，共同诱导和本质地构造了用于同步和关联等定理证明的大量lemmata。给出了这些定理的高度通用证据。值得注意的是，并发定理的证明仅需几行，而关联的证据仍然更长，但如果直接根据基本的lemmata而直接编写，则将是不可读的。从本质上讲，我们的框架通过暴露潜在模块化来提高对这些证据的理解的可读性和便利性。我们的框架已知实例的策划列表用于结束论文，并详细讨论了图形转换的双重俯卧以及sesqui-pushout语义。
A foundational theory of compositional categorical rewriting theory is presented, based on a collection of fibration-like properties that collectively induce and intrinsically structure 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 essence, our framework improves the readability and ease of comprehension of these proofs by exposing latent modularity. 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.
