2026-07-22T00:07:40Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:16309 2024-03-06T10:57:12Z ddc:004 open_access

Compositional Confluence Criteria Shintani, Kiraku Hirokawa, Nao term rewriting confluence decreasing diagrams 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. In addition to them, we prove that Toyama’s parallel closedness result based on parallel critical pairs subsumes his almost parallel closedness theorem. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Kiraku Shintani and Nao Hirokawa 2022 Is Part Of LIPIcs, Volume 228, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2022.28 urn:nbn:de:0030-drops-163095 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.28 eng https://creativecommons.org/licenses/by/4.0/legalcode