Theoretical Computer Science, 94(1):1-35, March 2, 1992. [Preprint]
Earlier version: Forschungsbericht 297, Fachbereich Informatik, Universität Dortmund, 1989.
Abstract: Order-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 ("non-overloaded" 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 parallelly, provided that certain notions are suitably defined.
The overloaded approach differs from the many-sorted and the non-overloaded case, 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 system, since it ensures that confluence and Church-Rosser property are equivalent, that the overloaded and non-overloaded 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 non-overloaded world, but not conversely, and that specifications exist that can only be completed using the non-overloaded semantics.