A fast algorithm for generating reduced ground rewriting systems from a set of ground equations (Q689111)

The author presents a compilation algorithm from a set of ground equations \(E\) to a reduced set of ground rewriting rules \(R\) equivalent to \(E\). In the worst case it consumes time cost \(O(n\log n)\), where \(n\) is the size of the set \(E\). The algorithm is completely graph-based and uses congruence closure to reduce a graph representation of \(E\) to a minimal form from which the rules \(R\) can be extracted. Moreover, the algorithm can be used to enumerate all reduced sets of rules equivalent to \(E\). The algorithm is based on the algorithm of Downey, Sethi and Tarjan for calculating the congruence closure of a relation \(R\) on an graph \(G= (V,A)\) in worst-time \(O(| A|\log(| A|))\). The main idea sketches as follows. First, given a set of ground equations \(E\) a subterm graph \(G_ E= (V,A)\) is created and the congruence closure \(\Pi\) of the relation \(\Pi_ E\) on the vertices \(V\) induced by \(E\) is computed. Second, for each congruence class a representative vertex is defined and all arcs in \(A\) are repointed to them. Third, determine the congruence closure of the identity relation on \(V\) (representing identical and hence redundant terms) and build the quotient graph by merging the redundant vertices. Finally, generate the relation \(T\) of congruent vertices \((u,v)\) in the quotient graph, where \(v\) is an representative and \(u\) is not. The corresponding relation on the subterms can be interpreted as a ground term rewriting system. An accompanying example illustrates excellent all steps of the algorithm and helps to understand the ideas. The algorithm requires quadratic space. If one reduces the necessary space resources to linear space the time costs reach \(O(n(\log n)^ 2)\).