Re: Deep inference and speed-up in proof search

On Friday 13 August 2004 17:40, Alessio Guglielmi wrote:
> At 13:23 +0200 13.8.04, Lutz Strassburger wrote:
> >I would like to make some clarifying comments on Alessio's example.
> >
> >An important observation to make here is that the size of the
> >formulas Gn (that is the number of atoms in it)  is exponential in
> >n. That means that the size of any proof of Gn (if we count the
> >number of symbols) must also be exponential in n. We should
> >therefore measure the size of the proof wrt the size of Gn.
>
> Hey clarifier! The size of Gn looks quadratic to me. If we agree on
> this, the other comments you make on the size are also wrong.

Arghh! 
Sorry, I had the wrong class of formulae in mind...

> >>The secret of success here is, of course, the absence of branching in
> >> CoS.
> >
> >No.
> >In this particular example the branching is innocent. The evil is
> >hidden in the associativity and the commutativity. If you build in
> >associativity and commutativity for conjunction in the sequent
> >calculus, you can mimic the CoS proof, because then
> >
> >A3^B3 = ((c1 V d1) ^ (c2 V d2) ^ -c3) ^ ((c1 V d1) ^ (c2 V d2) ^ -d3)
> >       = (c1 V d1) ^ (c1 V d1) ^ (c2 V d2) ^ (c2 V d2) ^ -c3 ^ -d3
> >
> >and you can split this anywhere and not only at the conjunction
> >between A3 and B3.
>
> I also maintain my statement that the secret of success is CoS
> absence of branching. This is a moral statement, and we can disagree
> on this, but my reasons are as follow. What do you mean by `if one
> builds in associativity and commutativity in the sequent calculus'?
> You can't do that *precisely* because of the *branching* nature of
> conjunction in the sequent calculus.

You are right in the general case. All I was saying ist that in that 
particular example, the situation is special. 

> You can mimic my proof only *after* having transformed the original
> Gn formula into a suitable one. The only way you can do this by the
> sequent calculus (as we know and love it) is by using cuts (and I
> don't even enter into the business of assessing the complexity here,
> since the point is not using cuts).

Again, in general this is true. But in the case at hand all you need to do is 
dropping all the parentheses whenever you have nested conjunctions, as you 
actually did it. This is what I meant by "building in associativity".
However, as soon as there are more conjunction-disjunction alternations, it 
doesn't work anymore.
 
> But then, why not going ahead and build into the sequent calculus
> also some simplification mechanism, like distributivity laws? They
> would work well in this case.

Distributivity is duplicating stuff...

> If you think to all this business from the point of view of the
> subformula property, what you (should) see is that the sequent
> calculus would need the same notion that we have: instead of tearing
> apart pieces of formulae in branches, it would need to build new
> formulae from pieces of old ones. This is again, precisely, the
> absence of branching, and not just built-in associativity.
>
> Finally, my remark was (I thought obviously) about CoS: in computing
> the complexity *for CoS*, one has to take into account the cost of
> associativity, which, contrary to the sequent calculus, is hidden in
> the use of equations. I guess I'm not wrong if I estimate this cost
> to be at most linear in n (do you agree?), and so, it doesn't change
> the fact that we have an exponential speed-up.

You know that I agree with you on all these points. All I wanted to point out 
is that there are several sources of the speed-up wrt. the sequent calculus. 
And your example explores only a very little one.

-Lutz