Subject: RE: Re: Deep cirquent calculus
Newsgroups: gmane.science.mathematics.frogs
Date: 2007-09-15 22:22:34 GMT (33 weeks, 5 days, 23 hours and 31 minutes ago)
Alessio, regarding your last posting - I see the things you talk about exactly the same way as you do. Thanks for your comments. > 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. The concept Paola&Alessio are suggesting appears to make sense in its own rights, and also deems analytic exactly the systems (after some trivial modifications) that we have been calling "analytic", including CL8. But is the name "analytic" best for it? Some word containing the substring "finit" might be more adequate. By the way, "finit". It is a desirable property because it binds the breadths of proof-search trees. However, if the depths of those trees remain unbounded, there is no point in caring about breadths. The suggested finitarization of the = rule reduces breadths at the expense of depths. Note that in cut-free sequent calculus depths are bounded, as long as contraction is used "reasonably" i.e., only before using &-introduction, to just make sure that each branch of the proof tree gets its own copies of side formulas. Now I want to go even farther and question the legitimacy of calling contraction an analytic rule. Something inside me is telling me that this is wrong. Because contraction does introduce some new material into the premise, even if only in the form of new copies of old stuff. Yet, this non-analytic behavior of contraction is not noticeable in sequent calculus, because, when used "reasonably" (in the sense explained above), contraction, while introducing new material if you look at the whole proof tree, does not really introduce any new material from the perspective of any particular branch of that tree. But in CoS, where all branches are combined within one formula, contraction loses its analytic innocence. As for cirquent calculus, it simply does not have contraction. And so, how about this suggestion: let us say that a rule is analytic if all terminals of the premise are also present in the conclusion. This makes CL8 analytic and, at the same time, the rules of cut (whether atomic or not, whether finitary or not) or coweakening non-analytic. Notice, my suggestion talks about *terminals* rather than *atoms*. Remember that the same atom may be sitting at different terminals. Well, this is just an impulsive thought, it may or may not turn out to be one worth pursuing. Giorgi Japaridze http://www.csc.villanova.edu/~japaridz/ ________________________________________ From: owner-frogs@... [owner-frogs@...sden.de] On Behalf Of Alessio Guglielmi [A.Guglielmi@...] Sent: Saturday, September 15, 2007 10:55 AM To: Frogs@... Subject: [Frogs] 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