The theory of many-sorted algebras provides a natural mathematical framework for a formal treatment of algebraic specifications. Since the generalization from the one-sorted to the many-sorted case is mostly just an exercise in formalism, the conceptual apparatus and the results of classical universal algebra are immediately at our disposal. In the context of abstract data types, however, good reasons exist for allowing some carrier sets of an algebra to be empty. This seemingly innocent deviation from the practice of algebra renders the obvious generalization of Birkhoff’s equational calculus unsound, a serious problem that has been extensively discussed in the literature.

This paper shows that the completeness and soundness of Birkhoff’s calculus extend to many-sorted algebras if a new notion of satisfiability, strong satisfiability, is adopted. Roughly speaking, an algebra strongly satisfies an equation if it satisfies all substitution instances of the equation. This condition may be hard to verify, but the authors show that in some cases it can be reduced to a weaker condition. They then study the relationships between their notions and some earlier work in the area. In fact, the paper is also a broad review of the ideas that have emerged around the problem. Although the presentation is mostly quite readable, I have a vague feeling that some basic clarifying insights are still missing.