The n-Category Café

Even better, by writing every morphism (element in $hom(x,x)$) in a sort of “standard form”, namely as a composition of just the three building blocks

>

>

and

every element in $x$ is written as a certain diagram.

You’re writing $\otimes$ here, but in a CCC we can be more specific and use $\times$, since CCCs have finite products. It’s only in the quantum case that we generalize to the tensor product.

In Keenan’s setup, this isomorphism is implicit whenever he slides one of his “boxes” (or “birds”) upwards and then vertically downwards into one of the filled black circles.

Yes; the isomorphism is applied to the object coming in on the left, and then the resulting morphism acts on the data coming in from above.

Urs wrote:

I have tried to translate the diagrammatic notation used by Keenan into ordinary string diagrams (“tangle diagrams”) used in monoidal categories. I believe I succeeded.

I spent the afternoon reading Keenan’s paper at the Shanghai branch of the n-Category Café, and I drew many pictures of my own. I understand this stuff a lot better now, and I think everything you said here is right.

I ended by expressing my hope that hence Keenan’s pictures should pretty much tell us what it means, when translated to CCC language, to go through a program step by step. I might be wrong about this. But its certainly an expectation well motivated from a naïve point of view.

Yes. Keenan’s style of drawing pictures is a bit idiosyncratic, since he’s not trying to fit it into the general “string diagram” framework for drawing morphisms in monoidal categories, or the general “movies of string diagrams” framework for drawing 2-morphisms in monoidal 2-categories.

However, by messing with his pictures a little, I was able to fit them into the general string diagram framework pretty nicely. So, I’m very happy! With any luck, all this should dovetail - pardon the pun - quite nicely with Seeley’s work on cartesian closed 2-categories.

I will say something hopelessly low-brow, which experts are invited to try to translate to sophisticated language, if possible. In a way, the “magic” in Keenan’s calculus happens when he turns data into code. In our language, that corresponds to applying the isomorphism $$x \stackrel{\sim}{\to} \mathrm{hom}(x,x) \,.$$ At least as far as I understand. In Keenan’s setup, this isomorphism is implicit whenever he slides one of his “boxes” (or “birds”) upwards and then vertically downwards into one of the filled black circles. In other words, drawing such a box with internal wiring is like specifying an element of $x$ by saying which morphism it corresponds to under the identification $$x \stackrel{\sim}{\to} \mathrm{hom}(x,x) \,.$$

Yes! Personally I like a notation that more clearly distinguishes between two other things that Keenan identifies: namely, a morphism $$f: x \to y$$ and its name, meaning the corresponding element $$\tilde{f}: 1 \to hom(x,y)$$ Both these have nice string diagram pictures. The morphism is a little circle labelled $f$ with one wire coming in at top and one wire going out at bottom. To draw its “name”, we take the input wire and fold it down to the left, getting a gadget with no input wires and two output wires - or more precisely, an output ribbon.

In the special case of the untyped $\lambda$-calculus, the isomorphism $$hom(x,x) \stackrel{\sim}{\to} x$$ can be drawn as a gadget with a ribbon coming in and a line coming out.

Given a morphism $f : x \to x$, and composing its name $\tilde{f}: 1 \to hom(x,x)$ with the above isomorphism, we obtain its nickname $$\bar{f}: 1 \to x .$$ This looks vaguely like a lollipop - draw it yourself, please!

Or, if we follow Smullyan and Keenan’s goofy terminology and call $f: x \to x$ a bird, then $\bar{f}: 1 \to x$ is the bird’s song.

We can then feed the song of one bird into another bird, and get a new song! Given a bird $$f : x \to x$$ and a bird $$g : x \to x$$ we take the song of $f$ $$\bar{f}: 1 \to x$$ and feed it into $g$ to get $$g \bar{f}: 1 \to x$$ which is the song of some other bird.

There’s a bit more to this formalism, for example the evaluation map $$ev: x \times x \to x .$$ So, just as Urs said, we get string diagrams for the untyped lambda calculus.

Then we need to categorify this! But, I’m getting a bit tired right now, so I won’t try to figure that out here.

If I go through his stuff carefully, I may finally understand these I, K, and S combinators and other clever tricks λ-hackers use.

One of those clever tricks you should be aware of is lambda abstraction; this is at the root of my explanation earlier.

In LISP, to apply a function f to a list of inputs (a, b, c) you write

(f a b c)

If we make the restriction that every atom is curried, then each function takes exactly one input:

(((f a) b) c)

But because we know how many inputs a function takes, we can get rid of the right parentheses:

(((f a b c

Now: given a lambda expression written this way, there’s a mechanical process to translate it into SKI notation.

For each variable v, starting with the innermost: 1. ( $\to$ ((S 2. v $\to$ I 3. term T not containing v $\to$ (K T

That’s it! In the case of the “arrow-order” applicator $\lambda$ xy.(y x,

1. $\lambda$ xy.(y x
2. $\lambda$ x.((S I (K x
3. ((S ((S (K I ((S (K K I

John Baez wrote:

A cartesian category cannot have duals for objects unless every object is isomorphic to 1.

Sorry to be Mr Pedantic again, but I don’t think that’s quite right. There is certainly such a thing as a non-trivial boolean algebra! On the other hand, this essentially exhausts the possibilities: a cartesian category with duals collapses to a preorder, i.e. no homset can contain more than one arrow.

alpheccar: I guess you’re thinking of Moggi’s work using strong monads?

My favourite star-autonomous category is the category of coherence spaces. It was Girard’s study of this category that gave him the idea for linear logic, so it’s historically important as well as being a jolly nice category. (The history of linear logic is actually the reverse of what you suggest: it started life as a semantics in search of a syntax!)

A coherence space is just an undirected graph, i.e. a set A together with a reflexive relation $\sim$ $\subseteq$ $A\times A$, called the coherence relation. The dual relation $\backsim$ is defined as: $x\backsim y$ iff $x\nsim y$ or $x = y$.

A morphism $R: A \to B$ is a relation s.t. whenever $a R b$ and $a' R b'$,

• if $a\sim a'$ then $b\sim b'$
• if $b\backsim b'$ then $a\backsim a'$

(I hope all these crazy symbols come out okay on your computer, or else this might be quite hard to follow!)

The dual A^$\bot$ of a coherence space A has the same underlying set as A, with the dual coherence relation. The tensor $A\otimes B$ has underlying set $A\times B$, with a coherence relation defined as

    (a,b) $\sim$ (a’,b’) iff $a\sim a'$ and $b\sim b'$

Notice that (A^$\bot$$\otimes$B^$\bot$)^$\bot$ is generally different from $A\otimes B$. (There is a little degeneracy though: the unit for tensor is the one-element space I, which is equal to I^$\bot$. In linear-logical terms, that means the model validates the MIX rule.)

The category of coherence spaces also has coproducts, given by the disjoint union of the graphs, hence (by duality) it has products too.

There are lots of nice examples of star-autonomous categories, but they typically have a very different flavour from the categories of mathematical objects that we’re most familiar with.

Dualisation is a fertile source of star-autonomous categories. If C is a SMCC with finite products then C$\times$C^op has a natural star-autonomous structure. Its tensor product is

(A,X)$\otimes$(B,Y) = (A$\otimes$B, $(A\multimap Y)\times(B\multimap X)$)

with unit (I, 1). The dual is of course defined as (A,X)^$\bot$ = (X,A).

Here’s a question/comment. Why do you think of terms as 1-dimensional objects? Maybe it’s because you can take a product of terms, and you want to represent these products using diagrams, with the product of $$\bullet \stackrel{x}{\to} \bullet$$ and $$\bullet \stackrel{y}{\to} \bullet$$ looking like $$\bullet \stackrel{x}{\to} \bullet \stackrel{y}{\to} \bullet \quad ?$$

If so, then I think something like this is going on:

Above I’m talking about “cartesian closed categories” and “cartesian closed 2-categories”. But, a cartesian category is always monoidal, and a monoidal category is just a 2-category with one object. So, “cartesian closed categories” are already 2-categories. Similarly “cartesian closed 2-categories” are already 3-categories.

If one likes extra dimensions, one can go further: a braided monoidal category is just a (weak) 3-category with one morphism, and a symmetric monoidal category is just a (weak) 4-category with one 2-morphism. This is why we draw morphisms in braided monoidal categories using string diagrams in 3-space, and computations in symmetric monoidal categories using string diagrams in 4-space.

So, a cartesian closed category is already a special sort of 4-category, and a “cartesian closed 2-category” is a special sort of 5-category!

In fact, this viewpoint underlies the diagrams in my course. I began introducing these diagrams here and went further here. These ideas are probably quite familiar to you - I may be reinventing the wheel. So far I’ve focused on closed monoidal categories, so the diagrams are just 2-dimensional. But when the braiding and symmetry become important, they’ll become 4-dimensional - with the 4th dimension merely letting us neglect the difference between a right-handed crossing

     \ /
      /
     / \

and a left-handed crossing

     \ /
      \
     / \

when drawing our string diagrams.

And later, when I categorify everything, the pictures will become 5-dimensional!

This is not as scary as it sounds, since it’s easy to draw a “movie” each of whose frames is a picture of a string diagram in 4 dimensions, where the 4th dimension merely lets us ignore the difference between

     \ /
      \
     / \

and

     \ /
      /
     / \

Peter Selinger was kind enough to send this reply:

Hi Mike,

your string diagrams are known as “sharing graphs” in the literature, and are extremely well-studied. See e.g.

[1] Stefano Guerrini, A general theory of sharing graphs (1997)

There is a reduction strategy on sharing graphs that is provably the most efficient possible reduction strategy for lambda calculus; this goes back to the work of Levy and Lamping (both cited in the above paper).

Guerrini also gives an algebraic semantics of these sharing graphs, see section 7. I don’t know whether it is related to your categorical view.

I also like the book by Peyton-Jones:

[2] Simon Peyton Jones, The Implementation of Functional Programming Languages (1987)

It shows how to use sharing graphs as the basis for a practical implementation of lazy programming languages. As far as I know, this is still state-of-the-art and is used in the implementation of Haskell. In keeping with the practical nature of the book, the sharing graphs are represented in slightly different form (with syntactic variables rather than backpointers), but this is of course equivalent.

As for the categorical semantics, what you have in mind is a kind of abstract syntax with variable binding. To put this into perspective, the semantics of ordinary abstract syntax (i.e., without variable binding), is given by an object A in a cartesian category, together with interpretations for each n-ary function symbol $f : A^n \to A.$ One can then inductively define the interpretation of terms, speak of the free such object, etc.

Things get slightly more complicated if one adds variable binding to this picture. This has also been studied, though perhaps not in the same form as you are proposing. Perhaps the closest to your approach is

[3] Martin Hofmann, Semantical analysis of higher-order abstract syntax (1999)

Here one has $var : V \to T,$ $app : T \times T \to T,$ and $lam : (V \Rightarrow T) \to T$ (see top of p.9, with the obvious changes in notation). You will note the use of a function space $(V \Rightarrow T)$ in place of your cartesian product $V^* \times T.$

Another very similar paper is

[4] M.P.Fiore, G.D.Plotkin and D.Turi. Abstract syntax and variable binding (1999) or here

Here, one has $var : V \to T$, $app : T \times T \to T$, and $lam : \delta T \to T$ (as contained e.g. in the commutative diagram on p.6). Again, $\delta T$ is something akin to the function space $V \Rightarrow T$, but is also isomorphic, in a suitable sense, to $T \Rightarrow T,$ as far as I remember (this is important for substitution, see below).

A third, technically slightly different (but conceptually similar) approach to abstract syntax with variable binders is:

[5] Murdoch J. Gabbay, Andrew M. Pitts: A new approach to abstract syntax with variable binding (1999)

[6] Murdoch J. Gabbay, Andrew M. Pitts: A new approach to abstract syntax with variable binding (2002)

See especially the second-to-last line of [6, p.356], and you immediately see the similarity. Their [A]T operation is akin to $V \Rightarrow T$ in [3] and $\delta T$ in [4].

It is fun to note that [3-5] all appeared (independently) in the same conference in 1999. Semantics of variable binders was clearly a pressing problem that year.

I can comment briefly on the main difference between these works and what you are proposing. One thing that is important in syntax is substitution (of a term for a variable). In fact, in the usual abstract syntax (without binders), a term with n variables is represented as a morphism $A^n \to A$. This is useful for substitution: namely, if $f : A \times A^n \to A$ represents the term $t(x,y_1,...,y_n)$ and $g : A^n \to A$ represents $s(y_1,...,y_n)$, then $f \circ \langle g, id \rangle$ represents $t[s/x].$

In the presence of variables, a term with n variables is represented as $1 \to V^{*n} \times T$ (in your notation). However, for reasons of substitution, one would still like this hom-set to be in 1-1 correspondence with $T^n \to T.$ Somehow this is what the papers [3-6] manage to do, each in their own way.

I hope these references will be useful. It would be great if you had a more abstract monoidal framework of which the particular constructions in [3-6] are concrete examples. I have always wondered about the precise connection between [3-6], and whether there is a bigger picture.

Good luck, and let me know how it goes! – Peter