RE: Re: Deep cirquent calculus

Dear Lutz,

Giving you some clarifications.

>> 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.

> I guess you mean balanced tautologies where each
> atom occurs once positive and once negative.

Tautologies where each atom has *at most* one positive
and *at most* one negative occurrence, and also
substitutional instances of such tautologies.

> Then, what do you mean by "capturing these objects"?

Capturing = axiomatizing (in some reasonable, natural
way).

> I am sure you are aware of the fact that testing
> such a formula for being a tautology is
> coNP-complete. So, you certainly do not have a
> polynomial proof system for them.

Sure not  polynomial. Just a proof system. Other
formalisms do not have that. Could you axiomatize
binary tautologies in CoS+extension? POINT 1 was
about expressiveness and not at all about proof
complexities, so coNP-completeness is irrelevant.

> No. That's the whole point of the extension, since
> there is nothing you can do to transform a formula
> consisting of only one atom.

Extend (disabbreviate) that atom to (large) A,
then transform A. This is what was meant.

> But I still claim that your sharing does exactly
> the same as the extension rule. This might not
> be entirely obvious when you look at Frege systems.
> But it is obvious when you look at CoS + extention.

Let us call *proof width* (in CoS) the maximal size of
formulas involved in the proof. And call *proof length*
the number of formulas in the proof. Sharing generally
allows us to reduce both width and length. Width is
reduced at the expense of merging identical parts in
formulas. And length is reduced at the expense of
merging identical steps in the proof (that could
otherwise have to be performed over an over again
within different occurrences of identical subformulas).
As for extension, it only reduces width, at the expense
of abbreviating large subformulas. Sure every
polynomial size cirquent can be represented as a
polynomial size formula, by introducing abbreviations
for all nodes of the cirquent and then indicating who
is whose parent/child. But this does not help when those
abbreviations have to be disabbreviated later to
perform transformations on (inside) them. Alessio
expressed very well what else I wanted to say:

Alessio Guglielmi wrote:
   "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."

> I don't think PHP is so "particular" in that respect.

Its particularity is that, morally, it only has a proof
breadth problem (in CoS without extension) but not a
proof length problem. Sharing is only used in it to merge
large identical parts in formulas, but not to merge identical
steps in the proof: no transformations are taking place
within shared components in that proof, which is quite
a “lucky case”.

Giorgi Japaridze
http://www.csc.villanova.edu/~japaridz/
________________________________________
From: owner-frogs-+VuHOhYSxa2v/2WfcVMNQPhqMcnVdK/bs0AfqQuZ5sE@xxxxxxxxxxxxxxxx 
[owner-frogs-+VuHOhYSxa2v/2WfcVMNQBAVNjQhY8rC@xxxxxxxxxxxxxxxxxxxxxxx] On 
Behalf Of Lutz Strassburger 
[lutz-TgEOGOHWQm0czSlqHMVBIP3zm4ADWneb@xxxxxxxxxxxxxxxx]
Sent: Sunday, September 16, 2007 12:29 PM
To: Giorgi Japaridze
Cc: Frogs-+VuHOhYSxa2v/2WfcVMNQPhqMcnVdK/bs0AfqQuZ5sE@xxxxxxxxxxxxxxxx
Subject: Re: [Frogs] Re: Deep cirquent calculus

Dear Giorgi,

On Fri, 14 Sep 2007, Giorgi Japaridze wrote:

>> This rule [extension] ... can simulate exactly the sharing or cirquents.
>
> Generally speaking, this is not so. Let me point out two things:

I am sorry, but I think that here we have something where we disagree.

> 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 guess you mean balanced tautologies where each atom occurs once positive
and once negative. Then, what do you mean by "capturing these objects"? I
am sure you are aware of the fact that testing such a formula for being a
tautology is coNP-complete. So, you certainly do not have a polynomial
proof system for them (otherwise you would be famous by now).

You should give some clarification.

> 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.

No. That's the whole point of the extension, since there is nothing you
can do to transform a formula consisting of only one atom.

> And iterating this effect might produce an exponential slowdown.

This is exacly the reason why "Frege + extension" is supposed to be better
than "Frege without extension"

> Well, one cannot rule out that there are some ways around, but at least
> this is not obvious.

Right. Nobody knows. But I still claim that your sharing does exactly the
same as the extension rule. This might not be entirely obvious when you
look at Frege systems. But it is obvious when you look at CoS + extention.

> 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.

I don't think PHP is so "particular" in that respect.

> 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?

Honestly, I do not care much about "traditional" vs "non-traditional", or
"analytic" vs "non-analytic". Alessio has mentioned some of the reasons in
his previous mail to that list.

All I am saying is that we should not insist on differences where in fact
we have only a slightly different syntax for the thing.

Ciao,
Lutz