Skip to Main content Skip to Navigation
New interface
Reports (Research report)

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.
Document type :
Reports (Research report)
Complete list of metadata
Contributor : Rapport De Recherche Inria Connect in order to contact the contributor
Submitted on : Wednesday, May 24, 2006 - 7:30:43 PM
Last modification on : Wednesday, October 26, 2022 - 8:16:34 AM
Long-term archiving on: : Friday, May 13, 2011 - 4:04:05 PM


  • 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⟩



Record views


Files downloads