Higher-Order Lazy Narrowing

Abstract

This chapter discusses our main approach for solving higher-order equations: lazy narrowing. Lazy narrowing is a goal directed method for solving goals in a top-down or outside-in manner. It can be seen as a direct extension of higher-order unification by some narrowing rules. After starting with a general version of lazy narrowing, we develop refinements of lazy narrowing. Some of them also apply to equational reasoning, while the others are tailored towards functional-logic programming. In the former, we only assume terminating rewrite systems; in the latter we will in addition exploit properties of left-linear rewrite rules. Conditional equations are discussed in Section 6.4. Alternative approaches to narrowing are examined in the following chapter.