×

Compositional confluence criteria. (English) Zbl 07814914

Summary: 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.

MSC:

68Q42 Grammars and rewriting systems

References:

[1] T. Aoto and Y. Toyama. Persistency of confluence. Journal of Universal Computer Science, 3(11):1134-1147, 1997. doi:10.3217/jucs-003-11-1134. · Zbl 0960.68082 · doi:10.3217/jucs-003-11-1134
[2] T. Aoto and Y. Toyama. A reduction-preserving completion for proving confluence of non-terminating term rewriting systems. Logical Methods in Computer Science, 8, 2012. doi:10. 2168/LMCS-8(1:31)2012. · Zbl 1238.68071 · doi:10.2168/LMCS-8(1:31)2012
[3] T. Aoto, J. Yoshida, and Y. Toyama. Proving confluence of term rewriting systems automatically. In Proc. 20th International Conference on Rewriting Techniques and Applications, volume 5595 of LNCS, pages 93-102, 2009. doi:10.1007/978-3-642-02348-4_7. · Zbl 1242.68125 · doi:10.1007/978-3-642-02348-4_7
[4] F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge University Press, 1998. doi:10.1017/CBO9781139172752. · Zbl 0948.68098 · doi:10.1017/CBO9781139172752
[5] N. Dershowitz. Open. Closed. Open. In Proc. 16th International Conference on Rewriting Techniques and Applications, volume 3467 of LNCS, pages 276-393, 2005. doi:10.1007/ 978-3-540-32033-3_28. · Zbl 1078.68653 · doi:10.1007/978-3-540-32033-3_28
[6] G. Dowek, G. Férey, J.-P. Jouannaud, and J. Liu. Confluence of left-linear higher-order rewrite theories by checking their nested critical pairs. Mathematical Structures in Computer Science, 32(7):898-933, 2022. doi:10.1017/S0960129522000044. · Zbl 1512.68128 · doi:10.1017/S0960129522000044
[7] L. de Moura and N. Bjørner. Z3: An efficient SMT solver. In Proc. 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, volume 4963 of LNCS, pages 337-340, 2008. The website of Z3 is: https://github.com/Z3Prover/z3. doi:10.1007/ 978-3-540-78800-3_24. · doi:10.1007/978-3-540-78800-3_24
[8] E. Eder. Properties of substitutions and unifications. Journal of Symbolic Computation, 1(1):31-46, 1985. doi:10.1016/S0747-7171(85)80027-4. · Zbl 0589.68063 · doi:10.1016/S0747-7171(85)80027-4
[9] B. Felgenhauer, A. Middeldorp, H. Zankl, and V. van Oostrom. Layer systems for proving confluence. ACM Trans. Comput. Logic, 16(2):1-32, 2015. doi:10.1145/2710017. · Zbl 1354.68138 · doi:10.1145/2710017
[10] B. Felgenhauer and V. van Oostrom. Proof orders for decreasing diagrams. In Proc. 24th International Conference on Rewriting Techniques and Applications, volume 21 of LIPIcs, pages 174-189, 2013. doi:10.4230/LIPIcs.RTA.2013.174. · Zbl 1356.03054 · doi:10.4230/LIPIcs.RTA.2013.174
[11] B. Gramlich. Confluence without termination via parallel critical pairs. In Proc. 21st International Colloquium on Trees in Algebra and Programming, volume 1059 of LNCS, pages 211-225, 1996. doi:10.1007/3-540-61064-2_39. · Zbl 1508.68156 · doi:10.1007/3-540-61064-2_39
[12] R. Gutiérrez, M. Vítores, and S. Lucas. Confluence framework: Proving confluence with CONFident. In Proc. 32nd International Symposium on Logic-Based Program Synthesis and Transformation, volume 13474 of LNCS, pages 24-43, 2022. doi:10.1007/978-3-031-16767-6_2. · doi:10.1007/978-3-031-16767-6_2
[13] N. Hirokawa and A. Middeldorp. Decreasing diagrams and relative termination. Journal of Automated Reasoning, 47:481-501, 2011. doi:10.1007/s10817-011-9238-x. · Zbl 1243.68199 · doi:10.1007/s10817-011-9238-x
[14] N. Hirokawa and A. Middeldorp. Commutation via relative termination. In Proc. 2nd Interna-tional Workshop on Confluence, pages 29-34, 2013.
[15] N. Hirokawa, J. Nagele, and A. Middeldorp. Cops and CoCoWeb: Infrastructure for confluence tools. In Proc. 9th International Joint Conference on Automated Reasoning, volume 10900 of LNCS (LNAI), pages 346-353, 2018. The website of COPS is: https://cops.uibk.ac.at/. doi:10.1007/978-3-319-94205-6_23. · doi:10.1007/978-3-319-94205-6_23
[16] N. Hirokawa, J. Nagele, V. van Oostrom, and M. Oyamaguchi. Confluence by critical pair analysis revisited. In Proc. 27th International Conference on Automated Deduction, volume 11716 of LNCS, pages 319-336, 2019. doi:10.1007/978-3-030-29436-6_19. · Zbl 1535.68122 · doi:10.1007/978-3-030-29436-6_19
[17] G. Huet. Confluent reductions: Abstract properties and applications to term rewriting systems. Journal of the ACM, 27:797-821, 1980. doi:10.1145/322217.322230. · Zbl 0458.68007 · doi:10.1145/322217.322230
[18] J.-P. Jouannaud and J. Liu. From diagrammatic confluence to modularity. Theoretical Computer Science, 464:20-34, 2012. doi:10.1016/j.tcs.2012.08.030. · Zbl 1253.68197 · doi:10.1016/j.tcs.2012.08.030
[19] S. Kahrs. Confluence of curried term-rewriting systems. Journal of Symbolic Computation, 19:601-623, 1995. doi:10.1006/jsco.1995.1035. · Zbl 0840.68063 · doi:10.1006/jsco.1995.1035
[20] D.E. Knuth and P.B. Bendix. Simple word problems in universal algebras. In J. Leech, editor, Computational Problems in Abstract Algebra, pages 263-297. Pergamon Press, 1970. doi:10. 1016/B978-0-08-012975-4.50028-X. · Zbl 0188.04902 · doi:10.1016/B978-0-08-012975-4.50028-X
[21] S. Kamin and J.J. Lévy. Two generalizations of the recursive path ordering. Technical report, University of Illinois, 1980. Unpublished manuscript.
[22] J. Liu and J.-P. Jouannaud. Confluence: The unifying, expressive power of locality. In Specification, Algebra, and Software, volume 8375 of LNCS, pages 337-358, 2014. doi: 10.1007/978-3-642-54624-2_17. · Zbl 1407.68101 · doi:10.1007/978-3-642-54624-2_17
[23] M. H. A. Newman. On theories with a combinatorial definition of “equivalence”. Annals of Mathematics, 43(2):223-243, 1942. doi:10.2307/1968867. · Zbl 0060.12501 · doi:10.2307/1968867
[24] J. Nagele, B. Felgenhauer, and A. Middeldorp. Improving automatic confluence analysis of rewrite systems by redundant rules. In Proc. 26th International Conference on Rewriting Techniques and Applications, volume 36 of LIPIcs, pages 257-268, 2015. doi:10.4230/LIPIcs.RTA.2015.257. · Zbl 1366.68125 · doi:10.4230/LIPIcs.RTA.2015.257
[25] E. Ohlebusch. Advanced Topics in Term Rewriting. Springer, 2002. doi:10.1007/ 978-1-4757-3661-8. · Zbl 0999.68095 · doi:10.1007/978-1-4757-3661-8
[26] S. Okui. Simultaneous critical pairs and Church-Rosser property. In Proc. 9th International Conference on Rewriting Techniques and Applications, volume 1379 of LNCS, pages 2-16, 1998. doi:10.1007/BFb0052357. · doi:10.1007/BFb0052357
[27] M. Oyamaguchi and Y. Ohta. A new parallel closed condition for Church-Rosser of left-linear term rewriting systems. In Proc. 8th International Conference on Rewriting Techniques and Applications, volume 1232 of LNCS, pages 187-201, 1997. doi:10.1007/3-540-62950-5_70. · Zbl 1379.68202 · doi:10.1007/3-540-62950-5_70
[28] M. Oyamaguchi and Y. Ohta. On the Church-Rosser property of left-linear term rewriting systems. IEICE Transactions on Information and Systems, E86-D(1):131-135, 2003.
[29] B. Rosen. Tree-manipulating systems and Church-Rosser theorems. Journal of the ACM, pages 160-187, 1973. doi:10.1145/321738.321750. · Zbl 0267.68013 · doi:10.1145/321738.321750
[30] K. Shintani and N. Hirokawa. CoLL: A confluence tool for left-linear term rewrite systems. In Proc. 25th International Conference on Automated Deduction, volume 9195 of LNCS (LNAI), pages 127-136, 2015. doi:10.1007/978-3-319-21401-6_8. · Zbl 1465.68127 · doi:10.1007/978-3-319-21401-6_8
[31] K. Shintani and N. Hirokawa. Compositional confluence criteria. In Proc. 7th International Conference on Formal Structures for Computation and Deduction, volume 228 of LIPIcs, pages 28:1-28:19, 2022. doi:10.4230/LIPIcs.FSCD.2022.28. · Zbl 1541.68184 · doi:10.4230/LIPIcs.FSCD.2022.28
[32] K. Shintani and N. Hirokawa. Experimental data for compositional confluence criteria, 2023. doi:10.5281/zenodo.8385068. · doi:10.5281/zenodo.8385068
[33] M. Takahashi. λ-calculi with conditional rules. In Proc. International Conference on Typed Lambda Calculi and Applications, volume 664 of LNCS, pages 406-417, 1993. doi:10.1007/ BFb0037121. · Zbl 0806.03014 · doi:10.1007/BFb0037121
[34] Terese. Term Rewriting Systems. Cambridge University Press, 2003. · Zbl 1030.68053
[35] Y. Toyama. On the Church-Rosser property of term rewriting systems. In NTT ECL Technical Report, volume No. 17672. NTT, 1981. Japanese.
[36] Y. Toyama. On the Church-Rosser property for the direct sum of term rewriting systems. Journal of the ACM, 34(1):128-143, 1987. doi:10.1145/7531.7534. · Zbl 1151.68453 · doi:10.1145/7531.7534
[37] Y. Toyama. Commutativity of term rewriting systems. In Programming of Future Generation Computers II, pages 393-407. North-Holland, 1988. · Zbl 0675.68022
[38] Y. Toyama. Confluence criteria based on parallel critical pair closing, March 2017. Presented at the 46th TRS Meeting: https://www.trs.cm.is.nagoya-u.ac.jp/event/46thTRSmeeting/.
[39] V. van Oostrom. Confluence for Abstract and Higher-Order Rewriting. PhD thesis, Vrije Univer-siteit, Amsterdam, 1994.
[40] V. van Oostrom. Developing developments. Theoretical Computer Science, 175(1):159-181, 1997. doi:10.1016/S0304-3975(96)00173-9. · Zbl 0903.68104 · doi:10.1016/S0304-3975(96)00173-9
[41] V. van Oostrom. Confluence by decreasing diagrams, converted. In Proc. 19th International Conference on Rewriting Techniques and Applications, volume 5117 of LNCS, pages 306-320, 2008. doi:10.1007/978-3-540-70590-1_21. · Zbl 1146.68044 · doi:10.1007/978-3-540-70590-1_21
[42] A. Yamada, K. Kusakari, and T. Sakabe. Nagoya termination tool. In Proc. 25th International Conference on Rewriting Techniques and Applications, volume 8560 of LNCS, pages 446-475, 2014. The website of NaTT is: https://www.trs.cm.is.nagoya-u.ac.jp/NaTT/. doi:10.1007/ 978-3-319-08918-8_32. · Zbl 1416.68183 · doi:10.1007/978-3-319-08918-8_32
[43] H. Zankl, B. Felgenhauer, and A. Middeldorp. CSI -a confluence tool. In Proc. 23th International Conference on Automated Deduction, volume 6803 of LNCS (LNAI), pages 499-505, 2011. doi:10.1007/978-3-642-22438-6_38. · Zbl 1341.68199 · doi:10.1007/978-3-642-22438-6_38
[44] H. Zankl, B. Felgenhauer, and A. Middeldorp. Labelings for decreasing diagrams. Journal of Automated Reasoning, 54(2):101-133, 2015. doi:10.1007/s10817-014-9316-y. This work is licensed under the Creative Commons Attribution License. To view a copy of this license, visit https://creativecommons.org/licenses/by/4.0/ or send a letter to Creative Commons, 171 Second St, Suite 300, San Francisco, CA 94105, USA, or Eisenacher Strasse 2, 10777 Berlin, Germany · Zbl 1315.68226 · doi:10.1007/s10817-014-9316-y
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.