Refinements of lazy narrowing for left-linear fully-extended pattern rewrite systems
Mircea Marin, Taro Suzuki, 哲雄 井田, 筑波大学電子・情報工学系 · 2001
Lazy narrowing is a general E-unification procedure for equational theories presented by confluent term rewriting systems. It has been deeply studied in the first order case and various higher-order extensions have been proposed in an attempt to improve its expressive power. Such extensions suffer from huge search space in guessing the solutions of variables of functional type. For practical purposes, the need to reduce the search space of solutions is of paramount importance. In this paper we introduce HOLN, a higher-order lazy narrowing calculus for E-unification in theories presented by pattern rewrite systems. The calculus is designed to deal with both oriented and unoriented equations, and keeps track of the variables which are to be bound to normalized solutions. We discuss the operating principle of HOLN, its main properties, and propose refinements to reduce its search space for solutions. Our refinements are defined for classes of left-linear fully-extended pattern rewrite systems which are widely used in higher-order functional logic programming.