Bureaucracy and identity

Hello,

it looks like the war to bureaucracy is basically won, and in many 
different ways. I also have some news myself, which I'll better 
explain in the next email.

I'd like to check whether we all agree on some informal notions. 
Otherwise, it's better we discuss these things a bit. I think this is 
important because it looks like several distinct papers will come out 
of this effort, and so it's better to speak the same language. 
Ideally, we should be able to motivate this research all in the same 
way (and then perhaps fight over the details).

At the end of the email I'll propose a problem that illustrates some 
of the difficulties in the war to bureaucracy.

In the following I will use `proof' and `derivation' interchangeably.


BUREAUCRACY AND IDENTITY

Do we agree that bureaucracy and identity of proofs are intimately related?

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.

I think there are two ways of tackling this problem:

1) We ask for purely technical properties to hold, like for example 
the non-collapsing of a categorical model, or the existence of 
canonical forms.

2) We start from the question of what `morally the same' means and go for that!

The two ways are not mutually distinct (on the contrary!), however, I 
insist on the importance of the second one because I believe that the 
first approach should *follow* the second, and not the other way 
around.

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 suspect many disagree on this, so please, let us discuss it.


HOW MANY KINDS OF BUREAUCRACY?

Do we agree that we should not suppose that there is only one kind of 
bureaucracy?

I think the best attitude is to suppose that, for any given logic, 
there are several possible notions of identity of proofs, and people 
can invent more and more of them.

Given a notion of identity and a formalism, either the formalism is 
able to express the identical proofs or it isn't: in this case, we 
have bureaucracy, and we have an enemy.

Our goal is to attack some specific, important kinds of bureaucracy, 
in order to improve the ability of proof theory to deal with 
bureaucracy. It is hopeless to try and define bureaucracy once and 
for all. However, it is now possible to define formalisms which get 
rid of the most brutal and medieval forms of bureaucracy.


BUREAUCRACY IN THE FORMALISM AND IN THE DEDUCTIVE SYSTEM

There are several sources of bureaucracy, and I think it is 
convenient to address them separately. It should be possible to make 
a broad distinction between bureaucracy induced by the formalism and 
bureaucracy induced by the specific deductive system used (in the 
given formalism).

I think a very clear understanding of this comes from the 
n-categorical approach that Yves Guiraud showed us at the last 
workshop (slides are available at 
<http://iml.univ-mrs.fr/~guiraud/exposes/dresde.pdf>). 
Formalism-related bureaucracy is dealt with in the first three 
dimensions, and deductive system-related bureaucracy is dealt with in 
the fourth dimension.

I guess we all agree that, say, formalism A takes care of bureaucracy 
of the kind

     [R' T']           [R' T']
   r'-------         r -------
     [R' T ]           [R  T']
   r -------   vs.   r'------- ,
     [R  T ]           [R  T ]

where the order of the application of two inference rules doesn't 
morally matter. In formalism A, one can write

      R'    T'
   [r--- r'---]
      R     T

and the problem is solved. This is an example of formalism-related 
bureaucracy: CoS only sees the two derivations above, and doesn't 
express the one below.

However, consider a deductive system where associativity is explicit 
(I mean, we are not working modulo associativity). Consider the 
following two derivations:


       [[a  a] a]
   ass -----------
        [a [a  a]]             [[a a] a]
    ac_ ----------         ac_ ---------
        [a  a]                    [a  a]
    ac_ ------       vs.      ac_ ------ .
         a                         a

They might be considered `morally the same', but it is difficult to 
fix the problem in the formalism definition. Perhaps, a better idea 
is to fix the deductive system. For example, one can propose a 
deductive system with sort of a `general atomic contraction', 
quotient by associativity, and go for the derivation

        [a a a]
   gac_ ------- .
           a

So, this could be an example of fixing the bureaucracy problems by 
fixing the deductive system (inside a given formalism).

Do we agree?


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?

I mean, we do not want to distinguish formulae, and so proofs, just 
because of the order of associations, right?

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

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

(I guess that recognising this symmetry is the very first step 
towards a *geometric* understanding of proofs, and not doing it means 
abandoning all hopes for that goal.)


A PROBLEM WITH COMMUTATIVITY AND ASSOCIATIVITY

Working under associativity and commutativity is difficult. Actually, 
it is also dangerous.

The very first thing that Francois told me after seeing deep 
inference for the first time was that I was going to have problems 
with the way I was using equations. So far, there was no problem, but 
I do have a serious problem now, in the war to bureaucracy.

This is actually not a problem in the technical sense (point 1 above) 
but it is a problem in a moral sense (point 2), so it's indeed 
serious!

Consider

        E   C
     [  |   | ]
      [A B] A
   * ---------- .
       A [B A]
     [ |   |  ]
       D   F

This is a derivation in formalism B in which two derivations are 
vertically composed by *, and we work under commutativity and 
associativity. The problem is that this is the only way I have in 
formalism B for representing (what I could graphically and 
imprecisely represent as)

        E    C
     [  |    | ]
      [A B]  A
       |  \  |   .
       A  [B A]
     [ |    |  ]
       D    F

However, the same derivation above could also stand for

        E   C
        |   |
     [[A B] A ] ,
        |   |
        F   D

and this of course is *morally different*!

What can I do? Well, I could stop working under commutativity and 
associativity: this way I could easily distinguish between the two 
cases. However, if I drop commutativity and associativity, I get back 
all the bureaucracy in formulae, with a vengeance, because now this 
bureaucracy scales up to proof composition.

In the next email I'll show you a solution to the problem.


Please comment on all of the stuff above, if you disagree. Perhaps I 
should use some of this blah blah in some web page, and we better 
agree on the contents (marketing)!

-Alessio