Re:Calculus of structures and sequent calculus

Hello,

sorry for being slow in answering.

At 11:51 +0100 14.2.05, Yves Guiraud wrote:
> > 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.
>
> Is it possible to have some insight on relation webs and "certain proof nets"?

Relation webs are simple to describe. They are the canonical 
representatives of equivalence classes of formulae modulo 
associativity and commutativity (and, optionally, unit equations).

To get a relation web, take all the atom occurrences in a formula: 
they are the nodes of the relation web of the equivalence class of 
the formula. Then, each couple of atoms/nodes stays in a logical 
relation, corresponding to the first common ancestor node in the 
formula tree; different logical relations correspond to different 
arcs in the relation web.

So, the relation web is a complete graph whose nodes are all atom 
occurrences of a formula. The graph is undirected in the case of 
commutative logical connectives. However, if you have noncommutative 
connectives, you can use directed arcs for those.

You can use relation webs as a basis of a semantics of proofs if you 
ask for certain properties. For example, suppose you have a relation 
web in which you can isolate two subwebs which are in a disjunction 
partition: this means that all nodes in subweb A are joined by 
`disjunction' arcs to every atom in subweb B. You could ask for 
something like

   `each upgrade of disjunction links in the partition to conjunction links,
    which leaves the relation web contractible and
    which does not disrupt cut elimination
    should have a corresponding derivation' .

Clearly, I have to tell you what `contractible` means and `does not 
disrupt cut elimination' means. Without getting into the details, 
suffice to say that these two properties are *locally checkable* in 
the relation web (this is actually fascinating, but it gets 
technical).

However, the point is that these locally checkable properties 
characterise an entire class of derivations you can make starting 
from the given relation web.

I started developing this in my paper `A System of Interaction and 
Structure', to appear in ACM ToCL and available from 
<http://iccl.tu-dresden.de/~guglielm/p/SystIntStr.pdf>.

So far, this semantics is not fully developed. I intended to do so, 
but then it happened that the switch rule scheme was already so 
powerful that we could develop all logics just by syntactic means, 
then Alwen found medial, then we got caught into cut elimination, and 
then a few years passed. So, we developed CoS, and we're very happy 
with it, but this is now almost over, and it's time for me to get 
back to relation webs. They will be very important for subatomic 
proof theory, where relation webs will be made out of units, instead 
of atoms.

Anyway, relation webs made possible two remarkable results:

1) They generated the rule schemes we use for all logical systems 
(what would have been extremely hard otherwise). In particular they 
tell you *why* all rules for binary operators operate on 
complementary couples, for a total of four subformulae. This is a 
deep property of contractible structures, and it's the secret of 
locality.

2) The semantics is powerful enough to tell you what is not provable. 
This was used by Alwen to show that his counterexample cannot be 
proved by shallow inference. For this fantastic paper, check 
<http://www.loria.fr/~tiu/deep.pdf>.

I always thought and I continue to think that reasoning in terms of 
formulae, i.e., trees, i.e. non-symmetric structures, is the cause of 
much trouble. If you see trees, you don't see where the interesting 
properties really are, they make you think in a way which is not 
local, not distributed.

Trees seem to be convenient because when you have a tree you have an 
easy structural induction, but people already squeezed everything 
they could out of these easy inductions. It's time to do a bit more 
sophisticated things!

OK. About `certain proof nets'. For this, I need a blackboard. I just 
tell you this. You can build nets out of relation webs. Suppose 
relation webs are slices in a tomography: their joining by `inference 
arcs' is the net. I think we can describe these nets with formalism 
B, but I never checked the details.

The next step would be to understand these objects *geometrically*. 
This would mean extracting and classifying shapes out of them. I 
suspect that some new algebraic topology has to be developed for 
that, as happened for concurrency algebraic/topologic semantics 
(Goubault et al.).

One thing is for sure: these objects are *bureaucracy-free* and 
*deductive*, which is one of the main objectives we have. They could 
then serve as concrete models for answering questions on identity of 
proofs.

> Speaking of syntax, I've find out that some people were rebuffed by 
> the notations (.,.) and [.,.] for usual connectives. Why use these 
> ones? Wouldn't be the systems clearer if the "old" ones were used 
> instead?

There are several reasons for using the new notation:


1) In deep inference, the accent is on the *shape* of inference 
rules, not on their *meaning*. The meaning comes out of all the rules 
of a system taken together. In other words: the switch rule is 
exactly the same in every deductive system, but in each case it deals 
with a different notion of conjunction/disjunction. If we used 
connectives, this idea would be blurred.

In the sequent calculus, people want to tell the difference between a 
multiplicative rule for ^ and the rule for linear logic's *. They are 
isomorphic but people want to tell you which logical system you are 
in.

In the case of CoS, we precisely don't want to do that, it would be 
misleading otherwise: a switch is a switch, and if you want 
contraction, you better add it separately. This stresses the fact 
that the algebraic composition of elementary rules is what matters, 
the sequent calculus tricks are possible but deprecated!


2) Structures are actually more similar to sequents than to formulae, 
because they stand for equivalence classes modulo associativity and 
commutativity (exactly like sequents). Now, in sequents you have 
commas separating formulae, and this is also what we have, it's 
pretty natural.


3) Deep inference rules don't branch and don't `eliminate 
connectives'. This means that if we connected formulae by bulky 
connectives instead of commas, we would have much more ink and 
confusion. I did some typographical tests with derivations we needed, 
replacing commas with connectives. The result was totally unreadable 
and ugly.


4) Connectives are perceived as connecting *formulae*, while we 
mostly want to connect *atoms*. Moreover, when people see a 
connective, they instinctively reach for the *root* connective. This 
is precisely what I want to avoid: the root connective has no special 
significance in deep inference.


As you see, all these reasons are psychological and aesthetical. It 
would be technically possible to use normal connectives, in some 
cases some of us did it. However, I believe that psychology is very 
important, especially when one wants to use these objects to discover 
new things.

> Then, when I first met Lutz, I had the feeling that CoS was, in some 
> way, an algebraisation of sequent calculus. What I mean is: I have 
> the feeling that CoS is a very good entry in proof theory for 
> mathematicians. Some evolution of CoS might be even better, but it 
> is already a much more mathematical object than sequent calculus 
> (and thus I prefer CoS, naturally!).

CoS *definitely* is more mathematical than the sequent calculus, it 
was done for being like that! I also can understand that algebraists 
and category theorists find it more natural than the sequent 
calculus, simply because everything in CoS is functorial.

However, I have the feeling that most people, including many 
mathematicians, are just happy with having some formal system that 
easily proves things and gives some sort of justification to informal 
arguing in English. For this, I don't think anything can beat the 
sequent calculus.

I mean: deep inference and CoS are for studying proofs; the sequent 
calculus does more, for example it can teach some syntax to people 
that don't know about category theory. Of course, it's not as good as 
CoS for studying proofs, that's clear.

> But here, there is maybe some concrete and objective way to compare 
> CoS and sequent calculus. The first question I have in mind is: is 
> there some kind of definition for the fact that a formal system 
> describes proofs in classical/linear/intuitionistic/etc. logic?

Of course. I'm not sure I get what you mean. If a system proves all 
and only the formulae of classical logic, its proofs are in classical 
logic.

At the present state of development of proof theory, formal systems 
are only matched against semantics of formulae, not semantics of 
proofs. This is clearly going to change, because computer science is 
pushing in favour of semantics of proofs, which is where the 
computational aspects take place.

> If so, this yields a way to separate formalisms from logics. And 
> thus to separate debates like CoS>sequents and linear>classical. 
> This is of interest for me, since I do not understand arguments in 
> the second one.

I agree with you that most of the arguments in favour of linear > 
classical are not convincing at all! Since you are in Marseille, you 
probably have somebody to complain about this just across the 
corridor.

I think that what happened with linear logic is that people tried to 
achieve objectives by fixing the logic instead of fixing the 
formalism. I mean: things like bureaucracy, absence of confluence, 
lack of locality, etc., are shortcomings of the *formalisms*, not of 
classical logic.

Instead, people took for granted the formalisms and tried to fix the 
logic. With hindsight, this is a mistake, it's like trying to reduce 
everything to Newtonian mechanics instead of going for relativity 
theory (due proportions made, of course).

However, that said, linear logic has been extremely important, also 
for deep inference. It certainly has been a revelation of many things 
to me.

> As I already said to Alessio, I have the analogy with universal 
> algebra in mind: there are many algebraic structures (groups, rings, 
> etc. ~ logics) and many objects to describe each one (operads, 
> Lawvere theories, 3-categories, etc. ~ formalisms).
>
> If this analogy stands, then I can see how to compare the properties 
> of two formal systems representing the same logic (like 
> 3-categories > Lawvere theories for commutative structures).
>
> But then, I don't see the point of the debate linear > classical 
> (are groups better than rings?)...

I agree with you: there are many formalisms, with many different uses 
and properties, and there are many logics, which differently capture 
aspects of languages and computation.

The two worlds are orthogonal and many debates are completely 
sterile. What matters are the properties, the theorems, etc.

I think ideology is *extremely* important for a scientist in order to 
find the motivations and the ideas. Research is not, in my opinion, 
going for mushrooms in the woods. It's a will power act driven by 
ideological convictions.

However, once you've got the results you wanted, you have to write 
your papers in such a way the everybody can understand them and as 
devoid of ideological bias as possible. Certainly one shouldn't be 
polemic or insulting! In the case of linear logic, Girard's ego 
succumbed to its own weaknesses in this respect.

I guess I'm sounding like a pompous old fart. Sorry! It's really what I think.

Okay, something I've read in the news: did you hear about that doctor 
in Lisbon that was able to convince his (girl) patients to stay naked 
in the balcony in order to have a mammography by satellite? THIS is 
genius!

> > 2) Finding reasonable, interesting and useful semantics of proofs;
>
> I don't really understand this one, since I've never understood what 
> is a semantic (is it a map preserving some kind of structure?). But 
> this is link to a question I've heard from a sequent calculus user: 
> is there any semantic for CoS, really different from proofs? (I do 
> not get the point here, maybe you can help me).

I don't think there is a definition of semantics. Broadly, semantics 
should be a `different way than syntax' of understanding things. And, 
also, syntax is operational/local, semantics is denotational/global.

Asking for a semantics for CoS is the same as asking whether there is 
a semantics for the sequent calculus. It means (almost) nothing.

An interesting question is whether there is a semantics of proofs 
for, say, system SKS, as there are semantics of proofs for many 
systems in the sequent calculus. This is now a very active area: 
Dominic Hughes, Francois Lamarche, Richard McKinley and Lutz 
Strassburger have now papers about this.

Let's talk about these things next week in Dresden.

> Thanks for taking some time to write it. Maybe some kind of >> 
> objective << comparison could be written between the two formalisms. 
> Stating all the known properties of each formalism for any logic, 
> together with the links between them, might be a good way to 
> convince sequent calculus addicts to (at least) take a look to CoS.

This might be an interesting thing to do. I cannot promise to do it 
myself: I started three months ago the web page on open problems and 
I'm barely halfway through!!

About the sequent calculus addicts: it depends on why they are 
addicted to it. If they like it for teaching, for example, I'd be 
happy to leave them with their addiction, because this is also my 
case.

If they think they can solve some of the interesting open problems in 
proof theory with it, then they'll have to change their mind. It's 
true that marketing is necessary, but I have to confess that I'm so 
fed up myself of doing it! I'm getting crazy with marketing, I 
couldn't imagine how much of it is needed. I thought in the beginning 
that having a good idea would have been enough. I've been sorely 
disappointed.

> By the way, I have another question. What can be said about cut 
> elimination in CoS (in the absolute, but also with respect to the 
> one of sequent calculus)? I kind of like the way it is described in 
> CoS (I mean as a factorisation of derivations, if I get the idea) 
> and would like to know if it's possible to express it as a local 
> computation on derivations.

Let's talk about this in person, we need a blackboard.

-Alessio