Universal coalgebra: A theory of systems.

*(English)*Zbl 0951.68038In 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 |

##### Keywords:

universal coalgebra
PDF
BibTeX
Cite

\textit{J. J. M. M. Rutten}, Theor. Comput. Sci. 249, No. 1, 3--80 (2000; Zbl 0951.68038)

Full Text:
DOI

##### References:

[1] | Abramsky, S., A domain equation for bisimulation, Inform and comput., 92, 2, 161-218, (1991) · Zbl 0718.68057 |

[2] | P. Aczel, Non-Well-Founded Sets, CSLI Lecture Notes, Vol. 14, Center for the Study of Languages and Information, Stanford, 1988. |

[3] | Aczel, P., Final universes of processes, (), 1-28 |

[4] | Aczel, P.; Mendler, N., A final coalgebra theorem, (), 357-365 |

[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 Cambridge, MA · Zbl 0971.68099 |

[9] | M. Barr, Terminal coalgebras in well-founded set theory, Theoret. Comput. Sci. 114 (2) (1993) 299-315. Some additions and corrections were published in Theoret. Comput. Sci. 124 (1994) 189-192. · Zbl 0779.18004 |

[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 |

[11] | J. Barwise, L.S. Moss, Vicious Circles, On the Mathematics of Non-wellfounded Phenomena, CSLI Lecture Notes, Vol. 60, Center for the Study of Language and Information, Stanford, 1996. · Zbl 0865.03002 |

[12] | M.-P. Béal, D. Perrin, Symbolic dynamics and finite automata, Report IGM 96-18, Université de Marne-la-Vallée, 1996. |

[13] | Borceux, F., Handbook of categorical algebra 1: basic category theory, encyclopedia of mathematics and its applications, vol. 50, (1994), Cambridge University Press Cambridge |

[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 Berlin |

[16] | Cohn, P.M., Universal algebra, mathematics and its applications, vol. 6, (1981), D. Reidel Publishing Company Dordrecht |

[17] | Corradini, A., A complete calculus for equational deduction in coalgebraic specification, report SEN-R9723, (1997), 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 Menlopark, CA |

[21] | E.P. de Vink, J.J.M.M. Rutten, Bisimulation for probabilistic transition systems: a coalgebraic approach, in: P. Degano, R. Gorrieri, A. Marchetti-Spaccamela (Eds.), Proc. ICALP’97, Lecture Notes in Computer Science, Vol. 1256, 1997, pp. 460-470. Theoret. Comput. Sci., to appear. · Zbl 0930.68092 |

[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, (), 352-363 |

[24] | 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 |

[25] | R. Goldblatt, Logics of time and computation, CSLI Lecture Notes, Vol. 7, Center for the study of Language and Information, Standard, 1987. |

[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, () · Zbl 0973.68174 |

[28] | T. Hagino, A categorical programming language, Ph.D. Thesis, University of Edinburgh, Edinburgh, 1987. · Zbl 0643.03010 |

[29] | Hennessy, M.; Plotkin, G.D., Full abstraction for a simple parallel programming language, (), 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, (), 105-121 |

[31] | C. Hermida, B. Jacobs, Structural induction and coinduction in a fibrational setting, Inform. and Comput. (1998) to appear. · Zbl 0941.18006 |

[32] | Honsell, F.; Lenisa, M., Final semantics for untyped \(λ\)-calculus, (), 249-265 · Zbl 1063.03516 |

[33] | Jacobs, B., Mongruences and cofree coalgebras, (), 245-260 |

[34] | B. Jacobs, Behaviour-refinement of object-oriented specifications with coinductive correctness proofs, Report CSI-R9618, Computing Science Institute, University of Nijmegen, 1996. Also in the Proc. TAPSOFT’97. |

[35] | Jacobs, B., Inheritance and cofree constructions, (), 210-231 |

[36] | Jacobs, B., Object and classes, co-algebraically, () |

[37] | Jacobs, B., Coalgebraic reasoning about classes in object-oriented languages, () · Zbl 0917.68127 |

[38] | B. Jacobs, L. Moss, H. Reichel, J.J.M.M. Rutten (Eds.), Proc. 1st Internat. Workshop on Coalgebraic Methods in Computer Science (CMCS) ’98), Electronic Notes in Theoretical Computer Science, Vol. 11, Elsevier Science B.V., Amsterdam, 1998. Available at URL: www.elsevier.nl/locate/entcs. · Zbl 0903.00067 |

[39] | Jacobs, B.; Rutten, J., A tutorial on (co)algebras and (co)induction, Bull. EATCS, 62, 222-259, (1997) · Zbl 0880.68070 |

[40] | B. Jacobs, J.J.M.M. Rutten (Eds.), Proc. 2nd Internat. Workshop on Coalgebraic Methods in Computer Science (CMCS ’99), Electronic Notes in Theoretical Computer Science, Vol. 19, Elsevier Science B.V., Amsterdam, 1999. Available at URL: www.elsevier.nl/locate/entcs. |

[41] | Joyal, A.; Nielsen, M.; Winskel, G., Bisimulation from open maps, Inform. and comput., 127, 2, 164-185, (1996) · Zbl 0856.68067 |

[42] | Y. Kawahara, M. Mori, A small final coalgebra theorem, Theoret. Comput. Sci. (1998) to appear. · Zbl 0952.68101 |

[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, (), 173-199 · Zbl 0653.18008 |

[45] | A. Kurz, Specifying coalgebras with modal logic, in: B. Jacobs, L. Moss, H. Reichel, J.J.M.M. Rutten (Eds.), Proc. 1st Internat. Workshop on Coalgebraic Methods in Computer Science (CMCS) ’98), Electronic Notes in Theoretical Computer Science, Vol. 11, Elsevier Science B.V., Amsterdam, 1998. · Zbl 0917.68134 |

[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, (), 102-118 |

[49] | M. Lenisa, Themes in final semantics, Ph.D. Thesis, University of Udine, Udine, Italy, 1998. |

[50] | Mac Lane, S., Categories for the working Mathematician, Graduate texts in mathematics, Vol. 95, (1971), Springer New York |

[51] | Manes, E.G., Algebraic theories, graduate texts in mathematics, vol. 26, (1976), Springer Berlin |

[52] | Manes, E.G.; Arbib, M.A., Algebraic approaches to program semantics, texts and monographs in computer science, (1986), Springer Berlin |

[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, (), 189-411 |

[55] | Milner, R., Processes: a mathematical model of computing agents, (), 157-173 |

[56] | Milner, R., A calculus of communicating systems, Lecture notes in computer science, Vol. 92, (1980), Springer Berlin |

[57] | Milner, R.; Tofte, M., Co-induction in relational semantics, Theoret. comput. sci., 87, 209-220, (1991) · Zbl 0755.68100 |

[58] | L.S. Moss, Coalgebraic logic, Ann. Pure Appl. Logic \((1998)\) to appear. · Zbl 0969.03026 |

[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, (), 15-32 |

[61] | Paulson, L.C., Mechanizing coinduction and corecursion in higher-order logic, J. logic comput., 7, 175-204, (1997) · Zbl 0878.68111 |

[62] | D. Pavlovic̀, Guarded induction on final coalgebras, in: B. Jacobs, L. Moss, H. Reichel, J.J.M.M. Rutten (Eds.), Proc. 1st Internat. Workshop on Coalgebraic Methods in Computer Science (CMCS) ’98), Electronic Notes in Theoretical Computer Science, Vol. 11, Elsevier Science B.V., Amsterdam, 1998. |

[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 |

[65] | G.D. Plotkin, A structural approach to operational semantics, Report DAIMI FN-19, Aarhus University, Aarhus, September 1981. |

[66] | R. Pöschel, M. Rößiger, A general Galois theory for cofunctions and corelations, Report MATH-AL-11-1997, Technische Universität Dresden, Dresden, 1997. · Zbl 1011.08008 |

[67] | J. Power, H. Watanabe, An axiomatics for categories of coalgebras, in: B. Jacobs, L. Moss, H. Reichel, J.J.M.M. Rutten (Eds.), Proc. 1st Internat. Workshop on Coalgebraic Methods in Computer Science (CMCS) ’98), Electronic Notes in Theoretical Computer Science, Vol. 11, Elsevier Science B.V., Amsterdam, 1998. · Zbl 0917.68124 |

[68] | Reichel, H., An approach to object semantics based on terminal coalgebras, Math. struct. comput. sci., 5, 129-152, (1995) · Zbl 0854.18006 |

[69] | M. Rößiger, From modal logic to terminal coalgebras, Report MATH-AL-3-1998, Technische Universität Dresden, Dresden, 1998. |

[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 |

[71] | J.J.M.M. Rutten, A calculus of transition systems (towards universal coalgebra), in: A. Ponse, M. de Rijke, Y. Venema (Eds.), Modal Logic and Process Algebra, a Bisimulation Perspective, CSLI Lecture Notes, Vol. 53, Stanford, CSLI Publications, 1995, pp. 231-256. FTP-available at ftp.cwi.nl as pub/CWIreports/AP/CS-R9503.ps.Z. |

[72] | J.J.M.M. Rutten, Universal coalgebra: a theory of systems, Report CS-R9652, CWI, 1996. FTP-available at ftp.cwi.nl as pub/CWIreports/AP/CS-R9652.ps.Z. |

[73] | J.J.M.M. Rutten, Automata and coinduction (an exercise in coalgebra), Report SEN-R9803, CWI, 1998. FTP-available at ftp.cwi.nl as pub/CWIreports/SEN/SEN-R9803.ps.Z. Also in the Proc. CONCUR ’98, Lecture Notes in Computer Science, Vol. 1466, Springer, Berlin, 1998, pp. 194-218. · Zbl 0940.68085 |

[74] | J.J.M.M. Rutten, Relators and metric Bisimulations, in: B. Jacobs, L. Moss, H. Reichel, J.J.M.M. Rutten (Eds.), Proc. 1st Internat. Workshop on Coalgebraic Methods in Computer Science (CMCS) ’98), Electronic Notes in Theoretical Computer Science, Vol. 11, Elsevier Science B.V., Amsterdam, 1998. · Zbl 0917.68146 |

[75] | Rutten, J.J.M.M.; Turi, D., On the foundations of final semantics: non-standard sets, metric spaces, partial orders, (), 477-530 |

[76] | J.J.M.M. Rutten, D. Turi, Initial algebra and final coalgebra semantics for concurrency, in: J.W. de Bakker, W.-P. de Roever, G. Rozenberg (Eds.), Proc. REX School/ Symp. ‘A decade of concurrency’, Lecture Notes in Computer Science, Vol. 803, Springer, Berlin, 1994, pp. 530-582. FTP-available at ftp.cwi.nl as pub/CWIreports/AP/CS-R9409.ps.Z. |

[77] | Schmidt, G.; Ströhlein, T., Relations and graphs, discrete mathematics for computer scientists, EATCS monographs on theoretical computer science, (1993), 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 |

[81] | D. Turi, Functorial operational semantics and its denotational dual, Ph.D. Thesis, Vrije Universiteit, Amsterdam, 1996. |

[82] | Turi, D., Categorical modelling of structural operational rules: case studies, (), 127-146 · Zbl 0881.18004 |

[83] | D. Turi, G.D. Plotkin, Towards a mathematical operational semantics, Proc. 12th LICS Conf., IEEE Computer Society Press, Silverspring, MD, 1997, pp. 280-291. |

[84] | R. van Glabbeek, The meaning of negative premises in transition system specifications II, Report STAN-CS-TN-95-16, Department of Computer Science, Stanford University, 1996. Extended abstract in: F. Meyer auf der Heide, B. Monien (Eds.), Automata, Languages and Programming, Proc. 23th International Colloquium, ICALP ’96, Paderborn, Germany, July 1996, Lecture Notes in Computer Science, Vol. 1099, Springer, Berlin, 1996, pp. 502-513. · Zbl 1046.68629 |

[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, (), 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. 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.