Higher-Order Equational Logic Programming
Higher-order equational logic programming is a paradigm which combines
first-order equational and higher-order logic programming, where
higher-order logic programming is based on a subclass of simply typed
lambda terms, called higher-order patterns. Central to the notion of
higher-order equational logic programming is the so-called
higher-order equational unification. This paper extends several
important classes of first-order equational unification algorithms to
the higher-order setting: only problems of the extensions are
discussed and first-order equational unifications are viewed as black
boxes whenever possible.
We first extend narrowing and show that the completeness of many
higher-order narrowing strategies reduces to that of their underlying
first-order counterparts. Then we propose an algorithm for
higher-order equational unification of free higher-order patterns in
an arbitrary equational theory. Finally a general approach to extend
first-order unification combination algorithms is sketched informally.
The termination property of the above higher-order extensions is
considered in a uniform way.
The paper is here.