Unique Normalization for Shallow TRS

Guillem Godoy 1 Florent Jacquemard 2
2 DAHU - Verification in databases
LSV - Laboratoire Spécification et Vérification [Cachan], ENS Cachan - École normale supérieure - Cachan, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8643
Abstract : Computation with a term rewrite system (TRS) consists in the application of its rules from a given starting term until a normal form is reached, which is considered the result of the computation. The unique normalization (UN) property for a TRS R states that any starting term can reach at most one normal form when R is used, i.e. that the computation with R is unique. We study the decidability of this property for classes of TRS defined by syntactic restrictions such as linearity (variables can occur only once in each side of the rules), flatness (sides of the rules have height at most one) and shallowness (variables occur at depth at most one in the rules). We prove that UN is decidable in polynomial time for shallow and linear TRS, using tree automata techniques. This result is very near to the limits of decidability, since this property is known undecidable even for very restricted classes like right-ground TRS, flat TRS and also right-flat and linear TRS. We also show that UN is even undecidable for flat and right-linear TRS. The latter result is in contrast with the fact that many other natural properties like reachability, termination, confluence, weak normalization, etc. are decidable for this class of TRS.
Type de document :
Communication dans un congrès
Treinen, Ralf. 20th International Conference on Rewriting Techniques and Applications (RTA), Jun 2009, Brazilia, Brazil. Springer, 5595, pp.63-77, 2009, Lecture Notes in Computer Science. 〈http://www.springerlink.com/content/21x87318813m43x3/〉. 〈10.1007/978-3-642-02348-4_5〉
Liste complète des métadonnées

Littérature citée [19 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00578959
Contributeur : Florent Jacquemard <>
Soumis le : mardi 22 mars 2011 - 17:24:12
Dernière modification le : jeudi 11 janvier 2018 - 06:22:14
Document(s) archivé(s) le : jeudi 23 juin 2011 - 02:56:09

Fichier

UNflat.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Guillem Godoy, Florent Jacquemard. Unique Normalization for Shallow TRS. Treinen, Ralf. 20th International Conference on Rewriting Techniques and Applications (RTA), Jun 2009, Brazilia, Brazil. Springer, 5595, pp.63-77, 2009, Lecture Notes in Computer Science. 〈http://www.springerlink.com/content/21x87318813m43x3/〉. 〈10.1007/978-3-642-02348-4_5〉. 〈inria-00578959〉

Partager

Métriques

Consultations de la notice

262

Téléchargements de fichiers

104