Return-Path: <@Sunburn.Stanford.EDU:asperti@cs.unibo.it> Date: Fri, 21 May 1993 12:28:40 +0200 From: asperti@cs.unibo.it (Andrea Asperti) To: linear@cs.stanford.edu Subject: paper announcement Sender: lincoln@cs.stanford.edu --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. asperti@cs.unibo.it cosimo@garfield.cma.fr 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:pt@doc.ic.ac.uk> From: Paul Taylor Date: Wed, 26 May 1993 17:38:45 +0100 X-Mailer: Mail User's Shell (7.2.3 5/22/91) To: linear@cs.stanford.edu Subject: par symbol in TeX Sender: lincoln@cs.stanford.edu --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: To: linear@cs.stanford.edu Subject: Re: par symbol in TeX Date: Thu, 27 May 93 17:33:46 PDT From: pratt@CS.Stanford.EDU Sender: lincoln@cs.stanford.edu --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.) Return-Path: <@Sunburn.Stanford.EDU:sa@doc.ic.ac.uk> Date: Fri, 28 May 1993 18:08:22 +0100 (BST) From: Samson Abramsky Mime-Version: 1.0 Content-Type: text/plain; charset=US-ASCII To: linear@cs.stanford.edu Subject: Thomas Streicher's message Sender: lincoln@cs.stanford.edu --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:bellin@ox.ac.uk> From: Gianluigi Bellin Date: Mon, 31 May 1993 19:11:48 +0100 To: linear@cs.stanford.edu Cc: bellin@maths.ox.ac.uk Subject: paper announcement Sender: lincoln@cs.stanford.edu --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: Date: Mon, 31 May 93 19:06:43 PDT From: Vaughan Pratt To: linear@cs.Stanford.EDU Subject: Portable par Sender: lincoln@cs.stanford.edu --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:cosimo@garfield.cma.fr> Date: Tue, 1 Jun 93 15:59:42 +0200 From: Laneve Cosimo To: linear@cs.stanford.edu Subject: Interaction Systems 1 Sender: lincoln@cs.stanford.edu --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. asperti@cs.unibo.it cosimo@garfield.cma.fr 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 Return-Path: From: anne@fwi.uva.nl (Anne S. Troelstra ) X-Organisation: Faculty of Mathematics & Computer Science University of Amsterdam Plantage Muidergracht 24 NL-1018 TV Amsterdam The Netherlands X-Phone: +31 20 525 5200 X-Telex: 16460 facwn nl X-Fax: +31 20 525 5101 To: linear@cs.stanford.edu Subject: natural deduction for linear logic; corrections;bibliography Sender: lincoln@cs.stanford.edu --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 anne@fwi.uva.nl or harold@fwi.uva.nl are always welcome. A. S. Troelstra Date: Tue, 8 Jun 1993 08:54:24 +0200 Return-Path: From: anne@fwi.uva.nl (Anne S. Troelstra ) X-Organisation: Faculty of Mathematics & Computer Science University of Amsterdam Plantage Muidergracht 24 NL-1018 TV Amsterdam The Netherlands X-Phone: +31 20 525 5200 X-Telex: 16460 facwn nl X-Fax: +31 20 525 5101 To: linear@cs.stanford.edu Subject: access file linbib.bib Sender: lincoln@cs.stanford.edu --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:bellin@maths.ox.ac.uk> From: bellin@maths.ox.ac.uk ( Dr G Bellin tel 2-76933) Date: Wed, 9 Jun 93 01:37:55 +0100 To: linear@cs.stanford.edu Subject: Preliminary Announcement Sender: lincoln@cs.stanford.edu --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 (galmiche@loria.crin.fr) P.Lincoln and T.Winkler, Constant-only Multiplicative Linear Logic is NP-Complete, Preprint. (Thanks L.Egidi for conversations on complexity.)