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
翻译:计算设备执行的两个连续步骤何时可被视为(因果)独立的?这是并发与分布式系统中的一个关键问题,因为独立性意味着这些步骤可以按任意顺序执行,并可能并行化。识别仅因独立步骤而不同的重写序列的等价关系,是许多形式主义并发理论的核心。我们在粘合范畴的一般设定下,基于双推出重写方法研究该问题。尽管针对可消耗、保留和生成实体的线性规则已存在完善的理论,本文聚焦于可能"合并"状态部分的左线性规则。这看似是最小但技术上困难的扩展,因为在左线性情况下,线性规则中用于推导并发理论发展所必需性质的独立性标准特征不再成立。本文深入研究了左线性规则的独立性概念:提出了独立性的新特征描述,识别了行为良好的左线性重写系统类别,并提供了包括Church-Rosser性质与并发计算规范等价证明存在性在内的若干基础结果。这些成果显著扩展了可在粘合框架中建模的形式主义类别。