一句话:提出基于 quantale 的定量与度量重写理论,并将 Newman 引理、Church-Rosser 定理等核心结果推广到该框架。
本文引入定量与度量重写系统的一般理论,其重写关系在 quantale 上丰富,以建模抽象数量。作者分别发展抽象重写系统与基于项的重写系统,并将重写理论中的 Newman 引理、Church-Rosser 定理及临界对式引理等基石结果精细化到度量与定量情形。为避免距离退化与合流性缺失,论文先引入非扩张、线性的项重写系统,再将其推广为新的分级项重写系统;这类系统使定量重写具有模态与上下文敏感特征,从而赋予重写以 coeffectful 行为。该工作为定量重写提供了统一框架,并推广了经典重写理论的核心结论。
We introduce a general theory of quantitative and metric rewriting systems, namely systems with a rewriting relation enriched over quantales modelling abstract quantities. We develop theories of abstract and term-based systems, refining cornerstone results of rewriting theory (such as Newman’s Lemma, Church-Rosser Theorem, and critical pair-like lemmas) to a metric and quantitative setting. To avoid distance trivialisation and lack of confluence issues, we introduce non-expansive, linear term rewriting systems, and then generalise the latter to the novel class of graded term rewriting systems. These systems make quantitative rewriting modal and context-sensitive, this way endowing rewriting with coeffectful behaviours.