Hilfe Wegweiser Impressum Kontakt Einloggen





Semantics of Order-Sorted Specifications


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

Externe Ressourcen
Es sind keine Externen Ressourcen verfügbar
Volltexte (frei zugänglich)
Es sind keine frei zugänglichen Volltexte verfügbar
Ergänzendes Material (frei zugänglich)
Es sind keine frei zugänglichen Ergänzenden Materialien verfügbar

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

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.