Help Guide Privacy Policy Disclaimer Contact us
  Advanced SearchBrowse




Journal Article

Semantics of Order-Sorted Specifications


Waldmann,  Uwe
Automation of Logic, MPI for Informatics, Max Planck Society;
Programming Logics, MPI for Informatics, Max Planck Society;

There are no locators available
Fulltext (public)
There are no public fulltexts available
Supplementary Material (public)
There is no public supplementary material available

Waldmann, U. (1992). Semantics of Order-Sorted Specifications. Theoretical Computer Science, 94(1), 1-35.

Cite as:
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.