Re: Wires and pipes

At 12:13 +0100 18.3.05, Lutz Strassburger wrote:
> On Thu, 17 Mar 2005, Alessio Guglielmi wrote:
> > Wired deduction is the realisation of a formalism which:
> >
> > 1  gets rid of associativity- and commutativity-bureaucracy;
> > 2  gets rid of type A and type B bureaucracy;
> > 3  does not generate non-canonical derivations for these forms of 
> > bureaucracy;
> > 4  it is deductive (in the sense that checking soundness is linear 
> > in the size of the proof, or, if you prefer, checking soundness is 
> > local);
> > 5  it is geometric (in the sense that it relies on graphs and 
> > normalisation can be defined locally).
>
> OK, if you ask only for these 5 points, wired deduction seems to 
> work (modulo the technicalities that I did not check)
>
> However (and this reminds me of (1) and (2) in your other mail), 
> from the "moral" point of view, I would also ask for
>
> 6  it contains all the information that is "essential" for the proof.
>
> Of course, we have to clarify what "essential" means. I do not have 
> the complete picture myself, but I strongly believe that at least 
> the following two points should be contained:
>
> (i) for each atom one can see how often it is used in the proof.
>
> (ii) for each use of an atom one can see what happens to it, i.e., 
> it is indicated which other atom is the killer.
>
> Of course, this is purely ideological, and you can disagree.
>
> All my objections to your wired deduction come in when it does not 
> meet (i) and (ii) above.

Well, the information about (i) and (ii) above *is* present in a 
wired deduction derivation: just follow the wires!

Notice that *nothing* is forgotten about a proof apart from what is 
necessary to reach objectives 1 and 2 about bureaucracy.

What am I missing here?

> I think we can say that this is the *one* point where we disagree.
>
> > I have three mystical reasons for this choice:
> >
> > 1  it is conceptually pure, and so very appealing to me;
> > 2  it sets the bar very high, but (apparently) not impossibly high;
> > 3  it is perfectly in line with `subatomic proof theory'.
> >
> > The best thing anybody can do about these opinions is to be 
> > skeptical, and maybe even consider them pure crap. This is better 
> > for me, too: I want to be challenged on this.
>
> From these three points only 3 counts as an argument for me. I don't 
> see why it sets the bar higher, and its "pureness" is questionable.

It sets the bar higher because it is not obvious that all logics can 
be expressed in wired deduction! For example, I don't know whether I 
can do linear logic, although I think it should be possible.

It is possible to do everything one does in CoS, in *nonlinear* wired 
deduction, *provided* systems have a completely atomic/local 
presentation. For example, MELL is a problem for the definition I 
posted: you can get it only by relaxing my definition a bit.

Of course, the purity is questionable, being a moral concept. My 
choice (like I do in subatomic logic) is to only consider primitive 
the logical units laws, like in (R t) == t. There are two ways of 
dealing with this: 1) you consider every wire (so, every relation web 
node in every slice) as subject to the law, or 2) you consider the 
law as only applicable globally.

1 does not lead to any geometric model, while 2 does it naturally. 
So, my choice here is compulsory, and, arguably, very pure! Of 
course, doing 2 does introduce a bit of bureaucracy on its own (I 
consider it the price to pay), but it is a mild price, because this 
bureaucracy is the easiest to get rid of: just move the units 
management down and forget about it.

You do realise that you do exactly the same in your nets, do you? You 
just push this aspect up in the net, instead of down.

> > This is perfectly possible also in wired deduction:
> >
> >       ( ([A a] [B    a])    t  )
> >     s    =|==\==|    |==\=  |
> >       ([( |    [|    |]) a] |  )
> >     s    =|=====|====|=  |  |
> >       ([( |     |)   |   |] |  ) .
> >     s    =|     |====|   |==|=
> >        [( |     |) ([a   a] t)]
> >   2c_     |     |   -|---|--|-
> >        [( A     B)   f   f  a ]
>
> This looks very weird to me and I have to think about it in order to 
> make constructive comments.

You can forget about the f's and the t's, move to nonlinear wired 
deduction, and it is completely isomorphic to the regular case, 
without bureaucracy, of course.

> > Yes: the ww_ rule is completely wacky! As I said above, it would be 
> > perfectly possible in wired deduction to substitute it with the 
> > innocuous one:
> >
> >        f
> >   aw_ -|- .
> >        a
> >
> > This would eliminate all problems of `horrible duplications' that 
> > Lutz points out.
>
> No. the dupplication appears when you introduce the f, what you 
> still have to do with this rule.

No. Of course, you also have to introduce rules for the missing 
equations: just do what you would do in KS and you'll be exactly as 
fine.

> > 2  I'm using ww_ in KSw because it allows me to *get rid of all 
> > unit equations* (i.e., of all equations that have no direct 
> > relevance to bureaucracy) and still simulate KS. Maybe there is a 
> > better way of doing so, but I couldn't find one (it's an 
> > interesting Rubik's kind of puzzle, if you have an hour in the 
> > dentist's waiting room.).
>
> I don't get the point. What do you mean by *get rid of all unit equations*?

For example (f f) == f. Just look at the rules r1--r8: these rules 
manage to do what the KS unit equations I want to get rid of do.

> Btw, wouldn't it be more sensible to use less weird rules like
>
>  ( R t )
> ---|-|---
>  [ R f ]
>
> (which is still weird because of the wire from t to f, but less 
> weird than having the need of duplicating a proof for going from R 
> to [R,f].)

It depends on what you want to do! I don't know whether this rule 
could get rid of the equations in the sense I specified above.

> > 3  The rule ww_ comes straight from subatomic proof theory, and it 
> > magically works. (I don't count this one among the things you 
> > should consider.)
>
> I told you already that I don't believe in magic.

It's a pity, because most art comes from believing in magic. At 
least, I hope you believe in ideology:

   no ideology == no revolution == power to the managers .

> > I mean no equations apart from those necessary to control bureaucracy.
>
> There have never been any other equations in CoS.

OK, you have an ideology, good.

> > > 2) In order to simulate an ordinary weakening in KS, you have to do a
> > >    horrible lot of duplications via additional contractions (I just had a
> > >    quick look at the technicalities because I couldn't believe it)
> > >    In my opinion this is "morally wrong" because you lose a lot of
> > >    information about the proof and introduce bureaucracy which is worse
> > >    that A and B.
> >
> > Why would you want to `simulate' w_? If you want it, just throw it in.
>
> Because in classical logic you need weakening to be complete.

I don't understand, but let's see. KSw is complete. If you want to 
observe more derivations, including some normal or canonical forms 
associated to some form of bureaucracy you might have in mind, just 
add rules that could give you those derivations; for example, add w_.

In general, getting rid of bureaucracy means adding rules, and it's 
easy. The problem is only complicated when adding rules does not cure 
global kinds of bureaucracy like A or B: in that case some more 
sophisticated technology is needed.

Do we agree on this?

> And you did the 'simulation' in your technicalities.

I only did it to *show completeness* and *good complexity behaviour*.

I know that there is bureaucracy involved in observing r7, but if r7 
is what you want, just throw it in and forget about the fine details!!

I guess I'm not good at marketing...

> > I'm not sure I understand what you mean by `losing information'.
>
> Exactly what I said in (i) and (ii) above. You change the 
> information about how often some atoms are used in the proof. I 
> consider this "essential".

I don't understand.

> > > I think completeness should not be the issue. Getting all 
> > > tautologies is not the interesting task of proof theory. We should 
> > > ask for all proofs of a tautology. And figure out what that 
> > > actually means.
> >
> > Do you have any clue about what (the hell) this question could 
> > mean? Should we ask for all the possible fathers of a child and 
> > figure out what that actually means?
>
> Well, we are doing proof theory. And we agree that an important 
> question is "When are two proofs the same?". For this, we need 
> (unlike in reproduction) to accept the fact that there are many 
> different proofs of a tautology.
>
> Maybe our big mistake was to ask "When are two proofs the same?". We 
> should ask instead "When are two proofs different?".

I understand even less. So, you mean, we should better ask ourselves 
`who's *not* the father'?

> > Yes, whenever you simulate anything into anything else, the size 
> > increases, but the question is whether it grows polynomially or 
> > not, and it looks to me that everything here behaves well.
>
> I did not check the details, but if every introduced f causes a 
> duplication, you have the potential of an exponential increase in 
> the number of f.

I don't think so, but I'm still waiting for some technical 
confirmation, maybe there are mistakes, but there is no conceptual 
reason for an exponential blowup, I would be very surprised.

-Alessio