## Paper: Decidability of the Confluence of Ground Term Rewriting Systems (at LICS 1987)

**Max Dauchet Sophie Tison Thierry Heuillard Pierre Lescanne**

### Abstract

The aim of this paper is to propose a simple algorithm to
decide the confluence of ground term rewriting systems. 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. The confluence is the property that
asserts that u ←^{*} s →^{*} v implies there exists
a term t such that u →^{*} t ←^{*} v. For example,
the reader may try to prove that the system {f(f(a)) → f(a), g(f(a))
→ f(g(f(a))), g(f(a)) → f(f(a))} is confluent and that the system {a → f(a,b), f(a,b)
→ f(b,a)} is not. It is well known 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 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.

### BibTeX

@InProceedings{DauchetTisonHeuilla-DecidabilityoftheCo, author = {Max Dauchet and Sophie Tison and Thierry Heuillard and Pierre Lescanne}, title = {Decidability of the Confluence of Ground Term Rewriting Systems}, booktitle = {Proceedings of the Second Annual IEEE Symposium on Logic in Computer Science (LICS 1987)}, year = {1987}, month = {June}, pages = {353--359 }, location = {Ithaca, NY, USA}, publisher = {IEEE Computer Society Press} }