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