Subject: Re: Deep cirquent calculus
Newsgroups: gmane.science.mathematics.frogs
Date: 2007-09-14 02:48:31 GMT (34 weeks, 2 days, 20 hours and 50 minutes ago)
Guten Tag (or bon jour?), Lutz. > This rule [extension] ... can simulate exactly the sharing or cirquents. Generally speaking, this is not so. Let me point out two things: POINT 1. Cirquents are generally more expressive and flexible than formalisms without sharing. For example, they allow us to capture binary tautologies that other systems fail to axiomatize (after all, it should be remembered that this was the original impulse for introducing cirquent calculus). I foresee that the ability to differentiate between shared and unshared nodes will become even more crucial when one tries to capture additive- and exponential-style (as seen in computability logic) connectives. E.g., semantically an additive gate shared between two parents is not the same as two separate additive getes (with the same content), one per parent. In the case of CL8, this is only true for terminals but not gates, which is accounted for by the presence of globalization and its dual, allowing us to merge or separate gates (but not terminals) at will. The same rule would have to be absent for additive gates. POINT 2. As for proof efficiency, here I again doubt that extension or substitution can fully simulate sharing. Imagine a large component A shared between n different parents in a cirquent. And imagine a given stage of a proof transforms (only) A. In cirquent calculus, such a transformation would have to be performed only once, within the single shared copy of A. But with substitution or extension (used to abbreviate A), without sharing, the identical transformation will have to be performed n times, once per each parent. And iterating this effect might produce an exponential slowdown. Well, one cannot rule out that there are some ways around, but at least this is not obvious. However, what you say is indeed true for the particular case of the pigeonhole proof given in my paper. Because there, by good luck, no transformations are taking place inside shared components, with such components being just "archival" ones. That is, sharing is used for reducing the otherwise exponential sizes of formulas (and this effect can indeed be simulated by extension), but not for reducing the number of steps in the proof which is polynomial anyway. Anyway, I was cautious enough in Section 7 to only say that the given pigeonhole proof illustrated a speedup over "traditional systems", with CoS+extension obviously not counting as such. That proof can apparently serve the cause of promoting not only cirquent calculus, but also promoting --- even if less directly --- CoS and deep inference in general. The quesion about whether my pigeonhole proof brings to light any moral differences between CL8 and CoS+extension, again, comes down to how one understands analyticity. Do you folks see CL8 as an analytic system? If not, what is that makes it non-analytic (as opposed to the analytic CoS)? And if yes, is CoS with extension or finitary cut also analytic? Or... perhaps it is time to forget analyticity altogether as an old-fashioned concept, meaningful only in the context of sequent calculus?