Re: Bureaucracy and identity

Dear Frogs,

here is just an e-mail to show that other people than Alessio and Lutz have finally read the e-mails 
about Bureaucracy and wires :-)
On each point I have a tendency to agree with one of you, and since Alessio encourages feedback, 
here are also a few comments.

> The same thing in other words: every time a `problem' (like `getting rid of bureaucracy') is not 
> formally defined, there is a strong temptation to define it *after* one has found a technical 
> solution. I think we should resist the temptation and set the bar (2) *before* making the jump 
> (1). (In computer `science', where formalised problems don't abound as much as in mathematics, 
> many people don't set the bar or set it after, and this of course is ridiculous, in my opinion.)
>
> Enough said. Do we agree on this?


Yes.

> BUREAUCRACY AND IDENTITY
>
> Do we agree that bureaucracy and identity of proofs are intimately related?

yes.

> There is no formal notion of bureaucracy, but I guess the consensus is that, when two proofs are 
> *morally the same*, but they differ in *inessential details*, then this is due to *bureaucracy*.
>
> If this is so, we should conclude that eliminating bureaucracy should lead us to eliminate the 
> inessential details that blur the `sameness', i.e., identity, of proofs.

yes.

> In particular, the notion of identity should be related to the notion of *inference step*, and I 
> think that inference steps become sort of confused both in categorical models and in term calculi. 
> I think that by looking at inference steps, we can get a better judgment of what is the same and 
> what is not.

I'm not sure. Inference steps are natural because they correspond more closely to human reasoning, 
but the latter can be bureaucratic and so far, sequentialising reasoning steps has always been a 
source of bureaucracy. Proof-nets are the typical formalism that gets rid of bureaucracy precisely 
by blurring completely the inference steps. If Wired Deduction gets rid of it, though it is still 
based on inference steps, I'd be extremely happy.
Also, having a formalism close to human reasoning might not be the first priority for some people. 
For instance, I'd be much happier to have a formalism suited for proof-search and automatic 
reasoning.

> HOW MANY KINDS OF BUREAUCRACY?
>
> Do we agree that we should not suppose that there is only one kind of bureaucracy?

yes

ABOUT LUTZ'S EXAMPLE OF BUREAUCRACY

I agree with Alessio's point of view. It's deductive-system bureaucracy, or bureaucracy of type C, 
and I wouldn't require the formalism to get rid of it. If the deductive system is not perfect, it's 
not the formalism's fault :-)

> 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.
>
> In other words: you cannot get rid of type A or B bureaucracy by simply adding rule schemes to a 
> deductive system. On the contrary, it is possible to do so in order-of-contractions bureaucracy 
> (see below for more details).

I agree again.

> BUREAUCRACY IN THE FORMALISM AND IN THE DEDUCTIVE SYSTEM
>
> [...]
> Do we agree?

completely.

> BUREAUCRACY IN FORMULAE
>
> Do we agree that the *very first* source of bureaucracy in *all deductive systems* in *all 
> formalisms* is associativity and commutativity (when present) in formulae?

No. Actually, I'd say it's the very last. Here is my argument:

I'd say that not only there is formalism-bureaucracy and deductive-system-bureaucracy, but there is 
also logic-bureaucracy.
There are some non-commutative logics after all. In the case of AC, most of the languages used in 
formalisms do not consider formulae modulo equations. CoS does, but Natural deduction, Sequent 
Calculus, or axiomatic Hilbert-style systems do not. By that I do not mean it is better not to do 
it.
But in all those formalisms the fact that A/\B is the same as B/\A is a theorem of the logic, not an 
axiom as in CoS. Actually, there are lots of other equivalences, and we do not want to consider 
formulae modulo all of them. The thing with AC is that not only the formulae are equivalent but 
there is also a *type isomorphism* between them. And the thing is that I see no reason to have a 
special treatment for AC and not for any random kind of type isomorphism. Yes, because of the 
equations on formulae, CoS identifies some type isomorphisms (even the one between AxB->C and 
A->(B->C) ). Considering formulae modulo AC breaks the statndard representation as a tree, but some 
day, someone will come up with a fancy logic and some never-heard-of type isomorphisms that make the 
equivalence clases of formulae look like weird mathematical objects (why not cycles, for instance?), 
and all the work we'll have done for AC might just not work there.
I think it is utopic to set as a task of the formalism to remove every kind of logic-bureaucracy 
that can ever come up in the future.
As you said yourself:

> It is hopeless to try and define bureaucracy once and for all.

That said, I think that if our formalism has all the qualities that we dream of, and we have some 
specific "plug-in" to deal with some logic-specific bureaucracy such as AC, it's even better!! So 
I'm not saying we should not adress the problem of AC, but it's something that is really my last 
priority. Again, that being said, I think that wires are really a great idea to address the problem. 
I'm much impressed.

> Do we agree that *every* war to bureaucracy should start from this realisation?

Well, as I said, no.

Lutz wrote:
> Right now, they are only of the "moral" kind. The first is that I think it should be possible to 
> deal with A and B independently from associativity and commutativity.
> And the second is that I guess that it is easier to deal with A and B without having to take care 
> of associativity and commutativity. So, I'd propose to do that first. Once we have done that, 
> i.e., we have formalisms A and B, we can think about the associativity-and-commutativity-problem 
> from a much better starting point.
> [...]
> And sometimes commutativity and associativity is not purely bureaucratic, but is needed to keep 
> track of what comes from what. This is my interpretation of the example.
>
> Of course I do not have the patent solution in my pockets, but my suggestion would be to try to 
> solve the two bureaucracy-problems seperately, and not at the same time.
>
>> So, what's the alternative? Suppose I have to write an introduction to the subject, what would 
>> you suggest?
>
> Explain the different types of bureaucracy, and say that they are *orthogonal* to each other, 
> i.e., can be dealt with independently.

I completely agree with Lutz.

> Do we agree that the only practical way of dealing with commutativity is working under an 
> equivalence relation that takes care of it?

Can't see any other yet, unless we move to a graphical notion.

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


What else would we ever consider equations (such horrible things) for? that's the least one can ask, 
and the least you use them the better.
otherwise it's rather easy to define equivalence classes of derivations in CoS, and there you have 
your perfect formalism. What we want is a formalism for canonical representatives.

> A PROBLEM WITH COMMUTATIVITY AND ASSOCIATIVITY
> [...]

Yes, that's exactly the problem Kaï and I spotted, which made us put commutativity and associativity 
as two-ways inference rules.
Let me point at this stage that this decision is completely orthogonal to having a deductive system 
or a term formalism with typing rules. It wouldn't be fair to disregard term syntaxes just because 
we decided not to adress the AC bureaucracy (though you may find other reasons why doing so).
The ideas in wired deduction could be presented in a term formalism as well. Your notion of pipe 
seems to be excatly our notion of tube.

ABOUT WIRED DEDUCTION

On the contrary to Lutz, I went directly to the technicalities, because it's hard to discuss 
something before it's been formalised.
As I said, I think that considering skeletons labelled by appropriate atoms is great.

Just wanted to mention the fact that the way you name the wires (whether it's with numbers or 
whatever) is completely arbitrary so it introduces exactly the same kind of bureaucracy as 
alpha-conversion. Of course this has been widely studied...

> 2  COMPOSITION OF RULES
>
>
> This part needs to be completed. For now, suffice to say that we compose rules
> like in the calculus of structures. Of course, it is possible to define more
> geometric notions of compositions, like for formalism B.


Well, that was actually the part I was waiting for, where you explain how all the bureaucracy is 
removed :-)
I'd really like to see how you define composition so that only canonical forms are produced.

> 3  CLASSICAL PROPOSITIONAL LOGIC
>
>
> *Proposition*   The _contraction_ rule
>
>       [P P]
>    c_ ~|~^~ ,
>        P
>
> is derivable for KSw.


Let's be precise here. What you seem to prove is that for all formula P, there is a derivation from 
[ P P ] to P.
the your contraction rule is rather a scheme of atomic rules.
Nothing to do with what you call a local rule having some kind of pipe, so you can't "permute" it 
with some derivation operating on P (anyway, the rule wouldn't be linear, and you forbid that, which 
is a safe choice).

Coming to linearity, I think I agree with Lutz: I dislike the wired versions of atomic contraction 
and rule ww. I see that this is how you ensure linearity, but maybe we do not want linearity of the 
wires.

> However, notice that it is possible to *trivially* modify wired inference in such a way that the 
> linearity constraint is abandoned. If you do so, any system in CoS, and so any logic, can 
> immediately be expressed in wired deduction in such a way that ass/comm-, A- and B-bureaucracy 
> types are absent.
> [...]
> it is possible to present regular KS in wired deduction in the obvious way: just translate all 
> rules into rules and all unit equations into rules. This would cure all of Lutz's criticism except 
> for the one on contraction. Going for a `nonlinear' wired deduction would be a cure for that, too 
> (we just would be back into CoS, but without the bureaucracy).


If you say that dropping the linearity constraint is a trivial thing to do and it still works, then 
I'd go for it.
Then it will be possible to present Sub-atomic logic as The logic in which wires are linear: 
duplication, birth and death are simply optical effects.
It will motivates sub-atomic stuff even more.

Stéphane