The Church-Rosser property for ground term-rewriting systems is decidable (Q1100890)

The paper proves the decidabilty of the Church-Rosser property (i.e. confluency) for any ground term-rewriting system (i.e. term rewriting system with rules not containing any variables), even if the system is not noetherian (i.e. it may contain infinite chains of reductions). While the noetherian property has been known to be decidable for ground term- rewriting systems, the problem solved in this paper has been an open problem for several years. Several technical notions are introduced for the purpose of the proof: For the analysis of reduction sequences, pattern trees and stable pattern trees are defined and their properties studied. A restricted notion of confluency, the k-restricted confluency, is considered, for which it is shown that the confluency problem can be reduced to the k-restricted confluency problem for some \(k>0\). The proof of the decidability of the confluency problem for ground term-rewriting systems is concluded by reducing k-restricted confluency to the equivalence problem for nondeterministic root-to-root automata (already shown to be decidable by Thatcher).