Subject: Re:Deep cirquent calculus
Newsgroups: gmane.science.mathematics.frogs
Date: 2007-09-13 01:26:32 GMT (34 weeks, 3 days, 22 hours and 11 minutes ago)
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.