10.4230/LIPICS.RTA.2011.91
Aoto, Takahito
Takahito
Aoto
Toyama, Yoshihito
Yoshihito
Toyama
A Reduction-Preserving Completion for Proving Confluence of Non-Terminating Term Rewriting Systems
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
2011
Article
Confluence
Completion
Equational Term Rewriting Systems
Confluence Modulo Equations
Schmidt-Schauß, Manfred
Manfred
Schmidt-Schauß
2011
2011-04-26
2011-04-26
2011-04-26
en
urn:nbn:de:0030-drops-31105
10.4230/LIPIcs.RTA.2011
978-3-939897-30-9
1868-8969
10.4230/LIPIcs.RTA.2011
LIPIcs, Volume 10, RTA 2011
22nd International Conference on Rewriting Techniques and Applications (RTA'11)
2013
10
12
91
106
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Schmidt-Schauß, Manfred
Manfred
Schmidt-Schauß
1868-8969
Leibniz International Proceedings in Informatics (LIPIcs)
2011
10
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
16 pages
630435 bytes
application/pdf
Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license
info:eu-repo/semantics/openAccess
We give a method to prove confluence of term rewriting systems that contain non-terminating rewrite rules such as commutativity and associativity. Usually, confluence of term rewriting systems containing such rules is proved by treating them as equational term rewriting systems and considering E-critical pairs and/or termination modulo E. In contrast, our method is based solely on usual critical pairs and usual termination. We first present confluence criteria for term rewriting systems whose rewrite rules can be partitioned into terminating part and possibly non-terminating part. We then give a reduction-preserving completion procedure so that the applicability of the criteria is enhanced. In contrast to the well-known Knuth-Bendix completion procedure which preserves the equivalence relation of the system, our completion procedure preserves the reduction relation of the system, by which confluence of the original system is inferred from that of the completed system.
LIPIcs, Vol. 10, 22nd International Conference on Rewriting Techniques and Applications (RTA'11), pages 91-106