[L5] ================================================ AMAST Links 02 01

           Proof-nets: The Parallel Syntax for Proof Theory
                          by Jean-Yves Girard

   The paper is available by anonymous ftp, both in
_dvi_ and in _postscript_ format, respectively at
URL: ftp://lmd.univ-mrs.fr/pub/girard/proofnets.dvi.Z,.ps.Z
  One year ago I announced essential progresses on additives, both on
proof-nets and on geometry of interaction. The paper on GOI was quickly
written, but the paper on proof-nets was postponed, since I found a bug
when I wrote the details. Recently I discovered the two systems with
constant cut-elimination complexity, ELL and LLL. I tried to make a
proof with old fashioned methods, i.e. sequent calculus. This was
extremely painful (difficult to avoid the nonsense of double layer
sequents, difficult to provide a natural size for proofs etc.) In fact
-assuming I had the patience to cope with these minor technicalities,
the reader would have got a symmetric problem, i.e. to find out what is
the central idea in this bureaucratic mess. The use of sequents here
was nothing but a childish game of encryption/decryption.
 This is why I decided to do it with proof-nets. The problem is that 
additives play an important role in LLL (not that much in ELL), and 
that I was never satisfied with the extant notion of proof-net. But 
it turns out that the extant notion (equipped with a lazy 
cut-elimination) normalizes in linear time, and that's enough for 
what I wanted to do. This is the reason why I decided to write a 
survey paper concerning proof-nets. Its aim is to provide an 
alternative syntax, in case one wants to do elegant proof-theory or 
achieve subtle aims, or simply protect forests...
  The paper mainly deals with additive proof-nets, for which the best 
known solution is presented, and their lazy normalization. The 
discussion about possible improvements and the description of the 
full procedure are postponed to an appendix. The paper proceeds with 
the unproblematic extension to quantifiers (which look like 
oversimplified additives), and the treatment of exponentials, for 
which we restrict to weakening and contraction: the other rules, 
e.g. the rules for LLL or ELL, will be considered in a forthcoming 
paper. The weakening rule is also slightly problematic, but this is a 
rather minor question.