The Knuth-Bendix Completion Procedure and Thue Systems

Abstract

The Knuth-Bendix completion procedure for term rewriting systems in many cases provides a decision procedure for equational theories and has been found to have many applications in various areas. We discuss the application of the Knuth-Bendix procedure to Thue systems. We use the notion of a reduced Thue system and show that for every Church-Rosser Thue system, there is a unique reduced Church-Rosser Thue system equivalent to it. Furthermore, the Knuth-Bendix completion procedure, when applied to a Thue system T, always produces the finite reduced Church-Rosser Thue system equivalent to T whenever such a system exists. Similar results can also be proved for almost-confluent Thue systems. Using properties of reduced Church-Rosser systems, we develop conditions under which a class of special Thue systems have equivalent finite Church-Rosser systems. In addition, we show that the completion procedure always terminates on finite parenthesized Thue systems, from which the termination of the completion procedure over ground-term-rewriting systems can be shown immediately. From the results discussed in this paper, we also obtain the termination of the Knuth-Bendix completion procedure for commutative Thue systems (commutative monoids) as a simple corollary.