Deep inference and speed-up in proof search

[Dale, Raj, Roy, this is one of things I didn't find time to talk you 
about in our recent meetings.   -A.]

Hello,

we started to address one of the obvious points about deep inference: 
the speed-up. There are two places where the use of deep inference 
can lead to lower complexity: complexity of cut elimination and 
complexity in proof search. In both cases the greater liberality of 
deep inference rules is advantageous.

In this email I will make the point about proof search: deep 
inference provides for an exponential speed-up in the size of proofs 
wrt shallow inference. In many important cases, the complexity passes 
from being exponential to being polynomial (with low exponent).

The big picture is the following:

- with shallow inference one has (seemingly!, relatively!) low 
nondeterminism and long proofs;

- with (uncontrolled!, naif!) deep inference one has high 
nondeterminism and short proofs.

Of course, the goal is to show that in the more liberal framework of 
deep inference one can develop techniques which drastically cut down 
on nondeterminism and still find short proofs (something like a deep 
version of Dale's uniform provability, for example). To this purpose, 
I remind you that very successful techniques like resolution are 
immediately available with deep inference, contrary to what happens 
in shallow inference.

In any case, a preliminary technical point we should make is to show 
that the proofs available in deep inference are indeed shorter than 
those available with shallow inference. Of course, miracles are 
unlikely, so, since it's reasonable to believe that NP /= coNP, we 
cannot reasonably hope for polynomial-size proofs in all cases. But 
we can of course hope for *exponential speed-ups* wrt to other 
deduction formalisms, which we do get!

This area is very active. In general, people study classes of 
tautologies and try to establish bounds on the size of their proofs, 
in systems with and without cut. One of the most studied such classes 
of tautologies is derived from the pigeonhole principle. For these 
formulae, in shallow inference, proofs with cuts can be polynomial 
(result by Buss), while proofs without cuts must be exponential 
(result by Haken).

Lutz told me that he has a result in which he proves that in cut-free 
CoS (system KS, I presume) there are polynomial-size proofs for 
pigeonhole tautologies. I didn't see the proof, but he told me it's 
rather intricate (what is to be expected because pigeonhole is 
devilish). Below, you'll find instead a *simple* argument which 
proves the same for another, less glamourous class of formulae, 
studied by Richard Statman, which has the same properties of 
pigeonhole for our purposes here: cut-free-shallow/exponential, 
with-cut-shallow/polynomial, cut-free-deep/polynomial.

In an upcoming update to an old note I wrote, I will show how *every* 
with-cut-shallow proof can be transformed into a deep-inference 
proof, in system SKS, whose complexity is the same (as a function of 
the size of the conclusion) and which only adopts a finite-choice 
version of the cut rule. In this case, the cut rule behaves like a 
contraction: it completely loses the infinitary character that makes 
it unimplementable for proof-search.

For now, I will show below how the Statman class of tautologies 
receives fair polynomial treatment by CoS system KS. It's a rather 
simple example that makes the point in a striking way. I'm thinking 
about adopting it as a standard way of introducing CoS, for example 
at my course at ESSLLI.

Ciao,

-Alessio


POLYNOMIAL CUT-FREE PROVABILITY OF A CLASS OF TAUTOLOGIES
---------------------------------------------------------

We start from propositional variables ci and di, for i >= 1.  We then
define:

          k
    Fk = /\ (cj V dj) ,   for k >= 1 ;
         j=1

    A1 = c1 ;
    B1 = d1 ;
    ...
    A{i+1} = Fi -> c{i+1} ;
    B{i+1} = Fi -> d{i+1} ;

    Gn = ((A1 V B1) ^ ... ^ (An V Bn)) -> (cn V dn) .

For example:

    G1 = (c1 V d1) -> (c1 V d1) ,

    G2 = ((  c1 V d1)          ^
          (((c1 V d1) -> c2) V
           ((c1 V d1) -> d2)
          )
         ) -> (c2 V d2) ,

    G3 = ((  c1 V d1
          )                                  ^
          (((c1 V d1) -> c2) V
           ((c1 V d1) -> d2)
          )                                  ^
          ((((c1 V d1) ^ (c2 V d2)) -> c3) V
           (((c1 V d1) ^ (c2 V d2)) -> d3)
          )
         ) -> (c3 V d3) .

One can easily check that, for n >= 1, the formulae Gn are tautologies.
The semantic argument for showing this is straightforward and amounts to
checking the chain of implications

    (c1 V d1) -> ... -> (cn V dn) ,

from left to right.

In the sequent calculus, the size of proofs of formulae Gn grows
exponentially, if cuts are not allowed.  In order to get an intuition
about this, consider G3 and the one-sided sequent one immediately
obtains from it:

    |- -A1 ^ -B1 , -A2 ^ -B2, -A3 ^ -B3 , c3 , d3 ,

which can be expanded to

    |- -c1 ^ -d1                     ,
       (c1 V d1) ^ -c2 ^
       (c1 V d1) ^ -d2               ,
       (c1 V d1) ^ (c2 V d2) ^ -c3 ^
       (c1 V d1) ^ (c2 V d2) ^ -d3   ,
       c3 , d3 .

The following is a possible proof, of which one branch is shown in part
(all the others are similar):

                                   .
                                   .
                                   .
    ----------------------------------------------------------------
    |- -c1 , (c1 V d1) ^ -d2 , (c1 V d1) ^ (c2 V d2) ^ -c3 , c3 , d3
                   =
        |- -A1, -B2, -A3, c3, d3
        ------------------------
                   .                           .      .      .
              .    .    .                        .    .    .
                .  .  .                            .  .  .
                  ...                                ...
    --------------------------------   --------------------------------
    |- -A1, -A2^-B2, -A3^-B3, c3, d3   |- -B1, -A2^-B2, -A3^-B3, c3, d3
    -------------------------------------------------------------------
    |- -A1^-B1, -A2^-B2, -A3^-B3, c3, d3

Clearly, for Gn there are 2^n branches.  Statman [*] proved that in a
cut free system the size of proofs always grows exponentially with n.

This is not the case if we allow the cut rule, because in this case we
can exploit the fact that all sequents

    |- -Fi , -A{i+1} ^ -B{i+1} , F{i+1}

are provable with bounded complexity proofs, and then join them together
by using cuts, what is linear in n.

In the cut free CoS system KS, there are linear proofs.  I show just
an example for G3 but the general pattern is the same (the syntax below
is the CoS one):

                  t
      i_ -------------------
         [(-c3,-d3) , c3,d3]
    2*i_ ------------------------------------------------
         [([c2,d2,(-c2,-d2)],-c3,[c2,d2,(-c2,-d2)],-d3) ,
          c3,d3]
     2*s ------------------------------------------------
         [(-c2,-d2),(-c2,-d2) ,
          ([c2,d2],-c3,[c2,d2],-d3) ,
          c3,d3]
    1*c_ ----------------------------
         [(-c2,-d2) ,
          ([c2,d2],-c3,[c2,d2],-d3) ,
          c3,d3]
    4*i_ ----------------------------------------------------------------
         [([c1,d1,(-c1,-d1)],-c2,[c1,d1,(-c1,-d1)],-d2) ,
          ([c1,d1,(-c1,-d1)],[c2,d2],-c3,[c1,d1,(-c1,-d1)],[c2,d2],-d3) ,
          c3,d3]
     4*s ----------------------------------------------------------------
         [(-c1,-d1),(-c1,-d1),(-c1,-d1),(-c1,-d1) ,
          ([c1,d1],-c2,[c1,d1],-d2) ,
          ([c1,d1],[c2,d2],-c3,[c1,d1],[c2,d2],-d3) ,
          c3,d3]
    3*c_ -------------------------------------------- .
         [(-c1,-d1) ,
          ([c1,d1],-c2,[c1,d1],-d2) ,
          ([c1,d1],[c2,d2],-c3,[c1,d1],[c2,d2],-d3) ,
          c3,d3]

The secret of success here is, of course, the absence of branching in CoS.

Remark: to be precise, one has to be more careful than I was with
parentheses and associativity; however, in all the arguments above, the
substance would not change.


[*] R. Statman.  Bounds for proof-search and speed-up in predicate
calculus.  Annals of Mathematical Logic, 15:225-287, 1978.