Decidability of the confluence of ground term rewriting systems
Résumé
The aim of this paper is to propose a simple algorithm to decide the confluence of ground term rewriting systems. This algorithm is derived from decidability results presented in (1). Here a simple view of the problem and its solution is proposed. Let us recall that a ground term rewriting system is a term rewriting system where each rule is a pair of ground terms, i.e., a pair of terms without variables. Recall the confluence is not decidable for general term rewriting systems, but this paper proves it is for ground term rewriting systems following a conjecture made by Huet and Oppen (3) in their survey. We also sketch a simple algorithm for checking this property. This algorithm is based on tree automata and tree transducers. Here, we regard them as rewriting systems and specialists in automata theory would translate that easily in their language. In the second part of this paper, a new class of tree transducers is introduced : ground tree transducers, GTT in short. In the third part, stability of GTT relation w.r.t inverse, composition, iteration and precongruence closure of union is proved. In the fourth part, each ground term rewriting system is associated with a GTT and the confluence of ground term rewriting system is reduced to the inclusion of GTT relations. Part 5 solves the decision problem by encoding GTT into rational tree languages.