Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
I reorganized linearly distributive category by moving the long block of history down to the bottom, adding an “Idea” section and a description of how $*$-autonomous categories give rise to linearly distributive ones and linearly distributive ones give rise to polycategories. I also cross-linked the page better with polycategory and star-autonomous category.
Thanks, Mike!
It should be pointed out that at least some of those coherence conditions are essentially tensorial strength conditions (noting that each of those $\delta$’s, read as strengths, can be read either as $\otimes$-ing with $A$ is strong over $\wp$, or $\wp$-ing with $A$ is strong over $\otimes$).
Feel free to add that to the page… (-:
The notion of linearly distributive category is not very intuitive to me, particularly as regards these constructions. I mean, looking at the definition of star-autonomous category, I don’t “see” a linearly distributive category underneath — heck, the definition doesn’t even include $\parr$ — and looking at the definition of linearly distributive category, I don’t “see” a polycategory underneath. Maybe I just need to practice to improve my vision, but if anyone can provide some extra intuition I wouldn’t mind.
I don’t know that I can help much, Mike. But usually I revert back to $\ast$-autonomous categories, knowing that every linearly distributive category (aka “weakly distributive category” back in the day) comes canonically from a $\ast$-autonomous category: if $C$ is linearly distributive then the unit $C \to U F C$ is an equivalence of linearly distributive categories, where $F \dashv U: \ast-Auton \to LinDist$ is the free-forgetful adjunction. (Linear logic is a conservative extension of the $(\otimes, \parr)$-fragment.)
From that point of view, the strengths just come from a corresponding strength for $\ast$-autonomous categories, e.g., $a^b \otimes c \to (a \otimes c)^b$ where $a^b$ is alternate shorthand for $b \multimap a$. (A fact that is useful: if $V$ is symmetric monoidal closed, then any unary functor $V \to V$ definable in the language of smc categories carries a canonical strength, in fact a unique strength by the coherence for smc categories. This extends to the case where we include contravariant functors $V \to V$ along with the covariant ones, although the notion of tensorial strength for contravariant functors might not be as well-known as for covariant ones.)
As for seeing the polycategory underneath, I guess you know that linearly distributive categories were invented in the first place to explain what polycategories are from the viewpoint of categorical algebra. You yourself wrote the blurb on how you get a polycategory out of a linearly distributive category (so again I don’t know I can help much further), but again, my tendency is to think directly in terms of linear logic and $\ast$-autonomous categories, where we know how to interpret two-sided sequents $A_1, \ldots, A_m \to B_1, \ldots, B_n$. Thus, if you can see an underlying polycategory in a $\ast$-autonomous category (or if you know how to build a $\ast$-autonomous freely out of two-sided sequents), then you can in a linearly distributive category (more directly in fact, since we cut out the linear $\neg$ middleman).
By the way, I wouldn’t say that polycategories are a “natural categorical semantics” for linearly distributive categories [1] – if I’d say anything along these lines, I’d say that’s backwards: it’s more that linearly distributive categories provide categorical semantics for polycategories! But even that is not how I’d put it. Normally one refers to categorical semantics of various fragments of (e.g. propositional) logic, so I’d really rather say that linearly distributive categories provide a semantics for the multiplicative conjunction and disjunction fragment of (linear) logic. Polycategories are actually slightly alien from the viewpoint of category theory, since we cut at only one formula at a time, but linearly distributive categories is how a category theorist might make sense of them.
[1] In fact I think it’s just wrong to say polycategories are a semantics for ld categories or for the $(\otimes, \parr)$-fragment, since general polycategories don’t interpret formulas $A \otimes B, A \parr B$.
Did I say that polycategories are a categorical semantics for linearly distributive categories? I agree that that makes no sense — categorical structures are categorical semantics for logic, not for each other. If that’s on one of the pages it should be fixed.
Richard Garner’s approach to polycategories (cited on the page now) describes them with a “multi-object cut” in terms of a pseudo-distributive law. In fact I think there is a theory of “generalized polycategories” analogous to “generalized multicategories” but as far as I know no one has written it down yet.
Regarding intuition, to be honest I still struggle with all three of these structures on their own, even before thinking about how they relate to each other. The cut rule for linear logic is still strange to me, possibly coming down to the meaning of $\parr$ again — how can you have a “disjunction” where you don’t know which of the disjuncts is true, but nevertheless you somehow have to “use up the resources” involved in all of them? Possibly what I need to do is spend more time with concrete examples like Chu constructions.
No, you didn’t say that. But it’s on the polycategory page (sorry not to have specified that earlier).
Now that you mention Richard Garner, I vaguely remember that Robin Houston also had a neat way of thinking about polycategories or $\ast$-autonomous categories, which I’ll try to recall when I have some time.
There are some good examples of linearly distributive categories on the star-autonomous category page, so that might be worth a look. However, another source of intuition though is proof nets. Is that something you’ve played with? The validity criterion for proof nets relies crucially on the structure of $\parr$-connectives (meaning instances of $\parr$ when looking at positive formulas, i.e., formulas of $\Delta$ on the right of a sequent $\Gamma \to \Delta$, or instances of $\otimes$ when looking at negative formulas, i.e., formulas of $\Gamma$).
I should really spend some time writing some of this up at the nLab, because it’s closely connected with my PhD thesis. In the meantime, you might also benefit from reading Girard’s original article Linear Logic and especially where he gets into proof nets and his “cyclic trips” and his longtrip criterion, which is the kind of thing I’m alluding to in the previous paragraph. A more streamlined approach to proof nets was later given by Danos and Regnier.
But in a nutshell, to decide whether a proof structure on a sequent $\to \Gamma$ is a proof net (is derivable in the theory of say $\ast$-autonomous categories or linearly distributive categories), the criterion is basically that for all the $2^n$ ways of setting switches at the $n$ $\parr$-connectives occurring in subformulas of $\Gamma$, the result is an acyclic connected graph – a tree. (For the moment I’m considering only those $\Gamma$ in which monoidal units do not appear – how to handle units requires an extension which was a major part of my thesis.)
Bah – I’m doing a terrible job trying to discuss this here. So much to say. I’d better spend some time in the Lab and organize my thoughts there, and when I come back up for some air, maybe we can discuss this further.
I don’t see it on the polycategory page either; what I see under “Internal logic” is “Polycategories provide a natural categorical semantics for linear logic.”
I’ve looked at proof nets a little, a while ago, but I don’t think they really help; it seems to me just a way of reformulating the confusing thing that doesn’t make it any less confusing.
Oops. So it does. My bad (although I still think that sentence needs to be brushed up a little).
Feel free to brush it up. (-: If what you’re worried about is that polycategories don’t have connectives, then maybe “…for the judgmental structure of classical linear logic”?
Is it true that any symmetric monoidal category is linearly distributive (but not, of course, $\ast$-autonomous) if we define $\parr = \otimes$?
Yes, all the required structure and coherence conditions follow straight from coherence for symmetric monoidal categories.
Great. I added that to the page. Two related questions:
Do you know whether anyone has written down a type theory for “symmetric monoidal categories regarded as linearly distributive”? I’m imagining a sequent calculus with multiple formulas in both antecedent and consequent, and where you’re allowed to cut on multiple formulas at once.
What is the free $\ast$-autonomous category on a symmetric monoidal category regarded as linearly distributive? Does it have a nice description?
I don’t know an answer to 1 off hand. But the lack of such might be related to an observation below.
The free $\ast$-autonomous category in this case would coincide with the free compact closed category. From a sequent calculus perspective, this is (I think) a weird case because IIRC there’s no good cut-elimination procedure. (Notice that string-theoretically, composition can produce loops or islands, which in the case of free compact closed categories on a category $C$, must be accounted for by taking the trace of a category $C$. Meanwhile loops don’t occur in a cut-free fragment, unless perhaps they are put in by hand as axioms, for each $C$.)
I am not aware of any really clean way of describing the free compact closed category on a symmetric monoidal category. The free compact closed category $F(C)$ on a category $C$ has I think a halfway decent description in terms of a kind of wreath product $F(1) \wr C$ where edges of graphs in $F(1)$ are labeled by morphisms in $C$ (and loops by elements of $tr(C)$). If $S(C)$ is the free symmetric monoidal category on $C$, then I guess the relatively free compact closed category on a symmetric monoidal category $C$ can be formed as a suitable kind of 2-colimit (a co-isoinserter? not sure) of a diagram of type
$F S C \rightrightarrows F C$which could be further described by applying rewrite rules on morphisms of $F C$, but I’m not sure such rewrite rules can be organized nicely.
Interesting; that will take some thought. Can you give any intuition for why the free $\ast$-autonomous category on a symmetric monoidal category qua linearly distributive category would coincide with the free compact closed category?
The free $\ast$-autonomous category on a linearly distributive category is formed by adjoining (in the doctrine of linearly distributive categories) objects $\neg A$ and arrows
$\top \to A \parr \neg A, \qquad \neg A \otimes A \to \bot$subject to triangular equations
$1_A = \left( A \cong \top \otimes A \to (A \parr \neg A) \otimes A \stackrel{dist}{\to} A \parr (\neg A \otimes A) \to A \parr \bot \cong A \right)$ $\,$ $1_{\neg A} = \left( \neg A \cong \neg A \otimes \top \to \neg A \otimes (A \parr \neg A) \stackrel{dist}{\to} (\neg A \otimes A) \parr \neg A \to \bot \parr \neg A \cong \neg A \right)$and where we have $\parr = \otimes, \bot = \top$, this is exactly how one would form the free compact closed category generated by the symmetric monoidal category $C$.
This construction is mentioned both in the original Cockett-Seely paper (page 159 ff) and in Blute-Cockett-Seely-Trimble.
By the way, that Cockett-Seely paper also handily spells out the definition of polycategories (which is due to Manfred Szabo); someone should just copy that over to the nLab (and that someone could be me).
Ah, I see! Somehow that makes $\ast$-autonomous categories and linearly distributive categories make some more sense to me: a $\ast$-autonomous category is one which is almost compact closed, but where the unit and counit of the “dualities” use different monoidal structures; and a linearly distributive category is one with two monoidal structures that interact in exactly the way that’s necessary for this to make sense.
Does it ever happen nontrivially (i.e. apart from the case where the two monoidal structures coincide) that the distributors in a linearly distributive category are isomorphisms?
Yes, exactly.
I’m pretty sure that if those constraints are isomorphisms, then the monoidal structures coincide. I should work this out more explicitly to satisfy myself, but this should be related to Brian Day’s result that when one localizes the free symmetric monoidal closed category on a symmetric monoidal category with respect to the strength constraints $(A \multimap B) \otimes C \to A \multimap (B \otimes C)$ (i.e., forcing them to be isomorphisms), then you get the free compact closed category on the symmetric monoidal category. That strength constraint corresponds to the linear distributivity.
Ah, I take it back: Cockett-Seely, 5.3 and 5.4, specify that linearly distributive categories where the distributivities are isomorphisms are the same as “shifted” (symmetric) monoidal categories. If I’m not mistaken, supervector spaces provides an instructive example of this.
Nice. I should have read that paper more carefully.
One other reason the notion of linearly distributive category is difficult for me is that it isn’t usually “packaged” in a categorically nice way, making it seem somewhat ad hoc. For instance, the notion of duoidal category seems a little weird when written out explicitly, but it makes more sense when you say that it’s just a pseudomonoid in the 2-category of monoidal categories and lax monoidal functors. The observation about tensorial strength is partway to the sort of thing I would like to say, but it doesn’t describe the structure completely.
Here’s a first attempt. If $C$ is any monoidal category, then there is a 2-category of (pseudo) $C$-modules (which I guess some people call “actegories”) and lax $C$-module morphisms. As noted at the page tensorial strength, we can regard $C$ as a $C$-module, and in this case the lax $C$-module maps $C\to C$ are precisely the tensorially-strong endofunctors. Now in fact, at least if $C$ is symmetric, then the 2-category of $C$-modules should be a 2-multicategory, where the multimorphisms are “lax in each variable separately”. One might then hope that a symmetric linearly distributive category is precisely a symmetric monoidal category $(C,\otimes)$ together with the structure $\parr$ of a symmetric pseudomonoid in this 2-multicategory on $C$ regarded as a $C$-module. However, this doesn’t seem quite right; I can’t see how to get out of it the “distribution and distribution” axiom in Cockett-Seely. Does it follow somehow? Or can one modify this definition so as to be able to get it out?
I added some more remarks to linearly distributive category and star-autonomous category based on this discussion.
Thanks for taking the time to help me understand all this, by the way.
One reason ordinary dual objects are interesting is that they allow us to define traces. With the “unit” and “counit” defined using different monoidal structures in a $\ast$-autonomous category, we can’t define a trace in the usual way. But this problem is somewhat reminiscent to me of what happens with bicategorical traces, so I wonder whether it has a similar solution. If we equip a $\ast$-autonomous category $C$ with a functor $sh:C\to D$ and isomorphisms $sh(A\otimes B) \cong sh(A\parr B)$, then we could define the trace of any endomorphism $f:A\to A$ to be the composite
$sh(\top) \to sh(A\parr A^*) \xrightarrow{f} sh(A\parr A^*) \cong sh(A^* \parr A) \cong sh(A^* \otimes A) \to sh(\bot)$I wonder whether there are any interesting examples of this?
I added a sketch definition of the 2-category of linearly distributive categories, and a remark that the forgetful functor from $\ast$-autonomous ones to linearly distributive ones also has a right adjoint. I also uniformized the notation on the page to $(\otimes,\top)$ and $(\parr,\bot)$ for the monoidal structures; I hope no one objects to that.
Actually, I now realized that there are actually three different notions of functor between linearly distributive category that appear in the literature: the Cockett-Seely “linear functors”, the linear functors whose $\otimes$-part and $\parr$-part agree as functors (which I’m tempted to call “Frobenius linear functors”), and the ones that moreover are strong monoidal for both structures. The “$\ast$-autonomous nucleus” of a linearly distributive category uses “linear functors”, whereas the free linearly distributive category on a polycategory uses strong Frobenius linear functors. Which notion of functor is the free $\ast$-autonomous category on a linearly distributive category (#16 above) free with respect to? I’m guessing also the strong Frobenius ones?
Dating back to revision 8 (Mike Shulman): “At that time this was generally thought to be a rather unsatisfactory and unnecessarily technical solution especially when compared to the normal forms to which the community was accustomed.”
Not that I’m doubting this, but it’s the first time I’m learning about it. Any citations?
Looks to me like that phrase was added in revision 5 by Urs.
I don’t remember writing this, nor do I know half of what it’s saying. If it was me who entered this into the entry, it must have been in helping somebody else get their comment into the $n$Lab. This must have been written by somebody with inside knowledge of the linear logic community – not me. Maybe this was a contribution to another forum or blog, and was thought to deserve to be archived on the $n$Lab. Feel free to edit as need be.
My guess is that Revision 5 was the outcome of the merger Urs made described at the following link.
https://nforum.ncatlab.org/discussion/6517/weakly-distributive-category/
If so, I’d guess that Robin Cockett is the author.
Okay, thanks – all that makes sense. Robin would be in a position to know I think.
1 to 33 of 33