Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations (Q1196302): Difference between revisions

This is the latest version of a paper which has been circulated informally since about 1978. It provides the basic facts about order- sorted algebras (OSA's). A second part is promised, which well treat the use of OSA's for exception handling, error recovery, and sort constraints. The motivation for the study of OSA is many-fold: it gives a semantic analysis for the topics of inheritance, polymorphism, meaningless expressions (such as top of the empty stack), partial operations which are total on equationally defined subsorts, and others. We give only the basic notion. Suppose that \((S,\leq)\) is a poset. An \(S\)- sorted order-sorted algebra \(A\) is an \(S\)-sorted algebra such that \(A_ s\subseteq A_{s'}\) when \(s\leq s'\), and such that the operations \(\sigma \in \Sigma_{w,s}\cap \Sigma_{w',s'}\) satisfy the condition: if \(w\leq w'\), then \(s\leq s'\). The paper describes an equational proof system for OSA, and gives a completeness theorem and an initial algebra construction for conditional equations. There is an existence theorem for initial algebras, and a Birkhoff variety theorem and a McKinsey-Malcev quasi-variety theorem. Many examples relevant to computer science are given, and the paper is written in the fluid style readers have come to expect. There are only a few minor typographical errors.