Games for recursive types
<_author_search_(samson abramsky)>Samson Abramsky and <_author_search_(guy mccusker)>Guy McCusker
13 October 1994
We present results concerning the solution of recursive domain equations in the category G of games, which is a modified version of the category presented in [AJM94]. New constructions corresponding to lifting and separated sum for games are presented, and are used to generate games for two simple recursive types: the vertical and lazy natural numbers.
Recently, the game semantics" paradigm has been used to model the multiplicative fragment of linear logic [AJ94], and to provide a solution to the full abstraction problem for PCF [AJM94, HO94], where the intensional structure of the games model captures both the sequential and functional nature of the language. In the light of these results, it is natural to ask whether recursive types can be handled in this setting. Here we show that they can: for a wide class of functors ?, including all of the usual type constructors, the equation D ' ?(D) has a (canonical) solution. In fact we solve this equation up to identity, and the solution can be constructed in the usual way by iterating the action of the functor on (the object corresponding to) the empty type.
1 Games and strategies
We define here a category of games and (equivalence classes of) history-free strategies which is almost identical to that used in [AJM94], which goes on to define the linear logic connectives ? (tensor), ( (linear implication), ! (the `of course' exponential) and N (the `with' product). The co-Kleisli category for the comonad ! is then a model of intuitionistic linear logic. We do not give the details of these constructions here, merely presenting those definitions which are essential to the rest of the paper. In particular we define (, since it is central to the definition of the category.