Item

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. \par
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. \par 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. \par 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. \par 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.