An algorithm for finding canonical sets of ground rewrite rules in polynomial time (Q4033833)

A Knuth-Bendix type completion procedure is a program that has as input a finite set of axioms (equations) and produces as output a canonical rewriting system equivalent to the input (if any). The termination of such procedure is assured by a reduction ordering included in the input. For the general case, a completion procedure can fail, even a canonical system for the input exists. When the axioms are defined on ground terms, because a total reduction ordering on ground terms exists, a completion procedure terminates and does not fail for any input. The paper presents a completion algorithm for the case of a finite set \(E\) of ground equations on the initial algebra \(T_ \Sigma\) with \(\Sigma\) a finite ranked alphabet, which runs in time \(O(n^ 3)\). The key of the algorithm is the observation that the critical pair rule, from the inference system for unfailing completion of \textit{Dershowitz} and \textit{Bachmair}, never applies for ground systems. So, the efficiency of an algorithm depends only the way how it applies the simplification rules. The algorithm given here, computes the partition of the equivalence defined by \(E\) and, at each step, uses this partition to apply efficiently the simplification rule. The most part of the paper deals with the termination and the correctness of the algorithm.