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