Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: deprecated: logic

Topic: Inference rules for sequents without exchange

Shea Levy (Oct 16 2020 at 11:00):

I'm trying to get a better handle on sequent calculus, in part to get a better intuition for polycategories down the road, and I noticed subtle differences in where inference rules (other than exchange and cut) act between the nLab article, the Wikipedia article, and the Sequent Calculus Primer linked from nLab.

With weakening, for example, nLab gives us:

$$\frac{ \overrightarrow{\phi}, \overrightarrow{\psi} \vdash \overrightarrow{\chi} }{ \overrightarrow{\phi}, \alpha, \overrightarrow{\psi} \vdash \overrightarrow{\chi} } \,$$

and

$$\frac{ \overrightarrow{\phi} \vdash \overrightarrow{\psi}, \overrightarrow{\chi} }{ \overrightarrow{\phi} \vdash \overrightarrow{\psi}, \alpha, \overrightarrow{\chi} } \,$$

Wikipedia gives us:

$$\frac{ \overrightarrow{\phi} \vdash \overrightarrow{\chi} }{ \overrightarrow{\phi}, \alpha \vdash \overrightarrow{\chi} } \,$$

and

$$\frac{ \overrightarrow{\phi} \vdash \overrightarrow{\chi} }{ \overrightarrow{\phi} \vdash \alpha, \overrightarrow{\chi} } \,$$

and the primer gives us:

$$\frac{ \overrightarrow{\psi} \vdash \overrightarrow{\chi} }{ \alpha, \overrightarrow{\psi} \vdash \overrightarrow{\chi} } \,$$

and

$$\frac{ \overrightarrow{\phi} \vdash \overrightarrow{\psi} }{ \overrightarrow{\phi} \vdash \overrightarrow{\psi}, \alpha } \,$$

They all three have cut only acting on the first element of the LHS and the last element of the RHS, so we can't just say Wikipedia and the primer have different notation unless this is a typo.

In the absence of exchange, are these interestingly different? Which one is "correct"/standard?

Amar Hadzihasanovic (Oct 16 2020 at 14:32):

In planar polycategories, for which the exchange rule is not sound, you have four inequivalent cut rules Screenshot-from-2020-10-16-17-30-58.png

Amar Hadzihasanovic (Oct 16 2020 at 14:33):

Whereas for weakening and contraction I believe you should use the “most generic” form, the nLab one (where the contexts on either side are allowed to be empty).

Amar Hadzihasanovic (Oct 16 2020 at 14:38):

I wouldn't exclude that “weakening on one side only” could be interesting in specific contexts, though -- perhaps in sequent calculi that are asymmetric in some specific way, eg sequent calculi for skew-monoidal categories

Shea Levy (Oct 16 2020 at 14:44):

Amar Hadzihasanovic said:

In planar polycategories, for which the exchange rule is not sound, you have four inequivalent cut rules Screenshot-from-2020-10-16-17-30-58.png

Is there an intuition for why these 4?

Amar Hadzihasanovic (Oct 16 2020 at 14:46):

This is from Craig Pastro's thesis -- “double” wires stand for multiple (0 or more) wires Screenshot-from-2020-10-16-17-45-22.png

Amar Hadzihasanovic (Oct 16 2020 at 14:47):

They correspond to the ways that two boxes with multiple input and multiple output wires can be connected along a single wire, without any of their wires “crossing”

Shea Levy (Oct 16 2020 at 14:47):

Amar Hadzihasanovic said:

I wouldn't exclude that “weakening on one side only” could be interesting in specific contexts, though -- perhaps in sequent calculi that are asymmetric in some specific way, eg sequent calculi for skew-monoidal categories

Yeah, the wiki paragraph on ordered type systems made me think the asymmetry might be desirable, given that stacks are asymmetric (direct access to "top", have to pop everything off to get to "bottom"). But wasn't sure how much intutition to take from that, especially since they don't have weakening or contraction

Shea Levy (Oct 16 2020 at 14:49):

Amar Hadzihasanovic said:

They correspond to the ways that two boxes with multiple input and multiple output wires can be connected along a single wire, without any of their wires “crossing”

Thanks! I really need to start thinking more visually as I get further into category theory... I have a very algebraic approach so far

Shea Levy (Oct 16 2020 at 14:50):

Amar Hadzihasanovic said:

This is from Craig Pastro's thesis -- “double” wires stand for multiple (0 or more) wires Screenshot-from-2020-10-16-17-45-22.png

https://arxiv.org/abs/math/0312422?

Amar Hadzihasanovic (Oct 16 2020 at 14:51):

Yes, I think polycategories are much easier to understand with the graphical calculus...

Amar Hadzihasanovic (Oct 16 2020 at 14:51):

Shea Levy said:

https://arxiv.org/abs/math/0312422?

Yes, that's the one! Probably a good starting point.

Cole Comfort (Oct 16 2020 at 14:58):

It is worth noting that polycategories thar are "representable on both sides" in the appropriate sense are linearly distributive categories, for which proof nets are the 2 dimensional graphical calculus. And there is even a 3 dimensional graphical calculus which avoids the awkwardness around the units.

Shea Levy (Oct 16 2020 at 15:01):

Is "the graphical calculus" something specific?

Chad Nester (Oct 16 2020 at 15:45):

@Shea Levy this explains what all this is about in a relatively approachable way: https://www.math.mcgill.ca/rags/misc/proof_theory-essay.pdf

Shea Levy (Oct 16 2020 at 16:35):

Amar Hadzihasanovic said:

In planar polycategories, for which the exchange rule is not sound, you have four inequivalent cut rules Screenshot-from-2020-10-16-17-30-58.png

Reading a bit through the thesis... Is there a reason to require planarity? Why not just allow cut in arbitrary places like nlab has for weakening etc.?

Chad Nester (Oct 16 2020 at 18:01):

The only time I’ve ever seen the planar version outside of the papers on linearly distributive categories themselves is in this line of work (formal grammar): https://arxiv.org/abs/1112.6384

Chad Nester (Oct 16 2020 at 18:05):

... I think there’s a whole book about this, but I can’t seem to find the title!

Shea Levy (Oct 16 2020 at 18:10):

Chad Nester said:

The only time I’ve ever seen the planar version outside of the papers on linearly distributive categories themselves is in this line of work (formal grammar): https://arxiv.org/abs/1112.6384

Yeah, it's just the frequent disjunction between planar and symmetric that's confusing to me. Why does lack of exchange imply we must want planar?

John Baez (Oct 16 2020 at 18:14):

To switch two things without them hitting each other you need 3 dimensions:

braid

Shea Levy (Oct 16 2020 at 18:17):

John Baez said:

To switch two things without them hitting each other you need 3 dimensions:

braid

Sure, but that assumes I care about things hitting each other :smile: Why should I when thinking about polycategories generally (or sequents specifically)?

Shea Levy (Oct 16 2020 at 18:17):

Or why should I assume I'm not already working in 10 dimensions? :sweat_smile:

John Baez (Oct 16 2020 at 18:18):

Are you just arguing that you don't like the word "planar"?

John Baez (Oct 16 2020 at 18:18):

If so, use some other term.

James Wood (Oct 16 2020 at 18:19):

One answer would be to ask Joyal and Street.

James Wood (Oct 16 2020 at 18:20):

But also, there's presumably some sense in which polycategories are inherently 2-dimensional. Definitely, monoidal categories are 2-dimensional, as they are a special case of bicategories.

James Wood (Oct 16 2020 at 18:21):

(And braided monoidal categories are 3-dimensional, as John illustrates.)

Shea Levy (Oct 16 2020 at 18:22):

John Baez said:

Are you just arguing that you don't like the word "planar"?

No, sorry. I just don't understand why we have "symmetric" polycategories (which, as I understand it, admit exchange) opposed to "planar" polycategories (which, as I understand it, do not admit exchange and do not admit crossing). Why isn't there a kind of polycategory which does not admit exchange and does admit crossing? Why is "not admit crossing" desirable?

John Baez (Oct 16 2020 at 18:34):

I thought "crossing" was just another name for "exchange". Are you saying there's a difference? If you can define polycategories that admit one and not the other, then we can study those.

Shea Levy (Oct 16 2020 at 18:58):

John Baez said:

I thought "crossing" was just another name for "exchange". Are you saying there's a difference? If you can define polycategories that admit one and not the other, then we can study those.

Working in sequent calculus, to me "exchange" means:

$$\frac{ \overrightarrow{\phi}, \alpha, \beta, \overrightarrow{\psi} \vdash \overrightarrow{\chi} }{ \overrightarrow{\phi}, \beta, \alpha, \overrightarrow{\psi} \vdash \overrightarrow{\chi} } \,$$

and

$$\frac{ \overrightarrow{\phi} \vdash \overrightarrow{\psi}, \alpha, \beta, \overrightarrow{\chi} }{ \overrightarrow{\phi} \vdash \overrightarrow{\psi}, \beta, \alpha, \overrightarrow{\chi} } \,$$

which, from my weak understanding, corresponds to "symmetric" polycategories.

Whereas (not necessarily planar) cut/composition is:

$$\frac{ (\overrightarrow{\Gamma} \vdash \overrightarrow{\Delta_1}, \alpha, \overrightarrow{\Delta_2}) \;\;\; (\overrightarrow{\Gamma_1}, \alpha, \overrightarrow{\Gamma_2} \vdash \overrightarrow{\Delta}) }{ \overrightarrow{\Gamma_1}, \overrightarrow{\Gamma}, \overrightarrow{\Gamma_2} \vdash \overrightarrow{\Delta_1}, \overrightarrow{\Delta}, \overrightarrow{\Delta_2} }\,$$

And the planar condition amounts to $\overrightarrow{\Gamma_1}$ or $\overrightarrow{\Delta_1}$ being empty and $\overrightarrow{\Gamma_2}$ or $\overrightarrow{\Delta_2}$ being empty.

Without this last condition, do we somehow recover exchange?

John Baez (Oct 16 2020 at 19:06):

Shea Levy said:

Working in sequent calculus, to me "exchange" means:

$$\frac{ \overrightarrow{\phi}, \alpha, \beta, \overrightarrow{\psi} \vdash \overrightarrow{\chi} }{ \overrightarrow{\phi}, \beta, \alpha, \overrightarrow{\psi} \vdash \overrightarrow{\chi} } \,$$

Okay, thanks. In category land this is exactly what you'd expect if you were working in a symmetric monoidal category.

So yes, I can easily imagine that this is one of the features that distinguishes a symmetric polycategory from a plain old polycategory. (I'd probably also want some way to switch things in the list of "outputs" or "consequences" or whatever you call them - the list you're calling $\chi$.)

Shea Levy (Oct 16 2020 at 19:08):

@John Baez Maybe the message got truncated? I have the RHS version further down

John Baez (Oct 16 2020 at 19:12):

Shea Levy said:

Whereas (not necessarily planar) cut/composition is:

$$\frac{ (\overrightarrow{\Gamma} \vdash \overrightarrow{\Delta_1}, \alpha, \overrightarrow{\Delta_2}) \;\;\; (\overrightarrow{\Gamma_1}, \alpha, \overrightarrow{\Gamma_2} \vdash \overrightarrow{\Delta}) }{ \overrightarrow{\Gamma_1}, \overrightarrow{\Gamma}, \overrightarrow{\Gamma_2} \vdash \overrightarrow{\Delta_1}, \overrightarrow{\Delta}, \overrightarrow{\Delta_2} }\,$$

And the planar condition amounts to $\overrightarrow{\Gamma_1}$ or $\overrightarrow{\Delta_1}$ being empty and $\overrightarrow{\Gamma_2}$ or $\overrightarrow{\Delta_2}$ being empty.

Without this last condition, do we somehow recover exchange?

Maybe. What I know for sure is that if I draw this rule using string diagrams I see that some wires must cross each other unless $\overrightarrow{\Gamma_1}$ or $\overrightarrow{\Delta_1}$ being empty and $\overrightarrow{\Gamma_2}$ or $\overrightarrow{\Delta_2}$ are empty. That is, I can only draw the diagram in a plane if these conditions hold. So the word "planar" seems quite reasonable to describe this condition.

Again, in a monoidal category we'd expect this rule to hold only when there are no crossings, but in a symmetric monoidal category it should hold even when there are crossings. Probably that's also true in a polycategory, though I don't understand those as well.

Shea Levy (Oct 16 2020 at 19:16):

John Baez said:

Maybe. What I know for sure is that if I draw this rule using string diagrams I see that some wires must cross each other unless $\overrightarrow{\Gamma_1}$ or $\overrightarrow{\Delta_1}$ being empty and $\overrightarrow{\Gamma_2}$ or $\overrightarrow{\Delta_2}$ are empty. That is, I can only draw the diagram in a plane if these conditions hold. So the word "planar" seems quite reasonable to describe this condition.

Again, in a monoidal category we'd expect this rule to hold only when there are no crossings, but in a symmetric monoidal category it should hold even when there are crossings. Probably that's also true in a polycategory, though I don't understand those as well.

Right, the nomenclature makes sense, I just don't get why we'd name that particular thing.

In the non-symmetric monoidal category, why doesn't it hold with crossings?

John Baez (Oct 16 2020 at 19:26):

Because a symmetry is what lets you switch two things past each other, and if you draw out the rule you're talking about, things need to cross. To fully explain this I need a picture. I drew it and took a picture with my cell phone, but it's taking a while to reach my laptop.

John Baez (Oct 16 2020 at 19:42):

Okay, here it is:

why crossings are needed in this deduction rule

John Baez (Oct 16 2020 at 19:44):

You can see wires cross each other unless $\overrightarrow{\Gamma_1}$ or $\overrightarrow{\Delta_1}$ is empty and $\overrightarrow{\Gamma_2}$ or $\overrightarrow{\Delta_2}$ is empty.

John Baez (Oct 16 2020 at 19:44):

Maybe you're not used to this topological way of thinking about things, but it's built into category theory; that's one of the great discoveries of our age.

Shea Levy (Oct 16 2020 at 19:44):

Right, it makes sense why we'd need the condition to avoid crossing. I just don't know what meaning I should give to "the wires cross" or "the wires don't cross" and, in particular, why "the wires don't cross" is somehow the opposite of "symmetric"

Shea Levy (Oct 16 2020 at 19:45):

John Baez said:

Maybe you're not used to this topological way of thinking about things, but it's built into category theory; that's one of the great discoveries of our age.

Yeah, this is a big gap in my background I'm looking to fill

Dan Doel (Oct 16 2020 at 19:45):

The wires crossing is exchange.

John Baez (Oct 16 2020 at 19:46):

I just don't know what meaning I should give to "the wires cross" or "the wires don't cross" and, in particular, why "the wires don't cross" is somehow the opposite of "symmetric"

In a symmetric monoidal category morphisms can be described using string diagrams where wires are allowed to cross, while in a merely monoidal category morphisms can be described using string diagrams where wires are not allowed to cross. The symmetry $S_{x,y} : x \otimes y \to y \otimes x$ is drawn as a crossing.

Shea Levy (Oct 16 2020 at 19:47):

Dan Doel said:

The wires crossing is exchange.

How does that relate to the exchange rule above? Exchange seems to let me cross wires into a given node, whereas non-planar composition lets me cross wires between nodes... I guess I'm not seeing the fundamental connection without an assumption that we're working in a plane.

Shea Levy (Oct 16 2020 at 19:48):

If the answer is "you'll understand once you learn to think topologically", that's fine. Happy to take this on faith while I work my way up to that.

Dan Doel (Oct 16 2020 at 19:49):

I don't think topologically.

John Baez (Oct 16 2020 at 19:49):

It might help to study how string diagrams work for monoidal categories and symmetric monoidal categories (and in between, braided monoidal categories - an intermediate case that's less important in logic but very important in topology).

I don't know the perfect reference for you but some people like this paper:

• John Baez and Mike Stay, Physics, topology, logic and computation: A Rosetta Stone.

Dan Doel (Oct 16 2020 at 19:53):

Anyhow, exchange is clearly crossing things. I think what the pictures are telling you is that if you allow your different cut, it will be impossible to eliminate.

Dan Doel (Oct 16 2020 at 19:54):

Because there is no way to detangle things down to non-cut primitives.

Dan Doel (Oct 16 2020 at 19:55):

So that cut is not admissible.

Shea Levy (Oct 16 2020 at 19:55):

Ah!

Dan Doel (Oct 16 2020 at 19:58):

And that also suggests that it doesn't make sense with respect to the stack behavior. The cut is enabling something that wouldn't be possible to write inline.

Dan Doel (Oct 16 2020 at 19:58):

Because it's accessing non-local parts of the stack.

Dan Doel (Oct 16 2020 at 20:01):

I don't have a very good intuition for how stacks work in this setting, though. I think there might be two stacks. One for inputs and one for outputs.

Shea Levy (Oct 17 2020 at 10:52):

Amar Hadzihasanovic said:

This is from Craig Pastro's thesis -- “double” wires stand for multiple (0 or more) wires Screenshot-from-2020-10-16-17-45-22.png

I assume that we require that these forms are equivalent when multiple are allowed? E.g. if f has a singleton output and g has a matching singleton input, I could use any of these to compose them, do we require the results to be equal?

Or in terms of a single form of composition requiring planarity, do we require that composition doesn't "inspect" the planarity proof? i.e. $\forall p_1 p_2, comp(g, f, p_1) = comp(g, f, p_2)$?

Shea Levy (Oct 17 2020 at 10:55):

Hmm, in the "untyped" version we already have composition being a partial operator even in (mono?)categories, not allowed to depend on some "proof" of the sources and targets lining up. I guess the way to think about it is the proof lives in the metatheory?

Shea Levy (Oct 18 2020 at 12:11):

Dan Doel said:

And that also suggests that it doesn't make sense with respect to the stack behavior. The cut is enabling something that wouldn't be possible to write inline.

When you shared this I was vaguely satisfied, got it to really click this morning. I think there are two stacks.

In terms of the general diagram:

2020-10-18-080701_397x525_scrot.png

We can interpret the g part of the diagram to require that, if $\Gamma_1$ comes first in the input, $\Delta$ comes first in the output, and if $\Gamma_2$ comes last in the input, $\Delta$ comes last in the output, and vice versa for f. These requirements can only be satisfied under planarity, and I think they ensure that you only have to inline the cut at "one place" in each stack to eliminate it (though I haven't proven it).

Shea Levy (Oct 18 2020 at 12:34):

Another way to think about it is to treat the ports of each node as a "staging area" between the input and output stacks, where once we start filling (consuming from) a staging area we must fully fill (consume from) it before we push more to the output (pop more from the input). So, for example, in the case where $\Delta_1$ and $\Gamma_2$ are empty, we can do:

1. pop $\Gamma_1$ off the top and stage them at the first part of g
2. Run all of $\Gamma$ through f
3. Stage the first output of f at the next input of g
4. Run g and put the output ($\Delta$) on the output stack
5. Put the remaining outputs of f ($\Delta_2$) on the output stack.

But if $\Delta_1$ hadn't been empty, we would've had to "skip" the already partially-staged g to put $\Delta_1$ on the output and then continue filling g later.

Shea Levy (Oct 18 2020 at 12:40):

We might think of the staging areas as input and output stack frames for (multi-output) procedures in the stack language, and cut elimination as just inlining them by stacking the frames on top of each other

Dan Doel (Oct 18 2020 at 16:51):

@Shea Levy I was thinking about it at the time, but then didn't bother to work it out. I think there's probably a way to state a single cut rule, but because of all this, you need to split up the contexts more, so they can be sandwiched back in the right order.

Shea Levy (Oct 18 2020 at 16:53):

Dan Doel said:

Shea Levy I was thinking about it at the time, but then didn't bother to work it out. I think there's probably a way to state a single cut rule, but because of all this, you need to split up the contexts more, so they can be sandwiched back in the right order.

The way I have it defined currently (in coq) just takes a planarity proof of $\Gamma_1$ and $\Delta_1$ and similar for the other side. I guess the alternative is to take 2 (instead of 4) "boundary contexts" plus some data that tells you where they go in order

Dan Doel (Oct 18 2020 at 16:53):

I guess that might not be terribly convenient, though, because it kind of amounts to isolating the thing you want to cut.