Re: Term syntax for derivations in Deep-Inference systems

Alessio Guglielmi wrote:

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

Yes, I defined weakening on formulas, not on arbitrary derivations. 
Contrary to, say, contraction, defining weakening on derivations does 
not reduce bureaucracy. At least I don't see how. But it's perfectly 
possible to define weakening on derivations and could be more uniform to 
do so.


> You clearly took the decision of defining negation on formulae only. 
> Again, this is something I'd like to think more about.


Ah, my fault, it's not clear from what I wrote. No. Negation is not only 
defined on formulas, but on derivations (namely as the dual derivation, 
as usual in Cos). The negation of a formula is just a special case of 
that. I took the decision to define identity and cut on formulas only, 
and not on derivations. But that's just a start. In the end I want to 
define them on derivations in order to get rid of even more bureaucracy. 
See point 3 of "stuff to do next".

... and I think I just found out how! I'll update the note as soon as I 
find time.


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


No. No equivalences. I define connectives on multisets of derivations 
which takes care of associativity and commutativity. I drop the 
equations for the units and add them as rules. In the general 
(non-atomic) system only one rule enters: t_. In order to reduce rules 
to atomic form we'll need to add one or two more rules like t_.


> I'm suspicious of `proofs are types': it's true in a technical sense 
> in your note, but what does that mean?? 

Boh?

> Are you taking it seriously or is it just a joke?

I did not choose the title so much for the pun. I simply couldn't think 
of a title that's more to the point.

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

To me, formalism B is very different from natural deduction and thus, as 
it is, says nothing at all about Curry-Howard.

> I'd be more than happy to be contradicted by a wonderful computational 
> interpretation of B, but I think it won't happen.


You're saying that there won't be a computational interpretation of the 
thing before we have even defined the thing...

Hmmm, anyway: typing programs by programs. Has anyone ever heard of 
something like that?


> If this is so, types don't quite belong to the picture, here, or at 
> least not in the usual sense.


I think it's too early to say.

-Kai