Decidable call-by-need computations in term rewriting |
| |
Authors: | Irne Durand Aart Middeldorp |
| |
Affiliation: | aLaboratoire Bordelais de Recherche en Informatique, Université de Bordeaux I, 33405 Talence Cedex, France;bInstitute of Computer Science, University of Innsbruck, 6020 Innsbruck, Austria |
| |
Abstract: | The theorem of Huet and Lévy stating that for orthogonal rewrite systems (i) every reducible term contains a needed redex and (ii) repeated contraction of needed redexes results in a normal form if the term under consideration has a normal form, forms the basis of all results on optimal normalizing strategies for orthogonal rewrite systems. However, needed redexes are not computable in general. In the paper we show how the use of approximations and elementary tree automata techniques allows one to obtain decidable conditions in a simple and elegant way. Surprisingly, by avoiding complicated concepts like index and sequentiality we are able to cover much larger classes of rewrite systems. We also study modularity aspects of the classes in our hierarchy. It turns out that none of the classes is preserved under signature extension. By imposing various conditions we recover the preservation under signature extension. By imposing some more conditions we are able to strengthen the signature extension results to modularity for disjoint and constructor-sharing combinations. |
| |
Keywords: | Term rewriting Strategies Call-by-need Tree automata |
本文献已被 ScienceDirect 等数据库收录! |
|