A needed narrowing strategy

Citation
S. Antoy et al., A needed narrowing strategy, J ACM, 47(4), 2000, pp. 776-822
Citations number
73
Categorie Soggetti
Computer Science & Engineering
Journal title
Volume
47
Issue
4
Year of publication
2000
Pages
776 - 822
Database
ISI
SICI code
Abstract
The narrowing relation over terms constitutes the basis of the most importa nt operational semantics of languages that integrate functional and logic p rogramming paradigms. It also plays an important role in the definition of some algorithms of unification module equational theories that are defined by confluent term rewriting systems. Due to the inefficiency of simple narr owing, many refined narrowing strategies have been proposed in the last dec ade. This paper presents a new narrowing strategy that is optimal in severa l respects. For this purpose, we propose a notion of a needed narrowing ste p that, for inductively sequential rewrite systems, extends the Huet and Le vy notion of a needed reduction step. We define a strategy, based on this n otion, that computes only needed narrowing steps. Our strategy is sound and complete for a large class of rewrite systems, is optimal with respect to the cost measure that counts the number of distinct steps of a derivation, computes only incomparable and disjoint unifiers, and is efficiently implem ented by unification.