×

Universal coalgebra: A theory of systems. (English) Zbl 0951.68038

In the semantics of programming, finite data types such as finite lists, have traditionally been modelled by initial algebras. Later final coalgebras were used in order to deal with infinite data types. Coalgebras, which are the dual of algebras, turned out to be suited, moreover, as models for certain types of automata and more generally, for (transition and dynamical) systems. An important property of initial algebras is that they satisfy the familiar principle of induction. Such a principle was missing for coalgebras until the work of P. Aczel [Non-Well-Founded sets, CSLI Lecture Notes, Vol. 14, center for the study of Languages and information, Stanford (1988)] on a theory of non-wellfounded sets, in which he introduced a proof principle nowadays called coinduction. It was formulated in terms of bisimulation, a notion originally stemming from the world of concurrent programming languages. Using the notion of coalgebra homomorphism, the definition of bisimulation on coalgebras can be shown to be formally dual to that of congruence on algebras. Thus, the three basic notions of universal algebra: algebra, homomorphism of algebras, and congruence, turn out to correspond to coalgebra, homomorphism of coalgebras, and bisimulation, respectively. In this paper, the latter are taken as the basic ingredients of a theory called universal coalgebra. Some standard results from universal algebra are reformulated (using the aforementioned correspondence) and proved for a large class of coalgebras, leading to a series of results on, e.g., the lattices of subcoalgebras and bisimulations, simple coalgebras and coinduction, and a covariety theorem for coalgebras similar to Birkhoff’s variety theorem.

MSC:

68Q10 Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.)
68Q55 Semantics in the theory of computing
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Abramsky, S., A domain equation for bisimulation, Inform and Comput., 92, 2, 161-218 (1991) · Zbl 0718.68057
[3] Aczel, P., Final universes of processes, (Brookes, S.; Main, M.; Melton, A.; Mislove, M.; Schmidt, D., Proc. 9th Internat. Conf. on Mathematical Foundations of Programming Semantics. Proc. 9th Internat. Conf. on Mathematical Foundations of Programming Semantics, Lecture Notes in Computer Science, Vol. 802 (1994), Springer: Springer Berlin), 1-28 · Zbl 1509.68179
[4] Aczel, P.; Mendler, N., A final coalgebra theorem, (Pitt, D. H.; Ryeheard, D. E.; Dybjer, P.; Pitts, A. M.; Poigne, A., Proc. Category Theory and Computer Science. Proc. Category Theory and Computer Science, Lectures Notes in Computer Science (1989), Springer: Springer Berlin), 357-365 · Zbl 1496.03206
[5] Arbib, M. A.; Manes, E. G., Machines in a category, J. Pure Appl. Algebra, 19, 9-20 (1980) · Zbl 0441.18010
[6] Arbib, M. A.; Manes, E. G., Parametrized data types do not need highly constrained parameters, Inform. and Control, 52, 2, 139-158 (1982) · Zbl 0505.68013
[7] America, P.; Rutten, J. J.M. M., Solving reflexive domain equations in a category of complete metric spaces, J. Comput. System Sci., 39, 3, 343-375 (1989) · Zbl 0717.18002
[8] de Bakker, J. W.; de Vink, E., Control Flow Semantics, Foundations of Computing Series (1996), The MIT Press: The MIT Press Cambridge, MA · Zbl 0971.68099
[10] Barr, M., Additions and corrections to “terminal coalgebras in well-founded set theory”, Theoret. Comput. Sci., 124, 1, 189-192 (1994) · Zbl 0788.18001
[13] Borceux, F., Handbook of Categorical Algebra 1: Basic Category Theory, Encyclopedia of Mathematics and its Applications, Vol. 50 (1994), Cambridge University Press: Cambridge University Press Cambridge · Zbl 0803.18001
[14] van Breugel, F., Terminal metric spaces of finitely branching and image finite linear processes, Theoret. Comput. Sci., 202, 1-2, 223-230 (1998) · Zbl 0902.68118
[15] Cı̂rstea, C., Coalgebra semantics for hidden algebra: parameterised objects and inheritance, Proc. 12th Workshop on Algebraic Development Techniques (1998), Springer: Springer Berlin
[16] Cohn, P. M., Universal Algebra, Mathematics and its Applications, Vol. 6 (1981), D. Reidel Publishing Company: D. Reidel Publishing Company Dordrecht · Zbl 0461.08001
[17] Corradini, A., A complete calculus for equational deduction in coalgebraic specification, Report SEN-R9723 (1997), CWI: CWI Amsterdam
[18] Csákány, B., Completeness in coalgebras, Acta Sci. Math., 48, 75-84 (1985) · Zbl 0593.08004
[19] Davis, R. C., Universal coalgebra and categories of transition systems, Math. Systems Theory, 4, 1, 91-95 (1970) · Zbl 0191.01203
[20] Devaney, R. L., An Introduction to Chaotic Dynamical Systems (1986), The Benjamin/Cummings Publishing Company: The Benjamin/Cummings Publishing Company Menlopark, CA · Zbl 0632.58005
[22] Fiore, M. P., A coinduction principle for recursive data types based on bisimulation, Inform. and Comput., 127, 2, 186-198 (1996) · Zbl 0868.68054
[23] Forti, M.; Honsell, F.; Lenisa, M., Processes and hyperuniverses, (Privara, I., Proc. 19th Internat. Symp. on Mathematical Foundations of Computer Science. Proc. 19th Internat. Symp. on Mathematical Foundations of Computer Science, Lecture Notes in Computer Science, Vol. 841 (1994), Springer: Springer Berlin), 352-363 · Zbl 1493.68245
[24] Goguen, J. A.; Thatcher, J. W.; Wagner, E. G., An initial algebra approach to the specification, correctness and implementation of abstract data types, (Yeh, R., Current Trends in Programming Methodology (1978), Prentice-Hall: Prentice-Hall Englewood Cliffs, NJ), 80-149
[26] Groote, J. F.; Vaandrager, F., Structured operational semantics and bisimulation as a congruence, Inform. and Comput., 100, 2, 202-260 (1992) · Zbl 0752.68053
[27] Gumm, H. P.; Schröder, T., Covarieties and complete covarieties, (Jacobs, B.; Moss, L.; Reichel, H.; Rutten, J. J.M. M., Proc. 1st Internat. Workshop on Coalgebraic Methods in Computer Science (CMCS ’98). Proc. 1st Internat. Workshop on Coalgebraic Methods in Computer Science (CMCS ’98), Electronic Notes in Theoretical Computer Science, Vol. 11 (1998), Elsevier Science B.V: Elsevier Science B.V Amsterdam) · Zbl 0973.68174
[29] Hennessy, M.; Plotkin, G. D., Full abstraction for a simple parallel programming language, (Becvar, J., Proc. 8th Symp. on Mathematical Foundations of Computer Science. Proc. 8th Symp. on Mathematical Foundations of Computer Science, Lecture Notes in Computer Science, Vol. 74 (1979), Springer: Springer Berlin), 108-120 · Zbl 0457.68006
[30] Hensel, U.; Huisman, M.; Jacobs, B.; Tews, H., Reasoning about classes in object-oriented languages: logical models and tools, (Hankin, Ch., Proc. European Symp. on Programming. Proc. European Symp. on Programming, Lecture Notes in Computer Science, Vol. 1381 (1998), Springer: Springer Berlin), 105-121
[32] Honsell, F.; Lenisa, M., Final semantics for untyped \(λ\)-calculus, (Dezani-Ciancaglini, M.; Plotkin, G., Proc. 2nd Conf. on Typed Lambda Calculus and Applications. Proc. 2nd Conf. on Typed Lambda Calculus and Applications, Lecture Notes in Computer Science, Vol. 902 (1995), Springer: Springer Berlin), 249-265 · Zbl 1063.03516
[33] Jacobs, B., Mongruences and cofree coalgebras, (Alagar, V. S.; Nivat, M., Algebraic Methods and Software Technology. Algebraic Methods and Software Technology, Lecture Notes in Computer Science, Vol. 936 (1995), Springer: Springer Berlin), 245-260 · Zbl 1496.68110
[35] Jacobs, B., Inheritance and cofree constructions, (Cointe, P., European Conference on Object-Oriented Programming. European Conference on Object-Oriented Programming, Lecture Notes in Computer Science, Vol. 1098 (1996), Springer: Springer Berlin), 210-231
[36] Jacobs, B., Object and classes, co-algebraically, (Freitag, B.; Jones, C. B.; Lengauer, C.; Schek, H.-J., Object-Orientation with Parallelism and Persistence (1996), Kluwer Academic Publishers: Kluwer Academic Publishers Dordrecht)
[37] Jacobs, B., Coalgebraic reasoning about classes in object-oriented languages, (Jacobs, B.; Moss, L.; Reichel, H.; Rutten, J. J.M. M., Proc. 1st Internat. Workshop on Coalgebraic Methods in Computer Science (CMCS) ’98). Proc. 1st Internat. Workshop on Coalgebraic Methods in Computer Science (CMCS) ’98), Electronic Notes in Theoretical Computer Science, Vol. 11 (1998), Elsevier Science B.V: Elsevier Science B.V Amsterdam) · Zbl 0917.68127
[39] Jacobs, B.; Rutten, J., A tutorial on (co)algebras and (co)induction, Bull. EATCS, 62, 222-259 (1997) · Zbl 0880.68070
[41] Joyal, A.; Nielsen, M.; Winskel, G., Bisimulation from open maps, Inform. and Comput., 127, 2, 164-185 (1996) · Zbl 0856.68067
[43] Keller, R. M., Formal verification of parallel programs, Comm. ACM, 19, 7, 371-384 (1976) · Zbl 0329.68016
[44] Kent, R. E., The metric closure powerspace construction, (Main, M.; Melton, A.; Mislove, M.; Schmidt, D., Proc. 3rd Workshop on Mathematical Foundations of Programming Language Semantics. Proc. 3rd Workshop on Mathematical Foundations of Programming Language Semantics, Lecture Notes in Computer Science, Vol. 298 (1988), Springer: Springer New Orleans), 173-199 · Zbl 0653.18008
[46] Larsen, K. G.; Skou, A., Bisimulation through probabilistic testing, Inform. Comput., 94, 1-28 (1991) · Zbl 0756.68035
[47] Lehmann, D. J.; Smyth, M. B., Algebraic specification of data types: a synthetic approach, Math. Systems Theory, 14, 97-139 (1981) · Zbl 0457.68035
[48] Lenisa, M., Final semantics for a higher-order concurrent language, (Kirchner, H., Proc. CAPP’96. Proc. CAPP’96, Lecture Notes in Computer Science, Vol. 1059 (1996), Springer: Springer Berlin), 102-118 · Zbl 1508.68211
[50] Mac Lane, S., Categories for the Working Mathematician. Categories for the Working Mathematician, Graduate Texts in Mathematics, Vol. 95 (1971), Springer: Springer New York · Zbl 0232.18001
[51] Manes, E. G., Algebraic Theories, Graduate Texts in Mathematics, Vol. 26 (1976), Springer: Springer Berlin · Zbl 0353.18007
[52] Manes, E. G.; Arbib, M. A., Algebraic Approaches to Program Semantics, Texts and Monographs in Computer Science (1986), Springer: Springer Berlin · Zbl 0599.68008
[53] Marvan, M., On covarieties of coalgebras, Arch. Math. (Brno), 21, 1, 51-64 (1985) · Zbl 0577.18004
[54] Meinke, K.; Tucker, J. V., Universal algebra, (Abramsky, S.; Gabbay, Dov. M.; Maibaum, T. S.E., Handbook of Logic in Computer Science, Vol. 1 (1992), Oxford University Press: Oxford University Press Oxford), 189-411
[55] Milner, R., Processes: a mathematical model of computing agents, (Rose, H. E.; Shepherdson, J. C., Logic Colloquium ’73, Studies in Logic, Vol. 80 (1975), North-Holland: North-Holland Amsterdam), 157-173
[56] Milner, R., A calculus of Communicating Systems. A calculus of Communicating Systems, Lecture Notes in Computer Science, Vol. 92 (1980), Springer: Springer Berlin · Zbl 0452.68027
[57] Milner, R.; Tofte, M., Co-induction in relational semantics, Theoret. Comput. Sci., 87, 209-220 (1991) · Zbl 0755.68100
[59] Moss, L. S.; Danner, N., On the foundations of corecursion, Logic J. IGPL, 231-257 (1997) · Zbl 0872.03030
[60] Park, D. M.R., Concurrency and automata on infinite sequences, (Deussen, P., Proc. 5th GI Conf.. Proc. 5th GI Conf., Lecture Notes in Computer Science, Vol. 104 (1981), Springer: Springer Berlin), 15-32
[61] Paulson, L. C., Mechanizing coinduction and corecursion in higher-order logic, J. Logic Comput., 7, 175-204 (1997) · Zbl 0878.68111
[63] Pitts, A. M., A co-induction principle for recursively defined domains, Theoret. Comput. Sci., 124, 2, 195-219 (1994) · Zbl 0795.68129
[64] Pitts, A. M., Relational properties of domains, Inform. and Comput., 127, 2, 66-90 (1996) · Zbl 0868.68037
[68] Reichel, H., An approach to object semantics based on terminal coalgebras, Math. Struct. Comput. Sci., 5, 129-152 (1995) · Zbl 0854.18006
[70] Rutten, J. J.M. M., Processes as terms: non-well-founded models for bisimulation, Math. Struct. Comput. Sci., 2, 3, 257-275 (1992) · Zbl 0798.68094
[75] Rutten, J. J.M. M.; Turi, D., On the foundations of final semantics: non-standard sets, metric spaces, partial orders, (de Bakker, J. W.; de Roever, W.-P.; Rozenberg, G., Proc. REX Workshop on Semantics. Proc. REX Workshop on Semantics, Lecture Notes in Computer Science, Vol. 666 (1993), Springer: Springer Berlin), 477-530
[77] Schmidt, G.; Ströhlein, T., Relations and Graphs, Discrete Mathematics for Computer Scientists, EATCS Monographs on Theoretical Computer Science (1993), Springer-Verlag: Springer-Verlag New York · Zbl 0900.68328
[78] Smyth, M. B.; Plotkin, G. D., The category-theoretic solution of recursive domain equations, SIAM J. Comput., 11, 4, 761-783 (1982) · Zbl 0493.68022
[79] Székely, Z., Maximal clones of co-operations, Acta Sci. Math., 53, 43-50 (1989) · Zbl 0695.08008
[80] Tarski, A., A lattice-theoretical fixpoint theorem and its applications, Pacific J. Math., 5, 285-309 (1955) · Zbl 0064.26004
[82] Turi, D., Categorical modelling of structural operational rules: case studies, (Moggi, E.; Rosolini, G., Proc. 7th CTCS Conf.. Proc. 7th CTCS Conf., Lecture Notes in Computer Science, Vol. 1290 (1997), Springer: Springer Berlin), 127-146 · Zbl 0881.18004
[85] van Glabbeek, R. J.; Smolka, S. A.; Steffen, B., Reactive, generative, and stratified models of probabilistic processes, Inform. and Comput., 121, 59-80 (1995) · Zbl 0832.68042
[86] Winskel, G.; Nielsen, M., Models for concurrency, (Abramsky, S.; M. Gabbay, Dov; Maibaum, T. S.E., Handbook of Logic in Computer Science, Vol. 4 (1995), Oxford Science Publications: Oxford Science Publications Oxford), 1-148
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.