Semantics of order-sorted specifications

AbstractOrder-sorted specifications (i.e. many-sorted specifications with subsort relations) have been proved to be a useful tool for the description of partially defined functions and error handling in abstract data types.Several definitions for order-sorted algebras have been proposed. In some papers an operator symbol, which may be multiply declared, is interpreted by a family of functions (“overloaded” algebras). In other papers it is always interpreted by a single function (“nonoverloaded” algebras). On the one hand, we try to demonstrate the differences between these two approaches with respect to equality, rewriting and completion; on the other hand, we prove that in fact both theories can be studied in parallel provided that certain notions are suitably defined.The overloaded approach differs from the many-sorted and the nonoverloaded one in that the overloaded term algebra is not necessarily initial. We give a decidable sufficient criterion for the initiality of the term algebra, which is less restrictive than GJM-regularity as proposed by Goguen, Jouannaud and Meseguer.Sort-decreasingness is an important property of rewrite systems since it ensures that confluence and Church-Rosser property are equivalent, that the overloaded and nonoverloaded rewrite relations agree, and that variable overlaps do not yield critical pairs. We prove that it is decidable whether or not a rewrite rule is sort-decreasing, even if the signature is not regular.Finally, we demonstrate that every overloaded completion procedure may also be used in the nonoverloaded world, but not conversely, and that specifications exist that can only be completed using the nonoverloaded semantics