Using First-Order Narrowing To Solve Goals Of Higher-Order Patterns


In this paper we propose a modular algorithm for higher-order pattern unification modulo a first-order term rewrite system. The modular algorithm is parameterized by a first-order narrowing algorithm and thus may lay a foundation for combining first-order functional logic programming and higher-order logic programming based on higher-order patterns. The abstract formulation of the modular algorithm clearly shows where else it can be applied.

The paper is here.


Zhenyu Qian