Abstract

The theorem of Huet and L&eactue;vy stating that for orthogonal rewrite systems (i) every reducible term contains a needed redex and (ii) repeated contraction of needed redexes results in a normal form if the term under consideration has a normal form, forms the basis of all results on optimal normalizing strategies for orthogonal rewrite systems. However, needed redexes are not computable in general.

In the paper we illustrate, based on the framework introduced in [6], how the use of approximations and their associated tree automata results allows one to obtain decidable conditions in a simple and elegant way.

We further show how the very same ideas can be used to improve the dependency pair method of Arts and Giesl for proving termination of rewrite systems automatically. More precisely, we show how approximations and tree automata techniques provide a better estimation of the dependency graph. This graph determines the ordering constraints that have to be solved in order to conclude termination. Furthermore, we present a new estimation of the dependency graph that does not rely on computationally expensive tree automata techniques.

BibTeX Entry

@inproceedings{M-WRS02,
 author    = "Aart Middeldorp",
 title	   = "Approximations for Strategies and Termination",
 booktitle = "Proceedings of the 2nd International Workshop on Reduction
              Strategies in Rewriting and Programming",
 series    = "Electronic Notes in Theoretical Computer Science",
 volume    = "70(6)",
 pages     = "1--20",
 year      = 2002,
 doi       = "10.1016/S1571-0661(04)80598-X"
}