04157892

j

04157892 Dauchet, Max Heuillard, Thierry Lescanne, Pierre Tison, Sophie Decidability of the confluence of finite ground term rewrite systems and of other related term rewrite systems. Inf. Comput. 88, No.2, 187-201 (1990). 1990 Elsevier Science (Academic Press), San Diego, CA EN confluence infinite ground term rewrite systems tree automata tree transducers

doi:10.1016/0890-5401(90)90015-A

Summary: We propose an algorithm to decide the confluence of finite ground term rewrite systems. Actually a more general class of possibly infinite ground term rewrite systems is studied. It is well known that the confluence is not decidable for general term rewrite systems, but we prove it is for ground term rewrite systems following a conjecture made by Huet and Oppen in their survey. The result is also applied to the confluence of left-linear and right-ground term rewrite systems. We also sketch an algorithm for checking this property. This algorithm is based on tree automata and tree transducers. Here, we regard them as rewrite systems and specialists in automata theory would translate that easily in their language.