On the existence of free models in abstract algebraic institutions (Q1085969): Difference between revisions

To provide a formal framework for discussing specifications of abstract data types we restrict the notion of Institution due to \textit{J. A. Goguen} and \textit{R. M. Burstall} [Lect. Notes Comput. Sci. 164, 221-256 (1984; Zbl 0543.68021)] 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 characterisation of algebraic specification languages that guarantee the existence of reachable initial models for any consistent set of axioms given by \textit{B. Mahr} and \textit{J. A. Makowsky} [Theor. Comput. Sci. 31, 49-59 (1984; Zbl 0536.68011)]. 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 to 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 characterisation of strongly liberal abstract algebraic institutions. We also show how to specialise there characterisation results for the partial algebras.