Log in

No account? Create an account
Wrote up that idea I had a few days ago. Turned out quite cute I… - Notes from a Medium-Sized Island [entries|archive|friends|userinfo]

[ website | My Website ]
[ userinfo | livejournal userinfo ]
[ archive | journal archive ]

[Nov. 11th, 2015|08:16 pm]

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.