尚未生成 AI 速览(可能缺少 API key 或等待下次运行补跑)。
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 原文 ·
@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}
}