Jason (jcreed) wrote,

John Baez's "Weekly Finds" article this week is right up my alley. It's essentially about construing the theorem-proving problem in the logic of implication and conjunction and one atomic proposition (equivalently, the inhabitation problem in the simply typed lambda calculus with only → and × types and one base type, equivalently the free CCC on one object) as a game in a way that seems different from most of the (not very many) papers I've read on game semantics. Take the type

(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.
Tags: games, linear logic, math
  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

  • 1 comment