Re: Wires and pipes

On Thu, 17 Mar 2005, Alessio Guglielmi wrote:

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

> There is *one* very ideological choice in the design of wired deduction, 
> namely the insistence on linearity. This is expressed by the idea that no 
> wire is created or destroyed, and that everything in the derivation happens 
> inside the rigid, predetermined amount of wires.

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.

...

> One word about different kinds of bureaucracy: it is not fair to consider 
> type A and type B on the same level as bureaucracy of the kind 
> `order-of-contractions', for example (see below). In fact, in order to get 
> rid of bureaucracy of type A or B, one has to have a *global* vision of a 
> given derivation, what is not the case for order-of-contractions.

I agree. In fact, it is a special case of type C bureaucracy that I was 
mentioning in another mail.

...

> However, I claim that the problem with contraction bureaucracy is a deeper 
> one, and moving to nonlinear wired deduction wouldn't help. The only real 
> cure is fixing the problem in the deductive system: this is a 
> deductive-system-level bureaucracy! Fixing the deductive system *can* be done 
> in wired deduction.
>
> The problem is simply one of associativity: take, in *any* deductive 
> formalism,
>
>       a   a
>        \ /          a   a a   a
>     a   a            \ /   \ /
>      \ /      and     a     a    .
>   a   a                \   /
>    \ /                  \ /
>     a                    a
>
> How do you equate these derivations? The only solution is to use an n-ary 
> atomic contraction rule:
>
>   a a a a
>   ------- .
>      a
>
> (The right attitude towards trees is that of the lumberjack.)

OK.

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

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

> However: there are two things to consider:
>
> 1  The ww_ rule is always permutable with any other rule: it uses two wires, 
> but it behaves like if it used just one. So, it is perfectly conceivable to 
> use some shortcut notation to deal with it, and one would never really notice 
> the difference with aw_. So: until you really want to get into some fine 
> details of unit behaviour, it's pure cosmetics, nothing deep.

I was also wondering about that. But this was not the source of trouble.

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

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

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

> Now, let's see the remaining points:
>
> > I believe that this would work only for multiplicative linear logic. As 
> > soon as you have contraction and weakening, you must duplicate or 
> > create/destroy wires.
>
> You might be right, of course, and this is why I'm saying that I'm setting 
> the bar high: the case when you have more than two logical units might be 
> tricky. However, you might also be wrong!
>
> Anyway, if you're right, then one would still be able to do linear logic in 
> *nonlinear* wired deduction. This would be the right punishment for linear 
> logic: in the end classical logic would shine in pure linearity and linear 
> logic would rotten in the nonlinear slums.

I wouldn't be sorry.

> > > So, this is propositional classical logic's system KSw; notice that there 
> > > are *no equations*:
> >
> > What do you mean by *no equations*? In the technical section you have 
> > equations for associativity and commutativity.
>
> I mean no equations apart from those necessary to control bureaucracy.

There have never been any other equations in CoS.

> > ww_ is weird in several ways:
> > 1) Having a t above wired to an f below is weird.
>
> I'm glad you noticed. I actually tried a bit getting rid of the anomaly, but 
> didn't insist too much. In any case the rule is sound, so, who cares?
>
> > 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. And you did 
the 'simulation' in your technicalities.

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

> > Well, I think you do increase the size simply because you need Thm <PP> for 
> > getting r7, which you need for an ordinary weakening.
>
> 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.

-Lutz