The n-Category Café

I was planning to spend some time this evening writing an account of how Dolan and Trimble’s work fits into the tradition of game semantics, linear logic etc. But I’ve realised I don’t quite understand what Dolan and Trimble are doing. It seems to me that there are some “holodeck strategies” which don’t correspond to elements of the free CCC.

Here’s an example. Sorry it’s so complicated: I’m not sure whether there is a simpler one.

Let $\alpha := X^{X\times X}$, and consider the game

$\alpha^{\alpha^{X^\alpha}}$

So that I can describe the strategy I have in mind, I’ll draw out the tree and label the moves:

    X   X
   a2\ /b2
      X
      |q2
      X
      | X    X
     x\ |a1 /b1
        X 
         \   X    X
        q1\  |a0 /b0
             X
             | q0

Now consider the following strategy:

q0 q1
q0 q1 a1 a0
q0 q1 b1 b0
q0 q1  x q2
q0 q1  x q2 a2 a0
q0 q1  x q2 b2 b0

(If player 1 plays q0, we play q1; if she then plays a1, we respond at a0, etc.) This is certainly a winning strategy, and I don’t see how it could correspond to any lambda term: the problem is that it exhibits non-local control flow, which isn’t possible in the pure lambda-calculus. In the usual innocent game models, strategies like this are excluded by a “bracketing” restriction, but Dolan and Trimble don’t appear to impose such a restriction.

Perhaps someone could explain where I’ve gone wrong.

These “Holodeck Games” and their strategies feel to me an awful lot like drawing Feynman diagrams for particles constrained to a tree, scattering off of (bad) consequences, and make me think of instantons. I wonder why…

(and I’m sorry about the google/planck/furlongs nonsense from before.)