October 23rd, 2006

beartato phd

(no subject)

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.
beartato phd

(no subject)

I found this half by accident looking for something to show arh006; it's got a pretty nice long bass solo over "Have you met Miss Jones":
http://youtube.com/watch?v=Cqm9FWXaOU8

Today I think I finally fixed my stupid logic programming HW 5, and did some silly but fun phantom types stuff with tom7. The takeaway idea is that you can get your index language to support first-order rewriting, if you don't mind putting in all the coercions yourself. The indexed type is exposed as a phantom type like type 'a foo = bar as usual, (where bar is the actual representation) and the things you use as indices are themselves elements of a type type 'a exp = unit, which has constructors exposed through a signature that express the allowable rewrites.

What we hacked up was a, ahem, proof of concept that you can, ahem, "do" higher-order rewriting too, by hacking up the first-order rewriting theory of S and K. It got sick very fast.