"Root-neededness and approximations of neededness"
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.
I. Durand and A. Middeldorp. Decidable Call by Need Computations in Term Rewriting (Extended Abstract). In Proc. of CADE'97, LNAI 1249:4-18, Springer-Verlag, Berlin, 1997.
F. Jacquemard. Decidable Approximations to Term Rewriting Systems. In Proc. of RTA'96, LNCSD 968:247-261, Springer-Verlag, Berlin, 1996.
A Middeldorp. Call by Need Computations to Root-Stable Form. In Proc. of POPL'97, ACM Press, 1997.