paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Compositional Confluence Criteria

组合式合流性判据
LMCS vol.Volume 20, Issue 12024匹配度 1/10 · 该论文研究项重写系统的合流性判据(递减图、规则标记、关键对系统等),属于纯重写理论与证明工程,与用户关注的静态分析/形式化验证和 LLM 交叉、浮点程序分析、贝叶斯程序分析等方向几乎没有交集。引用 2 inbox
Kiraku Shintani, Nao Hirokawa
crossref: 2026-09-10

AI 速览

一句话:将基于递减图的合流性判据推广为可组合形式,并给出消去无关重写规则的约简方法。

本文研究项重写系统中合流性判据的组合问题。作者把基于递减图(decreasing diagrams)的合流性判据推广为可与其他判据组合的形式,使不同判据可以在同一证明中协同使用。为展示该框架,他们将正交性、规则标记(rule labeling)和临界对系统(critical pair systems)这三类经典判据改写为可组合形式;并说明如何利用这种判据设计约简方法,删除对合流性分析不必要的重写规则。此外,作者证明基于并行临界对的 Toyama 并行封闭性结果蕴含其几乎并行封闭性定理。

问题
如何将基于递减图的合流性判据推广到可与其他合流判据组合的形式,并用于项重写系统的合流性分析。
方法
以递减图为基础定义可组合的合流判据,并将正交性、规则标记与临界对系统等判据改写为可组合形式,进而提出删除无关重写规则的约简方法。
评估
通过将这些判据重铸为可组合形式、给出规则约简应用,并证明 Toyama 基于并行临界对的并行封闭性结果蕴含几乎并行封闭性定理来展示方法。
原文摘要(Abstract)

We show how confluence criteria based on decreasing diagrams are generalized to ones composable with other criteria. For demonstration of the method, the confluence criteria of orthogonality, rule labeling, and critical pair systems for term rewriting are recast into composable forms. We also show how such a criterion can be used for a reduction method that removes rewrite rules unnecessary for confluence analysis. In addition to them, we prove that Toyama's parallel closedness result based on parallel critical pairs subsumes his almost parallel closedness theorem.

链接与引用

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

BibTeX
@article{paperbot2785,
  title = {Compositional Confluence Criteria},
  author = {Kiraku Shintani and Nao Hirokawa},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 20, Issue 1},
  year = {2024},
  doi = {10.46298/lmcs-20(1:6)2024}
}