Re: Term syntax for derivations in Deep-Inference systems

At 11:22 +0100 20.12.04, Steven Lengrand wrote:
> > 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...

OK Stéphane, I see your point: you want to deal 
with derivation normalisation in the term 
calculus, so you need to rely on `positional 
information' about the various terms. I think 
it's very neat and it provides a convenient 
language for dealing with most normalisation 
aspects we might be interested in. Clearly, in 
many cases, equations should be dealt with 
carefully, so it's probably better to have them 
as inference rules.

That said, your formalism will distinguish (M,N) 
from (N,M), for example. This is, in my opinion, 
a form of bureaucracy: being forced to choose a 
representative under commutativity. Technically, 
(M,N) and (N,M) might be both normal and there's 
no way to join them. The only solution is to 
consider everything under an equivalence relation 
including commutativity, and this step cannot be 
done in rewriting rules, of course.

In other words: I'm afraid that equations, when 
kept out of the door, might enter by the window. 
(This is why in CoS I bring them in since the 
beginning and `train the reader' to live with 
them...)

I've now read section 3 of your note: I think 
you're correct in spotting the problem of your 
rules with formalism B (whatever it is). The 
non-confluent example you mention shows (to me, 
at least) that the natural thing to do is 
considering inference rules as acting on 
derivations. In other words, I believe the 
problem stems inherently from the separation 
between structures and derivations.

Anyway, I do think that your approach for A is 
neat and very useful. As I told you already, my 
proposal is to write a paper about formalism A 
*before* tackling formalism B, and I think your 
typing rules should be part of the picture.

For Kai: it might very well be that your system 
is formalism B, it certainly looks like it is! I 
think you have or you'll have soon a nice 
definition. There a few things I have to digest 
still (BTW, why doesn't weakening introduce a 
generic derivation?). You clearly took the 
decision of defining negation on formulae only. 
Again, this is something I'd like to think more 
about.

In any case, the problems with equivalences apply 
to you, too, right? Everything should be defined 
modulo equivalence, right?

I'm suspicious of `proofs are types': it's true 
in a technical sense in your note, but what does 
that mean?? Are you taking it seriously or is it 
just a joke? To me, formalism B is a way of 
saying that Curry-Howard should not be taken too 
seriously, i.e., it's a coincidence, not a deep 
fact of nature. I'd be more than happy to be 
contradicted by a wonderful computational 
interpretation of B, but I think it won't happen. 
If this is so, types don't quite belong to the 
picture, here, or at least not in the usual sense.

-Alessio