Aoto, Takahito and Toyama, Yoshihito - A Reduction-Preserving Completion for Proving Confluence of Non-Terminating Term Rewriting Systems

lmcs:667 - Logical Methods in Computer Science, March 28, 2012, Volume 8, Issue 1
A Reduction-Preserving Completion for Proving Confluence of Non-Terminating Term Rewriting Systems

Authors: Aoto, Takahito and Toyama, Yoshihito

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 it also (partially) works even if the system is not terminating modulo E. We first present confluence 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 confluence of the original system is inferred from that of the completed system.


Source : oai:arXiv.org:1203.5121
DOI : 10.2168/LMCS-8(1:31)2012
Volume: Volume 8, Issue 1
Published on: March 28, 2012
Submitted on: October 28, 2011
Keywords: Computer Science - Logic in Computer Science,D.3.1, F.3.1, F.4.2, I.2.2


Share

Consultation statistics

This page has been seen 62 times.
This article's PDF has been downloaded 33 times.