论文标题
定量和度量重写：摘要，非专注和分级系统
Quantitative and Metric Rewriting: Abstract, Non-Expansive, and Graded Systems
论文作者
论文摘要
我们介绍了定量和度量重写系统的一般理论，即具有重写关系的系统富含数量建模的抽象数量。我们开发了基于抽象和术语的系统的理论，改进了重写理论的基石结果（例如纽曼的引理，教堂 - 劳动定理和类似关键的成对的诱饵）。为了避免距离琐碎的琐事和缺乏汇合问题，我们引入了非强度的线性术语重写系统，然后将后者推广到新颖的分级术语重写系统。这些系统使定量重写模态和上下文敏感，这是通过系数行为赋予重写的。我们将开发的理论应用于来自定量代数，编程语言语义和算法领域的几个示例。
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 endowing rewriting with coeffectful behaviours. We apply the theory developed to several examples coming from the fields of quantitative algebras, programming language semantics, and algorithms.
