no-short-trips on additive proof-nets

A paper available by anonymous ftp from theory.doc.ic.ac.uk: 

                         April 1993
                       Gianluigi Bellin 
        MALL-trips.ps                           MALL-trips.dvi.Z

It contains a very simple formulation of proof-nets (without boxes) for MALL,
using (a variant of) Girard's `no-short-trip' as correctness condition.

Remember (Girard 1987) that a *principal switching* (for a certain 
formula A in a proof-net R) is a choice of the `par' switches as follows:
in the part of the trip from the visit to A upwards to the visit downwards,
if any `par' link is reached *for the first time from above*, then 
the trip returns immediately upwards. It is easy to see that the empire
of A is precisely the part of the net visited during this part of the trip.
(It follows that the computation of the empire of A is linear in the size 
of the net.)

The main idea here is to regard *additive links* (namely, `with' links and 
additive contractions) as `ambivalent times-par links': in a trip they behave 
like `times' links when they are reached for the first time *from below* and 
as `par' links when they are reached for the first time *from above*. 

At the beginning of each trip we decide a switching for all the `times' and 
`par' links and also for the additive links, in case they behave like `times' 
links (independent switching). A principal switching for a formula occurrence 
can be regarded as a command which overruns the original switching in a part 
of the trip. 

Whenever an additive link, with premises X and Y, is reached for the first 
time from below, the trip continues from the premise chosen by the independent 
switch, say X; now a principal switching for X is enforced; when the trip 
returns to X, we know the empire of X and its `doors'. 

Next consider a trip exactly as before, except that at the additive link 
in question the switch is changed: such a trip continues from the other 
premise Y, and a principal switching for Y computes the empire of Y. 
Now compare the doors of eX and eY: if they `match' as premises of exactly one 
`with' link and of the same set of additive contractions (but not of any
`par' link; also they cannot be conclusions of R), then the test is successful;
otherwise, it fails.

In fact, it is possible (as shown in the paper) to detect the `matching' 
of the doors already within one trip, so that an unsuccessful trip 
actually stops (`short trip'). Anyway, it is clear that the computation of 
`additive correctness' (i.e., the verification that the doors `match') 
is linear in the complexity of the verification of correctness of the net
as a multiplicative structure. 

As long trips produce information about the empires of the premises
of `with' links, we can easily reintroduce additive boxes, by replacing
the `with' link and the associated additive contractions. 
A sketch of the present result was presented during a visit to the Universite' 
Paris VII in December 1992. Thanks to V.Danos for useful discussions. 

The present result improves previous work by the author (Bellin [1990, 1991]).
The previous version of the paper (Bellin 1991) is in fact a different project,
using another correctness condition for the multiplicatives, where the notion 
of empire is taken as primitive; it contains also results of slicing of 
additive nets and extensions of larger fragments. It is also available
in the file MALL-nets.ps or MALL-nets.dvi.Z. 

Girard [1987] `Linear Logic' TCS
Bellin [1990] `Mechanizing Proof Theory...', Thesis, Stanford CS-Dept. 
       Rep. STAN-CS-90-1319 and Edinburgh CS-Dept Report ECS-LFCS-91-165 
Bellin [1991] `Proof Nets for MALL', Edinburgh CS-Dept. ECS-LFCS-91-161. 

The papers
MALL-trips.dvi.Z    MALL-nets.dvi.Z [use uncompress to obtain the dvi-files];
MALL-trips.ps       MALL-nets.ps  
are available by anonymous ftp from 
The files are in the directory