Concluding Remarks

Abstract

This work was motivated by the idea that higher-order equations can be used in practical systems for equational reasoning and functional-logic programming. Towards this goal we have first examined decidable classes of higher-order unification. We have shown that for many practical purposes, higher-order unification is not only a powerful tool, but also terminates for several classes of terms. The main restriction we need is linearity, which is common in programming. It also explains to some degree why higher-order unification in logic programming [NM88] and higher-order theorem proving [Pau94, AINP90] rarely diverges. Secondly, we have developed a framework for solving higher-order equations by narrowing. For lazy narrowing, we were able to develop many important refinements, such as normalization and eager variable elimination for normalized solutions. Of similar practical importance are the extensions to conditional equations. We have also seen that some approaches such as plain narrowing are not suitable for the higher-order case.