Re: Deep cirquent calculus

Hello,

Paola and I wrote two pages about a definition of analytic rule that 
sets apart finitary cuts: <http://cs.bath.ac.uk/ag/p/Onan.pdf>. This 
is along the lines we suggested in our recent proof-complexity paper 
<http://cs.bath.ac.uk/ag/p/PrComplDI.pdf>. We are very interested in 
hearing your comments, both negative and positive. In case of a 
sufficient number of supportive comments, we would continue 
investigating this idea.

Just speaking for myself, I am skeptical that analyticity is really 
useful, because it seems to be too loosely connected with proof 
speed-ups: some non-analytic rules yield speed-ups, some don't, some 
are conjectured to do so, boh?

Also, the relevance of analyticity to proof search seems to me very 
dubious. It's literally true that a non-analytic rule like the atomic 
cut has an infinite choice of premisses, but, morally, the choice is 
to use some atom already present in the conclusion, or a new one, and 
it doesn't matter which one. So? It's morally a finite choice. Same 
for the substitution rule.

Maybe a different notion of analyticity could be more convincing?

At 05:00 +0000 13/9/07, Giorgi Japaridze wrote:
>Meanwhile, I have a question. What was your notion of analyticity 
>when calling analytic CoS "analytic CoS"?

Roughly, finite choice of premisses, but, as we point out in Section 
6.4, this leads to a somewhat unpleasant situation because the atomic 
finitary cut would be analytic, and so the thing becomes almost 
trivial.

However, I'm starting to think that the whole matter is indeed rather 
trivial in deep inference, and that perhaps analyticity is yet 
another artefact of shallow inference.

>Is there anything that makes the latter qualitatively more analytic 
>than cirquent calculus? (quantitatively, CoS is no doubt more 
>analytic by whatever measurement; but still not as analytic as 
>sequent calculus with its subformula property).

In this respect, I don't see any difference between CoS and deep 
cirquent calculus, neither qualitative nor quantitative.

Maybe you were saying that CoS is `more' analytic because the 
cirquent calculus compresses proofs more? If so, I think that the 
deep cirquent calculus probably has an exponential speed-up over CoS, 
but this is not due to anything related to analyticity, it's just the 
absence of repetitions in proofs, due to sharing in formulae. But I'm 
really confident about anything here.

I have a comment about the possibility of p-simulating deep cirquents 
by CoS + some extension. I cannot rule out entirely the possibility 
of this simulation by some extension, but I doubt that this can be 
Tseitin's extension; in any case this has to be really awkward (so, I 
agree with Giorgi and am sure that Lutz also agrees). That said, I 
think that the main point is not really to achieve the maximum 
speed-up `somehow', but to do it naturally.

In this sense, I see cirquents as a very welcome and natural 
improvement over formulae. Deep inference gets rid of trees in 
proofs, and cirquents get rid of trees in formulae. It was about 
time, there were too many trees around. The fact that the cirquents 
and deep inference fit together is also very nice.

In my opinion, we are a step closer to a geometric semantics of 
proofs, free from syntactic artefacts like trees.

-Alessio