paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Elements of Quantitative Rewriting

定量重写基础
POPL 7(POPL)2023匹配度 2/10 · 该论文属于纯重写理论与形式语义,讨论 quantale 上的定量/度量重写及 Newman 引理等推广,未涉及 LLM/Agent、静态分析、浮点程序分析或贝叶斯程序分析。仅与 PL/形式化方法有间接理论关联,与用户画像的核心交叉方向不匹配。引用 9 inbox
Francesco Gavazzo, Cecilia Di Florio
crossref: 2026-09-10

AI 速览

一句话:提出基于 quantale 的定量与度量重写理论,并将 Newman 引理、Church-Rosser 定理等核心结果推广到该框架。

本文引入定量与度量重写系统的一般理论,其重写关系在 quantale 上丰富,以建模抽象数量。作者分别发展抽象重写系统与基于项的重写系统,并将重写理论中的 Newman 引理、Church-Rosser 定理及临界对式引理等基石结果精细化到度量与定量情形。为避免距离退化与合流性缺失,论文先引入非扩张、线性的项重写系统,再将其推广为新的分级项重写系统;这类系统使定量重写具有模态与上下文敏感特征,从而赋予重写以 coeffectful 行为。该工作为定量重写提供了统一框架,并推广了经典重写理论的核心结论。

问题
如何将经典重写理论中的合流性、Church-Rosser 性质等核心结果推广到带有度量或定量信息的重写系统,同时避免距离退化与合流性失败。
方法
在 quantale 上丰富重写关系,建立抽象与项式重写理论,并提出非扩张线性项重写系统及更一般的分级项重写系统。
评估
以理论证明为主,通过将 Newman 引理、Church-Rosser 定理和临界对式引理等经典结果推广到定量与度量情形来评估该框架。
原文摘要(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 way endowing rewriting with coeffectful behaviours.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@article{paperbot2082,
  title = {Elements of Quantitative Rewriting},
  author = {Francesco Gavazzo and Cecilia Di Florio},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {7},
  number = {POPL},
  year = {2023},
  doi = {10.1145/3571256}
}