Call by Need Computations to Root-Stable Form

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.