Re: cartesian closed categories and holodeck games

[Dominic Hughes <dominic@theory.stanford.edu>]

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
>