Kiraku Shintani ; Nao Hirokawa - Compositional Confluence Criteria

lmcs:11045 - Logical Methods in Computer Science, January 23, 2024, Volume 20, Issue 1 - https://doi.org/10.46298/lmcs-20(1:6)2024
Compositional Confluence CriteriaArticle

Authors: Kiraku Shintani ; Nao Hirokawa

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.


Volume: Volume 20, Issue 1
Secondary volumes: Selected Papers of the 7th International Conference on Formal Structures and Deduction (FSCD 2022)
Published on: January 23, 2024
Imported on: March 8, 2023
Keywords: Computer Science - Logic in Computer Science

2 Documents citing this article

Consultation statistics

This page has been seen 3267 times.
This article's PDF has been downloaded 822 times.