μ -bicomplete categories and parity games

Luigi Santocanale

RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications (2002)

  • Volume: 36, Issue: 2, page 195-227
  • ISSN: 0988-3754

Abstract

top
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.

How to cite

top

Santocanale, Luigi. "$\mu $-bicomplete categories and parity games." RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications 36.2 (2002): 195-227. <http://eudml.org/doc/244885>.

@article{Santocanale2002,
abstract = {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 $\mu $-terms. We call the category $\mu $-bicomplete if every $\mu $-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 $\mu $-terms and parity games are equivalent, meaning that they define the same property of being $\mu $-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.},
author = {Santocanale, Luigi},
journal = {RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications},
keywords = {parity games; bicomplete categories; initial algebras; final coalgebras; inductive and coinductive types; initial algebra; final coalgebra; bicomplete category; parity game; inductive and coinductive type},
language = {eng},
number = {2},
pages = {195-227},
publisher = {EDP-Sciences},
title = {$\mu $-bicomplete categories and parity games},
url = {http://eudml.org/doc/244885},
volume = {36},
year = {2002},
}

TY - JOUR
AU - Santocanale, Luigi
TI - $\mu $-bicomplete categories and parity games
JO - RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications
PY - 2002
PB - EDP-Sciences
VL - 36
IS - 2
SP - 195
EP - 227
AB - 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 $\mu $-terms. We call the category $\mu $-bicomplete if every $\mu $-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 $\mu $-terms and parity games are equivalent, meaning that they define the same property of being $\mu $-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.
LA - eng
KW - parity games; bicomplete categories; initial algebras; final coalgebras; inductive and coinductive types; initial algebra; final coalgebra; bicomplete category; parity game; inductive and coinductive type
UR - http://eudml.org/doc/244885
ER -

References

top
  1. [1] P. Aczel, Non-well-founded sets. Stanford University Center for the Study of Language and Information, Stanford, CA (1988). Zbl0668.04001MR940014
  2. [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). Zbl1260.68235
  3. [3] J. Adámek and V. Koubek, Least fixed point of a functor. J. Comput. System Sci. 19 (1979) 163-178. Zbl0423.18007MR550196
  4. [4] J. Adámek and J. Rosický, Locally presentable and accessible categories. Cambridge University Press, Cambridge (1994). Zbl0795.18007MR1294136
  5. [5] A. Arnold and D. Niwinski, Rudiments of mu-calculus. Elsevier, North-Holland, Stud. Logic Found. Math. 146 (2001). Zbl0968.03002MR1854973
  6. [6] M. Barr, Terminal coalgebras in well-founded set theory. Theoret. Comput. Sci. 114 (1993) 299-315. Zbl0779.18004MR1228862
  7. [7] S.L. Bloom and Z. Ésik, Iteration theories. Springer-Verlag, Berlin (1993). The equational logic of iterative processes. Zbl0773.03033MR1295433
  8. [8] S.L. Bloom, Z. Ésik, A. Labella and E.G. Manes, Iteration 2-theories. Appl. Categ. Structures 9 (2001) 173-216. Zbl0981.18005MR1812303
  9. [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. Zbl0792.18008MR1192145
  10. [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. Zbl0874.68033MR1320236
  11. [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. [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. [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. Zbl0973.68120MR1826118
  14. [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). Zbl0903.18003MR1603831
  15. [15] P. Freyd, Algebraically complete categories, in Category theory (Como, 1990). Springer, Berlin (1991) 95-104. Zbl0815.18005MR1173007
  16. [16] E. Giménez, A tutorial on recursive types in Coq. Technical Report 0221, INRIA (1998). 
  17. [17] J.M.E. Hyland, The effective topos, in The L.E.J. Brouwer Centenary Symposium (Noordwijkerhout, 1981). North-Holland, Amsterdam (1982) 165-216. Zbl0522.03055MR717245
  18. [18] A. Joyal, Free bicomplete categories. C. R. Math. Rep. Acad. Sci. Canada 17 (1995) 219-224. Zbl0847.18001MR1362638
  19. [19] A. Joyal, Free lattices, communication and money games, in Logic and scientific methods (Florence, 1995). Kluwer Acad. Publ., Dordrecht (1997) 29-68. Zbl0897.90203MR1797101
  20. [20] G.M. Kelly, Elementary observations on 2 -categorical limits. Bull. Austral. Math. Soc. 39 (1989) 301-317. Zbl0657.18004MR998024
  21. [21] J. Lambek, A fixpoint theorem for complete categories. Math. Z. 103 (1968) 151-161. Zbl0149.26105MR224671
  22. [22] D.J. Lehmann and M.B. Smyth, Algebraic specification of data types: A synthetic approach. Math. Systems Theory 14 (1981) 97-139. Zbl0457.68035MR616960
  23. [23] M. Makkai and R. Paré, Accessible categories: The foundations of categorical model theory. American Mathematical Society, Providence, RI (1989). Zbl0703.03042MR1031717
  24. [24] R. McNaughton, Infinite games played on finite graphs. Ann. Pure Appl. Logic 65 (1993) 149-184. Zbl0798.90151MR1257468
  25. [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. Zbl0612.68046MR827531
  26. [26] D. Niwiński, Equational μ -calculus, in Computation theory (Zaborów, 1984). Springer, Berlin, Lecture Notes in Comput. Sci. 208 (1985) 169-176. Zbl0615.03013MR827532
  27. [27] C. Reutenauer, Ensembles libres de chemins dans un graphe. Bull. Soc. Math. France 114 (1986) 135-152. Zbl0616.05043MR860813
  28. [28] J.J.M.M. Rutten, Universal coalgebra: A theory of systems. Theoret. Comput. Sci. 249 (2000) 3-80. Zbl0951.68038MR1791953
  29. [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). Zbl0987.03057MR1897815
  30. [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. Zbl1077.03515MR1965563
  31. [31] L. Santocanale, Free μ -lattices. J. Pure Appl. Algebra 168 (2002) 227-264. Category theory 1999 (Coimbra). Zbl0990.06004MR1887159
  32. [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. MR1946083
  33. [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). MR1470024
  34. [34] I. Walukiewicz, Pushdown processes: Games and model-checking. Inform. and Comput. 164 (2001) 234-263. FLOC ’96 (New Brunswick, NJ). Zbl1003.68072
  35. [35] W. Zielonka, Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theoret. Comput. Sci. 200 (1998) 135-183. Zbl0915.68120MR1625527

NotesEmbed ?

top

You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

                
Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.