Decidable Call by Need Computations in Term Rewriting
DURAND, Irène
Linguistic signs, grammar and meaning: computational logic for natural language [SIGNES]
Laboratoire Bordelais de Recherche en Informatique [LaBRI]
Linguistic signs, grammar and meaning: computational logic for natural language [SIGNES]
Laboratoire Bordelais de Recherche en Informatique [LaBRI]
DURAND, Irène
Linguistic signs, grammar and meaning: computational logic for natural language [SIGNES]
Laboratoire Bordelais de Recherche en Informatique [LaBRI]
< Reduce
Linguistic signs, grammar and meaning: computational logic for natural language [SIGNES]
Laboratoire Bordelais de Recherche en Informatique [LaBRI]
Language
en
Communication dans un congrès
This item was published in
Proceedings of the 14th International Conference on Automated Deduction, Proceedings of the 14th International Conference on Automated Deduction, 14th International Conference on Automated Deduction, 1997. 1997 n° 1249, p. 4--18
Springer-Verlag
English Abstract
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 ...Read more >
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.Read less <
English Keywords
term rewriting
call-by-need computations
Origin
Hal imported