Subject: Re: Deep cirquent calculus
Newsgroups: gmane.science.mathematics.frogs
Date: 2007-09-13 05:00:49 GMT (34 weeks, 3 days, 17 hours and 59 minutes ago)
Hi, Allessio. > Your notion of analyticity is: an inference rule is analytic if all > what is in its premiss is also in its conclusion. > My comment is that under this notion of analyticity it is easy to > have analytic polynomial proofs of pigeonhole also in CoS. Actually I did expect such a comment, and I agree with you. What Subsection 6.1 says about analyticity was not meant to be a definition but it sounds like one. The wording apparently has to be changed yet I do not know how. Meanwhile, I have a question. What was your notion of analyticity when calling analytic CoS "analytic CoS"? 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). I have not thought enough about this, there may be a good answer here which I am eager to hear. > 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? Yes, I have seen it. And I am sure CL8 (more precisely, its easily obtainable local versions mentioned in Subsection 6.2) should pass that test for analyticity. Analyticity badly needs a good definition, and I would be excited to see your Sect.6.4 suggestion elaborated and recognized.