An Oxford survey of order sorted algebra (abstract)
Types are a fundamental organising principle in modern Computing Science,
including not only programming and specification languages, but also database
languages, knowledge representation languages, and more. Algebraic specification
techniques model types through the systematic use of sorts, and
in this context, it is natural to model subtypes with subsorts.
Following earlier works, the study of algebras with subsorts is called
order sorted algebra (abbreviated OSA). Many different variants
of OSA have been developed, and here we compare some of the main approaches,
emphasising motivation and intuitions, rather than proofs, and pointing
out issues that distinguish the original ``overloaded'' OSA approach from
some later developments. We have deliberately given an unusually large
of number of examples, in the belief that this can greatly help the reader
who is not an expert in this area. These illustrations use the OBJ3 language,
and in fact, all the OBJ code in the source file for this paper has actually
been executed, and most of the output is also included. In addition, we
present some new results about overloaded OSA and about Mosses's unified
algebra.
We emphasize the following points: (1) overloaded OSA can be developed
with minimal assumptions on signatures and algebras, and in particular,
without monotonicity or regularity; (2) it is useful to distinguish between
strong and weak forms of overloading; in the latter, a given
expression can have at most one value in a given algebra, even though it
may have several distinct parses; (3) strong overloading is needed for
certain important Computing Science applications of OSA, including dynamic
binding in object oriented programming, and operations on data with multiple
representations; (4) it seems to be much more difficult to establish certain
basic mathematical properties of (what we call) universe OSA than of overloaded
OSA; for example, it is not currently known whether or not universe OSA
satisfies the Birkhoff variety theorem; and (5) sort constraints and retracts
greatly increase the expressive and computational power of OSA.
back to Selected Publications