Higher-Order Equational Logic Programming
Abstract:
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.
FTP: ftp.uni-bremen.de:/pub/ZKW/INFORM/qian/hoelp.ps.gz
For a hard copy send a message to Zhenyu Qian.