I wonder if the late eighties and early nineties felt as exciting at the time as they look in retrospect for the logic community. I guess the answer is "yes" - I recall Bob Harper talking about one informal European workshop in that period where he was presenting LF, Girard was presenting linear logic, and maybe one of the uniform proofs people were presenting uniform proofs too? Maybe someone who's spending the summer in Pittsburgh can prod Bob into blogging about that meeting, it's a good story. (This reminds me, I need to add Bob's blog to the sidebar!).
Also: completeness of focusing via cut and identity
Speaking of uniform proofs: I've been fiddling for some time with this view of that the completeness of a focused sequent calculus can be proven more-or-less directly from the standard metatheory of the focused sequent calculus: cut admissibility and identity expansion. (The completeness of focusing, if you recall, is good for many reasons. It gives us logic programming, and it allows us to think in terms of synthetic inference rules in our logical frameworks.) Frank first observed this way back when, I cleaned up and Twelfed up his proof a long time ago and wrote up a version of the argument for ordered linear logic in a tech report recently. the main weakness of our strategy is that, in its current version, it doesn't deal with inversion on positive types, which is why I call it "weak focusing" instead of "focusing."
A recent MathOverflow question asked (in a slightly convoluted way) about the completeness of focusing with respect to a Prolog-like language. Since Prolog-like languages don't run into the problem with positive types, "our" strategy* works fine, so I used this as an excuse to finally write out the full argument in a setting that didn't have a lot of other extraneous stuff going on.
* I'd like to know if someone came up with this strategy before us!
Posts
No comments:
Post a Comment