8
$\begingroup$

Has anyone studied a variant of linear logic, or of its semantic counterpart (exponential modalities on linearly distributive categories / $\ast$-autonomous categories / polycategories) for which there is a distributive law

$$!? \to ?!$$

Presumably it would need to interact sensibly with the (co)monoidal structure of ! and ?. I haven't thought about whether there is a nice sequent calculus or resource interpretation. I ask for two reasons:

  1. Such a distributive law should imply that there is a "mixed Kleisli category" whose morphisms from $A$ to $B$ are the morphisms $!A \to ?B$. This would be more symmetrical and pleasing than the usual translation of classical logic involving morphisms $!?A \to ?B$.

  2. In $\rm Chu(Cat,Set)$ I believe there is such a distributive law, or at least a pseudo-distributive law, and a morphism $!A\to ?B$ should be precisely a profunctor from $A^+$ to $B^-$. So this would give a nice way of recovering $\rm Prof$ from $\rm Chu(Cat,Set)$.

$\endgroup$
3
  • $\begingroup$ The closest thing I can think of is differential linear logic, in which $A\multimap\,!A$ (and therefore $?A\multimap A$) is provable, so the distributive law you mention becomes provable, but the structure is too symmetric (the converse distributivity holds in the same way). In his Ph.D. thesis, Stéphane Gimenez considered differential linear logic with a "super-promotion" rule (which is asymmetric), but he didn't have distributive laws in mind, I'm not sure how relevant his work is for what you have in mind. $\endgroup$ Jun 8, 2020 at 6:04
  • $\begingroup$ Their is the paper On the Unity of Logic: a Sequential, Unpolarized Approach by Norihiro Yamada that adds the distributive law to a substystem of linear logic. $\endgroup$
    – Potato44
    Oct 9, 2020 at 8:28
  • $\begingroup$ @Potato44 Thanks! That certainly answers the question ("Has anyone studied..."), so if you post it as an answer I'll accept it. $\endgroup$ Oct 9, 2020 at 15:48

1 Answer 1

2
$\begingroup$

I would tend to say "no".

However, besides my comment above, which is not very pertinent, let me mention the paper Combining effects and coeffects via grading, by Marco Gaboardi, Shin-ya Katsumata, Dominic Orchard, Flavien Breuvart and Tarmo Uustalu. They consider "graded" monads and comonads, which include usual monads and comonads as the special case in which the grading is trivial (I don't know who introduced these first, I learned of graded comonads from this note by Paul-André Melliès). The programming language underlying their work is linear and their comonads are graded in a semiring (rather than just a monoid) so that they are a generalization of the exponential modality $!(-)$ of linear logic (the additive structure of the semiring grades weakening/contraction, i.e. the monoidal structure of the comonad, while the multiplicative structure of the semiring grades the actual comonad structure, i.e., the counit and the comultiplication). They then study graded versions of the usual distributive law between monads and comonads in order to account for the simultaneous presence of "quantitative" effects and coeffects in programming languages (e.g., not just tell whether a program may raise an exception but tell, if possible, how many exceptions it will raise, or whatever. This is what the increased expressiveness given by the grading is meant to be used for).

So, forgetting the grading, i.e., if we grade everything with the trivial semiring and the trivial monoid, we are close to what you describe, but not quite: while the trivially graded version of their comonad is, indeed, the $!(-)$ modality of linear logic, the $?(-)$ modality does not fit into their axiomatization, because the trivially graded version of their monad is necessarily strong, and $?(-)$ is not a strong monad. So, strictly speaking, this work says nothing about the distributive law you are looking at.

I skimmed through the references given by Gaboardi et al. in relation with distributive laws and none of them seems to mention linear logic. This supports my belief that no one has ever introduced/studied the variant of linear logic you mention... but of course I can't be sure!

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.