Mathematical Structures in Computer Science

Research Article

An Oxford survey of order sorted algebra

Joseph Goguena1 and Răzvan Diaconescua1

a1 Programming Research Group, Oxford University


This paper surveys several different variants of order sorted algebra (abbreviated OSA), comparing some of the main approaches (overloaded OSA, universe OSA, unified algebra, term declaration algebra, etc.), emphasising motivation and intuitions, and pointing out features that distinguish the original ‘overloaded’ OSA approach from some later developments. These features include sort constraints and retracts; the latter is particularly useful for handling multiple data representations (including automatic coercions among them). Many examples are given, for most of which, runs are shown on the OBJ3 system.

This paper also significantly generalises overloaded OSA by dropping the regularity and monotonicity assumptions, and by adding signatures of non-monotonicities, which support simple semantics for some aspects of object oriented programming. A number of new results for this generalisation are proved, including initiality, variety, and quasi-variety theorems. Axiomatisability results à la Birkhoff are also proved for unified algebras.

(Received June 25 1992)

(Revised March 15 1994)


The research reported in this paper has been supported in part by grants from the Science and Engineering Research Council, and contracts with Fujitsu Laboratories Limited, the CEC under ESPRIT-2 BRA Working Groups 6071, IS-CORE (Information Systems Correctness and REusability) and 6112, COMPASS (COMPrehensive Algebraic Approach to System Specification and development), and the Information Technology Promotion Agency, Japan, as part of the R & D of Basic Technology for Future Industries ‘New Models for Software Architecture’ project sponsored by NEDO (New Energy and Industrial Technology Development Organization).