Root-neededness and approximations of neededness


Salvador Lucas


When dealing with reduction strategies for term rewriting systems, needed reduction is only adequate for defining normalizing strategies. However, Middeldorp has shown that root-needed reduction provides a suitable basis for the definition of root-normalizing, normalizing, and infinitary normalizing strategies. Since neededness and root-neededness are undecidable, some notion of approximation is necessary. In this paper, we investigate whether it is possible to approximate root-neededness by using well-known decidable approximations to neededness and sequentiality (such as strong, NV, NVNF, shallow, and growing approximations). We show that NV-sequentiality (hence strong sequentiality, a particular case of NV-sequentiality) is the most general approximation to root-neededness. We also demonstrate that NVNF-sequentiality only approximates root-neededness in terms that have a normal form. Shallow and growing approximations do not approximate root-neededness in general. As a consequence, only NV-sequentiality seems to provide a suitable general basis for the definition of infinitary normalizing strategies.


neededness, root-neededness, sequentiality, strategies, term rewriting.