TY - JOUR

T1 - A reduction-preserving completion for proving confluence of non-terminating term rewriting systems

AU - Aoto, Takahito

AU - Toyama, Yoshihito

PY - 2012

Y1 - 2012

N2 - We give a method to prove con uence of term rewriting systems that contain non-terminating rewrite rules such as commutativity and associativity. Usually, con uence 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 it also (partially) works even if the system is not terminating modulo E. We first present con uence criteria for term rewriting systems whose rewrite rules can be partitioned into a terminating part and a 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 con uence of the original system is inferred from that of the completed system.

AB - We give a method to prove con uence of term rewriting systems that contain non-terminating rewrite rules such as commutativity and associativity. Usually, con uence 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 it also (partially) works even if the system is not terminating modulo E. We first present con uence criteria for term rewriting systems whose rewrite rules can be partitioned into a terminating part and a 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 con uence of the original system is inferred from that of the completed system.

KW - Completion

KW - Confluence

KW - Confluence Mod-flulo Equations

KW - Equational Term Rewriting Systems

UR - http://www.scopus.com/inward/record.url?scp=84859956721&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84859956721&partnerID=8YFLogxK

U2 - 10.2168/LMCS-8(1:31)2012

DO - 10.2168/LMCS-8(1:31)2012

M3 - Article

AN - SCOPUS:84859956721

VL - 8

JO - Logical Methods in Computer Science

JF - Logical Methods in Computer Science

SN - 1860-5974

IS - 1

ER -