Higher-Order Narrowing with Definitional Trees
Michael Hanus, Christian Prehofer
Functional logic languages with a sound and complete
operational semantics are mainly based on an inference rule
called narrowing. Narrowing extends functional evaluation
by goal solving capabilities as in logic programming. Due to
the huge search space of simple narrowing, steadily improved
narrowing strategies have been developed in the past. Needed
narrowing is currently the best narrowing strategy for
first-order functional logic programs due to its optimality
properties w.r.t. the length of derivations and the number
of computed solutions. In this paper, we extend the needed
narrowing strategy to higher-order functions and lambda-terms
as data structures. By the use of definitional trees,
our strategy computes only incomparable solutions. Thus,
it is the first calculus for higher-order functional logic
programming which provides for such an optimality result. Since
we allow higher-order logical variables denoting lambda-terms,
applications go beyond current functional and logic programming
languages.