Re:Calculus of structures and sequent calculus

At 11:24 +0100 11.2.05, Yves Guiraud wrote:
>"What are the benefits of calculus of structures with respect to 
>sequent calculus?" (and conversely)

First of all, I'd say the fair comparison is between CoS and the 
*one-sided* sequent calculus. It is possible of course to devise deep 
inference formalisms that would match with the sequent calculus in 
general, and what I'm going to say below wouldn't change.

Technically speaking, the one-sided sequent calculus has no benefits 
over CoS, simply because every proof in the sequent calculus can be 
isomorphically represented in CoS, and every deductive system in the 
sequent calculus can be faithfully designed in CoS, and all these 
translations are trivial.

That said, one has of course to show that there are technical 
advantages in moving to CoS. In addition to this, one also has to 
argue about possible psychological, or methodological advantages and 
disadvantages.

Let's start from the latter. Much of the psychological and 
methodological value of a formalism is of course a subjective matter. 
Just speaking for myself, I don't think, for example, that there is 
any advantage in teaching, say, the syntax of classical logic in CoS, 
to students who only have a mild interest in proof theory. I always 
refused to do it and I stuck to the sequent calculus and natural 
deduction.

I also find it very difficult to find inspiration in syntax, in 
particular in that of CoS, which is still very hard for me, despite 
being rather familiar with it. When I think about deductions, I think 
in terms of relation webs (which is my pet semantics) or in terms of 
certain proof nets which I have vaguely in mind.

As a matter of fact, when I started this business, CoS was only meant 
to be a by-product of semantics. I didn't suspect it would have had 
so much future and most of my plans were about developing relation 
web semantics. I started changing my mind on this only after seeing 
the very fast progress Alwen, Kai and Lutz were doing, mostly by just 
manipulating syntax.

CoS is still young, so it can only improve in its psychological and 
methodological helpfulness. In some cases, it's the only clean and 
simple way of presenting certain logics, like several modal logics 
and systems like BV and NEL, which can represent process algebras 
like CCS. In all these cases, the sequent calculus fails so badly 
that CoS has clearly a psychological advantage: at least you can 
write papers that can be read by normal people and not just expert 
cryptographers and Egyptologists.

I should mention the unquestionable fact that in any case the syntax 
of CoS is by far the cleanest available, and it's the only uniform 
one. *Each* of the tens of systems we produced so far wins the 
comparison with their sequent calculus counterpart in terms of 
elegance, conciseness, uniformity, etc. This has a psychological 
value of some sort, because at least you work with nice stuff. It 
might not be easy for those not used to CoS, but, as always, elegance 
has a price. I guess it's like learning to walk on high heels, or 
something like that.

All that said, there are huge *technical* advantages in moving from 
the sequent calculus to CoS if one is interested in certain 
proof-theoretic objectives. These objectives are actually all the hot 
ones, in my opinion; they are:

1) Getting rid of bureaucracy in proofs;
2) Finding reasonable, interesting and useful semantics of proofs;
3) Expressing `syntactically difficult' logics, also of interest in 
computer science;
4) Lowering the complexity of proofs;

and, arguably,

5) Finding efficient implementations.

We have now plenty of evidence and papers about 1-4, and very 
promising preliminary results about 5.

So, here we go, in order:


1) Bureaucracy. We all know that proofs in the sequent calculus have 
bureaucracy, of several different kinds. CoS *exposes* all the 
sources of bureaucracy, thanks to the possibility of using local 
inference rules. Since the inference rules operate on the minimal 
amount possible of information, all the big chunks of `logical 
material' that give rise to bureaucracy can be disintegrated.

In technical terms, one gets permutability and decomposition theorems 
that are provably impossible in any other existing formalism, 
including the sequent calculus. Based on this, we are designing new 
formalisms (called for now A and B) that completely get rid of 
bureaucracy, meaning that they exhibit bureaucracy-free proofs.


2) Semantics of proofs. I'm no expert in categorical semantics, 
however my feeling is that understanding semantics of proofs is not a 
purely abstract enterprise. I think one needs some concrete support 
model, which most likely is some sort of proof net. There are now 
several papers (by Lamarche, McKinley and Strassburger) that show 
that deep inference and CoS can provide such concrete models, or at 
least heavily inspire them.

One of my personal research objectives is to get to a formalism which 
I'm calling at present `deductive derivation nets'. I can't tell you 
much about the categories it lives in, and I don't think the 
algebraic topology needed to classify its proofs exists already. 
However, I can right now draw on the blackboard its proofs, and 
everybody would agree with me that they are deductive, there is no 
bureaucracy, and you can state and solve problems like identity of 
proofs therein.


3) Syntactically difficult logics. First of all, Alwen showed (in one 
of the most spectacular mathematical structures I've ever seen) that 
there are simple logics, like BV, that the sequent calculus cannot 
capture, simply because they require deep inference. The interest of 
BV and extensions is that they capture sequential composition in 
process algebras, something of obvious independent interest outside 
of proof theory.

Then, there are modal logics, like S5, which are notoriously 
difficult to express in the sequent calculus. In CoS, they get the 
most straightforward presentation conceivable, and get all the good 
properties like locality and cut elimination. Moreover, they do so in 
the usual uniform, elegant way, without having to resort to any extra 
machinery, like is often the case for the sequent calculus (certainly 
for S5, or should I say Mess 5).


4) Low proof complexity. Given that deep inference is more liberal in 
applying inference rules, proofs become much shorter than without 
deep inference. So, you get exponential speed-ups over the sequent 
calculus for many classes of tautologies, and in no case a worse 
complexity, given that you can mimic in CoS the sequent calculus. No 
paper out on this yet, but Paola and I are almost done on one that 
shows that CoS is better than any other formalism (not resorting to 
meta-tricks like Tseitin's extension, which are still applicable to 
CoS, though).


5) Implementations. Here, the problem is to fight nondeterminism, 
because in deep inference there are bags and bags of it. However, in 
deep inference we also have splitting theorems, which essentially 
give us a very powerful weapon against nondeterminism. Ozan showed me 
recently a class of systems in CoS which are extremely efficient in 
this respect *and still very elegant*. So it's now obvious that 
getting to efficient implementations is just a matter of time (and 
hard work!).


I hope I didn't forget anything. I should say that I wrote this very 
hastily (I'm much pressed for time, these days). Please send me 
comments and suggestions. Maybe we can turn this text into something 
to be put on one of our web pages?

Anyway, conclusion: my (certainly very biased and immodest) opinion 
on CoS vs sequent calculus is the following. I don't see CoS taking 
the place of the sequent calculus in elementary textbooks. However, I 
do think that CoS and deep inference will be more and more central to 
the development of (structural) proof theory in the next ten years, 
and I think they will become part of the classical landscape in the 
discipline very soon.

Bof,

-Alessio