Complete Polymorphic Order-Sorted Unification

Unification in a polymorphic order-sorted signature differs substantially from the non-polymorphic order-sorted unification. For the polymorphic order-sorted unification we need a type unification algorithm instead of a simple infimum function as in the non-polymorphic case. In this paper we solve the type unification problem, design a type unification algorithm and derive from this a polymorphic order-sorted unification algorithm. 1 Introduction The theory of order-sorted algebras has already been developed for OBJ [3, 4, 5]. In [9] we extend this theory by introducing parametric polymorphism (like it was done for sml [8, 2]) and present a corresponding programming language, we called OBJ--P. Similar approaches are presented in [10, 11, 14, 1]. For logic programming languages which are based on a theory of order-sorted algebras, we need a unification algorithm for order-sorted terms. The non-polymorphic ordersorted unification problem is considered in [6], [12], and [16]. In this pap..