μ-bicomplete categories and parity games
Santocanale, Luigi
RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 36 (2002), p. 195-227 / Harvested from Numdam
Access to full text
Full (PDF)
Full (DJVU)

For an arbitrary category, we consider the least class of functors containing the projections and closed under finite products, finite coproducts, parameterized initial algebras and parameterized final coalgebras, i.e. the class of functors that are definable by μ-terms. We call the category μ-bicomplete if every μ-term defines a functor. We provide concrete examples of such categories and explicitly characterize this class of functors for the category of sets and functions. This goal is achieved through parity games: we associate to each game an algebraic expression and turn the game into a term of a categorical theory. We show that μ-terms and parity games are equivalent, meaning that they define the same property of being μ-bicomplete. Finally, the interpretation of a parity game in the category of sets is shown to be the set of deterministic winning strategies for a chosen player.

Publié le : 2002-01-01
DOI : https://doi.org/10.1051/ita:2002010
Classification:  18A30,  68Q65,  91A43 
@article{ITA_2002__36_2_195_0,
     author = {Santocanale, Luigi},
     title = {$\mu $-bicomplete categories and parity games},
     journal = {RAIRO - Theoretical Informatics and Applications - Informatique Th\'eorique et Applications},
     volume = {36},
     year = {2002},
     pages = {195-227},
     doi = {10.1051/ita:2002010},
     mrnumber = {1948769},
     zbl = {1024.18001},
     language = {en},
     url = {http://dml.mathdoc.fr/item/ITA_2002__36_2_195_0}
}

Santocanale, Luigi. $\mu $-bicomplete categories and parity games. RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 36 (2002) pp. 195-227. doi : 10.1051/ita:2002010. http://gdmltest.u-ga.fr/item/ITA_2002__36_2_195_0/

[1] P. Aczel, Non-well-founded sets. Stanford University Center for the Study of Language and Information, Stanford, CA (1988). | MR 940014 | Zbl 0668.04001

[2] P. Aczel, J. Adámek and J. Velebil, A coalgebraic view of infinite trees and iteration, edited by M.L.A. Corradini and U. Montanari. Elsevier Science Publishers, Electron. Notes in Theoret. Comput. Sci. 44 (2001).

[3] J. Adámek and V. Koubek, Least fixed point of a functor. J. Comput. System Sci. 19 (1979) 163-178. | MR 550196 | Zbl 0423.18007

[4] J. Adámek and J. Rosický, Locally presentable and accessible categories. Cambridge University Press, Cambridge (1994). | MR 1294136 | Zbl 0795.18007

[5] A. Arnold and D. Niwinski, Rudiments of mu-calculus. Elsevier, North-Holland, Stud. Logic Found. Math. 146 (2001). | MR 1854973 | Zbl 0968.03002

[6] M. Barr, Terminal coalgebras in well-founded set theory. Theoret. Comput. Sci. 114 (1993) 299-315. | MR 1228862 | Zbl 0779.18004

[7] S.L. Bloom and Z. Ésik, Iteration theories. Springer-Verlag, Berlin (1993). The equational logic of iterative processes. | MR 1295433 | Zbl 0773.03033

[8] S.L. Bloom, Z. Ésik, A. Labella and E.G. Manes, Iteration 2-theories. Appl. Categ. Structures 9 (2001) 173-216. | MR 1812303 | Zbl 0981.18005

[9] J.R.B. Cockett and D. Spencer, Strong categorical datatypes. I, in Category theory 1991 (Montreal, PQ, 1991). Providence, RI, Amer. Math. Soc. (1992) 141-169. | MR 1192145 | Zbl 0792.18008

[10] J.R.B. Cockett and D. Spencer, Strong categorical datatypes. II. A term logic for categorical programming. Theoret. Comput. Sci. 139 (1995) 69-113. | MR 1320236 | Zbl 0874.68033

[11] R. Cockett and T. Fukushima, About Charity, Yellow Series Report No. 92/480/18. Department of Computer Science, The University of Calgary (1992).

[12] E.A. Emerson and C.S. Jutla, Tree automata, mu-calculus and determinacy (extended abstract), in 32nd Annual Symposium on Foundations of Computer Science. IEEE (1991) 368-377.

[13] E.A. Emerson, C.S. Jutla and A.P. Sistla, On model checking for the μ-calculus and its fragments. Theoret. Comput. Sci. 258 (2001) 491-522. | MR 1826118 | Zbl 0973.68120

[14] Z. Ésik and A. Labella, Equational properties of iteration in algebraically complete categories. Theoret. Comput. Sci. 195 (1998) 61-89. Mathematical foundations of computer science, Cracow (1996). | MR 1603831 | Zbl 0903.18003

[15] P. Freyd, Algebraically complete categories, in Category theory (Como, 1990). Springer, Berlin (1991) 95-104. | MR 1173007 | Zbl 0815.18005

[16] E. Giménez, A tutorial on recursive types in Coq. Technical Report 0221, INRIA (1998).

[17] J.M.E. Hyland, The effective topos, in The L.E.J. Brouwer Centenary Symposium (Noordwijkerhout, 1981). North-Holland, Amsterdam (1982) 165-216. | MR 717245 | Zbl 0522.03055

[18] A. Joyal, Free bicomplete categories. C. R. Math. Rep. Acad. Sci. Canada 17 (1995) 219-224. | MR 1362638 | Zbl 0847.18001

[19] A. Joyal, Free lattices, communication and money games, in Logic and scientific methods (Florence, 1995). Kluwer Acad. Publ., Dordrecht (1997) 29-68. | MR 1797101 | Zbl 0897.90203

[20] G.M. Kelly, Elementary observations on 2-categorical limits. Bull. Austral. Math. Soc. 39 (1989) 301-317. | MR 998024 | Zbl 0657.18004

[21] J. Lambek, A fixpoint theorem for complete categories. Math. Z. 103 (1968) 151-161. | MR 224671 | Zbl 0149.26105

[22] D.J. Lehmann and M.B. Smyth, Algebraic specification of data types: A synthetic approach. Math. Systems Theory 14 (1981) 97-139. | MR 616960 | Zbl 0457.68035

[23] M. Makkai and R. Paré, Accessible categories: The foundations of categorical model theory. American Mathematical Society, Providence, RI (1989). | MR 1031717 | Zbl 0703.03042

[24] R. Mcnaughton, Infinite games played on finite graphs. Ann. Pure Appl. Logic 65 (1993) 149-184. | MR 1257468 | Zbl 0798.90151

[25] A.W. Mostowski, Regular expressions for infinite trees and a standard form of automata, in Computation theory (Zaborów, 1984). Springer, Berlin, Lecture Notes in Comput. Sci. 208 (1985) 157-168. | MR 827531 | Zbl 0612.68046

[26] D. Niwiński, Equational μ-calculus, in Computation theory (Zaborów, 1984). Springer, Berlin, Lecture Notes in Comput. Sci. 208 (1985) 169-176. | MR 827532 | Zbl 0615.03013

[27] C. Reutenauer, Ensembles libres de chemins dans un graphe. Bull. Soc. Math. France 114 (1986) 135-152. | Numdam | MR 860813 | Zbl 0616.05043

[28] J.J.M.M. Rutten, Universal coalgebra: A theory of systems. Theoret. Comput. Sci. 249 (2000) 3-80. | MR 1791953 | Zbl 0951.68038

[29] L. Santocanale, The alternation hierarchy for the theory of μ-lattices. Theory Appl. Categ. 9 (2002) 166-197. A special volume of articles from the Category Theory 2000 Conference (CT2000). | MR 1897815 | Zbl 0987.03057

[30] L. Santocanale, A calculus of circular proofs and its categorical semantics, in FOSSACS02, Foundations of Software Science and Computation Structures. Springer-Verlag, Lecture Notes Comput. Sci. 2303 (2002) 357-371. | MR 1965563 | Zbl 1077.03515

[31] L. Santocanale, Free μ-lattices. J. Pure Appl. Algebra 168 (2002) 227-264. Category theory 1999 (Coimbra). | MR 1887159 | Zbl 0990.06004

[32] A.K. Simpson and G.D. Plotkin, Complete axioms for categorical fixed-point operators, in Proc. of 15th Annual Symposium on Logic in Computer Science (2000) 30-41. | MR 1946083

[33] W. Thomas, Languages, automata, and logic edited by G. Rozenberg and A. Salomaa. Springer-Verlag, New York, Handbook of Formal Language Theory III (1996). | MR 1470024

[34] I. Walukiewicz, Pushdown processes: Games and model-checking. Inform. and Comput. 164 (2001) 234-263. FLOC '96 (New Brunswick, NJ). | Zbl 1003.68072

[35] W. Zielonka, Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theoret. Comput. Sci. 200 (1998) 135-183. | MR 1625527 | Zbl 0915.68120