A Fast Algorithm for Generating Reduced Ground Rewriting Systems from a Set of Ground Equations

In this paper we give a fast method for generating reduced sets of rewrite rules equivalent to a given set of ground equations. Since reduced sets of ground rewrite rules are in fact canonical, this is an efficient Knuth-Bendix procedure for the ground case. The dominant cost of the algorithm is for congruence closure, so the method runs in O(n log n) time and quadratic space, or in O(n (log n)2) time and linear space, where n is the number of occurrences of symbols in the original set of ground equations E. We also show how our method provides a precise characterization of the (finite) collection of all reduced sets of rewrite rules equivalent to a given ground set of equations E, and prove that our algorithm is complete in the sense that it can enumerate every member of this collection. Finally, we show that a modified version of this procedure can produce a reduced ground rewriting system contained in the lexicographic path ordering generated by a given total precedence ordering on the symbols of E , still in a worst-case time of O(n log n).