On the existence of free models 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 (1984) which formalises 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. Our main results concern the problem of the existence of free constructions in abstract algebraic institutions. We generalise a characterization of algebraic specification languages that guarantee the existence of reachable initial models for any consistent set of axioms given by Mahr and Makowsky (1984). Then the more general problem of the existence of free functors (left adjoints to forgetful functors) for any theory morphism is analysed. We give a construction of a free model of a theory over a model of a subtheory (with respect to an arbitrary theory morphism) which requires only the existence of initial models. This yields a characterization of strongly liberal abstract algebraic institutions. We also show how to specialise there characterisation results for the partial algebras