[Prev][Next][Index][Thread]
no-short-trips on additive proof-nets
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.)
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.
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