Root-neededness and approximations of neededness
Author
Salvador Lucas
Abstract
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.
Keywords
neededness, root-neededness, sequentiality, strategies, term rewriting.