Abstract

The following theorem of Huet and Lévy forms the basis of all results on optimal reduction strategies for orthogonal term rewriting systems: every term not in normal form contains a needed redex and repeated contraction of needed redexes results in the normal form, if the term under consideration has one. We generalize this theorem to computations to root-stable form and we argue that the resulting notion of root-neededness is more fundamental than (other variants of) neededness when it comes to infinitary normalization.

BibTeX Entry

@inproceedings{M-POPL97,
 author      = "Aart Middeldorp",
 title       = "Call by Need Computations to Root-Stable Form",
 booktitle   = "Proceedings of the 24th Annual ACM SIGPLAN-SIGACT Symposium
                on Principles of Programming Languages",
 publisher   = "ACM Press",
 pages       = "94--105",
 year        = 1997,
 doi         = "10.1145/263699.263711"
}