Skip to Main content Skip to Navigation
New interface
Conference papers

Unique Normalization for Shallow TRS

Guillem Godoy 1 Florent Jacquemard 2 
2 DAHU - Verification in databases
LSV - Laboratoire Spécification et Vérification [Cachan], Inria Saclay - Ile de France
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 metadata

Cited literature [19 references]  Display  Hide  Download
Contributor : Florent Jacquemard Connect in order to contact the contributor
Submitted on : Tuesday, March 22, 2011 - 5:24:12 PM
Last modification on : Thursday, January 20, 2022 - 4:13:06 PM
Long-term archiving on: : Thursday, June 23, 2011 - 2:56:09 AM


Files produced by the author(s)



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⟩



Record views


Files downloads