The n-Category Café

Mike Stay wants to work out the syntax for symmetric monoidal categories with duals.

How will this differ from what Abramsky and Duncan have done?

The difficulty with developing the syntax of something like compact closed categories is that the tensor connective is self-dual (which mucks around with cut elimination procedures). Shirahata’s paper that you point to does resolve the situation here though. As I understand it, the syntax for symmetric monoidal categories with duals is provided by linearly distributive categories with duals (weakly distributive in the old language), which are equivalent to star-autonomous categories.

As far as logic goes, taking 2Cob as a model of MLL is not totally ideal, because of its frobenius structure, which is not present in the logic. An interesting question to warm up on could be to derive a sequent calculus for frobenius algebras.

If you care about classical computation, then this can be modelled as a monad on a CCC - this insight is usually credited to Moggi. There’s also a nice geometric interpretation of this situation.

So, are these dagger-compact closed categories the elusive ‘quantum topoi’? There certainly seems a lot to support the analogy

Hilb is to dagger-compact closed categories

as

Set is to topoi.

Is this the right way to think about things? And if it is, I suppose it must just be another way of saying

linear logic is to intuitionistic linear logic

as

nonlinear logic is to intuitionistic nonlinear logic.

What’s more interesting to me is the hypothesised connection between quantum mechanics and spacetime. There seems to be plenty of circumstantial evidence, but has anybody actually suggested a construction for this? Is it really possible to take something like Hilb, and end up with something like nCob? That’s a pretty big question, especially given that the solution to the measurement problem should be hiding somewhere in the answer!

Jamie Vicary writes:

So, are these dagger-compact closed categories the elusive ‘quantum topoi’?

They’re a step in that direction, but I wouldn’t put it that way. They aren’t “maximally nice” the way topoi are - for example, they don’t even have finite coproducts, the way Hilb does. I’d say they’re about as nice as you can get while still including both nCob and Hilb as examples - this is why I’ve been pushing them as a framework for unifying general relativity and quantum theory.

What’s more interesting to me is the hypothesised connection between quantum mechanics and spacetime. There seems to be plenty of circumstantial evidence, but has anybody actually suggested a construction for this? Is it really possible to take something like Hilb, and end up with something like nCob?

I’ve been working on this for almost 10 years now, together with lots of other people. The basic idea is to set up categories of spin foams, which are sort of intermediate between Hilb and nCob.

Spin foams look like 2-dimensional - or perhaps ultimately even higher-dimensional! - generalizations of Feynman diagrams. So, in fact, to glue these entities together in all the obvious ways, one needs to treat them not just as morphisms in a category, but as n-morphisms in an n-category. This is one reason I’m so interested in n-categories with duals. Symmetric monoidal categories with duals - aka “dagger-compact closed categories” - just happen to be a really tractable example.

I don’t really want to discuss quantum gravity on this thread, though. We’ll have plenty of other chances for that. The goal of this particular thread is to ponder quantum computation with the help of symmetric monoidal categories with various extra bells and whistles (like duals).

Urs writes:

What precisely does “syntax” and “semantics” mean here?

I will only tackle this question here, not your harder question about the double role of Feynman diagrams in topological quantum field theory, and what it might mean for quantum computers. That’s a really interesting puzzle, but I’ve already spent too much time blogging today, writing a long comment about the inner automorphism 3-group of a 2-group!

Mike has already given a fine answer to this question about syntax and semantics.

But, the duality between syntax and semantics is one of the grand themes of logic, so one can never say too much about it.

So, I’ll take this excuse to repeat some introductory stuff I said in week227. I can’t resist expanding it a bit in the process, though, because this stuff is so cool!

Logic can be divided into two parts: SYNTAX and SEMANTICS. Roughly speaking, syntax concerns the symbols you scribble on the page, while semantics concerns what these symbols mean.

A bit more precisely, imagine some kind of logical system where you write down some theory - like the axioms for a group, say - and use it to prove theorems.

In the realm of syntax, we focus on the form our theory is allowed to have, and how we can deduce new sentences from old ones. So, one of the key concepts is that of a proof. The details will vary depending on the kind of logical system we’re studying.

In the realm of semantics, we are interested in gadgets that actually satisfy the axioms in our theory - for example, actual groups, if we’re thinking about the theory of groups. Such a gadget is called a model of the theory. Again, the details vary immensely.

In the realm of syntax, we say a list of axioms X implies a sentence P if we can prove P from X using some deduction rules, and we write this as

X |- P

In the realm of semantics, we say a list of axioms X entails a sentence P if every model of X is also a model of P, and we write this as

X |= P

We also say P is provable from X when X |- P, and valid given X when X |= P.

We say a logical system is sound if provability implies validity. We say it’s complete if validity implies provability.

You can begin to see a kind of “duality” between syntax and semantics here. But in fact, they are “dual” in an even more precise way, at least if you fix a specific class of logical systems. This duality is akin to the usual relation between vector spaces and their duals, or more generally groups and their categories of representations. The idea is that given a theory T you can figure out its models, which form a category Mod(T) - and conversely, given the category of models Mod(T), perhaps with a little extra information, you can reconstruct T.

A little extra information? Well, in some cases a model of T will be a set with some extra structure - for example, if T is the theory of groups, a model of T will be a group, which is a set equipped with some operations. So, in these cases there’s a functor

U: Mod(T) → Set

assigning each model its underlying set. And, you can easily reconstruct T from Mod(T) together with this functor.

This idea was worked out by Lawvere for a class of logical systems called algebraic theories, which I discussed in “week200”.

But, the same idea goes by the name of “Tannaka-Krein duality” in a different context: a Hopf algebra H has a category of comodules Rep(H), which comes equipped with a functor

U: Rep(H) → Vect

assigning each comodule its underlying vector space. And, you can reconstruct H from Rep(H) together with this functor. The proof is even very similar to Lawvere’s proof for algebraic theories!

A beautiful thing about Tannaka-Krein duality is that it generalizes the Pontryagin duality between locally compact abelian groups and locally compact abelian groups. And this, in turn, generalizes the Fourier duality between the integers Z and the circle S¹, or the real line R and itself, or any finite-dimensional vector space V and its dual V*.

Pontryagin noticed that any locally compact abelian group has a “dual”, and there’s a kind of Fourier transform taking L² functions on the group to L² functions on the dual. The dual of the dual is always the original group.

The dual of Z is S¹, the dual of S¹ is Z, the dual of R is R, and the dual of any finite-dimensional vector space V is its usual dual V*.

So, Pontryagin duality subsumes Fourier duality and the usual duality for vector spaces.

When we try to generalize Pontryagin duality to nonabelian groups it turns out to be hard until we generalize still further, and then we get Tannaka-Krein duality.

So, amazingly enough, Fourier duality and the duality between syntax and semantics for algebraic theories are part of the same family of ideas.

With more work one could find a common generalization and prove a theorem which had both of these results as a special case. I don’t know if anyone has done this yet. If not, they should!

Urs writes:

So when John writes:

The λ-calculus provides a syntax for cartesian closed categories.

has he in mind that there is some category $C$ which we call “λ-calculus” such that any CCC “is” some functor $C\to \mathrm{Set}$. Which category is that?

No, I didn’t mean that. I don’t even think Mike was trying to say that. Furthermore, it’s not true.

Let me try to say what I meant. Mike has already infected you with Lawvere’s “functorial” approach to syntax, which is great - but unfortunately you caught a mutant strain, and it seems to be making you sick. Instead of trying to straighten that out, I want to explain what I was actually saying, which was based on a much more traditional notion of syntax.

I don’t know how much logic you’ve studied, but you may know that logicians like to scribble down “theories”, which consist mainly of lists of “axioms” in some “language” or other, and deduce “theorems” from them, using various “deduction rules”.

There are lots of ways to play this game - each of the quoted terms covers lots of ground. But let’s say that any choice of a “language” and “deduction rules” is a “syntax”. I could list a lot of examples, but I’ll just list one: the typed lambda calculus.

(We’ve been talking a lot about the untyped lambda calculus in this thread, but mainly because this highly popular setup is far trickier in certain ways than the typed lambda calculus, and I wanted to understand it. For the question at hand, everything will work out infinitely more elegantly if we use the typed lambda calculus - that’s why they invented it!)

To specify a lambda theory we need to list:

1. a set of generating “types”,

2. a set of generating “function symbols”, each of which has a specified input type and output type,

3. a set of “axioms”, which are equations built using the function symbols.

You may not know what this jargon means, and I’m probably not even using the standard jargon. But that’s okay, because in a minute you’ll see these three things are secretly objects, morphisms and equations between morphisms in a certain category.

Let me write down an example, though:

1. Let’s choose two generating types, say $A$ and $B$. This immediately gives us infinitely many more types, like $A\times B$ and $\mathrm{hom}(A\times A,\mathrm{hom}(B,A))$ and so on.

2. We could choose two function symbols, say $F$ and $G$. Since we’re doing the typed lambda calculus we have to say what type of input this function symbol eats, and what type of output it spits out. Let’s say the input type of $F$ is $\mathrm{hom}(A,B)$ and its output type is $\mathrm{hom}(B,A)$. So $F$ is the name of some operation that eats operations from $A$ to $B$, and spits out operations from $B$ to $A$. Similarly, let’s say the input type of $G$ is $\mathrm{hom}(B,A)$ and its output type is $\mathrm{hom}(B,A)$.

3. Now we can write down some axioms. Here’s a really simple one:

   $$\lambda f:\mathrm{hom}(A,B).G(F(f))=\lambda f:\mathrm{hom}(A,B).f$$

   This should look vaguely like stuff you’ve seen in the untyped lambda calculus, except that now all our variables are “typed”, so we have to say what type the variable $f$ is - and when we say $f:\mathrm{hom}(A,B)$, we’re declaring that it’s an operation that eats guys of type $A$ and spits out guys of type $B$.

   This “type declaration” business might be new to you - but if you’ve done some computer programming, you’ve seen something like it.

   Anyway, our axiom says that if we hit any such $f$ with $F$, and then hit it with $G$, we get back $f$.

This is not a thrilling example. A cooler one is the system “PCF” that Robin Houston was talking about - see Selinger’s notes. This has types called “natural numbers” and “truth values”, and enough function symbols and axioms so you can really do a lot of stuff. Another example is the “lambda theory of groups”, which is just the axioms for a group, written out in the lambda calculus.

If you think about it, I hope you can see that a lambda theory can have “models” in any cartesian closed category $Y$ In a model, all the types are interpreted as objects of $Y$, and the function symbols are interpreted as morphisms, and the axioms have to hold as equations. For example, a model of the lambda theory of groups in the category Set is just a group.

This is the typed lambda calculus in its traditional form. But we can also take a more modern view: any lambda theory determines a cartesian closed category!

To get this, you just take your generating types as objects, and throw in all the other objects you know must exist by virtue of having a CCC. You take your function symbols as morphisms between objects, and throw in all the other morphisms you know must exist by virtue of having a CCC. And, you take your axioms as equations between morphisms, and throw in all the equations you can derive from these by virtue of having a CCC!

Conversely, any CCC gives a theory in the typed lambda calculus. We can do this systematically by taking all the objects as generating types, and putting in isomorphisms whenever needed to cut down the redundancy this creates.

So, once you get the hang of it, you see that a CCC and a theory in the typed lambda calculus are almost the same thing.

However, they still feel a bit different. The theory feels like “syntax” - you’re fiddling around with variables, and using deduction rules to prove theorems from axioms (i.e. derive new equations from old ones). The CCC feels like “semantics” - you’ve got actual objects and morphisms floating around.

In particular, there are lots of famous CCC’s, like Set, or Cat, which are tricky to describe as a typed lambda theory. You might need tons of types, and tons of function symbols, and tons of axioms, to describe one of these typed lambda theories - even if you feel you understand the corresponding CCC perfectly well!

Also, there are lots of famous lambda theories, like the axioms for a group, or PCF, which are tricky to describe as a CCC. It might be really hard to understand all the objects and morphisms of some CCC - even if you feel you understand the corresponding lambda theory perfectly well!

So, the duality between syntax and semantics is interesting, even if from certain viewpoints it seems trivial.

Now for Lawvere’s new-fangled concept of “model”, which is equivalent to the old one, but slicker. You’ll like it. For this, we take a lambda theory and right away replace it by its corresponding CCC, say $X$. A model of our lambda theory is then a product-preserving functor

$F:X\to Y$

where $Y$ is some other CCC. We also call this a model of $X$ in $Y$.

Note that this deliberately blurs the roles of syntax and semantics, because we’re using the CCC $X$ as a stand-in for its corresponding lambda theory.

But, the moral difference between syntax and semantics is still there! What we do in practice is take a CCC, say $X$, that we can understand really well syntactically, and look at models of it

$F:X\to Y$

where $Y$ is a CCC that we can understand really well semantically. For example, $X$ could be the CCC corresponding to the axioms for a group, and $Y$ could be Set. Then $F$ would be a “model of the lambda-theory of groups in Set” - in other words, a group!

If we switched the roles here, and looked at things like

$F:Y\to X$

these would be quite hard to understand.

The moral: we map out of syntax, into semantics.

That’s all I have time for now, but I hope it helps. All the stuff I just wrote is what I mean when I say

The λ-calculus provides a syntax for cartesian closed categories.

Most people probably won’t understand what Mike just said, since it involves knowing the history of our previous conversations. So, I’ll discuss our current crop of puzzles a bit more thoroughly.

1. Say we take the doctrine of categories with finite products and finite-product-preserving functors - also called the doctrine of algebraic theories. Th(Grp) lives in here. A model of Th(Grp) in Set is just a group. What’s a model of Th(Grp) in Vect?

It’s called a group object in Vect, but what it turns out to be is simply a vector space! The point is this. If we have a vector space to be equipped with an extra group operation which is linear, we can show this new group operation has to be the same as addition in the vector space!

So, any vector space can be made into a group object in Vect in a unique, boring way.

Similarly, a group object in Grp is an abelian group. A group object in Ab is also an abelian group.

2. Say we take the doctrine of symmetric monoidal categories and symmetric monoidal functors - also called the doctrine of PROPs. (FinSet,+) lives in here, where we use disjoint union of finite sets as the tensor product. What’s a model of (FinSet,+) in (Vect,$\otimes$) called?

Hmm - actually I don’t feel like answering this one. It’s fun to work it out. It’s a fairly well-known kind of thing! If anyone gets stuck, the answer is in my universal algebra lecture notes. And, the answer is nice not just for models in (Vect, $\otimes$), but for models in any symmetric monoidal category.

3. What’s a model of the PROP (FinSet,+) in (Vect,$\oplus$) called?

Mike took a stab at this but then claimed he didn’t recognize the answer. I’m pretty sure he’ll recognize it when he thinks harder - I’m pretty sure it’s an incredibly famous thing!

Maybe someone else can help him out.

4. Finally, about another puzzle Mike and I were discussing. There is no PROP for groups. But there is an algebraic theory for groups, and there’s an adjunction between PROPs and algebraic theories. So, we can take the algebraic theory of groups and turn it into a PROP. What do we get?

As Mike notes, this amounts to taking stuff we have in any algebraic theory - the diagonal

$$\Delta :G\to G\times G$$

and the map to the terminal object

$$e:G\to 1$$

and turning them into explicit extra operations in our PROP. They come “for free” when we have an algebraic theory, but not when we have a PROP.

So, we get a PROP for algebraic gadgets that have the usual group operations but also a comultiplication $\Delta$ and a counit $e$.

The obvious guess is that this is the PROP for Hopf algebras. That’s what I wrote at first in my lecture notes where I explained this puzzle in detail.

But, I later realized that we get more axioms than just the bare-bones Hopf algebra axioms! We also get the cocommutative law: if you apply $\Delta$, and then switch the two outputs, it’s the same as just applying $\Delta$. This is a feature of the diagonal in any category with finite products. So, it’s inherited by our PROP.

So, right now I think the answer is the PROP for cocommutative Hopf algebras.

Unfortunately, I haven’t checked this - there could be other axioms I’m forgetting. Indeed, the first axiom I noticed was not the cocommutative law, but the involutory law - if you take the inverse of a group element twice, you get back the same thing. This law does not hold for an arbitrary Hopf algebra. But, it holds for all cocommutative Hopf algebras. So, right now I’m hoping the cocommutative law is all we need. And, I have some theoretical reasons for guessing that.