reperiendi

Blue calculus

Posted in Programming by Mike Stay on 2008 August 3

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:

P := x \;|\; (P P) \;|\; \lambda x.P

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

The beta-reduction rule says

((\lambda x.P)\; P')

\Downarrow

P[P'/x] if the variables in P' are all free in P.

The part in brackets reads “with P' replacing x.”  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:

\nu x.((P\; x) \;|\; (x \Leftarrow P'))

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

  1. a “small” application

    (P\; x)

    in which a term P may only be applied to a variable x;

  2. a resource assignment

    x \Leftarrow P

    in which a variable x is associated to a one-time use of the term P;

  3. a new variable declaration

    \nu x.P

    that introduces a new bound variable into scope; and

  4. a symmetric monoidal product of terms, thought of as “parallel processes”

    P \;|\; P

    The monoidal unit here is the “do-nothing” term (\nu x.x).

Blue calculus also splits beta reduction into two parts:

  1. a “small” beta reduction

    ((\lambda x.P)\; x')

    \Downarrow

    P[x'/x] if x' is free in P;

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

    (\ldots ((x\;y_0)\; y_1)\; \ldots \;y_{n-1}) \;|\; (x \Leftarrow P)

    \Downarrow

    (\ldots ((P\; y_0)\; y_1)\; \ldots \; y_{n-1}).

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

(x\; y) \;|\; (x \Leftarrow P) \;|\; (x \Leftarrow Q)

has two valid reductions,

(P\; y)  \;|\; (x \Leftarrow Q)

or

(Q\; y)  \;|\; (x \Leftarrow P).

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

(x\; y) \;|\; (x\; z) \;|\; (x\; \Leftarrow P)

\Downarrow

(P\; y) \;|\; (x\; z) or (x\; y) \;|\; (P\; z).

The application term \nu k.((\lambda x.P)\; k) \;|\; (k \Leftarrow P')) is a linear term. If the term P uses x 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:

x = P

\Updownarrow

(x \Leftarrow P) \;|\; (x = P)

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:

P := x \;|\; (P\; x) \;|\; \lambda x.P \;|\; \nu x.P \;|\; (x \Leftarrow P) \;|\; (x = P) \;|\; (P|P)

Lambda terms embed like this:

\begin{array}{rcl} [x] & \Rightarrow & x \\ ~[\lambda x.M] & \Rightarrow & \lambda x.[M] \\ ~[MN] &\Rightarrow & \nu u.([M]u \;|\; (u = [N])) \quad \mbox{where } u \mbox{ does not appear in } M \mbox{ or } N\end{array}

Pi terms embed like this:

\begin{array}{rcl} [\bar{u}x_1\ldots x_n] & \Rightarrow & ux_1\ldots x_n \\ ~[ux_1\ldots x_n.P] & \Rightarrow & (u \Leftarrow \lambda x_1\ldots x_n.P) \\ ~[(P \;|\; Q)] & \Rightarrow & ([P] \;|\; [Q]) \\ ~[\nu u.P] & \Rightarrow & \nu u.[P] \end{array}

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.

Advertisements

2 Responses

Subscribe to comments with RSS.

  1. saintali said, on 2008 August 17 at 3:53 pm

    That’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?

  2. reperiendi said, on 2008 August 17 at 5:08 pm

    In 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.


Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: