Re: Calculus of structures and sequent calculus

Hi Kai,

> I don't know about locality of cut elimination. It depends on you notion of 
> locality. Do you have an example of cut elimination procedures in the sequent 
> calculus that you consider local? We have Tait-style (in some sense global) 
> and Gentzen-style (in some sense local) proof transformations for eliminating 
> the cut. Personally, I consider both of them non-local since also Gentzen's 
> procedure is duplicating unbounded-size trees all over. If your notion of 
> locality is as strict as mine, then I think we don't have a local cut 
> elimination procedure and I wonder whether there is one at all.

I mean local with respect to the derivations algebraic structure. I don't 
have any example, since I don't have identified the structure of 
derivations in the sequent calculus. But I have that kind of process in 
mind:

   A
 ----- R
   B
 ----- cut
   C

is replaced by:

   A
 ----- cut'
   B'
 ----- R'
   C

This is of course a simple case. Then, this computation step is propagated 
with respect to the structure.

The case with duplication of unbounded-size derivations might be handled 
with some kind of ressource-management explicit calculus, so it is not 
really an obstruction.

Is that kind of process has any chance to exist in CoS? Maybe it is not 
with cut but with another class of rules?

> I'll see you in Dresden so we can chat there. Btw, I tried to read the 
> introduction of your thesis. I was impressed but had to give up in the end. 
> Can you recommend an introductory exposition of higher-dimensional rewriting 
> which is written in English?

You can take a look at the following, but some are not online:

Albert Burroni, "Higher-dimensional word problem with application to 
equational logic", Theoretical Computer Science 1993.

Yves Lafont, "Towards an algebraic theory of boolean circuits", Journal of 
Pure and Applied Algebra 2003.
ftp://iml.univ-mrs.fr/pub/lafont/circuits.ps.gz

Francois Metayer, "Resolutions by polygraphs", Theory and applications of 
categories 2003.
http://www.tac.mta.ca/tac/volumes/11/7/11-07.pdf

There is a preprint on my page with the main results from my thesis:
"Termination orders for 3-dimensional rewriting".
http://iml.univ-mrs.fr/~guiraud/recherche/erm.pdf

There is no real reference on higher-dimensional rewriting. For the 
moment, most results concern 3-dimensional rewriting (or computational 
properties of operad presentations, as I call it in my thesis).

The reason is that there was no available example of a computation living 
in any higher dimension. But this is going to change thanks to CoS: since 
its derivations can be interpreted as the 3-dimensional arrows of a 
3-category, any rewriting calculus on them is 4-dimensional (this is the 
principle of higher-dimensional rewriting).

And by rewriting calculus, I mean any computational process specified by 
local rules (so you see where I'm going with my question about 
cut-elimination!). The only example I have for the moment is this (rather 
trivial) one (in SKS, but with connectives written the usual way):

     x
  ------- =
   x v 0                \         x
  ------- x v w(x)  ==== \     ------- x
   x v x            ==== /        x
  ------- c(x)          /
     x


where x is an atom, w(x) is down-weakening applied at x and c(x) is 
down-contraction applied at x.

Of course, the 4-dimensional nature of this computation does not appear 
clearly in this representation!

I hope I have time to explain all this next week!

Yves