(X × X → X) × X → X
Which in some sense represents the game tree
\/ \/In order to inhabit it, I have to make X, given (X × X → X) and X. My term-in-progress looks like λx.M, and I need to find M. My choices at this stage are plays in a game. Do I play (i.e. choose as the head of the term under the λ) (X × X → X) or X? Well, let's try (X × X → X). My term-in-progress is λx.(π1 x) <M',M''>. The fact that I have to build a pair to satisfy the arguments of the function I'm using corresponds to the adversarial nondeterminism of my opponent; I have to have a response no matter what she does! In this particular case, what type do M and M'' have to be? X. Crap! I can't build anything of type X, it's a base type. Or do I? Wait, I started out trying to build something of type X given some assumptions, which, since I'm working in intuitionistic logic not linear logic, I still have. Thus, if I can win the game at all, I can "win" it even once I've "lost".
So this game is of a peculiar sort that Doland and Trimble call a "holodeck game" where you can rewind back to earlier parts of the game tree. Alternatively, we're looking for "holodeck winning strategies" for an ordinary game.
In this particular case there is a short winning strategy, which I have deliberately not mentioned until now. It's going straight for the X in the second projection: λx.π2 x. The "holodeck" aspect of things means we could wedge this winning strategy into the points in that other partial strategy where we "lost": λx.(π1 x) <π2 x,π2 x> is also a winning strategy. The cute thing is that if I had written in the first place the type
(X & X -o X) & X -o X
instead, then "holodeck" strategies would be forbidden. The only winning strategy here is λx.π2 x. The holodeck aspect of intuitionistic logic is exactly the use of ! every other polarity switch to allow one player to rescind bad descisions by starting over at that save point - by invariant the context is always empty anyway whenever &s appear on the right, so !ing them doesn't make any difference.