Re: Term syntax for derivations in Deep-Inference systems

Hello,

we are living exciting times: the war to bureaucracy has been 
declared, also from normally neutral countries like Switzerland.

Since Frogs grew quite a bit as of late, I thought that in order for 
everybody to follow the developments I should make available some 
material about this war and its weapons. You can read the two notes:

    Formalism A: <http://iccl.tu-dresden.de/~guglielm/p/AG11.pdf>
    Formalism B: <http://iccl.tu-dresden.de/~guglielm/p/AG13.pdf>

in addition to Stephane's and Kai's. The one on formalism B is simply 
the message I've sent to Frogs last February (at that time the list 
was not archived on Gmane).

The idea is to free proof theory from bureaucracy and come up with a 
bureaucracy-free *deductive* formalism, where bureaucracy means 
`inessential syntactic details' (notice that regular proof nets are 
not deductive). The word `bureaucracy' comes, of course, from Girard, 
but the methods we use are simpler and more effective than the ones 
Girard uses.

Some time ago I suggested a two-step movement: from CoS to formalism 
A and from formalism A to formalism B. The picture right now looks 
like a sort of continuum between CoS and semantics:

CoS  <->  A  <->  B =? ded. proof nets  <->  proof nets  <->  Tarski

Each <-> maintains properties between formalisms: for example, if A 
normalises, then B normalises, and if B normalises wrt properties 
that A possesses, then A normalises too wrt to those properties. I 
think that the game of identity of proofs will be played in the 
deductive proof nets arena, and I also think that deductive proof 
nets are the concrete representation of formalism B (probably 
obtained from relation webs, which are the ideal concrete 
representation of structures).

I have some quick preliminary comments on the two notes by Stephane 
and Kai, but for serious comments I need some more time to think.

First of all, I think Stephane's idea of using type judgments for 
describing the new formalisms is absolutely excellent, especially 
because it is super-clean.

That said, I also think that there is a difference between concrete 
derivations and their description by typing rules. One of our goals 
is to come up with geometric objects corresponding to proofs: these 
objects will be `concrete derivations', and they are intrinsically 
much more complex to be found than typing rules. However, since 
finding them means knowing their properties, typing rules are 
probably our best key to get where we want.

Comment for Stephane: I instinctively dislike the idea of associating 
inference rules to equations. I also have better reasons than just my 
instinct, for example the fact that invertibility of rules should be 
invisible to geometry (one could object about contraction and 
interaction but I have counter-objections; it's a long story).

Much better, I believe, integrating equations in typing rules, like in

    A -M-> B   B = C   C -N-> D
    --------------------------- .
             A -M.N-> D

Is there any objection against this?

Comments for Kai: I still have to digest the very provocative title. 
I'll think about that.

You ask me whether I agree that your formalism is B. Ha! I gave no 
definition for B, and no name, how could I disagree? It looks like 
the main idea of B, i.e., inference rules operate on *derivations* is 
captured by your system.

There is one point, though, which makes me doubt a bit: you still 
need a distinction between formulae/structures and derivations, in 
the interaction rule. Pure B, whatever that is, should abolish the 
distinction, which means that we have to decide what is the negation 
of a derivation.

On the other hand, could be that your formalism succeeds in capturing 
and eliminating all bureaucracy without having to decide this 
difficult question. If this is so, it's very good, because we can 
postpone the decision until we know more.

Other comments as soon as I understand better, probably tomorrow 
night. Francois, what do you think?

-Alessio