A Combinator-based Order-sorted Higher-order Unification Algorithm

Abstract

This paper develops a sound and complete transformation-based algorithm for unification in an extensional order-sorted combinatory logic supporting constant overloading and a higher-order sort concept. Appropriate notions of order-sorted weak equality and extensionality - reflecting order-sorted βη-equality in the corresponding lambda calculus given by Johann and Kohlhase - are defined, and the typed combinator-based higher-order unification techniques of Dougherty are modified to accommodate unification with respect to the theory they generate. The algorithm presented here can thus be viewed as a combinatory logic counterpart to that of Johann and Kohlhase, as well as a refinement of that of Dougherty, and provides evidence that combinatory logic is well-suited to serve as a framework for incorporating order-sorted higher-order reasoning into deduction systems aiming to capitalize on both the expressiveness of extensional higher-order logic and the efficiency of order-sorted calculi.