### Higher Categories for Concurrency

#### Posted by John Baez

*guest post by Mike Stay*

Way back in 2006 when this blog started, we had a discussion about cartesian closed categories and the lambda calculus. There we learned about Lawvere’s invention of categorical semantics and how modern programming languages use his ideas for defining and implementing datatypes. Basically, a datatype declaration is a presentation of a cartesian closed category. Implementations of the datatype are cartesian closed functors from that category to Set; these pick out a set of values for the datatype along with functions that act on those values and satisfy the given relations. The datatype declaration is “syntax”, and the implementation functor assigns “semantics” in Set to the syntax.

In Robin Milner’s 1991 Turing Award
lecture, he explained
how Set doesn’t work as a target for implementing *concurrent*
programs. He showed how the two programs

{A: x = 1; x = x + 1;}

and

{B: x = 2;}

when run individually, assign to ` x ` the same value. But if we
run them concurrently, `x` may be either 2 or 3 depending on
whether program `A` completes before or after the first statement
in program `B`. So we need to look elsewhere for a categorical
semantics for concurrent programs.

Milner contributed a great deal to the study of concurrent programming; the award cited the following:

LCF, the mechanization of Scott’s Logic of Computable Functions, probably the first theoretically based yet practical tool for machine assisted proof construction;

ML, the first language to include polymorphic type inference together with a type-safe exception-handling mechanism

CCS, a general theory of concurrency. In addition, he formulated and strongly advanced full abstraction, the study of the relationship between operational and denotational semantics.

In CCS, the topology of interacting processes was fixed; Milner, Parrow, and Walker extended it and proposed a concurrent programming language with a dynamic topology called pi calculus, which we’ve discussed before. Bruno and Montanari gave a categorical semantics for the pi calculus in terms of cartesian closed double categories.

Gérard Boudol’s blue calculus is an elegant fusion of typed lambda calculus and pi calculus; there are faithful embeddings of both into the blue calculus. I’ve been trying to find a higher category whose objects are types, whose morphisms are blue terms with a single free variable, and whose 2-morphisms are the rewrite rules. I think I’ve succeeded, and I’d like to lay out the parts of this construction for comments. I’m in the process of writing it up as part of my thesis.

There are various features we want in the higher category:

Since we can embed lambda calculus into it, it should be at least symmetric monoidal closed.

Since concurrent processes can compete for resources, there’s the opportunity for nondeterminism: when two withdrawals hit the same account and there’s not enough to cover both, it matters which one happens first! In the blue calculus, this happens at the level of rewrite rules; unlike the lambda calculus, rewrite rules in the blue calculus are nonconfluent, so we can’t mod out by them without losing a lot. This means we’ll need at least a bicategory.

One way to think of a bunch of concurrent processes is as a “chemical soup” of terms where any two compatible terms may engage in a “chemical reaction”, interacting to become a new term. In the chemical world, such a reaction would look something like this:

$\displaystyle \begin{array}{c}Na^+ | Cl^- \\ \Downarrow \\ NaCl\end{array}$

The simplest concurrent interaction looks like this:

$\displaystyle \begin{array}{c}send y on the channel x | receive z on the channel x, then do P \\ \Downarrow \\ P[where y replaces z]\end{array}$

In blue calculus, the monoidal product from embedding lambda calculus types differently from running two processes concurrently, so we’ll need separate operations for those.

The blue calculus has a notion of

*names*; in actual programming practice, these are often called references or pointers or addresses. Names should have something to do with natural numbers and allocating resources.

### Symmetric monoidal closed bicategories

Paddy
McCrudden
defined symmetric monoidal bicategories; by defining $A \multimap -$
to be right pseudoadjoint to $- \otimes A$, we get symmetric monoidal
closed bicategories. Simon Ambler’s
thesis gives a term calculus
for symmetric (weakly) monoidal closed categories; by treating the
rewrites as 2-morphisms, it should provide a 2-term calculus for
symmetric monoidal closed *bi*categories.

### Tensor product versus concurrency

In the blue calculus, one can run any two terms of the same type concurrently and get a new term of that type:

$\displaystyle \frac{\Gamma \vdash T:X \quad \quad \Gamma \vdash T':X}{\Gamma \vdash (T|T'):X},$

where $\Gamma$ is a typing context. Since morphisms are just terms
with a single free variable, this suggests that we should be enriching
over the monoidal bicategory SymMonCat so that the category Hom($A,B$)
is symmetric monoidal: the tensor product is | and the unit is the
do-nothing process $0$. In a symmetric monoidal closed bicategory
enriched over SymMonCat, the tensor product $\otimes$ distributes over
the tensor product $|$, which is analogous to how multiplication
distributes over addition. To emphasize this, I’ll talk about the
tensor *product* of objects, 1-morphisms, and 2-morphisms and the
concurrent *sum* of 1-morphisms and 2-morphisms. I think this is a
critical feature that has been missing from previous attempts to give
categorical semantics to concurrent calculi.

### Aside: physics

Physicists can get some intuition of categories enriched over SymMonCat using an example that John Baez and I came up with in Singapore. 2Hilb—the category of 2-Hilbert spaces, linear functors, and linear natural transformations—is an example of a symmetric monoidal closed bicategory enriched over SymMonCat. Concurrent processes correspond to sums of linear functors acting on the same 2-Hilbert space, whereas parallel processes act on different 2-Hilbert spaces. If we allow formal sums of cobordisms that have the same source and target manifolds, then $n Cob_2$ is also one of these kinds of bicategories: the tensor product is horizontal juxtaposition and the concurrent sum is the formal sum. An extended TQFT is a structure-preserving functor between such bicategories.

### Names

Ian Stark’s work on the nu calculus shows that we can model names by introducing a natural-number object $N$ and then introducing the monad $N \multimap -$, where

$\begin{array}{rrcl}\mu_X:&N \multimap N \multimap X & \to & \N \multimap X\\&f & \mapsto & \lambda n.f(n, n+1)\\ \\ \eta_X:&X & \to & N \multimap X \\ &x & \mapsto & \lambda n.x \end{array}$

Given such a monad, we can then define the inference rule

$\displaystyle \frac{\Gamma, n:N \vdash T:X}{\Gamma \vdash (\lambda n.T)(fresh):X}$

where the fresh number comes from the monad. In the nu calculus, this curry-then-apply-to-fresh operation is written

$\displaystyle \frac{\Gamma, n:N \vdash T:X}{\Gamma \vdash (\nu n.T):X}$

In many programming languages, the $\nu$ operator is called “new”; the Greek “nu” is a pun.

### Blue calculus

We’re now in a position to introduce the blue calculus:

$\displaystyle \begin{array}{rlc}T, T' ::= & x &|\\& T x &|\\& \lambda x.T &|\\& (x = T) &|\\& (x \Leftarrow T) &|\\& T|T' &|\\& \nu x.T\end{array}$

Note that the second term constructor says that unlike in the lambda calculus, one can only apply terms to variables. To enforce this, we use an endofunctor of bicategories $P$ in our typing rules; whereas the simple term $x:X$ is merely a value with no potential for side-effects, we read $T:P(X)$ as being a process of type $X$ that may result in the creation of new names. A standard choice for $P$ is $N \multimap -$.

$\displaystyle \frac{}{x_1:X_1, \ldots, x_n:X_n \vdash x_i:X_i} \quad 1 \le i \le n$

$\displaystyle \frac{}{x:X \vdash x:P(X)}$

$\displaystyle \frac{\Gamma \vdash T:P(X \multimap Y) \quad \quad \Gamma \vdash x:X}{\Gamma \vdash T x:P(Y)}$

$\displaystyle \frac{\Gamma, x:X \vdash T:P(Y)}{\Gamma \vdash (\lambda x.T):P(X \multimap Y)}$

$\displaystyle \frac{\Gamma \vdash x:X \quad \quad \Gamma \vdash T:P(X)}{\Gamma \vdash (x=T):P(Y)}$

$\displaystyle \frac{\Gamma \vdash x:X \quad \quad \Gamma \vdash T:P(X)}{\Gamma \vdash (x\Leftarrow T):P(Y)}$

$\displaystyle \frac{\Gamma \vdash T:P(X) \quad \quad \Gamma \vdash T':P(X)}{\Gamma \vdash (T|T'):P(X)}$

$\displaystyle \frac{\Gamma, x:N \vdash T:P(Y)}{\Gamma \vdash (\nu x.T):P(Y)}$

We should model these inference rules as (di)natural transformations (of functors between bicategories of this kind).

The interactions between the concurrent sum of terms looks like this in the blue calculus:

$\displaystyle \begin{array}{c}x y | (x \Leftarrow T) \\ \Downarrow \\ T y \end{array}$

If $T$ is a term of the form $\lambda z.T'$ then at this point beta reduction happens just as in lambda calculus. Interactions and the beta and eta rules should be modeled as modifications.

### Conclusion

Symmetric monoidal closed bicategories, enriched over the monoidal bicategory SymMonCat and equipped with a datatype and a monad for names, provide

the ability to embed lambda calculus

the ability to model nonconfluent rewrite rules

concurrent sums different from the monoidal product

interactions on named channels

which together, I believe, are sufficient for modeling Boudol’s blue calculus.

## Re: Higher Categories for Concurrency

Hi Mike,

I am not quite following yet. Maybe you can help me a bit.

I see that you say that you need a category enriched in symmetric monoidal categories, but I do not quite follow why exactly. I do get the rough idea that somehow the tensor product is supposed to take care of the parallelism, which makes a lot of sense, but that alone would just suggest to enrich just in abelian monoids = symmetric monoidal 0-categories, no? How is the 2-categorical aspect related to the concurrency? Sorry, maybe I am missing the whole point. But then, maybe you can expand.

Sorry for the dumb question. I think what would help me is if you could systematically, in a textbook kind of fashion, tell me what the

2-categorical semanticsis that you are thinking of. You do define above the blue calculus (why “blue”?), and I gather there is now be supposed to be a set of rules for how to interpret that in some kind of 2-category with monoidal hom-categories. (Did you even say what kind of such 2-category precisely you need?)I would enjoy if you could spell out that 2-categorical semantics (at least a fragment of it) explicitly. Thanks.