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.
@InProceedings{shintani_et_al:LIPIcs.FSCD.2022.28, author = {Shintani, Kiraku and Hirokawa, Nao}, title = {{Compositional Confluence Criteria}}, booktitle = {7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)}, pages = {28:1--28:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-233-4}, ISSN = {1868-8969}, year = {2022}, volume = {228}, editor = {Felty, Amy P.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.28}, URN = {urn:nbn:de:0030-drops-163095}, doi = {10.4230/LIPIcs.FSCD.2022.28}, annote = {Keywords: term rewriting, confluence, decreasing diagrams} }
Feedback for Dagstuhl Publishing