{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,1]],"date-time":"2026-05-01T00:41:42Z","timestamp":1777596102132,"version":"3.51.4"},"reference-count":27,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2012,3,28]],"date-time":"2012-03-28T00:00:00Z","timestamp":1332892800000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>We give a method to prove confluence of term rewriting systems that contain\nnon-terminating rewrite rules such as commutativity and associativity. Usually,\nconfluence of term rewriting systems containing such rules is proved by\ntreating them as equational term rewriting systems and considering E-critical\npairs and\/or termination modulo E. In contrast, our method is based solely on\nusual critical pairs and it also (partially) works even if the system is not\nterminating modulo E. We first present confluence criteria for term rewriting\nsystems whose rewrite rules can be partitioned into a terminating part and a\npossibly non-terminating part. We then give a reduction-preserving completion\nprocedure so that the applicability of the criteria is enhanced. In contrast to\nthe well-known Knuth-Bendix completion procedure which preserves the\nequivalence relation of the system, our completion procedure preserves the\nreduction relation of the system, by which confluence of the original system is\ninferred from that of the completed system.<\/jats:p>","DOI":"10.2168\/lmcs-8(1:31)2012","type":"journal-article","created":{"date-parts":[[2012,9,6]],"date-time":"2012-09-06T10:03:11Z","timestamp":1346925791000},"source":"Crossref","is-referenced-by-count":5,"title":["A Reduction-Preserving Completion for Proving Confluence of Non-Terminating Term Rewriting Systems"],"prefix":"10.46298","volume":"Volume 8, Issue 1","author":[{"given":"Takahito","family":"Aoto","sequence":"first","affiliation":[]},{"given":"Yoshihito","family":"Toyama","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2012,3,28]]},"reference":[{"key":"10.2168\/LMCS-8(1:31)2012_DD","unstructured":"T. Aoto. Automated confluence proof by decreasing diagrams based on rule-labelling. In C. Lynch, editor,Proc. of RTA 2010, volume 6 ofLIPIcs, pages 7-16. Schloss Dagstuhl, 2010."},{"key":"10.2168\/LMCS-8(1:31)2012_Rcomp","unstructured":"T. Aoto and Y. Toyama. A reduction-preserving completion for proving confluence of non-terminating term rewriting systems. In M. Schmidt-Schau\u00df, editor,Proc. of RTA 2011, volume 10 ofLIPIcs, pages 91-106. Schloss Dagstuhl, 2011."},{"key":"10.2168\/LMCS-8(1:31)2012_ACP","doi-asserted-by":"crossref","unstructured":"T. Aoto, Y. Yoshida, and Y. Toyama. Proving confluence of term rewriting systems automatically. In R. Treinen, editor,Proc. of RTA 2009, volume 5595 ofLNCS, pages 93-102. Springer-Verlag, 2009.","DOI":"10.1007\/978-3-642-02348-4_7"},{"key":"10.2168\/LMCS-8(1:31)2012_BaaderFandNipkowT:TR","doi-asserted-by":"crossref","unstructured":"F. Baader and T. Nipkow.Term Rewriting and All That. Cambridge University Press, 1998.","DOI":"10.1017\/CBO9781139172752"},{"issue":"2-3","key":"10.2168\/LMCS-8(1:31)2012_BD89","first-page":"173","volume":"67","author":"L. Bachmair and N. Dershowitz","year":"1981","journal-title":"Theoretical Computer Science"},{"issue":"4","key":"10.2168\/LMCS-8(1:31)2012_GOO98","first-page":"992","volume":"39","author":"H. Gomi, M. Oyamaguchi, and Y. Ohta","year":"1998","journal-title":"Transactions of IPSJ"},{"key":"10.2168\/LMCS-8(1:31)2012_Gramlich:PCP","doi-asserted-by":"crossref","unstructured":"B. Gramlich. Confluence without termination via parallel critical pairs. In H. Kirchner, editor,Proc. of CAAP'96, volume 1996 ofLNCS, pages 211-225. Springer-Verlag, 2006.","DOI":"10.1007\/3-540-61064-2_39"},{"issue":"4","key":"10.2168\/LMCS-8(1:31)2012_Hue80","doi-asserted-by":"crossref","first-page":"797","DOI":"10.1145\/322217.322230","volume":"27","author":"G. Huet","year":"1980","journal-title":"Journal of the ACM"},{"issue":"4","key":"10.2168\/LMCS-8(1:31)2012_JK86","doi-asserted-by":"crossref","first-page":"1155","DOI":"10.1137\/0215084","volume":"15","author":"J.-P. Jouannaud and H. Kirchner","year":"1986","journal-title":"SIAM Journal of Computing"},{"key":"10.2168\/LMCS-8(1:31)2012_JKR83","unstructured":"J.-P. Jouannaud, H. Kirchner, and J. L. Remy. Church-Rosser properties of weakly terminating equational term rewriting systems. In A. Bundy, editor,Proc. of 8th IJCAI, pages 909-915, 1983."},{"key":"10.2168\/LMCS-8(1:31)2012_LB77c","unstructured":"D. S. Lankford and A. M. Ballantyne. Decision procedures for simple equational theories with commutative-associative axioms: complete sets of commutative-associative reductions. Technical Report ATP-39, Department of Computer Sciences, University of Texas at Austin, 1977."},{"key":"10.2168\/LMCS-8(1:31)2012_LB77a","unstructured":"D. S. Lankford and A. M. Ballantyne. Decision procedures for simple equational theories with commutative axioms: complete sets of commutative reductions. Technical Report ATP-35, Department of Computer Sciences, University of Texas at Austin, 1977."},{"key":"10.2168\/LMCS-8(1:31)2012_LB77b","unstructured":"D. S. Lankford and A. M. Ballantyne. Decision procedures for simple equational theories with permutative axioms: complete sets of permutative reductions. Technical Report ATP-37, Department of Computer Sciences, University of Texas at Austin, 1977."},{"key":"10.2168\/LMCS-8(1:31)2012_AMrep1991","unstructured":"A. Middeldorp and M. Star\u00c4\u008devi\u00c4\u0087. A rewrite approach to polynomial ideal theory. Report CS-R9160, CWI, Amsterdam, 1991."},{"key":"10.2168\/LMCS-8(1:31)2012_Ohl98","doi-asserted-by":"crossref","unstructured":"E. Ohlebusch. Church-Rosser theorems for abstract reduction modulo an equivalence relation. In T. Nipkow, editor,Proc. of RTA-98, volume 1379 ofLNCS, pages 17-31. Springer-Verlag, 1998.","DOI":"10.1007\/BFb0052358"},{"key":"10.2168\/LMCS-8(1:31)2012_Oku98","doi-asserted-by":"crossref","unstructured":"S. Okui. Simultaneous critical pairs and Church-Rosser property. In T. Nipkow, editor,Proc. of RTA-98, volume 1379 ofLNCS, pages 2-16. Springer-Verlag, 1998.","DOI":"10.1007\/BFb0052357"},{"key":"10.2168\/LMCS-8(1:31)2012_OO97","doi-asserted-by":"crossref","unstructured":"M. Oyamaguchi and Y. Ohta. A new parallel closed condition for Church-Rosser of left-linear TRS's. In H. Comon, editor,Proc. of RTA-97, volume 1232 ofLNCS, pages 187-201. Springer-Verlag, 1997.","DOI":"10.1007\/3-540-62950-5_70"},{"key":"10.2168\/LMCS-8(1:31)2012_OO04","unstructured":"M. Oyamaguchi and Y. Ohta. On the open problems concerning Church-Rosser of left-linear term rewriting systems.IEICE Trans. Information and Systems, E87-D(2):290-298, 2004."},{"issue":"2","key":"10.2168\/LMCS-8(1:31)2012_PS81","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1145\/322248.322251","volume":"28","author":"G. E. Peterson and M. E. Stickel","year":"1981","journal-title":"Journal of the ACM"},{"key":"10.2168\/LMCS-8(1:31)2012_Toy81","unstructured":"Y. Toyama. On the Church-Rosser property of term rewriting systems. Technical Report 17672, NTT ECL, 1981."},{"key":"10.2168\/LMCS-8(1:31)2012_ToyRTA","doi-asserted-by":"crossref","unstructured":"Y. Toyama. Confluent term rewriting systems (invited talk). In J. Giesl, editor,Proc. of RTA 2005, volume 3467 ofLNCS, page 1. Springer-Verlag, 2005. Slides are available from http:\/\/www.nue.riec. tohoku.ac.jp\/user\/toyama\/slides\/toyama-RTA05.pdf.","DOI":"10.1007\/978-3-540-32033-3_1"},{"key":"10.2168\/LMCS-8(1:31)2012_TO94","doi-asserted-by":"crossref","unstructured":"Y. Toyama and M. Oyamaguchi. Church-Rosser property and unique normal form property of non-duplicting term rewriting systems. In N. Dershowitz and N. Lindenstrauss, editors,Proc. of CTRS-94, volume 968 ofLNCS, pages 316-331. Springer-Verlag, 1994.","DOI":"10.1007\/3-540-60381-6_19"},{"key":"10.2168\/LMCS-8(1:31)2012_TO01","unstructured":"Y. Toyama and M. Oyamaguchi. Conditional linearization of non-duplicating term rewriting systems.IEICE Trans. Information and Systems, E84-D(5):439-447, 2001."},{"issue":"2","key":"10.2168\/LMCS-8(1:31)2012_CRbyDD","doi-asserted-by":"crossref","first-page":"259","DOI":"10.1016\/0304-3975(92)00023-K","volume":"126","author":"V. van Oostrom","year":"1994","journal-title":"Theoretical Computer Science"},{"issue":"1","key":"10.2168\/LMCS-8(1:31)2012_Dev","doi-asserted-by":"crossref","first-page":"159","DOI":"10.1016\/S0304-3975(96)00173-9","volume":"175","author":"V. van Oostrom","year":"1997","journal-title":"Theoretical Computer Science"},{"key":"10.2168\/LMCS-8(1:31)2012_converted","doi-asserted-by":"crossref","unstructured":"V. van Oostrom. Confluence by decreasing diagrams: converted. In A. Voronkov, editor,Proc. of RTA 2008, volume 5117 ofLNCS, pages 306-320. Springer-Verlag, 2008.","DOI":"10.1007\/978-3-540-70590-1_21"},{"issue":"2","key":"10.2168\/LMCS-8(1:31)2012_YoshidaJSSST","first-page":"76","volume":"26","author":"J. Yoshida, T. Aoto, and Y. Toyama","year":"2009","journal-title":"Computer Software"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/667\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/667\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T19:53:31Z","timestamp":1681242811000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/667"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,3,28]]},"references-count":27,"URL":"https:\/\/doi.org\/10.2168\/lmcs-8(1:31)2012","relation":{"is-same-as":[{"id-type":"arxiv","id":"1203.5121","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1203.5121","asserted-by":"subject"}],"is-part-of":[{"id-type":"doi","id":"10.4230\/lipics.rta.2011","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"value":"1860-5974","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,3,28]]},"article-number":"667"}}