Quasi-varieties in abstract algebraic institutions

AbstractTo provide a formal framework for discussing specifications of abstract data types we restrict the notion of institution due to Goguen and Burstall (“Lecture Notes in Computer Sci.,” No. 164, pp. 221–256, Springer, Berlin, 1984) which formalizes the concept of a logical system for writing specifications, and deal with abstract algebraic institutions. These are institutions equipped with a notion of submodel which satisfy a number of technical conditions. In this framework we introduce an abstract notion of ground equation which, in turn, determines notions of abstract infinitary conditional equation and inequation. We prove that quasi-varieties (i.e., classes of models closed under submodels and nonempty products) are exactly classes of models definable by abstract infinitary conditional equations and inequations. As a consequence we obtain “syntactic” characterizations of abstract algebraic institutions which guarantee the existence of reachable initial models for any consistent set of axioms, as well as those which guarantee the existence of a free model of a theory generated by any model of a subtheory (with respect to an arbitrary theory morphism). We also show how to specialize these results for abstract algebraic institutions of, respectively, total, partial, and continuous algebras