A Completion Procedure for Globally Finite Term Rewriting Systems

Abstract

The Knuth-Bendix Algorithm is not able to complete term rewriting systems (TRS) with cyclic rules such as commutativity, associativity etc. A solution for this problem is to separate the cyclic rules from the TRS and incorporate them into the unification algorithm. This requires a unification algorithm for the specific theory. Usually it is very difficult to develop such algorithms, and we therefore discuss another way to solve this problem. We propose an extension of the completion procedure for globally finite TRS. For a globally finite TRS cycles may occur in a reduction chain, but for each term there is only a finite set of reductions. A confluent and globally finite TRS R provides a decision procedure for the equality induced by R: Two terms are equal iff there is a common term in their reduction sets. This extension requires new methods for testing whether a given TRS is confluent and globally finite. For proving that a TRS is globally finite appropriate ordering relations are required, which are usually reflexive. Proving the confluence of a globally finite TRS is more difficult than for nötherian TRS and the set of critical pairs which has to be tested is in general infinite. Therefore a completion procedure with this test may not terminate. Further work has to be done to decrease this critical pair set.