Decidable Call by Need Computations in Term Rewriting
Résumé
The following theorem of Huet and Lévy [HL79] forms the basis of all results on optimal normalizing reduction strategies for orthogonal term rewriting systems (TRSs): every reducible term contains a needed redex, i.e., a redex which is contracted in every rewrite sequence to normal form, and repeated contraction of needed redexes results in a normal form, if the term under consideration has a normal form. Unfortunately, needed redexes are not computable in general. Hence, in order to obtain a computable optimal reduction strategy, we are left to find (1) decidable approximations of neededness and (2) decidable properties of TRSs which ensure that every reducible term has a needed redex identified by (1). Starting with the seminal work of Huet and Lévy [HL79] on strong sequentiality, these issues have been extensively investigated in the literature[C95,J96,JS95,KM91,NST95,O93,T92]. In all these works Huet and Lévy's notions of index, omega-reduction, and sequentiality figure prominently. We present an approach to decidable call by need computations to normal form in which issues (1) and (2) above are addressed directly. Besides facilitating understanding this enables us to cover much larger classes of TRSs. For instance, an easy consequence of our work is that every orthogonal right-ground TRS admits a computable call by need strategy whereas none of the sequentiality-based approaches cover all such TRSs. Our approach is based on the easy but fundamental observation that needed redexes are uniform but not independent of other redexes in the same term. Uniformity means that only the position of a redex in a term counts for determining neededness.