arXivDaily arXiv每日学术速递 周一至周五更新
arXiv 2407.06181cs.LOmath.CTmath.LO
收藏

粘合范畴中的左线性重写

Left-Linear Rewriting in Adhesive Categories

Paolo Baldan, Davide Castelnovo, Andrea Corradini, Fabio Gadducci

AI总结:

本文研究粘合范畴中左线性重写规则的因果独立性问题,提出新的独立性刻画,识别良态重写系统类别,并证明Church-Rosser性质及规范等价证明的存在性,扩展了粘合框架可建模的形式化体系范围。

摘要:

计算设备执行的两个顺序步骤何时可以被视为(因果)独立?这是并发与分布式系统中的一个重要问题,因为独立意味着它们可以以任意顺序执行,并且可能并行执行。识别仅因独立步骤而不同的重写序列的等价关系,是许多形式化体系并发理论的核心。我们在粘合范畴这一一般设定下,采用双推出方法研究重写中的这一问题。虽然对于可以消耗、保留和生成实体的线性规则已有成熟理论,但本文关注的是左线性规则,这类规则还可以“合并”状态的某些部分。这看似是一个极小的增强,但在技术上却相当困难,因为在线性情形下能够推导出若干性质的标准独立性刻画——这些性质对于并发理论的发展至关重要——在左线性情形下不再成立。本文对左线性规则的独立性概念进行了深入研究:引入了一种新的独立性刻画,识别了行为良好的左线性重写系统类别,并提供了一些基础性结果,包括Church-Rosser性质以及并发计算规范等价证明的存在性。这些结果恰当地扩展了可以在粘合框架中建模的形式化体系类别。

英文摘要:

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

机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。

↑