paper availbale by ftp


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

The paper is available by anonymous ftp
directory : \pub\girard
files : proofnets.ps.Z and proofnets.dvi.Z

Happy Christmas and New Year 


Jean-Yves GIRARD
Directeur de Recherche

CNRS, Laboratoire de Mathematiques Discretes
163 Avenue de Luminy, case 930
13288 Marseille cedex 9

(33) 91 82 70 25
(33) 91 82 70 26 (Mme Bodin, secretariat)
(33) 91 82 70 15 (Fax)