Subject: paper announcement
From: [email-masked] (Andrea Asperti)
To: [email-masked]
Date: Fri, 21 May 1993 12:28:40 +0200

--text follows this line--

*****************************************************************

			Interaction Systems II
                 The Practice of Optimal Reductions

          Andrea Asperti                   Cosimo Laneve

      Department of Mathematics,       INRIA - Sophia Antipolis,
      University of Bologna,           2004, Route des Lucioles,
      Piazza Porta S. Donato 5,        B.P.93 - 06902,
      40127 Bologna, Italy.            Sophia Antipolis, France.
      [email-masked]	       [email-masked]

                              Abstract:

Lamping's optimal graph reduction technique for the lambda-calculus 
is generalized to a new class of higher order rewriting systems,
called Interaction Systems. Interaction Systems provide a nice 
integration of the functional paradigm with a rich class of data 
structures (all inductive types), and some basic control flow 
constructs such as conditionals and (primitive or general) recursion.
We describe a uniform and optimal implementation, in Lamping's style,
for all these features.
This work is the natural continuation of our previous paper 
"Interaction systems I, the theory of optimal reductions", where 
we focused on the theoretical aspects of optimal reductions in IS's 
(family relation, labeling, extraction, an so on).

******************************************************************

Comments: 

The paper is related to Linear Logic in two ways:

1. At the syntactical level: Interaction Systems are the intuitionistic
generalization of Lafont's Interaction Nets, which in turn generalize
Proof Nets of Linear Logic. 

2. At the operational level: the optimal reduction technique has been
inspired by Gontheir's and al. systematization of Lamping's work,
based on a tight relation with Linear Logic and the Geometry of Interaction.

****************************************************************

The paper is available by anonymous FTP from the area 
		ftp.cs.unibo.it
in the directory
		/pub/TR/UBLCS. 
The file, in postscript compressed form, is named 
		93-12.ps.Z 
(technical report 93-12 of the University of Bologna, Laboratory for
Computer Science). 


Return-Path: <@Sunburn.Stanford.EDU:[email-masked]>
From: Paul Taylor <[email-masked]>
Date: Wed, 26 May 1993 17:38:45 +0100
X-Mailer: Mail User's Shell (7.2.3 5/22/91)
To: [email-masked]
Subject: par symbol in TeX
Sender: [email-masked]
--text follows this line--

Once upon a time I wrote some MetaFont to generate an upside down
ampersand for use as Girard's par symbol, and occasionally I get
enquiries about it.  This message is to advise you that I don't
intend to maintain or supply it any more, because there's a whole
font full of interesting symbols, and macros compatible with both the
original Lamport and new Mittelbach-Schoepf font selections.

It is called "stmary" and was written by Alan Jeffery, now at Sussex (England).
You can get it from the International TeX Archive at
	Stuttgart, ftp.uni-stuttgart.de, 129.69.1.12
	Aston, ftp.tex.ac.uk, 134.151.44.19
or	SHSU, ftp.shsu.edu, 192.92.115.10
in a directory with a name like
	/pub/archive/macros/latex/styles/contrib/stmary/ 
There are both MF and PK files available.
To use it, do \documentstyle[stmaryrd]
then the par symbol is called \bindnasrepma.

Happy linear-TeXing!

Paul Taylor


Return-Path: <[email-masked]>
To: [email-masked]
Subject: Re: par symbol in TeX
Date: Thu, 27 May 93 17:33:46 PDT
From: [email-masked]
Sender: [email-masked]
--text follows this line--

	It is called "stmary" and was written by Alan Jeffery, now at Sussex (England).
	You can get it from the International TeX Archive at
		Stuttgart, ftp.uni-stuttgart.de, 129.69.1.12
		Aston, ftp.tex.ac.uk, 134.151.44.19
	or	SHSU, ftp.shsu.edu, 192.92.115.10
	in a directory with a name like
		/pub/archive/macros/latex/styles/contrib/stmary/ 
	There are both MF and PK files available.
	To use it, do \documentstyle[stmaryrd]
	then the par symbol is called \bindnasrepma.

Let me encourage people who broadcast instructions for retrieving
something to check that the instructions work on all machines listed,
exactly as given.  This will save us all a lot of time.  (I wasted
fifteen minutes wandering around all three of the above machines
without finding a single stmary?.mf file using the above instructions,
trying various creative permutations of the above pathname.)

--
Vaughan

----------------
(linear moderator:  I agree with Vaughan.  I found the material on
machine ftp.tex.ac.uk in direcotry  /pub/archive/fonts/stmary  
only after some fiddling.)


Date: Fri, 28 May 1993 18:08:22 +0100 (BST)
From: Samson Abramsky <[email-masked]>
To: [email-masked]
Subject: Thomas Streicher's message
Sender: [email-masked]
--text follows this line--

In reply to Thomas' message:

1. ``Making a category out of Geometry of Interaction'' was done by me
in October 1991. For the ``product form of GoI'' this appeared in my
paper with Radha Jagadeesan on ``New Foundations for the Geometry of
Interaction'' in LICS '92.
I also considered the ``coproduct form'', i.e. the Girard GoI
(henceforth GGI). The problems Thomas mentions with this are exactly
those which arise with correctness of GGI, which is why the correctness
of the intepretation is stated with restrictions in Girard's paper on
''Geometry of Interaction I''. I talked about this in my tutorial
lecture and talk at LICS 92.

2. The games and history-free strategy semantics of Linear Logic  given
by myself and Radha agree EXACTLY with  GGI at the level of
interpretation of proofs. That is, the partial functions on moves
determining the history-free strategies are exactly the functions
assigned to proofs in GGI (where GGI is cut down to the essential
content of partial 1-1 maps); moreover, the execution formula coincides
exactly with the composition of strategies.  All of this is laid out
very clearly and explicitly as far as the multiplicatives are concerned
in my paper with Radha on ``Games and Full Completeness for MLL''.

3. The history-free semantics for the exponentials is not discussed in
that paper. It was worked out subsequently by us, and will appear in a
paper currently under preparation. This history-free semantics again
coincides exactly with that of GGI at the level of interpretation of
proofs. (Incidentally, the interpretation of the exponentials could also
be said to be that of Blass - going all the way back to 1972!). The key
point is that the games provide the missing notion of type, which allows
us to make an honest model out of GGI, and more, to get Full
Completeness theorems, previously completely out of reach.

4. This leaves the question raised by Thomas: how do we overcome the
commutation problems with the exponentials? This was quite non-trivial -
it took us about 3 months to find the right definitions. Briefly, we
enrich the notion of game with a specified automorphism group, and
impose an equivalence on strategies using these groups - the equivalence
is ``logical relations extended in time''. This solves all commutation
problems, and opens up the possibility of very strong full completeness
results for various intuitionistic fragments; these to be described in
the forthcoming paper. Incidentally, products ARE well-defined in the
co-Kleisli category.

In slightly more detail. The refined version of a category of games G we
use has objects A with an extra component G_A, where
G_A is a subgroup of Aut(A), the automorphism group of A in the category
G^e of games as embeddings, as described in my previous paper with
Radha. Thus an automorphism is a permutation on the alphabet which
preserves all the structure of the game.
This group G_A induces an equivalence on positions in A : s equiv t if
e*(s) = t for some e in G_A, where e* is the extension of e to sequences.

Now given two strategies sigma, tau on A, we define a relation sigma
equiv tau iff:
for all sab in sigma, ta'b' in tau of even length :  if sa equiv ta'
then sab equiv ta'b'.
This is a PARTIAL Equivalence relation on strategies. Morphisms in the
category are then equivalence classes of strategies satisfying the
partial equiv. relation. Of course, one must check that the relation is
compatible with the various constructions in the category; the
interesting case to check is composition.
The fact that sigma equiv sigma expresses a ``representation
independence'' property of strategies; the fact that sigma equiv tau
expresses that they are the same modulo insignificant coding conventions.

To complete the picture, we must say how the various constructions act
on the permutation groups. The multiplicatives do so trivially, just
combining permutations by disjoint union. Negation does nothing at all
to the permutation group.
For the exponentials, we define the moves of !A as
omega times M_A. The index i in (i,a) delineates which copy of A we are
in. The history-free monad structure etc. for !A works on these indices
as described by Blass, or as in GGI (but we insist that !A is negative;
only opening moves by Opponent are allowed). To define G_!A, we take all
permutations alpha x beta, where alpha is an arbitrary permutation on
omega, and beta is in G_A.
It is quite a thing of beauty to see how all this works out, e.g. for
the contraction (comultiplication) morphisms
 !A -> !A (x) !A.
Once you have done some of the calculations, you should be convinced
that these definitions are exactly right.
To repeat, products work on the nose in the history-free co-Kleisli
category. This is why GGI works for the lambda calculus, despite the
correctness problems with full Linear Logic.

All the best,

Samson Abramsky


Return-Path: <@Sunburn.Stanford.EDU:[email-masked]>
From: Gianluigi Bellin <[email-masked]>
Date: Mon, 31 May 1993 19:11:48 +0100
To: [email-masked]
Cc: [email-masked]
Subject: paper announcement
Sender: [email-masked]
--text follows this line--

                  Announcement of a paper:

            Proof Nets ans Typed Lambda Calculus
 
                  I. Empires and Kingdoms

                            by 

                G.Bellin and J.van de Wiele
   
         (Oxford University - Universite' de Paris VII)

Abstract: 
This paper is the first part of a study of Proof Nets and of Natural
Deduction derivations as graphs with different forms of orientations.
Results reached so far include a representation of linear lambda terms
as oriented Chinese Characters Diagrams, arising in the study of
Vassiliev invariants in knot theory; a translation preserving
normalization of natural deduction for linear logic into oriented
proof-nets; conditions for orientability of proof-nets yielding
the inverse translation. In the present paper, extending previous
unpublished results by Girard, Danos, Gonthier, Joinet, Regnier,
we provide a system of first order proof-nets without boxes for
the full system of linear logic and we investigate the structure
of the subnets of a proof-net.
                          -------
The paper ``Proof Nets ans Typed Lambda Calculus I. Empires and Kingdoms''
is available by anonymous ftp from 
                    theory.doc.ic.ac.uk
in the directory
                    /papers/Bellin
in the files 
          king.dvi.Z                   king.ps
use uncompress king.dvi.Z to obtain the dvi-file king.dvi. 
                          -------
Comments: The reader can use this (rather long) paper in several ways. 
1. in the preface we discuss the motivations for the project and give 
an outline of some results; 
2. in the section on multiplicative proof nets we develop the theory of 
the subnets of a multiplicative proof net, based on Danos and Regnier's 
correctness condition;
3. in the Appendix II we give equivalent correctness conditions for the 
multiplicative fragment; 
4. in the sections on the additives and the exponentials we generalize 
Danos and Regnier's method to the whole system of linear logic;
we also discuss these results as a contribution to the ``elimination
of boxes''; 
5. we consider the computational complexity of some constructions; 
6. in the section on the problem of irrelevance (Weakening boxes)
we recall and discuss systems of Direct Logic, namely, Linear Logic 
with the rule of Mix (Mingle). 

We made a special effort to give proper credit for the results;
unfortunately, omission of relevant results and/or credits is always 
possible and will be corrected; please let us know. 


Return-Path: <[email-masked]>
Date: Mon, 31 May 93 19:06:43 PDT
From: Vaughan Pratt <[email-masked]>
To: [email-masked]
Subject: Portable par
Sender: [email-masked]
--text follows this line--

Out of the past 4000 retrievals of Latex files from Boole.Stanford.EDU
(abstracts in /pub/ABSTRACTS), I have had hardly any complaints about
incompatibilities with anyone's Latex environment.  (All /pub files on
Boole are archived in both .tex and .dvi form; current retrieval
preference is running 7:1 for Latex over DVI.)  Naturally this requires
sticking to stock standard Latex, which rules out custom fonts like
stmary, and custom .sty files are explicitly inserted in each file to
be exported.

My preferred source of inverted ampersands has therefore been the
75-line sprite definition (anonymous? from McGill?) rather than one of
the metafont versions.  However it has turned out that quite a few
sites do not have sprite.sty, generating several complaints, the only
ones I've gotten in recent memory.  I've been dealing with this by
including sprite.sty itself in the .tex file, the total then coming to
140 lines.

Needing an excuse this weekend not to work on whatever it was I was
supposed to be working on, I had a hack attack which yielded the
following 6-line Tex macro package implementing a \draw command
intended mainly for drawing character-sized objects.  This allows
inverted ampersand (and any other character that might take your fancy)
to be implemented in two lines, with a drawing (hence initialization)
time of around 0.3 seconds on a 10-Mips machine (the sprite version
takes 8 seconds to initialize), plus an additional line defining a
boxed version rendering in < .02 second (the sprite boxed version is
~0.1 second).  Furthermore the boxed version uses some tricky coding to
get the bare minimum of typesetting commands per character, permitting
up to 300 of the fast boxed characters per page, compared with
approximately 20 in the sprite solution.  Usable in Tex, Latex, and
AMSTex.

At present you change drawing size when needed by redefining \scl, as
in \def\scl{.07} or \def\scl{.09}) before invoking \draw (as from
\invamp).  Someday some of these things will be more automatic.  I'd
also hoped to draw dots of size proportional to velocity, to permit
variable-width strokes (what is the smallest possible dot one can
typeset in tex?), along with various other bells, whistles, and viols
da gamba, but fortunately my hack attack expired before I got myself
any deeper into this mire.  Please feel free to hack up these or
worthier improvements yourself, provided you can do so without tripling
the size.

Incidentally I have a couple of other packages of a similar size, one
for Boolean circuits, another for Hasse diagrams, for anyone
interested.  These give a level of positioning accuracy and neatness
that is next to impossible to get with fig, at lower all round overhead
to boot.

Vaughan Pratt

%  \draw package.  Vaughan Pratt  (C) 1993
%
%	*+,-|.|/012	Table of 81 vectors in [-4,4]x[-4,4]
%	3456|7|89:;	Use as parameters to tell \draw how to step along
%	<=>?|@|ABCD	\draw zzzzzzz\end draws a straight line 7 steps
%	EFGH|I|JKLM	   down and to the right
%       ----+-+----
%	NOPQ|R|STUV	R = (0,0), C = (3,2), * = (-4,-4), r = (-4,4)
%       ----+-+----
%	WXYZ|[|\]^_	\draw -./9:CMV_gpowvukjaWNE=45\end
%	`abc|d|efgh	   draws a reasonable circle
%	ijkl|m|nopq
%	rstu|v|wxyz
%
\newcount\PLv\newcount\PLw\newcount\PLx\newcount\PLy\newdimen\PLyy\newdimen\PLX
\newbox\PLdot \setbox\PLdot\hbox{\tiny.} \def\scl{.08} % resettable scale
\def\PLot#1{\PLx`#1\advance\PLx-42\PLy\PLx\PLv\PLx\divide\PLy9\PLw\PLy\multiply
\PLw9\advance\PLx-\PLw\advance\PLx-4\PLy-\PLy\advance\PLy4\PLX=\the\PLx pt
\advance\PLyy\the\PLy pt\wd\PLdot=\scl\PLX\raise\scl\PLyy\copy\PLdot}
\def\draw#1{\ifx#1\end\let\next=\relax\else\PLot#1\let\next=\draw\fi\next}

%  Girard's inverted ampersand.  Usage: \invamp. Draw time @ 10 Mips: .33 sec
\def\invamp{\hbox{\PLyy=70pt\draw :::;DMV_gqppyyyyyooooxxxnnwvlutkjaWNE=5-./9%
9:::CCCC:::99/..--544=EENWWaajjjkktttttttNNNVVVVVVVV\end \hskip4pt}}
%  \Invamp = Boxed \invamp.  Draw time < .02 sec, but max ~300 chars/page
\newbox\iabox\setbox\iabox\invamp \def\Invamp{\copy\iabox}


Return-Path: <@Sunburn.Stanford.EDU,@sophia.inria.fr:[email-masked]>
Date: Tue, 1 Jun 93 15:59:42 +0200
From: Laneve Cosimo <[email-masked]>
To: [email-masked]
Subject: Interaction Systems 1
Sender: [email-masked]
--text follows this line--

Several people has asked to us the first part of our work
on Interaction Systems:

*****************************************************************

			Interaction Systems I
                 The Theory of Optimal Reductions

          Andrea Asperti                   Cosimo Laneve

      Department of Mathematics,       INRIA - Sophia Antipolis,
      University of Bologna,           2004, Route des Lucioles,
      Piazza Porta S. Donato 5,        B.P.93 - 06902,
      40127 Bologna, Italy.            Sophia Antipolis, France.
      [email-masked]	       [email-masked]

                              Abstract:

A new class of higher order rewriting systems, called Interaction
Systems, is introduced. From one side, Interaction Systems provide the
intuitionistic generalization of Lafont's Interaction Nets 
(recall that Interaction Nets are linear). In particular, we keep the
idea of binary interaction, and the syntactical bipartition of operators into
constructors and destructors. From the other side, Interaction Systems
are the
subsystem of Klop's Combinatory Reduction Systems where the
Curry-Howard analogy still ``makes sense''. This means that we can associate
with every
IS a suitable logical (intuitionistic) system: constructors and destructors
respectively correspond to right and left introduction rules,
interaction is cut, and computation is cut-elimination.

Interaction Systems have been primarily motivated by the necessity of extending
Lamping's optimal graph reduction technique for the lambda-calculus
to other computational constructs than just beta-reduction. This
implementation style can be smootly generalized to arbitrary IS's, providing
in this way a uniform description of essential rules such as conditionals and
recursion.

The optimal implementation of IS's will be only sketched here (it will
eventually be the subject of the Part II). The main aim of this
paper is to introduce this new class of Systems, to discuss the motivations
behind its definition, and to investigate the {\em theoretical} aspect of
optimal reductions (in particular, the notion of {\em redex-family}).

****************************************************************

The paper is available by anonymous FTP from the area 
		    cma.cma.fr
in the directory
		/pub/papers/cosimo 
The file, in postscript compressed form, is named 
		IS1.ps.Z 

Cosimo Laneve


Date: Mon, 7 Jun 1993 10:28:47 +0200
From: [email-masked] (Anne S. Troelstra )
To: [email-masked]
Subject: natural deduction for linear logic; corrections;bibliography
Sender: [email-masked]
--text follows this line--

The following is the abstract of a paper delivered on occassion of Dirk van
Dalen's 60th birthday, in april.

ABSTRACT Natural deduction for intuitionistic linear logic 
by A.S. Troelstra

The paper deals with two versions of the fragment with unit, 
tensor, linear implication
and storage operator (the exponential !) of intuitionistic linear logic. The
first version, ILL, appears in a paper by Benton, Bierman, Hyland and de
Paiva; the second one, ILLP, is described in this paper. ILL has a
contraction rule and an introduction rule !I for the exponential; in ILLP,
instead of a contraction rule, multiple occurrences of labels for
assumptions are permitted under certain conditions; moreover, there is a
different introduction rule for the exponential, !I+, which is closer in
spirit to the necessitation rule for the normalizable version of 
S4 discussed by Prawitz in his monograph ``Natural Deduction''.

It is relatively easy to adapt Prawitz's treatment of natural 
deduction for intuitionistic logic to ILLP; in particular one can 
formulate a notion of strong validity (as in Prawitz's ``Ideas and 
Results in Proof Theory'') permitting a proof of strong normalization.

The conversion rules for ILL explicitly mentioned in the paper by 
Benton et. al. do not suffice for normal forms with subformula property, 
but we can show that this can be remedied by addition of a single conversion 
rule.

ILLP also suggests the study of a class of categorical models, more special
than the class introduced by Benton et. al.

The paper just mentioned can be obtained by anonymous ftp
to vera.fwi.uva.nl, login name: anonymous, password ident.
The paper, and two others (sse below) are contianed in the file pub/illc/astro

The directory "astro" contains files of papers by A.S.Troelstra.

Description of the contents:

1. The file nat.ps is the postscript file of the paper "Natural deduction for
intuitionistic linear logic", report ML-93-09 of The Institute for Logic.
Language and Computation of the University of Amsterdam (ILLC). The paper is 28
pages.

2. The file lincorr.ps contains corrections to the book "Lectures on linear
logic" by A.S. Troelstra
and will be updated if necessary. The list of errata is three pages long.

3. The file linbib.bib is a bibtex file and
contains a bibliography of linear logic compiled by
H.A.J.M. Schellinx and A.S. Troelstra; the file is regularly updated.
Corrections and additions for the bibliography to [email-masked] or
[email-masked] are always welcome.

				A. S. Troelstra

Date: Tue, 8 Jun 1993 08:54:24 +0200
From: [email-masked] (Anne S. Troelstra )
To: [email-masked]
Subject: access file linbib.bib
Sender: [email-masked]
--text follows this line--

I have corrected the permissions. It should be allright now, everyone
can read linbib.bib
		A.S. Troelstra


Return-Path: <@Sunburn.Stanford.EDU:[email-masked]>
From: [email-masked] ( Dr G Bellin tel 2-76933)
Date: Wed, 9 Jun 93 01:37:55 +0100
To: [email-masked]
Subject: Preliminary Announcement 
Sender: [email-masked]
--text follows this line--

                      SLICING THE ADDITIVE BOXES 

                       Preliminary Announcement

                   Gianluigi Bellin and Janice Hudgings
  
                          (Oxford University)

Abstract: In Multiplicative and additive linear logic (without constant) 
the problem of deciding whether an arbitrary family of slices is the slicing 
of a sequent derivation, is polynomial in the size of the the data. 

---------------------------------------------------------------------------
Comments: Slices for MALL- (MALL without weakening for \bottom) are defined 
like multiplicative proof-structures, but with `plus' links and 
*one-premise* `with' links. 

                                Part (i) 

Given a sequent derivation D in MALL- (or the corresponding proof-net with 
additive boxes) we can associate a set Sl(D) of additive slices; such a 
representation of MALL- proofs satisfies the Church-Rosser property. E.g.,

           |- A,-A  |- A,-A     |- A,-A  |- A,-A  
         & ----------------   & ----------------  
               |- A&A, -A          |- A, -A&-A     
           cut -------------------------------
                       |- A&A,   -A&-A      

is sliced into four copies of
  
                       ------    -------
                       A   -A    A    -A
                      ---  --------  -----
                      A&A     cut    -A&-A

The cardinality of the set of slices is determined by the following rule.
If | Sl(D1) | = n and | Sl(D2) | = m, then 
* if D comes from D1, D2 by a with-rule,  then | Sl(D) | = n+m
* if D comes from D1, D2 by a times-rule, then | Sl(D) | = n.m

                           Part (ii) 

Consider the inverse problem, given an arbitrary family of slices {Q1,...,Qn} 
to decide whether there is a sequent derivation D such that 
                    {Q1,...,Qn} = Sl(D). 
Clearly, all the Qi must satisfy the conditions for multiplicative proof-nets;
by a result of Danos, this is quadratic in the size of Q1,...,Qn. 

In addition, we would like to have a non-trivial condition which guarantees
that the we could transform {Q1,...,Qn} into a proof-net with boxes.
We show that the problem of deciding whether or not  a set of multiplicatively 
correct slices {Q1,...,Qn} can be sequentialized is quadratic in the size 
of {Q1,...,Qn}.

We modify the decision procedure for sequent derivations in MALL- by 
Galmiche and Perrier: starting with the conclusions Gamma, the same in 
all slices, we construct a sequent derivation upwards by breaking links
in the following order: (1) par, (2) with, (3) plus, (4) times. 

Step (4) involves finding a splitting times in each slice; this is done by 
testing the empires of the premises of times link. Testing each empire is 
linear in the size of the slice, therefore the process of finding a sequent 
derivation, if it exists, is at worst quadratic in the size of {Q1,...,Qn}.

In the process we obtain a *classification* of the slices;
we increase the number of classes whenever 

* a formula is conclusion of an axiom link in some slices, not in others
                                                   A     B
* at step (2), in different slices we break links --- , ---, with A not= B;
                                                  A&B   A&B
                                                   A     B
* at step (3), in different slices we break links --- , ---, with A not= B;
                                                  A+B   A+B
* at step (4), in different slices the splitting times are different formulas.

Finally, we need check whether the *classification* can be refined to an
appropriate *partition* of the slices (notice that in the case of a &-link 
with conclusion A&A, as in our example, when we proceed upwards we do not 
have enough information to refine our classification). 
Starting from the axioms, we proceed *downwards* as described in part (i) 
to check that ``there is the right number of slices of the appropriate form''. 
Since this involves only testing the data once more, the process remains 
quadratic, as claimed.

                        (Final remarks)

The representation of proofs in MALL- by slicing
* is the only representation (we know) having the Church-Rosser property;
* has a natural interpretation in abstract languages for parallelism,
  e.g., in R.Milner's pi-calculus;
* has a feasible correctness condition, i.e., polynomial time 
  sequentializability. 
It is of course true that sequentializability is not an *interesting* 
correctness condition. The result, however, is itself interesting, since
by a result of Lincoln and Winkler, sequentializability for MALL (MALL- 
with the \bottom rule) is NP-complete. 

References: 
J-Y.Girard, Linear Logic, 1987, Section 6. 
Galmiche and Perrier, Automated Deduction in Additive and Multiplicative
            Linear Logic, in International Symposium on Logical 
            Foundations of Computer Science: Logic at TVER, 
            Tver Region, Russia 1992 ([email-masked])
P.Lincoln and T.Winkler, Constant-only Multiplicative Linear Logic
            is NP-Complete, Preprint. 

(Thanks L.Egidi for conversations on complexity.)