|
Abstract : |
Abstract: The narrowing relation over terms constitutes the basis of the most important operational semantics of languages that integrate functional and logic programming paradigms. It also plays an important role in the denition of some algorithms of unication modulo equational theories which are dened by con uent term rewriting systems. Due to the ineciency of simple narrowing, many rened narrowing strategies have been proposed in the last decade. This paper presents a new narrowing strategy which is optimal in several respects. For this purpose we propose a notion of a needed narrowing step that, for inductively sequential rewrite systems, extends the Huet and Levy notion of a needed reduction step. We dene a strategy, based on this notion, that computes only needed narrowing steps. Our strategy is sound and complete for a large class of rewrite systems, is optimal w.r.t. the cost measure that counts the number of distinct steps of a derivation, computes only incomparable and disjoint uniers, and is eciently implemented by uni cation., |
