Higher-Order Narrowing

Higher-order narrowing is a general method for higher-order equational reasoning and serves for instance as the foundation for the integration of functional and logic programming. We present several renements of higher-order lazy narrowing for convergent (terminating and con uent) term rewrite systems and their application to program transformation. The improvements of narrowing include a restriction of narrowing at variables, generalizing the rst-order case. Furthermore, functional evaluation via normalization is shown to be complete and a partial answer to the eager variable elimination problem is presented.

• Type: Conference
• Year: 1994
• Where: LICS
• Authors: Christian Prehofer
• Keywords: Automated Reasoning, Eager Variable Elimination, LICS 1994, Narrowing, Term Rewrite Systems