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.
1 to 20 of 20
Blute-Cockett-Seely-Trimble describes a string diagram / circuit diagram / proof net calculus for linearly distributive categories, which is significantly complicated by the presence of units; as discussed in section 2.3 of the paper, some of the unit and counit links have to be “attached” to other strings to prevent diagrams that should be distinct from getting identified. However, the example given there depends on the fact that the units and for the tensor and cotensor products are different; as noted therein, if in the example were replaced by then the two problematic diagrams would represent the same morphism. This makes me wonder, if we have a linearly distributive category that happens to satisfy , then does the whole string diagram calculus work without these extra attachments?
This would be especially convenient because any closed monoidal category can be embedded by a closed functor into a linearly distributive (indeed -autonomous) category in which , namely . So we could soundly use linearly distributive string diagrams to reason about closed monoidal categories, without the need for the clunky “boxes” that are sometimes used to deal with internal-homs.
Oops, I’m not sure why I thought the embedding of in is closed; it’s strong monoidal but doesn’t preserve internal-homs. So that’s not as interesting as I thought it was.
Sorry, I’ve been away from the nForum for a while. I’m pretty certain that the usual string diagram calculus (or the calculus of ordinary proof nets or Kelly-Mac Lane graphs) suffices for the case . I think this equation is sometimes referred to as the “mix” rule, and that a reference for the claim might be Blute’s thesis.
Ah, interesting; I hadn’t made the connection, but now I can see that that’s similar to the mix rule. I’ve usually seen the mix rule as
which I can see follows from and a cut. I guess there should be a 0-ary mix rule
as well? Do these two rules suffice to prove ?
Hi, one reference is Cockett and Seely, Proof theory for full intuitionistic linear logic, bilinear logic, and mix categories. An “isomix” category is one where ⊤≅⊥ — Lemma 6.6.
Thanks, Sam; that is also, I imagine, a better reference than Blute’s thesis for the claim about coherence.
Ah, thanks! I’ve read other parts of that paper, but always skipped the bit about mix. (-: I created mix rule to record this.
Thanks, Mike!
Thanks. I added a link from compact closed categories.
I think mix gives a different perspective on composition and perhaps hypergraphs are the right place to consider mix.
Say a “hypergraph” on a set of vertices is a species coloured by , ie a presheaf on the free symmetric monoidal category generated by .
Then we can say a “mix hypergraph” is a monoid for the Day convolution structure. It’s a model of linear logic without any connectives, without cut, but with mix.
If we consider hypergraphs with an involution on , then we can also define “traced -hypergraph” as one where every edge on has an associated trace edge on , satisfying some conditions.
And then I think we can define “traced mix -hypergraph”, by putting on some more coherence conditions. Polycategory-like composition can then be defined by first using mix and then tracing. So traced mix -hypergraphs can be thought of as polycategories, and hopefully the representable ones are precisely the compact closed categories.
Shouldn’t you consider directed hypergraphs, maybe as presheaves on ?
I was thinking of one sided sequents. So for each list of vertices, there is a set of edges. And mix associates to each edge on , and each edge on , an edge on .
But for the 2-sided formulation, I agree, a directed hypergraph should have, for each pair of lists of edges, a set of vertices. I suppose you meant ?
Yes, . It seems to me like if you want something with “no connectives” your sequents should be 2-sided; making things 1-sided generally presupposes a negation connective.
Is there a standard notion of “mix polycategory”? It seems like kind of the “dual” of a properad: a polycategory composes only simply connected graphs, a properad composes connected ones, a prop composes arbitrary ones, while a “mix polycategory” would I guess compose disjoint unions of simply connected ones.
Hi Mike, I have been meaning to come back to this because the literature on these things seems sparse and perhaps you or others understand it better than me. Regarding the role of negation,
When you form , it seems that you are freely adding a strict negation, in a similar way to the way that a multicategory is a coloured PRO, is that right?
In many presentations of classical linear logic, it seems that negation is not a “connective” but something more primitive. e.g. wikipedia
Do you know examples of naturally occurring linear distributive categories that are not *-autonomous, but that still feel like models of classical linear logic? (so other than distributive lattices and when the two monoidal structures coincide?)
Good questions.
I don’t think so; if is a presheaf on then means a morphism , and there’s no operation that mixes the ’s and the ’s.
Right, it took me a long time to really understand this. The key phrase that helped me is negation normal form, which means a way of expressing a formula in which all the negations are “pushed all the way inside”. The provable laws of ordinary classical (linear) logic, in which negation is a connective, imply that every formula is equivalent to one in negation normal form. This suggests that we could set up a system in which only formulas in negation normal form are permitted, where “negation” is an operation on formulas (i.e. on syntax) rather than a connective (an inductive constructor of syntax). It’s actually the same sort of thing as cut-elimination: every derivation is equivalent to one in “normal form” that doesn’t use cut, so we can set up a system in which only cut-free derivations exist, with cut as an operation on cut-free derivations (i.e. given cut-free derivations of and we can construct a cut-free derivation of ).
No. (-:
Re: the third question, I don’t know whether to consider Dialectica-like models as “naturally occurring”, but they do give examples. E.g. if you apply a Dialectica construction to the fibration of subobjects in a cartesian closed coherent (but not Boolean) category, I think you get a linearly distributive category that is not -autonomous, not a distributive lattice, and whose two monoidal structures don’t coincide.
Hi, Thanks for the Dialectica idea, I’ll have a look.
Regarding 1 in #16. I’ll say that a “strict *-polycategory” is a polycategory with involution where and . And I’ll assume all polycategories are symmetric. So a strict *-polycategory might as well be one-sided. We could even define it this way, with a one-sided composition . I think many naturally occurring models of CLL are of this form.
Now what I meant was that if is a polycategory with objects then it seems we can define a strict *-polycategory with objects by saying that , and that , and something about the permutation action. (This might well be a free construction.) And now I think we can regard a polycategory over as the same thing as a strict *-polycategory over that satisfies the last two conditions.
This seems to be in line with how you were defining directed hypergraphs. The point I was trying to make is that just as sometimes coloured PROs seem more basic than multicategories (and vice versa), so the same might be true for 1- versus 2-sided sequent calculi.
I agree that you can freely generate a -polycategory from any polycategory in that way, and that you should be able to recover the original polycategory in sort of the same way that you can recover a multicategory from the monoidal category that it freely generates. But in such an -polycategory a morphism has both a source and a target, each of which can contain both objects and their duals, so there is a formal distinction between “ in the domain” and “ in the codomain” that isn’t present in .
This may be what you’re trying to get at with a “strict” -polycategory, if by “” you mean a literal equality of ZFC-style sets. But that sort of definition is fraught with problems, so if that’s what you want I think it’s better to actually define it one-sidedly. (In the literature on cyclic operads, the one-sided versions are called “entries-only”.) So we’re not “freely adding” a strict negation, we’re just representing domains and codomains in a different equivalent way.
By the way, although one of the early definitions of “PRO” included the assumption that it was generated by a multicategory (i.e. every morphism with target is a tensor product of morphisms with target ), nowadays people don’t usually include that. So not every PRO is generated by a multicategory.
Thanks Mike. Yes, that’s what I meant. (I also prefer the one-sided version than the strict thing I wrote, but I got the impression that you didn’t like one-sided things, perhaps mistakenly.) I’d still like to put , if you don’t mind. So can I put it like this?:
To give a polycategory with object set is to give an entries-only *-polycategory with object set where such that a permutation condition holds.
(I think the permutation condition is that the presheaf on comes from a presheaf on .)
I did think this would be a free construction, left adjoint to a forgetful functor (EntriesOnly-*Poly) (Poly), but I haven’t checked.
In general I prefer two-sided things, but I prefer honestly one-sided things over one-sided things that are pretending to be two-sided. (-:
Would you like to make star-polycategory?
1 to 20 of 20