Jason (jcreed) wrote,

Since it's the weekend, I'm chipping away at the backlog of not-immediately-work research ideas. Do I know how to have fun or what? Woo?

I finally wrote up "Focusing as Token-Passing", because it seemed to be important to clarify those ideas before moving on to the modal logic stuff I wanted to say, since understanding the innards of pfenning-davies box (resp. diamond, circle) seems to depend on really understanding the downshift (resp. upshift, [and again for circle also] upshift) contained within it.

It is a "theorems for cheap" sort of paper. Given "microfocused" connectives q⊗ and q⊸ (for an an atomic proposition q) whose right and left rules respectively demand the atom be in the context right now you can simulate all of focusing inside linear logic. Then you can prove all the theorems you want (cut-elim and identity for the focusing logic, completeness of focusing) and you can prove them internally by splicing together easy-to-prove propositional equivalence derivations. The real point is that even if the translations are a little involved, the proof is O(n) big in the number of connectives because it is modular, rather than O(n2) big, like other proofs that consider how different connectives interact. It also implements the ordered asynchronous context used in focusing without having any ordered contexts in the host language, by doing a little destination-passing trick.

I think of it as a sequel to "Focalizing Linear Logic in Itself". The main difference is that I don't sweep the asynchronous stuff under the rug here: the entire machinery of focusing can be faithfully simulated with token-passing. Also it's just a little bit less sloppy of a paper all around I think.

Turned out to be 13 pages even while I was trying not to be particularly unterse about it. Still not an unreadable length, I hope. I would super-appreciate comments. Especially if you think you should be able to make sense out of it because of the material (and really, I think this is anyone who knows linear logic and a is at least a little familiar with focusing) but are unable to because of the quality of the writing.
Tags: focusing, math, modal logic

  • (no subject)

    Had a disappointing time at climbing (although I nearly got a new V2), but a rousing good time at D's. The draft root beer may be a bit overpriced,…

  • (no subject)

    Had a decent if not spectacular time climbing. New successes were a V0+ and V1 inside the side cave. The V0+ in particular was something I'd been…

  • (no subject)

    Got some work done in the morning. Later went climbing with a ton of people. That V2 jump-start is still awfully fun. I'm getting more consistent at…

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded