Left-Linear Rewriting in Adhesive Categories

TL;DR

This work extends the DPO rewriting framework to left-linear rules in $M$-adhesive categories to study when two sequential steps are causally independent. It introduces a novel independence notion and switchability concept, defines well-switching rewriting systems, and proves a Local Church–Rosser theorem that ensures switchability under suitable conditions, effectively restoring a form of concurrency reasoning. Although left-linear merges invalidate a standard permutation-based canonical form, the authors establish weakened globality, preserved switching consistency, and a canonical switching form, enabling canonical proofs of equivalence for concurrent computations. The results apply to broad categorical models, including sets, graphs, and e-graphs, and pave the way for a rigorous concurrent semantics for left-linear rewriting in adhesive categories, with potential connections to weak prime domains and related semantic frameworks.

Abstract

When can two sequential steps performed by a computing device be considered (causally) independent? This is a relevant question for concurrent and distributed systems, since independence means that they could be executed in any order, and potentially in parallel. Equivalences identifying rewriting sequences which differ only for independent steps are at the core of the theory of concurrency of many formalisms. We investigate the issue in the context of the double pushout approach to rewriting in the general setting of adhesive categories. While a consolidated theory exists for linear rules,which can consume, preserve and generate entities, this paper focuses on left-linear rules which may also "merge" parts of the state. This is an apparently minimal, yet technically hard enhancement,since a standard characterisation of independence that - in the linear case - allows one to derive a number of properties, essential in the development of a theory of concurrency, no longer holds. The paper performs an in-depth study of the notion of independence for left-linear rules: it introduces a novel characterisation of independence, identifies well-behaved classes of left-linear rewriting systems,and provides some fundamental results including a Church-Rosser property and the existence of canonical equivalence proofs for concurrent computations. These results properly extends the class of formalisms that can be modelled in the adhesive framework

Figures (12)

• Figure 1: Rewriting rules for the coffee example.
• Figure 2: A sequence of rewriting steps.
• Figure 3: A rewriting system in $\mathbf{Graph}$.
• Figure 4: The derivation $\underline{\mathscr{D}}$.
• Figure 5: The derivation $\underline{\mathscr{E}}$.

Theorems & Definitions (79)

• Definition 1: Van Kampen property
• Definition 2: $\mathcal{M}$-adhesive category
• Remark 3
• Example 4
• Theorem 5
• Example 6
• Definition 7: habel2012mathcalheindel2009category
• Definition 8: Derivation
• Definition 9: Abstraction equivalence
• Definition 10: Sequential independence