Higher-order narrowing

Introduces several approaches for solving higher-order equational problems by higher-order narrowing, and gives some completeness results. The results apply to higher-order functional-logic programming languages and to higher-order unification modulo a higher-order equational theory. We lift the general notion of first-order narrowing to so-called higher-order patterns and argue that the full higher-order case is problematic. Integrating narrowing into unification (called `lazy narrowing´) can avoid these problems and can be adapted to the full higher-order case. For the second-order case, we develop a version where the needed second-order unification remains decidable. Finally, we discuss a method that combines both approaches by using narrowing on higher-order patterns with full higher-order constraints