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.
@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},
volume = {46},
year = {2012},
pages = {231-259},
doi = {10.1051/ita/2012001},
mrnumber = {2931248},
zbl = {1279.68187},
language = {en},
url = {http://dml.mathdoc.fr/item/ITA_2012__46_2_231_0}
}
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) pp. 231-259. doi : 10.1051/ita/2012001. http://gdmltest.u-ga.fr/item/ITA_2012__46_2_231_0/
[1] and , Games and full completeness for multiplicative linear logic, J. Symb. Log. 59 (1994) 543-574. | MR 1276632 | Zbl 0822.03007
[2] , Non-wellfounded sets. CSLI Lecture Notes 14 (1988). | MR 940014 | Zbl 0668.04001
[3] and , Vicious Circles. CSLI Lecture Notes 60 (1996). | MR 1423600 | Zbl 0865.03002
[4] , and , Winning Ways. Academic Press (1982).
[5] , On Numbers and Games, 2nd edition (1st edition by Academic Press (1976). AK Peters Ltd. (2001). | MR 1803095 | Zbl 0972.11002
[6] and , Set-theory with free construction principles. Ann. Scuola Norm. Sup. Pisa Cl. Sci. 10 (1983) 493-522. | Numdam | MR 739920 | Zbl 0541.03032
[7] , , and , When not losing is better than winning : abstraction and refinement for the full μ-calculus. Inform. Comput. 205 (2007) 1130-1148. | MR 2340897 | Zbl pre05182185
[8] , Mathematics and games. Eureka 2 (1939) 6-8.
[9] and , Conway Games, algebraically and coalgebraically. Log. Meth. Comput. Sci. 7 (2011). | MR 2831240 | Zbl 1238.91041
[10] and , Games on Graphs and Sequentially Realizable Functionals, in Proc. of LICS'02. IEEE Computer Science Press (2002) 257-264.
[11] and , Complementation of Coalgebra Automata, in Proc. of CALCO'09. Lect. Notes Comput. Sci. 5728 (2009) 81-96. | MR 2557823 | Zbl 1239.68048
[12] and , A Tutorial on (Co)algebras and (Co)induction. Bull. of EATCS 62 (1997) 222-259. | Zbl 0880.68070
[13] , Remarques sur la théorie des jeux à deux personnes. Gaz. Sci. Math. du Québec 1 (1977).
[14] , , and , 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] , and , 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] , From Programs to Games : Invariance and Safety for Bisimulation, in Proc. of CSL'09 (2009) 485-496. | MR 1859464 | Zbl 0973.68040
[17] , Free μ-lattices. J. Pure Appl. Algebra 168 (2002) 227-264. | MR 1887159 | Zbl 0990.06004
[18] , Über mathematische kampfspiele. Tohoku Math. J. 41 (1935) 438-444. | Zbl 0013.29004
[19] , Infinite games and verification, in Proc. of CAV'02. Lect. Notes Comput. Sci. 2404 (2002) 58-64. | Zbl 1010.68504
[20] , Extensive games as process models, J. Log. Lang. Inf. 11 (2002). | MR 1909616 | Zbl 1003.03530