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

Authors: 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}
  }