This "backtracking game" characterisation has been known since around '93-'94, in the work of Hyland and Ong: M. Hyland and L. Ong. On full abstraction for PCF. Information and Computation, Volume 163, pp. 285-408, December 2000. [Under review for 6 years!] ftp://ftp.comlab.ox.ac.uk/pub/Documents/techpapers/Luke.Ong/pcf.ps.gz (PCF is an extension of typed lambda calculus.) My D.Phil. thesis extended the lambda calculus (free CCC) characterisation to second-order, published in: Games and Definability for System F. Logic in Computer Science, 1997 http://boole.stanford.edu/~dominic/papers/ To characterise the free CCC on an *arbitrary* set {Z,Y,X,...} of generators (rather than a single generator, as you discuss), one simply adds the following Copycat Condition: (*) Whenever first player plays an occurrence of X, the second player must play an occurrence of X. [Try it: see how X -> Y -> X has just one winning strategy.] Although the LICS'97 paper cited above appears to be the first place the Copycat Condition appears in print, I like to think it was already understood at the time by people working in the area. Technically speaking, winning strategies correspond to eta-expanded beta-normal forms. See pages 5-7 of my thesis for an informal description of the correspondence. It sounds like you've reached the point of trying to figure out how composition should work. Proving associativity is fiddly. Hyland and Ong give a very elegant treatment, via a larger CCC of games in which *both* players can backtrack. The free CCC subcategory is carved out as the so-called *innocent* strategies. This composition is almost identical to that presented by Coquand in: A semantics of evidence for classical arithmetic. Thierry Coquand. Proceedings of the CLICS workshop, Aarhus, 1992. Dominic PS A game-theoretic characterisation with an entirely different flavour (winning strategies less "obviously" corresponding to eta-long beta-normal forms) is: Abramsky, S., Jagadeesan, R. and Malacaria, P., Full Abstraction for PCF. Info. & Comp. 163 (2000), 409-470. http://web.comlab.ox.ac.uk/oucl/work/samson.abramsky/pcf.pdf [Announced concurrently with Hyland-Ong, around '93-'94.] On Sun, 22 Oct 2006, John Baez wrote:
Dear Categorists -
This contains a popularization of Dolan and Trimble's work on game theory and the free cartesian closed category on one object. It also has links to more detais.
Best, jb
....................................................................
Also available as http://math.ucr.edu/home/baez/week240.html