Comparing Focusing Strategies

by ivoysey

Any unfocused sequent calculus can induce multiple viable focused calculi. Trivially, if you take one focused version you can leave off some of the focus in the conclusions. For example, the synchronous rule for tensor in focused linear logic is usually given as

\frac{\Gamma;\Delta_1 \vdash [A] \qquad \Gamma;\Delta_2 \vdash [B]}{\Gamma;\Delta_1, \Delta_2 \vdash [A \otimes B]}

but there’s nothing wrong, per se, with taking the \otimes R rule to be

\frac{\Gamma;\Delta_1 \vdash A \qquad \Gamma;\Delta_2 \vdash [B]}{\Gamma;\Delta_1, \Delta_2 \vdash [A \otimes B]}

or the symmetric omission of focusing on the right premise, or even the degenerate

\frac{\Gamma;\Delta_1 \vdash A \qquad \Gamma;\Delta_2 \vdash B}{\Gamma;\Delta_1, \Delta_2 \vdash [A \otimes B]}

There are certainly more proofs of particular theorems either calculus than the normal one, and to someone who knows about focusing they’ll feel wrong, but both systems are sound and complete. In general, the result of this kind of transformation will still be both sound and complete with respect to the unfocused version:

  • The same soundness proof will probably still work, because soundness for focusing systems is usually quite easy to prove and amounts to just careful erasure and local contraction.
  • Completeness is always a little bit harder. Here, you have to wonder about the structure of proof of the premise that would have been in focus but now isn’t—if the bottom-most rule was a synchronous one, i.e. one that only applies to a focused sequent, you’ll need to refocus before you can apply it. You’ll be able to do that, because the polarities must match or else the synchronous rule wouldn’t have applied. If the bottom-most rule was an asynchronous one then, at least in the way Frank’s notes present focusing, there must be a blur before that rule is applied as we enter an asynchronous phase. Here, the unfocused premise is effectively the result of that blur, so we can just drop that bottom blur and then use the rest of the proof.

That’s all a long-winded, constructive, way of arguing that there are lots of possibilities—or at least more than one—for how to take an unfocused sequent and add focusing to it. Each small variation in what’s focused in the premise or conclusion of any one rule constitutes a different potential focused variant of the unfocused source; lots of them will be unsound or incomplete, but there’s at most finitely many choices.

So given multiple derived focused calculi from one original system, how do you pick between them? More importantly, how do we know that the standard focusing strategies that we feel good about are actually the right ones?

An experienced logician will be able to look at the source sequent and have a great intuition about what the focused version ought to look like. This is really annoyingly fuzzy, though. Even if we end up in the same place, it’d be much nicer to know why the one that feels right is optimal, in some formal sense.

I think the right way to do it is to argue almost combinatorially. The whole point of focusing, as described by Andreoli, is to make proof search easier by making the number of possible proofs of theorems small but not zero—that is the focused system is useless unless it’s complete with respect to the original. Therefore, the reasonable metric of quality for a focusing system is to know how much smaller the number of proofs of different theorems actually is.

I know how to do this  empirically for toy calculi. It’s not that hard to enumerate all the formulae with less than a certain number of connectives and then enumerate all the proofs of them in multiple calculi and count how many there are. I’d like to hack that up for some fragments of linear logic and see what the graph looks like.

I don’t know how to do it in a more principled way or in a way that scales to non-toy calculi or interesting theorems in the toy calculi; maybe looking at such graphs would help to think of it? I don’t even know if, for an fixed calculus, there’s a best-possible focusing strategy unique up to some sane notion of rule-equality under this metric.

I think you’d want to treat all focused proofs that are the same up to permutations of the asynchronous rules in unfocused phases as the same, though; if more than one rule applies in that situation, the choice of rule is effectively an implementation detail, and does not produce proofs that are meaningfully different. So once you identify those proofs, you’re really counting equivalence classes of the set of proofs of a given theorem under a given calculus; it’d be easy enough to add other properties to the equivalence relation as they arise.