### (no subject)

Dude, it's so much not that I mind that you're some weird guy in a obnoxiously space-filling puffy jacket and you decided to sit down next to me inexplicably in flagrant disregard of standard restaurant protocol and pester both me and subsequently the people on your left as if fuel and fuddle half-price is prime meeting-new-people time, in spite of the fact that I came there with a notebook of math to do and was as conspicuously as I could muster not making any eye contact or otherwise suggesting I wanted to make conversation with total strangers tonight.

What bothers me is that you smell like

In other news, the math to do worked out

In short, focusing is only about as complicated to prove correct as cut elimination is for a slightly expanded logic.

Anyway I plan to make a quick writeup of it tomorrow after my advisor meeting... there is still more programming to do before then in hopes of making a decent demo.

What bothers me is that you smell like

*poo*. And when you smell like poo, my sandwich tastes like it. I do not like that.In other news, the math to do worked out

*excellently*. I think I finally have answered (or at least gotten a reasonably sufficient partial answer to) a question that's been nagging at me for years: is there a suitably nice short syntactic proof of the completeness of focusing proof-search? Answer: yes! The proof takes a lovely scenic detour through a sequent calculus very close to Paul Levy's Call-By-Push-Value. The key idea (unless I messed up the quick check of the cut elimination proof, which I fear I might have) is a substructural judgment that is kind of a blend of cointuitionistic logic and lax logic; you can only have B lax on the left if you have some B' lax on the right, and moreover you can only have at most one B lax on the left at all. In such a restricted setting, you cannot even define tensor or lollipop: just ampersand, and unrestricted arrow. Basically (though I'm lying about disjunction) the connectives you can define coherently at that judgment are just the negative ones, and you can define all the positive ones at ordinary truth, and the completeness of focusing takes place*internally*in terms of a bunch of little bite-sized derivations in the system, and cut is the only thing of any difficulty to show, and even it is pretty straightforward.In short, focusing is only about as complicated to prove correct as cut elimination is for a slightly expanded logic.

Anyway I plan to make a quick writeup of it tomorrow after my advisor meeting... there is still more programming to do before then in hopes of making a decent demo.