Categorifying CCCs: Computation as a Process
Posted by John Baez
This entry is an excuse for discussing ways to categorify the notion of a cartesian closed category (CCC), so we can see computations in the λcalculus as 2morphisms.
To get what I’m talking about, start with the most fun introduction to the λcalculus you can find:

Raymond Smullyan, To Mock a Mockingbird, Alfred A. Knopf, New York, 1985.
It begins like this:
A certain enchanted forest is inhabited by talking birds. Given any birds A and B, if you call out the name of B to A, then A will respond by calling out the name of some bird to you; this bird we designate AB. Thus AB is the bird named by A upon hearing the name of B.
Next, take Smullyan’s stories and make movies of the process of computation in the λcalculus, all in terms of birds.
Luckily, you don’ t need to do this yourself  someone already has:

David Keenan, To dissect a mockingbird: a graphical notation for the lambda calculus with animated reduction.
If you stare carefully at these movies, and think hard, you’ll see they depict 2morphisms in a cartesian closed 2category. So, Keenan is secretly categorifying the concept of CCC, to see computation as a kind of process! That’s something I want to understand better.
I’ll start the discussion with a kind of confession.
When I first heard about categories in computer science, people told me that the λcalculus could be seen as a particularly elegant computer language, in which computations were really just proofs. They told me Lambek had shown the λcalculus was in some sense equivalent to the formalism of cartesian closed categories (CCCs). They seemed to be saying that objects of the CCC correspond to “data types”.
So, I put two and two together and got… umm… five. I guessed that a morphism in a CCC
f: x → y
represents a program that takes data of type x as input and spits out data of type y. Or, a proof that takes some assumptions x and derives some conclusions y.
I then got upset when people told me morphisms in a CCC were really more like equivalence classes of proofs, where the equivalence relation seemed to wash out some really interesting stuff  stuff that looks like “2morphisms between morphisms”.
I got even more upset when these “2morphisms” seemed to be precisely the “computational work” that a computer implementing the λcalculus would need to do to actually compute anything. I’m talking about things like βreduction.
A theory of computation that neglects the process of computation?
I documented a certain stage of my befuddlement in week227, where I wrote:
Anyway, the stuff Phil Scott told me about was mainly over on the syntax side. Here categories show up in another way. Oversimplifying as usual, the idea is to create a category where an object P is a sentence  or maybe a list of sentences  and a morphism
f: P → Q
is a proof of Q from P  or maybe an equivalence class of proofs.
We can compose proofs in a more or less obvious way, so with any luck this gives a category! And, different kinds of logical system give us different kinds of categories.
Quite famously, the multiplicative fragment of intuitionistic logic gives cartesian closed categories. (The "multiplicative fragment" is the portion that deals with "and" and "implies" but leaves out "or" and "not". I’m calling it this because "and" acts like multiplication, while "or" acts like addition.) Similarly, the multiplicative fragment of linear logic gives *autonomous categories. Fullfledged intuitionistic logic gives cartesian closed categories with finite coproducts, and fullfledged linear logic gives us even fancier kinds of categories!
One thing that intrigues me is the equivalence relation we need to get a category whose morphisms are equivalence classes of proofs. In Gentzen’s "natural deduction" approach to logic, there are various deduction rules. Here’s one:
P  Q P  Q'  P  Q & Q'This says that if P implies Q and it also implies Q’, then it implies Q & Q’.
Here’s another:
P  Q => R  P and Q  RAnd here’s a very important one, called the "cut rule":
P  Q Q  R  P  RIf P implies Q and Q implies R, then P implies R!
There are a bunch more… and to get the game rolling we need to start with this:
P  PIn this setup, a proof f: P → Q looks vaguely like this:
fcrud fcrud fcrud fcrud fcrud fcrud  P  QThe stuff I’m calling "fcrud" is a bunch of steps which use the deduction rules to get to P  Q.
Suppose we also we also have a proof
g: Q → R
There’s a way to stick f and g together to get a proof
fg: P → R
This proof consists of setting the proofs f and g side by side and then using the cut rule to finish t he job. So, fg looks like this:
fcrud gcrud fcrud gcrud fcrud gcrud fcrud gcrud   P  Q Q  R  P  RNow let’s see if composition is associative. Suppose we also have a proof
h: R → S
We can form proofs
(fg)h: P → S
and
f(gh): P → S
Are they equal? No! The first one looks like this:
fcrud gcrud fcrud gcrud fcrud gcrud hcrud fcrud gcrud hcrud   hcrud P  Q Q  R hcrud   P  R R  S  P  Swhile the second one looks like this:
gcrud hcrud gcrud hcrud fcrud gcrud hcrud fcrud gcrud hcrud fcrud   fcrud Q  R R  S   P  Q Q  S  P  SSo, they’re not quite equal! This is one reason we need an equivalence relation on proofs to get a category. Both proofs resemble trees, but the first looks more like this:
\ / / \/ / \ / while the second looks more like this:
\ \ / \ \/ \ / So, we need an equivalence relation that identifies these proofs if we want composition to be associative!
This sort of idea, including this "tree" business, is very familiar from homotopy theory, where we need a similar equivalence relation if we want composition of paths to be associative. But in homotopy theory, people have learned that it’s often better NOT to impose an equivalence relation on paths! Instead, it’s better to form a weak 2category of paths, where there’s a 2morphism going from this sort of composite:
\ / / \/ / \ / to this one:
\ \ / \ \/ \ / This is called the "associator". In our logic context, we can think of the associator as a way to transform one proof into another.
The associator should satisfy an equation called the "pentagon identity", which I explained back in "week144". However, it will only do this if we let 2morphisms be equivalence classes of proof transformations.
So, there’s a kind of infinite regress here. To deal with this, it would be best to work with a "weak ωcategory" with
sentences (or sequences of sentences) as objects,
proofs as morphisms,
proof transformations as 2morphisms,
transformations of proof transformations as 3morphisms,…and so on. With this, we would never need any equivalence relations: we keep track of all transformations explicitly. This is almost beyond what mathematicians are capable of at present, but it’s clearly a good thing to strive toward.
So far, it seems Seely has gone the furthest in this direction. In his thesis, way back in 1977, he studied what one might call "weak cartesian closed 2categories" arising from proof theory. You can read an account of this work here:
R.A.G. Seely, Weak adjointness in proof theory, in Proc. Durham Conf. on Applications of Sheaves, Springer Lecture Notes in Mathematics 753, Springer, Berlin, 1979, pp. 697701. Also available at http://www.math.mcgill.ca/rags/WkAdj/adj.pdf
R.A.G. Seely, Modeling computations: a 2categorical framework, in Proc. Symposium on Logic in Computer Science 1987, Computer Society of the IEEE, pp. 6571. Also available at http://www.math.mcgill.ca/rags/WkAdj/LICS.pdf
Can we go all the way and cook up some sort of ωcategory of proofs? Interestingly, while the logicians at Geocal06 were talking about ncategories and the geometry of proofs, the mathematician Vladimir Voevodsky was giving some talks at Stanford about something that sounds pretty similar:
Vladimir Voevodsky, lectures on homotopy lambda calculus, notice at http://math.stanford.edu/distinguished_voevodsky.htm
Voevodsky has thought hard about ncategories, and he won the Fields medal for his applications of homotopy theory to algebraic geometry.
Anyway, in our conversation about categories and computation on this blog, the whole issue came up again: Mike Stay got upset when Robin Houston told him that morphisms in a CCC correspond to αβη equivalence classes of terms in the λcalculus, and Robin pointed out Seely’s work involving 2categories, which tackles this problem. Then Urs Schreiber pointed out Keeney’s bird calculus for drawing things like βreduction as 2morphisms  which indeed looks very much like the “movies” people use in the theory of braided monoidal 2categories. So, I think the time is ripe to categorify CCCs and understand computation as a process!
Re: Categorifying CCCs: computation as a process
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 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.
I will say something hopelessly lowbrow, 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
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 identitfication
Even better, by writing every morphism (element in $\mathrm{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.