A Reduction-Preserving Completion for Proving Confluence of Non-Terminating Term Rewriting Systems

TL;DR

This paper introduces a novel method for proving confluence in non-terminating term rewriting systems by using a reduction-preserving completion procedure, which enhances applicability over traditional methods.

Contribution

It presents a new confluence proof technique that preserves reduction relations and works even when systems are not terminating modulo equational theories.

Findings

The method effectively proves confluence in systems with non-terminating rules.

The reduction-preserving completion enhances the applicability of confluence criteria.

It differs from Knuth-Bendix by preserving reduction relations instead of equivalence.

Abstract

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.