Symbol different term rewrite systems (Q492918)

A term containing no variables is called a ground term. The ground reachability problem for a term rewrite system (TRS) \(R\) is the problem of deciding for any given ground terms \(s\) and \(t\) whether \(s\) can be transformed to \(t\) by \(R\) while the ground word problem asks whether \(s\) and \(t\) are equivalent with respect to the congruence defined by \(R\). Both problems are encountered in applications of term rewriting, but since they are undecidable for a general \(R\), approximating the ground reducibility relation \(\rightarrow_{R,g}^*\) or the ground equivalence relation \(\leftrightarrow_{R,g}^*\) of \(R\) by some decidable relation has been proposed as a way to settle instances of the two problems. Here the author presents three heuristics for finding ground tree transducers (GTT) (cf. [\textit{M. Dauchet} et al., Inf. Comput. 88, No. 2, 187--201 (1990; Zbl 0705.68067)]) or extended ground term rewriting systems (EGTRS) (cf. [\textit{J. Engelfriet}, Inf. Comput. 152, No. 1, 1--15 (1999; Zbl 1045.68580)]) that yield upper approximations of \(\rightarrow_{R,g}^*\) and \(\leftrightarrow_{R,g}^*\) as well as associated heuristics for using these approximations for showing that two given ground terms are not related by \(\rightarrow_{R,g}^*\) or \(\leftrightarrow_{R,g}^*\). In numerous examples the heuristics are compared with each other or with previously presented methods. The search for such approximations leads to the problem of deciding whether a given GTT is an upper approximation of a given TRS. It is not known whether the question is decidable in its general form, but the author proves its decidability for symbol-different term-rewrite systems (SDTRS), a new class of TRSs introduced here. This main result of the paper entails also the fact that it is decidable whether a given EGTRS is an upper approximation of a given SDTRS. On the other hand, it is undecidable for a linear SDTRS \(R\) and a deterministic bottom-up tree automaton \(\mathcal{A}\) whether the GTT \((\mathcal{A},\mathcal{A})\) is a lower approximation of \(R\). Furthermore, it is shown that the ground word problem and the ground reachability problem are undecidable for SDTRSs.