zbMATH — the first resource for mathematics

On the existence of free models in abstract algebraic institutions. (English) Zbl 0608.68014
To provide a formal framework for discussing specifications of abstract data types we restrict the notion of Institution due to J. A. Goguen and 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 B. Mahr and 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.

68P05 Data structures
68Q65 Abstract data types; algebraic specification
18C10 Theories (e.g., algebraic theories), structure, and semantics
Full Text: DOI
[1] Goguen, J.A.; Thatcher, J.W.; Wagner, E.G., An initial algebra approach to the specification, correctness, and implementation of abstract data types, (), 80-149, IBM Res. Rept. RC 6487
[2] Goguen, J.A.; Thatcher, J.W.; Wagner, E.G.; Wright, J.B., Initial algebra semantics and continuous algebras, J. ACM, 24, 1, 68-95, (1977) · Zbl 0359.68018
[3] Andreka, H.; Nemeti, I., Generalization of the concept of variety and quasivariety to partial algebras through category theory, Dissertationes math. (rozprawy mat.), 204, (1983) · Zbl 0518.08007
[4] also: Math. Inst. Hung. Acad. Sci., Preprint No. 5/1976.
[5] Andreka, H.; Nemeti, I., A general axiomatizability theorem formulated in terms of cone-injective subcategories, (), 13-35
[6] Andreka, H.; Nemeti, I., Injectivity in categories to represent all first-order formulas, Demonstratio math., 12, 717-732, (1979) · Zbl 0497.03029
[7] Arbib, M.A.; Manes, E.G., Arrow, structures and functors: the categorical imperative, (1975), Academic Press New York · Zbl 0306.18002
[8] Banaschewski, B.; Herrlich, H., Subcategories definable by implications, Houston J. math., 2, 149-171, (1976) · Zbl 0344.18002
[9] Barwise, K.J., Axioms for abstract model theory, Ann. math. logic, 7, 221-265, (1974) · Zbl 0324.02034
[10] Bauer, F.L.; Wössner, H., Algorithm language and program development, (1982), Springer Berlin
[11] Bloom, S.L.; Wagner, E.G., Many-sorted theories and their algebras, with examples from computer science, ()
[12] Broy, M.; Wirsing, M., Partial abstract types, Acta inform., 18, 47-64, (1982) · Zbl 0494.68020
[13] Burmeister, P., Partial algebras—survey of a unifying approach towards a two-valued modeltheory for partial algebras, Algebra universalis, 15, 306-358, (1982) · Zbl 0511.03014
[14] Burstall, R.M.; Goguen, J.A., The semantics of \scclear, a specification language, (), 292-332 · Zbl 0456.68024
[15] Burstall, R.M.; Goguen, J.A., Algebras, theories and freeness: an introduction for computer scientists, () · Zbl 0518.68009
[16] de Carvalho, R.L.; Maibaum, T.S.E.; Pequeno, T.H.C.; Pereda, A.A.; Veloso, P.A.S., A model theoretic approach to the theory of abstract data types and data structures, ()
[17] Chang, C.C.; Keisler, H.J., Model theory, (1973), North-Holland Amsterdam · Zbl 0276.02032
[18] Ehrig, H.; Wagner, E.G.; Thatcher, J.W., Algebraic specifications with generating constraints, (), 188-202 · Zbl 0518.68019
[19] Gogolla, M.; Drosten, K.; Lipeck, U.; Ehrich, H.D., Algebraic and operational semantics of specifications allowing exceptions and errors, () · Zbl 0553.68012
[20] Goguen, J.A., Abstract errors for abstract data types, () · Zbl 0373.68024
[21] Goguen, J.A., Order sorted algebras: exceptions and error sorts, coercions and overloaded operators, ()
[22] Goguen, J.A.; Burstall, R.M., Introducing institutions, (), 221-256 · Zbl 1288.03001
[23] Goguen, J.A.; Burstall, R.M., Some fundamental algebraic tools for the semantics of computation, part 1: comma categories, colimits, signatures and theories, Theoret. comput. sci., 31, 175-210, (1984) · Zbl 0566.68065
[24] Goguen, J.A.; Meseguer, J., Initiality, induction and computability, () · Zbl 0571.68004
[25] Grätzer, G., ()
[26] Guttag, J.V., The specification and application to programming of abstract data types, () · Zbl 0395.68020
[27] Herrlich, H.; Strecker, G.E., Category theory, (1973), Allyn and Bacon Rockleigh · Zbl 0265.18001
[28] Liskov, B.; Zilles, S., Specification techniques for data abstraction, IEEE trans. software engrg., SE-1, 1, 7-19, (1975)
[29] MacLane, S., Categories for the working Mathematician, (1971), Springer New York
[30] Mahr, B.; Makowsky, J.A., Characterizing specification languages which admit initial semantics, Theoret. comput. sci., 31, 49-60, (1984) · Zbl 0536.68011
[31] Makowsky, J., Why Horn formulas matter in computer science: initial structures and generic examples, (), 374-387 · Zbl 0563.68013
[32] Mal’cev, A.I.; Mal’cev, A.I., Quasiprimitive classes of abstract algebras, (), Dokl. akad. nauk. SSSR, 108, 187-189, (1956), (in Russian) · Zbl 0073.25804
[33] Milner, R., A theory of type polymorphism in programming, J. comput. system. sci., 17, 348-375, (1978) · Zbl 0388.68003
[34] Nemeti, I.; Sain, I., Cone-injectivity and some Birkhoff type theorems in categories, (), 535-578
[35] Reichel, H., Initially restricting algebraic theories, (), 504-514 · Zbl 0469.68026
[36] Reichel, H., Structural induction on partial algebras, () · Zbl 0546.08004
[37] Sannella, D.T.; Tarlecki, A., Building specifications in an arbitrary institution, (), 337-356
[38] Tarlecki, A.; Tarlecki, A., Free constructions in algebraic institutions, (), 526-534, long version:
[39] Tarlecki, A., Abstract algebraic institutions which strongly admit initial semantics, ()
[40] Tarlecki, A., Quasi-varieties in abstract algebraic institutions, () · Zbl 0622.68033
[41] Tarlecki, A.; Wirsing, M., Continuous abstract data types—basic machinery and results, (), 431-441, long version to appear in Fund. Inform.
[42] Wand, M., Final algebra semantics and data type extensions, J. comput. system sci., 19, 27-44, (1979) · Zbl 0418.68020
[43] Wirsing, M.; Pepper, P.; Partsch, H.; Dotsch, W.; Broy, M., On hierarchies of abstract data types, Acta inform., 20, 1-33, (1983) · Zbl 0513.68015
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.