Unification of Term Schemes - Theory and Applications

Abstract

We present a new approach for solving certain infinite sets of first order unification problems represented by term schemes. Within the framework of second order equational logic solving such scheme unification problems amounts exactly to solving (variable-) restricted unification problems. A method known for solving first order restricted unification problems is generalized to the second order case. Essentially this is achieved by transforming a restricted unification problem into an unrestricted one, solving the latter and retransforming the solutions obtained. The results on second order restricted unification are then used to solve the original problem, namely to decide the solvability of scheme unification problems and - in the positive case - to compute the corresponding most general unifiers. Finally the results are applied to provide sufficient conditions for a property of "repeated unifiability” which in turn is crucial for the analysis of divergence of completion procedures for term rewriting systems. Although the study of divergent completion behaviour was the starting point for the work presented, the results obtained are not only applicable to divergence analysis but may be useful for other applications, too.