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,
It also allows for resource contention; here, the resource assignment acts as a mutex:
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.