## Blue calculus

The lambda calculus is a Turing-complete language, but doesn’t handle concurrency very well; in particular, there’s no concept of a *reference* as opposed to a *value*. The lambda calculus has three productions:

The first production, , is a variable; the second is an application of one term to another; and the third is abstraction.

The beta-reduction rule says

if the variables in are all free in .

The part in brackets reads “with replacing .” There are different evaluation strategies that one can use with the lambda calculus; one strategy that always reduces the term to its normal form if it has one is called “lazy evaluation.” With this strategy, you only reduce a term if it’s necessary to do so.

The blue calculus builds this strategy into the language. Here is an application term in the blue calculus:

Blue calculus splits application into four parts, or “processes”:

- a “small” application
in which a term may only be applied to a variable ;

- a resource assignment
in which a variable is associated to a one-time use of the term ;

- a new variable declaration
that introduces a new bound variable into scope; and

- a symmetric monoidal product of terms, thought of as “parallel processes”
The monoidal unit here is the “do-nothing” term .

Blue calculus also splits beta reduction into two parts:

- a “small” beta reduction
if is free in ;

- and a resource fetching rule that gets the value of a variable only when it’s needed
.

By splitting things up this way, the blue calculus allows patterns like nondeterministic choice. The blue calculus term

has two valid reductions,

or

.

It also allows for resource contention; here, the resource assignment acts as a mutex:

or .

The application term is a *linear* term. If the term uses more than once, then only the first usage will be able to fetch the resource: a resource assignment is consumed by the small beta rule. However, the blue calculus also supports resource replication:

This allows the blue calculus to subsume both the lambda calculus and the pi calculus in a nice way. Blue terms are formed as follows:

Lambda terms embed like this:

Pi terms embed like this:

There are reduction rules for scope migration, associativity, distributivity, replication, and so forth; see the paper for more details.

The upshot of all this is that blue calculus variables are really references, and so one can build the whole theory of concurrent objects on top of it.

saintalisaid, on 2008 August 17 at 3:53 pmThat’s all so wonderful and everything fits in its own place, building a type system for this calculus should be more straightforward than for Pi-calculus. But I can see that it has been published 10 years ago, then the question comes to mind about what has been the academic community’s reaction to the Blue Calculus?

reperiendisaid, on 2008 August 17 at 5:08 pmIn his paper, Boudol shows how to type the blue calculus, both with the simple typing from lambda calculus and the well-sorting from pi-calculus.

As for the response, it’s been muted at best. The paper I cited is hard to read; it took me a long time to understand as much as I have. That, combined with the proliferation of various calculi, each designed to illustrate one point or another, probably means that no one will pay attention to it unless someone promotes it heavily.

My real interest in it is to understand how to model concurrent objects using category theory, and from there to get a category-theoretic description of object capabilities.