Equivalences and Congruences on Infinite Conway Games
RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 46 (2012) no. 2, pp. 231-259.

Taking the view that infinite plays are draws, we study Conway non-terminating games and non-losing strategies. These admit a sharp coalgebraic presentation, where non-terminating games are seen as a final coalgebra and game contructors, such as disjunctive sum, as final morphisms. We have shown, in a previous paper, that Conway's theory of terminating games can be rephrased naturally in terms of game (pre)congruences. Namely, various conceptually independent notions of equivalence can be defined and shown to coincide on Conway's terminating games. These are the equivalence induced by the ordering on surreal numbers, the contextual equivalence determined by observing what player has a winning strategy, Joyal's categorical equivalence, and, for impartial games, the denotational equivalence induced by Grundy semantics. In this paper, we discuss generalizations of such equivalences to non-terminating games and non-losing strategies. The scenario is even more rich and intriguing in this case. In particular, we investigate efficient characterizations of the contextual equivalence, and we introduce a category of fair strategies and a category of fair pairs of strategies, both generalizing Joyal's category of Conway games and winning strategies. Interestingly, the category of fair pairs captures the equivalence defined by Berlekamp, Conway, Guy on loopy games.

DOI : https://doi.org/10.1051/ita/2012001
Classification : 68Q55,  91A40,  91A80
Mots clés : Conway games, non-wellfounded games, coalgebras, equivalences, Joyal's category
@article{ITA_2012__46_2_231_0,
     author = {Honsell, Furio and Lenisa, Marina and Redamalla, Rekha},
     title = {Equivalences and Congruences on Infinite Conway Games},
     journal = {RAIRO - Theoretical Informatics and Applications - Informatique Th\'eorique et Applications},
     pages = {231--259},
     publisher = {EDP-Sciences},
     volume = {46},
     number = {2},
     year = {2012},
     doi = {10.1051/ita/2012001},
     zbl = {1279.68187},
     mrnumber = {2931248},
     language = {en},
     url = {http://www.numdam.org/articles/10.1051/ita/2012001/}
}
Honsell, Furio; Lenisa, Marina; Redamalla, Rekha. Equivalences and Congruences on Infinite Conway Games. RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 46 (2012) no. 2, pp. 231-259. doi : 10.1051/ita/2012001. http://www.numdam.org/articles/10.1051/ita/2012001/

[1] S. Abramsky and R. Jagadesaan, Games and full completeness for multiplicative linear logic, J. Symb. Log. 59 (1994) 543-574. | MR 1276632 | Zbl 0822.03007

[2] P. Aczel, Non-wellfounded sets. CSLI Lecture Notes 14 (1988). | MR 940014 | Zbl 0668.04001

[3] J. Barwise and L. Moss, Vicious Circles. CSLI Lecture Notes 60 (1996). | MR 1423600 | Zbl 0865.03002

[4] E. Berlekamp, J. Conway and R. Guy, Winning Ways. Academic Press (1982).

[5] J.H. Conway, On Numbers and Games, 2nd edition (1st edition by Academic Press (1976). AK Peters Ltd. (2001). | MR 1803095 | Zbl 0972.11002

[6] M. Forti and F. Honsell, Set-theory with free construction principles. Ann. Scuola Norm. Sup. Pisa Cl. Sci. 10 (1983) 493-522. | Numdam | MR 739920 | Zbl 0541.03032

[7] O. Grumberg, M. Lange, M. Leucker and S. Shoham, When not losing is better than winning : abstraction and refinement for the full μ-calculus. Inform. Comput. 205 (2007) 1130-1148. | MR 2340897

[8] P.M. Grundy, Mathematics and games. Eureka 2 (1939) 6-8.

[9] F. Honsell and M. Lenisa, Conway Games, algebraically and coalgebraically. Log. Meth. Comput. Sci. 7 (2011). | MR 2831240 | Zbl 1238.91041

[10] M. Hyland and A. Schalk, Games on Graphs and Sequentially Realizable Functionals, in Proc. of LICS'02. IEEE Computer Science Press (2002) 257-264.

[11] C. Kissig and Y. Venema, Complementation of Coalgebra Automata, in Proc. of CALCO'09. Lect. Notes Comput. Sci. 5728 (2009) 81-96. | MR 2557823 | Zbl 1239.68048

[12] B. Jacobs and J.J.M.M. Rutten, A Tutorial on (Co)algebras and (Co)induction. Bull. of EATCS 62 (1997) 222-259. | Zbl 0880.68070

[13] A. Joyal, Remarques sur la théorie des jeux à deux personnes. Gaz. Sci. Math. du Québec 1 (1977).

[14] P.L. Curien, H. Herbelin, J.L. Krivine and P.A. Melliès, Categorical semantics of linear logic, in Interactive models of computation and program behaviour. Panoramas et Synthèses, Société Mathématique de France 27 (2009). | MR 2605802 | Zbl 1206.03052

[15] P.A. Melliès, N. Tabareau and C. Tasson, An explicit formula for the free exponential modality of linear logic, in Proc. of ICALP'09. Lect. Notes Comput. Sci. 555 (2009). | MR 2544800 | Zbl 1248.03080

[16] M. Pauly, From Programs to Games : Invariance and Safety for Bisimulation, in Proc. of CSL'09 (2009) 485-496. | MR 1859464 | Zbl 0973.68040

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

[18] R. Sprague, Über mathematische kampfspiele. Tohoku Math. J. 41 (1935) 438-444. | Zbl 0013.29004

[19] W. Thomas, Infinite games and verification, in Proc. of CAV'02. Lect. Notes Comput. Sci. 2404 (2002) 58-64. | Zbl 1010.68504

[20] J. Van Benthem, Extensive games as process models, J. Log. Lang. Inf. 11 (2002). | MR 1909616 | Zbl 1003.03530