headers
Alessio Guglielmi | 8 Sep 2007 12:37
Picon
Favicon

Macros and FAQ

Hi,

I cleaned up and extended my macros for formulae, derivations and now 
also atomic flows. They're available at 
<http://alessio.guglielmi.name/res/vl/>. They supersede the previous 
macros (DedStraker and earlier) but they're not compatible, because 
the cleaning up entailed some changes in their usage. If you want to 
see something fixed or implemented, please let me know.

Prompted by a referee, I wrote the below FAQ entry (for the page 
<http://alessio.guglielmi.name/res/cos/faq.html>). Comments always 
welcome.

BTW, I've had for a long time the intention to transfer the deep 
inference pages to a wiki, so that everybody can edit them and they 
don't look as personal as they look now. Tom has a prototype already, 
but, so far, I couldn't find the time to do the transfer. Hopefully, 
we will do it before the end of the year. In the meantime, please let 
me know if there are additions or corrections you want me to do.

Ciao,

-Alessio

The good properties of the proofs in the calculus of structures are 
obtained by an extensive use of hidden equalities; are you cheating?

No, we are not cheating. The equations are exclusively used in 
correspondence of invertible, linear inference rules. These inference 
rules do not alter the geometry of proofs, in the sense of relation
(Continue reading)

Permalink | Reply | 0 comments |
headers
Giorgi Japaridze | 11 Sep 2007 17:11
Favicon

Deep cirquent calculus

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
(Continue reading)

Permalink | Reply | 11 comments |
headers
Alessio Guglielmi | 13 Sep 2007 03:26
Picon
Favicon

Re:Deep cirquent calculus

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.
(Continue reading)

Permalink | Reply | 10 comments |
headers
Giorgi Japaridze | 13 Sep 2007 07:00
Favicon

Re: Deep cirquent calculus

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?
(Continue reading)

Permalink | Reply | 9 comments |
headers
Lutz Strassburger | 13 Sep 2007 18:18
Picon
Picon

Re: Re: Deep cirquent calculus


Dear Giorgi and Alessio,

Let me add, that in CoS, you can also have polynomial size proofs of PHP 
without using the finitary cuts that Alessio was mentioning:

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

Avoiding this cut is done by adding a different version of the extenstion 
rule as it is done in the paper by Paola and Alessio: 
<http://cs.bath.ac.uk/ag/p/PrComplDI.pdf>

The rule I have in mind is

    C{a_i}
    ------
    C{A_i}

(with the usual side conditions for the extension rule)

This rule can be used independently from the cut, and can simulate exactly
(Continue reading)

Permalink | Reply | 6 comments |
headers
Giorgi Japaridze | 14 Sep 2007 04:48
Favicon

Re: Deep cirquent calculus

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.
(Continue reading)

Permalink | Reply | 5 comments |
headers
Giorgi Japaridze | 11 Sep 2007 08:48
Favicon

Deep cirquent calculus

Dear all,

Just to advertise 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
(Continue reading)

Permalink | Reply | 1 comment |
headers
Giorgi Japaridze | 14 Sep 2007 22:35
Favicon

RE: Deep cirquent calculus

Woops, my apologies for multiple postings. Something funny is going on: posted (unsuccessfully) 4 days
ago, appeared only now.

Giorgi Japaridze
http://www.csc.villanova.edu/~japaridz/
________________________________________
From: owner-frogs@...
[owner-frogs@...sden.de] On Behalf Of Giorgi
Japaridze [giorgi.japaridze@...]
Sent: Tuesday, September 11, 2007 2:48 AM
To: Frogs@...
Subject: [Frogs] Deep cirquent calculus

Dear all,

Just to advertise 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
(Continue reading)

Permalink | Reply | 0 comments |
headers
Alessio Guglielmi | 15 Sep 2007 16:55
Picon
Favicon

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
(Continue reading)

Permalink | Reply | 1 comment |
headers
Giorgi Japaridze | 16 Sep 2007 00:22
Favicon

RE: Re: Deep cirquent calculus

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
(Continue reading)

Permalink | Reply | 0 comments |

Gmane