Technical Report MPI-I-93-243, Max-Planck-Institut fuer Informatik
Short version in Proc. of the 21st ACM Symposium on Principles of Programming Languages
Narrowing is the operational principle of languages that integrate functional and logic programming. 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 define 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 independent unifiers, and is efficiently implemented by pattern matching.
Available: DVI BibTeX-Entry