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]
< Réduire
Linguistic signs, grammar and meaning: computational logic for natural language [SIGNES]
Laboratoire Bordelais de Recherche en Informatique [LaBRI]
Langue
en
Communication dans un congrès
Ce document a été publié dans
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
Résumé en anglais
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 ...Lire la suite >
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.< Réduire
Mots clés en anglais
term rewriting
call-by-need computations
Origine
Importé de halUnités de recherche