Re:Deep cirquent calculus

Hi Giorgi, and everybody,

I have a comment about the very interesting paper you announced yesterday.

Your notion of analyticity is: an inference rule is analytic if all 
what is in its premiss is also in its conclusion. Then you build 
analytic polynomial proofs for pigeonhole in the cirquent calculus.

My comment is that under this notion of analyticity it is easy to 
have analytic polynomial proofs of pigeonhole also in CoS. More: 
analytic CoS would p-simulate CoS, and so Frege, the sequent calculus 
with cut, etc.

It goes like this: take a polynomial proof of pigeonhole in the 
sequent calculus, with cut of course, but write it in CoS in the 
canonical way (branching is conjunction). Then, replace all cuts with 
their expansions only involving atomic cuts, i.e., do the typical CoS 
localisation. This transformation, in CoS, is local, and so 
polynomial.

Now, the atomic cuts you get are analytic (in your sense), and so you 
have analytic polynomial proofs of pigeonhole. In fact, you have cuts 
of this shape

   C(a ^ -a)
   --------- ,   where a appears in C{ }.
     C{f}

We call these cuts finitary cuts.

Note that the construction also works when the sequent-calculus cut 
instances introduce atoms that do not appear in the conclusion (what 
anyway is not the case for pigeonhole proofs, if I'm not mistaken). 
In fact, the resulting non-finitary atomic cuts can be easily 
eliminated by substituting true and false to the atoms they introduce 
and by propagating these along the proof.

You can find the details of this construction in the paper `A First 
Order System with Finite Choice of Premises', by Kai Bruennler and 
myself <http://www.iam.unibe.ch/~kai/Papers/FinitaryFOL.pdf>.

All this means that you cannot so easily make the point that (sharing 
in) cirquents provide for a speed-up over (non-sharing) formulae.

However, I agree with you that cirquents indeed seem more efficient 
than formulae, and that the cirquent calculus is more efficient than 
CoS, because in your pigeonhole proofs you don't use any cut, no 
matter how finitary.

So, the question is: what is a natural, general notion of analyticity 
that brings to light the speed-up that we want to observe?

There is a brief discussion of this point in Sect. 6.4 of `On the 
Proof Complexity of Deep Inference', by Paola Bruscoli and myself 
<http://cs.bath.ac.uk/ag/p/PrComplDI.pdf>. There, we suggest an idea 
for discriminating, based on asking for analytic rules to be local 
(the atomic finitary cut is not). Whether this idea might be 
applicable to the cirquent calculus, I don't know, as the calculus is 
too new for me and I don't feel very confident in my judgment.

What do you think?

Ciao,

-Alessio


At 3:11 PM +0000 9/11/07, Giorgi Japaridze wrote:
> Dear all,
>
> Just to announce the following paper:
>            
>                   Giorgi Japaridze
>              Cirquent Calculus Deepened
>
> Full text available at http://arxiv.org/abs/0709.1308
> A kind of marriage between (the earlier version of) cirquent calculus and CoS.
> Comments welcome.
>
>                  
> ABSTRACT. Cirquent calculus is a new proof-theoretic framework, whose main
> distinguishing feature is sharing: unlike the more traditional frameworks that
> manipulate tree- or forest-like objects such as formulas (Frege), sequents
> (Gentzen), hypersequents (Avron, Pottinger) or structures (Guglielmi),
> cirquent calculus deals with circuit-style  constructs called cirquents, in
> which children may be shared between different parent nodes. Among its
> advantages are greater efficiency, flexibility and expressiveness. The
> approach was born in "Introduction to cirquent calculus and abstract resource
> semantics" (Journal of Logic and Computation, v.16). That so far the only
> paper on the subject introduced cirquent calculus in a special, "shallow"
> form, where the depths of cirquents were limited to two. While the shallow
> version of cirquent calculus was sufficient to achieve the main goal of that
> paper --- taming the otherwise wild class of binary tautologies and their
> instances --- the paper also outlined the possibility and expediency of
> studying more general, deep versions of cirquent calculi. The present article
> contains a realization of that outline. It elaborates a deep cirquent calculus
> system CL8 for classical propositional logic and the corresponding fragment of
> the resource-conscious computability logic. It also shows the existence of 
> polynomial-size analytic CL8-proofs of the pigeonhole principle --- the family
> of tautologies known to have no such proofs in traditional systems.