Compositional Confluence Criteria
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 h...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2024-01-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/11045/pdf |
| _version_ | 1827070573400817664 |
|---|---|
| author | Kiraku Shintani Nao Hirokawa |
| author_facet | Kiraku Shintani Nao Hirokawa |
| author_sort | Kiraku Shintani |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-04-25T01:32:44Z |
| format | Article |
| id | doaj.art-c2070ffc2b89408daaa019f58c4d849f |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2025-03-20T00:24:40Z |
| publishDate | 2024-01-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-c2070ffc2b89408daaa019f58c4d849f2024-10-10T07:36:13ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742024-01-01Volume 20, Issue 110.46298/lmcs-20(1:6)202411045Compositional Confluence CriteriaKiraku ShintaniNao HirokawaWe 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.https://lmcs.episciences.org/11045/pdfcomputer science - logic in computer science |
| spellingShingle | Kiraku Shintani Nao Hirokawa Compositional Confluence Criteria Logical Methods in Computer Science computer science - logic in computer science |
| title | Compositional Confluence Criteria |
| title_full | Compositional Confluence Criteria |
| title_fullStr | Compositional Confluence Criteria |
| title_full_unstemmed | Compositional Confluence Criteria |
| title_short | Compositional Confluence Criteria |
| title_sort | compositional confluence criteria |
| topic | computer science - logic in computer science |
| url | https://lmcs.episciences.org/11045/pdf |
| work_keys_str_mv | AT kirakushintani compositionalconfluencecriteria AT naohirokawa compositionalconfluencecriteria |