Left-Linear Rewriting in Adhesive Categories

TL;DR

This paper extends the theory of concurrency in adhesive categories by analyzing independence in left-linear rewriting systems, introducing new characterizations and fundamental properties like Church-Rosser, enabling broader formal modeling.

Contribution

It introduces a novel characterization of independence for left-linear rules and establishes key properties, expanding the adhesive framework's applicability.

Findings

New characterization of independence for left-linear rules

Identification of well-behaved classes of rewriting systems

Proven Church-Rosser property and canonical equivalence proofs

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