Notes from a Medium-Sized Island [entries|archive|friends|userinfo]
Jason

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

[Apr. 24th, 2012|11:04 am]
Jason
 [ Tags | focusing, math ]

Here's a bit of math that I kind of expect only the people who read my ill-fated paper with Frank will care about, but here's the deal with it anyway:

The paper-with-Frank is about how a variety of (substructural, and also secretly some modal) logics can be very well-simulated (meaning: preserving the reduced nondeterminism imposed by focusing) by a fragment of first-order focused logic (with no fancy substructural stuff!) with just the negative connectives.

These notes are about how you can take the target language of that translation, and go even farther, still preserving the restrictions of the focusing discipline, down to a logic that isn't focused! The price you pay is just that you have to throw back in the positive connectives, and one funny "jumbo connective" Ux.A(x) that binds a first-order variable, and is equivalent to ∀x.A(x) ⇒ #(x), for a distinguished atomic proposition #.

 From: 2012-04-25 04:07 pm (UTC) (Link)
So is the point you can do ALL THE LOGICS in FF, and you can do FF in the "Target Language"? "Source" and "Target" aren't quite denoteful enough for me.
 From: 2012-04-25 06:07 pm (UTC) (Link)
Yeah yeah sorry.

"lots of logics" -> FF -> FOL+U

FOL+U is ordinary intuitionistic first-order-logic with the U connective.
 From: 2012-04-25 07:11 pm (UTC) (Link)
Do you think there's value/advantage to skipping the FF step? I kind of expected you to be doing that.
 From: 2012-04-25 07:35 pm (UTC) (Link)
I actually worked that out first, yeah.

It's debatable which way's better. I think the two-translation way is just barely edging out the one-translation in my mind right now, having seen both of them. The reason is that there are two warts of the overall translation, and the two-translation approach confines each wart to one of the two phases. The ALL THE LOGICS -> FF step involves the weird continuation-passing translation that you've already seen in the Ill-Fated paper. The FF -> FOL+U step has a pair of intertwined translation functions that do different things to a proposition depending on which side of the turnstile it's on. If you have One Monolithic Translation from ALL THE LOGICS -> FOL+U, it has continuations *and* intertwining, and it's hard to see what's going on all at once.
 From: 2012-04-26 12:36 am (UTC) (Link)
I buy it. Especially since I do consider the know-which-side-you're-on to be the larger wart, I guess.

So I guess my current take on the world is that focusing makes sense in itself, especially once you have polarities, so the story of just cut and identitying FF and then using that to prove focalization for FF is the one I'd lean towards to deal with FF. As I put it in the SF paper, "The cut admissibility and identity expansion lemmas for the focused sequent calculus are strong enough for the unfocused sequent calculus to inherit its metatheory from the force of the theorems in the focused setting."

What you're emphasizing here is something different and still-interesting-to-me, and something that goes back to the Focusing Linear Logic In Itself note - you're addressing the question of what's the minimum amount of stuff on top of extra logic you need to get the structure of focusing. Is that a reasonable take?
 From: 2012-04-26 12:41 am (UTC) (Link)
Yeah, the cut and identity proof for FF is really rather easy, and I buy that there's not a huge market for making it any simpler.

Stilllll I can't help but remain a tiny bit sketched out by the dot-dot-dotness of the identity proof, and it makes me feel nice to know there's another proof.

And yeah, I think I do care about "what's the minimum amount of stuff on top of extra logic you need to get the structure of focusing", and the answer (as far as I care) is essentially nothing. The answer is actually "the connective Ux.A(x)", but I think that is barely anything. If we're willing to not be scared by, say, negation as a first-class connective (despite the fact that it's definable from implication and false) we needn't be scared by this U.
 From: 2012-04-26 12:48 am (UTC) (Link)
Yeah, but Structural Focalization takes care of dot dot dot perfectly. See 2.3.3 and 2.3.4 of the one existing chapter for the clearest discussion I've written, but don't read past that because it's all wrong and I'm fixing it.
 From: 2012-04-26 12:53 am (UTC) (Link)
Oh right hm I totally forgot that development. I am super scatterbrained tonight.
 From: 2012-04-26 12:50 am (UTC) (Link)
That said, the separate observation that you need basically nothing to get focusing is very interesting to me as an independent point.
 From: 2012-04-26 05:27 am (UTC) (Link)
And yeah, I think I do care about "what's the minimum amount of stuff on top of extra logic you need to get the structure of focusing", and the answer (as far as I care) is essentially nothing.

I find myself somewhat depressed by this answer. Since Noam's thesis, I've been thinking of focusing as a good way to talk about effects intelligently. However, if all that's really going is a cunning quasi-CPS translation, since Ux.A(x) is morally ∀x. A(x) → #(x), then focusing fixes evaluation order and *nothing else* --- which means we are still as far from a type-theoretic account of effects as ever.

I mean, it's still great that we can specify evaluation order without also getting control operators (which is the problem with CPS), but I want more! :)