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.
Document type :
Conference papers
Complete list of metadatas

Cited literature [19 references]  Display  Hide  Download

https://hal.inria.fr/inria-00578959
Contributor : Florent Jacquemard <>
Submitted on : Tuesday, March 22, 2011 - 5:24:12 PM
Last modification on : Thursday, February 7, 2019 - 5:29:23 PM
Long-term archiving on : Thursday, June 23, 2011 - 2:56:09 AM

File

UNflat.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Guillem Godoy, Florent Jacquemard. Unique Normalization for Shallow TRS. 20th International Conference on Rewriting Techniques and Applications (RTA), Jun 2009, Brazilia, Brazil. pp.63-77, ⟨10.1007/978-3-642-02348-4_5⟩. ⟨inria-00578959⟩

Share

Metrics

Record views

298

Files downloads

176