Decidability of the confluence of ground term rewriting systems

Abstract : 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.
Type de document :
[Research Report] RR-0675, INRIA. 1987
Liste complète des métadonnées
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 19:30:43
Dernière modification le : samedi 17 septembre 2016 - 01:06:55
Document(s) archivé(s) le : vendredi 13 mai 2011 - 16:04:05



  • HAL Id : inria-00075878, version 1



Pierre Lescanne, Thierry Heuillard, Max Dauchet, Sophie Tison. Decidability of the confluence of ground term rewriting systems. [Research Report] RR-0675, INRIA. 1987. 〈inria-00075878〉



Consultations de la notice


Téléchargements de fichiers