Unification in an Extensional Lambda Calculus with Ordered Function Sorts and Constant Overloading

Abstract

The introduction of sorts in first-order automatic theorem proving has been accompanied by a considerable gain in computational efficiency via reduced search spaces. This suggests that sort information can be employed in higher-order theorem proving with similar results. This paper develops an order-sorted higher-order calculus suitable for automatic theorem proving applications — by extending the extensional simply typed lambda calculus with a higher-order ordered sort concept and constant overloading — and extends Huet’s well-known techniques for unification in the simply typed lambda calculus to arrive at a complete transformation-based unification algorithm for this sorted calculus. Consideration of an order-sorted logic with functional base sorts and arbitrary term declarations was originally proposed by the second author in a 1991 paper; we give here a corrected calculus which supports constant, rather than arbitrary term, declarations, as well as a corrected unification algorithm, and prove in this setting results corresponding to those claimed in that earlier work.