Quantitative and Metric Rewriting: Abstract, Non-Expansive, and Graded Systems
Abstract
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.
Keywords
Cite
@article{arxiv.2206.13610,
title = {Quantitative and Metric Rewriting: Abstract, Non-Expansive, and Graded Systems},
author = {Francesco Gavazzo and Cecilia Di Florio},
journal= {arXiv preprint arXiv:2206.13610},
year = {2022}
}