Jason (jcreed) wrote,

Wrote up that idea I had a few days ago. Turned out quite cute I think! I asked around and maybe it's not actually already a well-known result. The standard phase semantics for inutitionistic linear logic seems to involve a closure operator standing in for the \bot\bot of classical phase semantics. So what focusing is doing is exactly splitting that closure operator (i.e. monad) into a galois connection (i.e. adjunction). It's nothing new to me that upshift and downshift are sorta adjoint somehow, but the phase semantics makes it really obvious --- and I wasn't familiar until recently with the fact that there was a semantic appearance of the corresponding monad. (Because I have traditionally been super ignorant of anything to do with semantics)

But... viewed semantically, I like that focusing appears to simplify an existing mess, (or at least all of the mess is carefully tucked away in the shift operators) in contrast to the proof-theoretic case, where it makes the proof system a bit more messy (but in a way that has obvious benefits). If Andreoli hadn't figured it out from the angle of optimizing proof search, I feel like you'd still want to have invented focusing just to clean up the phase semantics.

Of course the really weird thing to me is that by doing semantics at all, I'm working in the ambiently classical world of set theory --- and basically the identical set of "semantic" clauses give the same result of capturing ILL when I interpret them proof theoretically, i.e. in an ambiently intuitionistic world. My best guess is that the foralls in the definition of the shifts are hiding what's effectively a forall over kripke worlds.
Tags: math

  • (no subject)

    Something that's bugged me for a long time is this: How many paths, starting at the origin, taking N steps either up, down, left or right, end up at…

  • (no subject)

    Didn't sleep well. Long day of work. Dinner with akiva at hanamichi.

  • (no subject)

    K was going to do a thing for her dad's birthday, but scheduling kept slipping and slipping so I guess we're going to try doing it tomorrow instead.

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded