8 Sep 12:37 2007

### 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
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
```

11 Sep 17:11 2007

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

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

13 Sep 03:26 2007

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

```

13 Sep 07:00 2007

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

13 Sep 18:18 2007

### 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
```

14 Sep 04:48 2007

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

```

11 Sep 08:48 2007

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

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

14 Sep 22:35 2007

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

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

15 Sep 16:55 2007

### 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
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
```

16 Sep 00:22 2007

### RE: Re: Deep cirquent calculus

```Alessio, regarding your last posting - I see the things you talk about exactly

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