Tetsuo Ida
Institute of Information Sciences and Electronics
University of Tsukuba, Japan

"Higher-order Lazy Narrowing for Left-Linear Fully-Extended Pattern Rewrite Systems"

ABSTRACT:

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, need to reduce the search space of solutions. In this talk 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 used in higher-order functional logic programming.

Back to Talks Page