A theory for game theories

Abstract

Game semantics is a valuable source of fully abstract models of programming languages or proof theories based on categories of socalled games and strategies. However, there are many variants of this technique, whose interrelationships largely remain to be elucidated. This raises the question: what is a category of games and strategies? Our central idea, taken from the first author's PhD thesis [11], is that positions and moves in a game should be morphisms in a base category: playing move m in position f consists in factoring f through m, the new position being the other factor. Accordingly, we provide a general construction which, from a selection of legal moves in an almost arbitrary category, produces a category of games and strategies, together with subcategories of deterministic and winning strategies. As our running example, we instantiate our construction to obtain the standard category of Hyland-Ong games subject to the switching condition. The extension of our framework to games without the switching condition is handled in the first author's PhD thesis [11]. © Springer-Verlag Berlin Heidelberg 2007.