Fundamentals of Compositional Rewriting Theory

TL;DR

This paper develops a foundational, highly generic categorical rewriting theory that simplifies and modularizes proofs of key theorems like concurrency and associativity, enhancing understanding and applicability.

Contribution

It introduces a new compositional categorical rewriting framework based on fibration-like properties, improving proof modularity and clarity, and discusses conditions for graph transformation semantics.

Findings

Concise proof of the concurrency theorem

Enhanced readability of associativity proof

Conditions for compositional graph transformation semantics

Abstract

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.