Re: Term syntax for derivations in Deep-Inference systems

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

well, that's what I suggested in the first place (i.e. that's just equivalent to considering in 
typing rules the structures up to equations), but then the counter-example I mentionned applies and 
the subject reduction is flawed in the sense that applying the reduction rules unrestrictedly is 
unsound.
That's connected to the following fact: if I give you A (up to equation) and M, you would find it 
hard to choose a B such that A -M-> B, precisely because equations introduce some ambiguity about 
where the inference rules recorded in M are applied.

Anyway, I fully agree with you, I dislike this treatment of equations, but
1) that's this only way I see to restrict the reduction rules to sound cases (i.e. that satisfy 
Subject Reduction)
2) apart from proving theorems you can hide the symbols corresponding to equations and have the 
typing rules that you suggest
3) the syntax is just a step towards some proof-net formalism that will clearly deal with relation 
webs, so the problem will disappear anyway at some point...

Stéphane