A stronger multiplexing rule for soft linear logic?

Question

In (intuitionistic) linear logic the usual rules for the storage modality $!$ are promotion, dereliction, contraction, and weakening:

$$\frac{!\Gamma\vdash A}{!\Gamma\vdash !A}(prom) \qquad \frac{\Gamma,A \vdash C}{\Gamma,!A\vdash C}(der) \qquad \frac{\Gamma,!A,!A\vdash C}{\Gamma,!A\vdash C}(ctr) \qquad \frac{\Gamma\vdash C}{\Gamma,!A\vdash C}(wk)$$

Lafont's soft linear logic is obtained by observing that these rules are equivalent to soft promotion, multiplexing, and digging:

$$\frac{\Gamma\vdash A}{!\Gamma\vdash !A}(sp) \qquad \frac{\Gamma,\overbrace{A,\dots,A}^n\vdash C}{\Gamma,!A\vdash C}(mpx) \qquad \frac{\Gamma,!!A\vdash C}{\Gamma,!A\vdash C}(dig)$$

and then removing the digging rule. Soft linear logic (SLL) is interesting because it corresponds closely to polynomial-time computation in various precise senses. For instance, Lafont showed that polytime functions are precisely those representable in second-order SLL in a certain sense, while McKinley showed that they are also those representable in a naive set theory based on SLL, and lambda calculi based on SLL can also characterize polytime computation (plus other complexity classes when augmented with additional features).

My question is what happens if in SLL we replace the multiplexing rule (which is actually a rule schema consisting of one rule for each external natural number $n$) with the following "strong multiplexing" or "weak contraction" rule?

$$\frac{\Gamma,!A,A\vdash C}{\Gamma,!A \vdash C}\qquad (*)$$

(and also weakening, which is a special case of ordinary multiplexing but not of $(*)$)

Ordinary contraction says that we can use $!A$ as two $!A$'s — hence any number of $!A$'s, and hence any number of $A$'s — while ordinary multiplexing says that we can use $!A$ as any number of $A$'s as long as we do it all at once. So, for instance, if we have $!A$ and two branches of a derivation both need some $A$'s, then ordinary contraction says we can give them both a whole $!A$, while ordinary multiplexing says we need to decide right away before doing the branch how many $A$'s each branch needs.

The rule $(*)$ seems to be in between: it says that from $!A$ we can extract any number of $A$'s and keep the $!A$ around, but we can't get more than one $!A$. So if we have $!A$ and two branches of a derivation both need some $A$'s, then we can give one of them a whole $!A$ but we need to decide right away how many $A$'s the other branch needs.

The question "what happens" is admittedly a bit vague, but it could be made precise in various ways. Is rule $(*)$ conservative over ordinary multiplexing? Is contraction conservative over rule $(*)$? Does SLL+$(*)$ still correspond to polytime computation, in any or all of the ways that ordinary SLL does? Or does it correspond to some larger complexity class? I would be interested in answers to any of these questions.

(My reason for asking is partly curiosity, but also partly practical: it could be inconvenient for some purposes that ordinary multiplexing is a rule schema indexed by external natural numbers, whereas $(*)$ is a single rule.)

Answer 1

Your rule $(\ast)$ is sometimes referred to as "absorption". I think the first who considered it was Jean-Marc Andreoli in his paper on focusing proofs. Indeed, it makes a lot of sense in proof search: read bottom-up, it says that when you have $?A$ (on the right), you may extract a copy of $A$ and try and do something with it, while keeping $?A$ for future use.

Of course, as you know, absorption plus weakening and promotion (the usual one, i.e., functoriality of $!(-)$ + comonad comultiplication) gives a system equivalent to full linear logic. You are asking about the system obtained by also taking promotion to be strictly functorial (what Lafont calls "soft promotion"). Let me call it $\mathbf{PL}^-$, for reasons I'll clarify momentarily.

As you rightly observe, $\mathbf{PL}^-$ is much more powerful than $\mathbf{SLL}$. Indeed, and this is essentially a computational reformulation of your answer, the untyped term calculus underlying $\mathbf{PL}^-$ is Turing-complete, whereas the untyped calculus underying $\mathbf{SLL}$ has exactly the same expressiveness as $\mathbf{SLL}$: its terms strongly normalize in $O(s^d)$ steps, where $s$ is the size and $d$ the exponential depth of the term being normalized (this is the key feature of so-called "light" logics: their normalization does not rely on the logical complexity of formulas. Types/formulas are there only to ensure that the normal forms are of a prescribed shape: integers, strings, booleans, etc.).

Now I must apologize for invoking my own work, but it is truly relevant to your question: $\mathbf{PL}^-$ is actually the intersection of linear logic and a system I call parsimonious logic ($\mathbf{PL}$), which is a variant of linear logic based on the the fact that the exponential modality obeys the isomorphism

$$!A \cong (A\&1)\,\otimes\,!A$$

and nothing more (except functoriality, of course). With Kazushige Terui, we refer to this iso as Milner's law, because of its similarity with the structural equality $!P\equiv P\mathrel{|}\,!P$ in the $\pi$-calculus (especially if one considers the affine version of parsimonious logic, which is most frequent in applications). Milner's law does not hold in $\mathbf{LL}$, so $\mathbf{PL}$ is not a subsystem of linear logic. On the other hand, the $!(-)$ of linear logic is a comonad and has contraction, which is not the case in $\mathbf{PL}$, so this latter is not a supersystem of $\mathbf{LL}$. Categorically, a model of $\mathbf{PL}$ is just a SMCC with products (in fact, free copointed objects suffice) and with a monoidal endofunctor $!(-)$ satisfying Milner's law (naturally in $A$). Comparatively, models of $\mathbf{LL}$ are much more complex to describe.

As you see, the implication from left to right of Milner's law gives you precisely weakening and absorption (composing with the projections of $\&$, which is the product as usual). So the system you are asking about is $\mathbf{PL}$ with only "half" of Milner's law, and in fact $\mathbf{PL}^-=\mathbf{PL}\cap\mathbf{LL}$.

Not unlike $\mathbf{SLL}$, it turns out that $\mathbf{PL}$ has quite interesting complexity properties. However, quite unlike $\mathbf{SLL}$ and Girard's light linear logic, complexity is not controlled by the structure of the logical rules (they are Turing-complete) but by the types: simply-typed $\mathbf{PL}$ captures $\mathsf L$ (deterministic logspace), whereas $\mathbf{PL}$ with linear polymorphism (i.e., where the $X$ in $\forall X.A$ may only be instantiated with a $!$-free formula) captures $\mathsf P$ (deterministic polytime). I also conjecture that "parsimonious system F" ($\mathbf{PL}$ with full polymorphism) captures primitive recursion. When I say "captures" above I mean that one defines types $\mathsf{Str}$ of binary strings and $\mathsf{Bool}$ of booleans (more or less as usual) and looks at the class of problems decidable by terms of type $\mathsf{Str}\multimap\mathsf{Bool}$ (or instantiations of them when polymorphism is absent/limited).

The side of Milner's law that's missing from $\mathbf{PL}^-$ is necessary for the completeness with respect to logspace and polytime (for instance, without it you cannot type the predecessor with simple types $\mathsf{Nat}\multimap\mathsf{Nat}$). So simply-typed (resp. linear polymorphic) $\mathbf{PL}^-$ does not correspond to any class I know of: you will only be able to solve logspace (resp. polytime) problems in it, but you'll be missing some of those. However, when you have full second order (or when you are untyped), $\mathbf{PL}^-$ seems to be (is) just as expressive as $\mathbf{PL}$. In particular, one may play around with "parsimonious OCaml", which is a (fictional, I haven't implemented it :-) ) variant of OCaml following the type discipline prescribed by $\mathbf{PL}^-$. The funny thing about such a language is that it does not have general fixpoints, only linear fixpoints: when you write

$$\mathtt{letrec}\ \mathtt f\ \mathtt x = \mathtt{code}$$

$\mathtt{code}$ may only contain one occurrence of $\mathtt f$ (in every branch of an $\mathtt{if\ldots then\ldots else}$ statement). Since while loops are exactly linear (tail) recursions, parsimonious Ocaml is Turing-complete. However, there's lots of "natural" OCaml programs you'll have to non-trivially rewrite for them to run in parsimonious OCaml! (Pretty much every structural recursion on binary trees for example). In a sense that I would like (but don't know how) to make precise, parsimonious logic (and hence the logic you are asking about) is the "logic of while loops". I think that this is the ultimate reason why it behaves so well from the complexity viewpoint.

I'm going to stop here and give you some pointers, in case you are more curious. There is a series of papers (by myself and co-authors) on parsimonious logic and complexity, all available on my web page. However, things are a bit scattered here and there and I think that the most readable account is in Chapter 3 of my habilitation thesis, so I suggest you go there instead.

Answer 2

Here is a partial answer: the rule $(*)$ is not conservative over SLL. Indeed, McKinley showed that soft linear set theory with unrestricted comprehension is nontrivial — but adding $(*)$ makes it trivial, by the usual Russell/Curry argument:

Given any proposition $P$, let $C = \{ x \mid \;!(x\in x) \multimap P\}$. Then if $!(C\in C)$, by $(*)$ we can get $!(C\in C)$ and $C\in C$. The latter gives, by definition of $C$, that $!(C\in C) \multimap P$. Combined with the former, we therefore get $P$. So we have shown that $!(C\in C) \multimap P$.

Now we can perform this derivation twice. The second time, we follow it by the observation that, by definition of $C$, the conclusion $!(C\in C) \multimap P$ gives $C\in C$. This derivation of $C\in C$ is in the empty context, so soft promotion gives $!(C\in C)$. Now cut this with the first copy of the derivation of $!(C\in C) \multimap P$ to get $\vdash P$.