Re: Term syntax for derivations in Deep-Inference systems

At 2:40 +0100 5.1.05, Kai Brünnler wrote:
> 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.

Yes, I agree with you that weakening is a 
degenerate case, not involved with bureaucracy. 
Still, I think that for uniformity it should be 
defined in general.

The problem of reducing rules like contraction 
and weakening to atomic form still has a meaning 
in formalism B, so one better starts from the 
most general case and then goes through the whole 
spectrum, from derivations to atoms, I believe.

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

Are you sure you want to identify the two proofs 
in point 3? I don't see a reason why a proof with 
cocontraction should be assimilated to one with 
contraction. I see a reason when you transform 
derivation nets, but this should come later, it's 
beyond bureaucracy.

Anyway, negation is what is defined by the 
interaction rule, because this is the only place 
where you can observe it. This means that if you 
take the ordinary notion of duality-by-flipping, 
then how do you design interaction in such a way 
that it can be reduced to atomic form? What am I 
missing here?

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

This is very Lutz-esque. Give us a hint.

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

OK, it's the same.

> 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 see. Is there a reason?

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

What about `Giu` la testa!', like the Sergio 
Leone's movie about the revolution in Mexico. You 
play the Irish anarchist (James Coburn), I do the 
Eli Wallach character.

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

Yes, but that's the point! To me, it *could* mean 
that computation can only be observed when you 
have enough bureaucracy. I'm sure, for example, 
that German bureaucracy, like Conway's automata, 
is Turing-complete. Well, undecidable is for sure!

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

Well, you have a definition. I also have a 
definition since the beginning: close the set of 
derivations by inference rules which operate on 
them (plus all the usual trivialities). This is a 
perfectly regular definition, don't you agree?

When I say `we don't have a definition' I mean 
that we didn't settle/explore enough the little 
detail of being only able to define identity on 
structures instead of on full derivations. We 
still are unsure about this, but the rest looks 
pretty agreed upon to me, right?

Now, I didn't think much to it, but I'm really 
having pain imagining what a computational 
interpretation could be here, resembling anything 
we are accustomed to. Of course, as soon as you 
have any normalisation process that expands 
proofs considerably, you can always claim that 
that is computation. OK! But is that *meaningful* 
computation? That's the difficult question.

I mean, in Curry-Howard you have that 
normalisation corresponds to beta-reduction. I 
never thought very much about this (it's a 
coincidence!), but it is stunningly clear what 
kind of computation we deal with and it's also 
perfectly natural. In fact, beta-reduction has 
been defined independently.

Now, what are the chances that some *independent* 
mechanism corresponds to any of the 
normalisations possible in B?

If you want to have great fun, look at 
<http://www.419eater.com/html/samuel_eze.htm>.

-Alessio

Welcome_to_the_419_Eater.webloc
Description: application/applefile

Welcome_to_the_419_Eater.webloc
Description: application/applefile