Re: Bureaucracy and identity

At 11:08 +0100 18.3.05, Lutz Strassburger wrote:
>On Thu, 17 Mar 2005, Alessio Guglielmi wrote:
>>>>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.
>>>It certainly is bureaucracy. But not necessarily the "very first". 
>>>You simply lose importaint aspects if you take that for granted.
>>
>>Which aspects? I might very slightly agree about associativity, but 
>>I feel I will never agree about commutativity. Give examples!
>
>If you per se identify A*(B*C) and C*(A*B) you lose the information 
>in which order the three guys are associated. Of course, you can 
>consider this a pure act of bureaucracy, and probably you are right 
>in most cases. But sometimes you need the information about this 
>additional structure.
>
>You came up yourself with the best example I can think of. Before I 
>have seen it I wasn't sure whether the problem was real or just a 
>gut feeling.

My example is not about *formulae*, it's about *derivations*.

If you want to observe associativity in formulae by observing 
derivations, just introduce constructor inference rules, like in

    A * (B * C)
    -----------
     A * true   .
     --------
       true

Anyway, my question was whether there are situations in which one 
wants to observe associativity and commutativity in formulae *in 
addition* (of course!) to when one really wants just that.

>>>I have my objections to putting this on a higher level than "type 
>>>A" or "type B" bureaucracy.
>>
>>The plot thickens... Which objections?
>
>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.

Of course, it is possible, it's what Kai and Stephane do, and I can 
do the same.

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

I think it is as difficult as stating the necessary laws, in general.

However, it would be completely artificial not to work under 
associativity and commutativity *in a geometric setting*. A bunch of 
wires is a bunch of wires, you want to forget about more structure 
than that, it's the whole point of the thing.

When you grow a tree in the sequent calculus or tableaux or natural 
deduction, you have a bunch of branches, you forget about the rest. 
In this sense, I say that getting rid of associativity and 
commutativity is the first thing to do: because it gets you closer to 
the geometry of the thing.

See things from a different perspective: in (model theoretic) 
semantics you don't worry about associativity and commutativity. 
These are syntactic artefacts that are introduced by the 
one-dimensional limitations of the language. Once you move to higher 
dimensional graphs, it seems perverse to me to try and carry on the 
syntactic burden of grammars and strings.

>>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 think it is more inspiring to tell people that we try to give them 
a better language than strings. I agree with you on the technical 
things, like orthogonality of A, B and ass/comm, but this is 
something that comes later, it's the technicalities, not the 
inspiration.

-Alessio