Say I have a sequent A,B,C,D |- E,F. I can picture this graphically as the diagram on the left. Squinting at it a bit, one may see it as a sort of a circuit, which maps the input wires A,B,C and D to the output wires E and F. Of course, as it stands, this is not a morphism, but we'll make it into one in just a sec.
Before doing that, let's think about composition. How can we compose two sequents? The answer, of course, is that we use cut. For instance, we could cut our sequent A,B,C,D |- E,F with the sequent F,G,H |- L,K,M to obtain A,B,C,D,G,H |- E,L,K,M. It's easier to think of this geometrically, as in the diagram on the right.
Let's try and make these diagrams mathematically respectable. To do so, we'll generalise the notion of a category. Normally, a category consists of a bunch of objects, together with maps that go between objects. For our generalisation, we'll take
lists of objects and maps between these lists. After doing the obvious things in order to ensure that everything is kosher, what we end up with is something called a
polycategory. For instance, we generalise morphisms between objects, to
polymorphisms between lists of objects. Just as we have functors between categories, we have
polyfunctors between polycategories. These do what you expect. Say A and B are polycategories and F:A -> B is a polyfunctor. Then, each object a of A gets sent to F(a) and every polymorphism f: a1, a2, ..., an -> aa1, aa2, ..., aam gets sent to F(f):F(a1), F(a2), ..., F(an) -> F(aa1), F(aa2), ..., F(aam). Well, to be honest, defining composition of polymorphisms is slightly tricky. But not too tricky - we just use cut!
It is clear that we can view sequents as polymorphisms in the evident polycategory generated by the ambient deductive system. And composition becomes easy to understand if we draw polymorphisms as boxes with wires!
But wait, I promised that we would turn these diagrams into morphisms, not polymorphisms! How to do this? What we need to do is to recall that the comma in a sequent is really just a proxy for conjunction on the left and disjunction on the right. So, a sequent A,B,C |- D,E is really the same as A ⊗ B ⊗ C |- E ⊕ F. I'm using ⊗ for conjunction, because it is easier to talk about this stuff with a multiplicative conjunction, which is really just a tensor product. Similarly, disjunction is represented as ⊕ - direct sum! Both of these are examples of monoidal structures on a category. In fact, we can add it to a category too. It turns out that, in a well defined sense, adding ⊗ and ⊕ to a polycategory is a conservative extension. Let's name these things ⊗⊕-polycategories.
We're not quite all the way to viewing the boxes as morphisms in some category. What is missing is something that tells us how ⊗ and ⊕ interact. So, we need to make sure that they play nicely with each other, by saying that there is a natural transformation from A ⊗ (B ⊕ C) to (A ⊗ B) ⊕ C and, dually, there is one from (A ⊕ B) ⊗ C to A ⊕ (B &otimes C). After throwing in these natural transformations and writing down some sensible commutative diagrams, we get what is known as a
weakly distributive category.
Here's the cool part. The 2-category consisting of all ⊗⊕-polycategories is equivalent to the 2-category consisting of all weakly distributive categories. With less jargon, polycategories and weakly distributive categories are essentially the same thing! Neato! So, I have kept my promise. The first box is a morphism from A ⊗ B ⊗ C ⊗ D to E ⊕ F in some weakly distributive category. If you want to see how to prove this, plus a bunch of other cool results, look no further than:
Weakly distributive categories; J.R.B. Cockett and R.A.G. Seely
I can't resist pointing to the world's coolest application of polycategories. This is sort of a continuation of
something I wrote about a while ago. Namely, it is an application to causal quantum evolution in physics. The basic idea is that we can view a system of interacting quantum systems as a directed acyclic graph, where the nodes are subsystems and the edges represent the causality relation. From this, we can go ahead and derive a polycategory in a straightforward way. Then we can do all sorts of cool things like whacking on some hilbert space representations, density matrices and the like in order to describe the system. I could go on about this, but instead I'll just point to the relevant paper, since everything is explained beautifully in it!
Discrete quantum causal dynamics; Richard F. Blute, Ivan T. Ivanov and Prakash Panangaden.
Update: Weakly distributive categories tell us all about how to use polycategories to model the multiplicative fragment of linear logic. If you want to see how to deal with the additive fragment, including a neat application to concurrent processes, you should check out:
SigmaPi-Polycategories, additive linear logic and process semantics; Craig Pastro
