Semantics of order-sorted specifications

Uwe Waldmann

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.


Previous | Up | Next
Uwe Waldmann <uwe@mpi-inf.mpg.de>, 1997-10-02.
Imprint | Data Protection