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

PROOF-NETS FOR MULTIPLICATIVE AND ADDITIVE LINEAR LOGIC
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.)

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

References:
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
theory.doc.ic.ac.uk
The files are in the directory
/papers/Bellin

```