### Categories and Computation

#### Posted by John Baez

My student Mike Stay and I are working on category theory and quantum computation. But, I still have some catching up to do when it comes to category theory and ordinary computation!

If anyone else wants to learn about this, here are some fun, easy places to start:- Mark Chu-Carroll, Lambda calculus
- Mark Chu-Carroll, Category theory
- Phil Scott, Some aspects of categories in computer science

The first two appear on Mark’s blog, *Good Math, Bad Math*.

I’m not going to explain this stuff here. I’m just going to dive in.

Here’s something Mike wrote, and my reply. He wrote:

JB wrote:

We’ve gotta figure out what the heck is really going on here.

I talked to Jim some more and we figured out what it is. You get programs for free in a lambda theory. As soon as you have one type, you get a whole bunch of programs as morphisms in the category, everything you can write using typed S and K combinators. These programs are proofs in intuitionistic logic.

The terms that we mention explicitly in a lambda theory are like ports on the outside of a black box. We know what we can plug in, but not what happens inside. So our programs can now call these things as well, but we don’t know what they *do* yet. From the “programs as proofs” view, they’re additional axioms in the intuitionistic logic. Then the axioms of the lambda theory become equivalences of proofs in the intuitionistic logic.

When you take a model of the theory in Set, you assign sets to the types and functions to the explicit terms, but both of these can (in principle) be uncomputable! For example, using the lambda theory of groups, you could take the free group over the set of all halting programs—this set is only computably enumerable, not computable. If you had the free lambda theory with one type N and one function f:N->N, then the image of N could be the natural numbers and f could be the function that produces the nth bit of an omega number. It would be a programming language with an oracle.

So if we want the sets and functions to be computable, we need to look at *computable functors* from the theory to Set!

I replied:

Good! I’m going to respond to this at the n-category cafe. As long as we’re discussing stuff that’s not “top secret” new research, and perhaps even when we are, I’d like to talk there. Some categorical logicians may come along and help us out.

We need a precise dictionary, something that starts maybe sorta like this:

COMPUTATION LOGIC CATEGORY THEORY data type proposition object program proof morphismA program takes data of one type and spits out data of some other type. A proof takes a proposition as its assumption and spits out another proposition as conclusion.

Note, if an object x is a “data type”, specific data of that type is a morphism f: 1 → x. We can apply a “program” g: x → y to this data and get data of type y, namely gf: 1 → y.

In the “logic” column we say all this stuff differently. We say g: x → y is a proof of y from x, while f: 1 → x is a proof of x from “true”, i.e. just a proof of x. We can compose these to get a proof of y, namely gf: 1 → y.

Note that in the “logic” column, the product means “and”, and 1, or “true”, is the unit for “and”. Using “and” we can reduce a list of propositions to a single proposition.

Figure out what’s going on here in the “computation” column:

COMPUTATION LOGIC CATEGORY THEORY data type proposition object program proof morphism ?? and product ?? true 1Now, this stuff I sort of understood. I start getting mixed up when people say that computation proceeds by doing alpha- conversion and beta-reduction to a lambda-calculus expression. It actually seems we need a whole new column here:

LAMBDA-CALCULUS COMPUTATION LOGIC CATEGORY THEORY ?? data type proposition object ?? program proof morphism ?? ?? and product ?? ?? true 1 expression ?? ?? ?? alpha-conversion ?? ?? ?? beta-reduction ?? ?? ??Of course this new column is just the “syntax” for which the category theory column is the “semantics”. So, there might not be a simple 1-1 correspondence between each item of the first column and each item of the last, but our syntax-semantics theorem should tell us their relationship.

What is it?

And, what does it mean to think of computation as doing “lazy evaluation” repeatedly to a lambda calculus expression? I mean, what does this correspond to in the other columns? Programs as morphisms are fine, but where in the category-theoretic view do we see the program “grind away” as it does a computation step by step?

**Note:**after a huge discussion I’ve decided to turn off comments on this entry; if you wish to talk about this stuff, please post a comment to one of these:

The first thread is solely for questions that stay within the existing theory of CCC’s and lambda calculus - for example, questions about formulating the untyped lambda calculus as a CCC, questions about the free CCC on one object, questions about PCF, etc.

The second is for attempts to see computation as a process, for example by seeing β- and η-reduction as 2-morphisms in some kind of “cartesian closed 2-category”.

The third is for attempts to generalize CCC’s for the purposes of quantum computation - mainly in the direction of symmetric monoidal categories, typically with other bells and whistles.

## Re: Categories and computation

One interesting aspect of

untyped$\lambda$-calculus is that objects and morphisms are in a way identical.Every (untyped) $\lambda$-expression is a little program that eats other little programs of its kind and spits out yet another program of that sort.

Better yet, the way all these programs work is beautifully self-referential, in that every program just encodes a way to evaluate the program it gets as argument on other programs.

So for instance the expression

takes four programs $f$, $g$, $x$ and $y$ as arguments and evaluates them on each other in the way indicated.

As you know, feeding two programs into this beast that are of the form

produces another program of this form, with the number of $f$s being the

sumof the $f$s of the two inputs.So the above program is addition of natural numbers. But you can feed any other program into it, one that does not encode a natural numbers, and the above program still produces a well defined output. It provides a perfectly general notion of what it means to add two programs (of the sort that map programs to programs which map programs to programs which …).

When I was a kid I got pretty excited about this beautiful self-referentiality, which produces lots of interesting structure from virtually nothing.

Of course it is very familiar in computation, that you can regard code as data, but in the untyped $\lambda$-calculus this phenomenon appears in a particularly explicit form. Here one cannot distinguish code from data, even in principle. Unless, that is, you pass to typed $\lambda$-calculus.

I always wondered if

untyped $\lambda$-calculus is somehow related to $\omega$-categories, It seems that in both cases there is a certain way in which objects and morphisms are identified.But I cannot make this hunch precise, unfortunately.

And, it seems, my problem with doing so rests precisely in some of the question marks that you drew into your table above.

So I am very interested in what you will come up with.

But as a first step, I’d suggest that you start by replacing the first two question mark entries in the top left of your table both with then entry “expression”. In $\lambda$-calculus, $\lambda$-expression are both data as well as program.

This would allow to remove the two bottom lines completely.

But that’s just my suggestion.