非线性重写理论的并发性定理
计算机科学中的逻辑
2021-05-07 v1
摘要
沿非线性规则且针对单态匹配的半推挽（SqPO）重写众所周知可建模顶点与边的融合和克隆，但迄今为止尚无合适的并发性定理的构造。缺乏此类定理反过来使得对此类重写系统的组合推理在很大程度上不可行。我们在本文中针对准拓扑范畴（包含黏附范畴之例）中的非线性 SqPO 重写，且要求匹配为给定范畴的正则单态，发展了合适的并发性定理。我们的构造在计算规则复合时揭示了一种有趣的“反向传播效应”。此外，我们导出了 rm-黏附范畴中非线性双推挽（DPO）重写的并发性定理。我们的结果将非线性 SqPO 和 DPO 语义向并发性、规则代数和迹理论所提供的丰富静态分析技术敞开。
引用
@article{arxiv.2105.02842,
title = {Concurrency Theorems for Non-linear Rewriting Theories},
author = {Nicolas Behr and Russ Harmer and Jean Krivine},
journal= {arXiv preprint arXiv:2105.02842},
year = {2021}
}
备注
19+14 pages, LNCS style; ICGT 2021 conference paper extended version