Home

The pi-Calculus in Direct Style

The pi-Calculus in Direct Style

We introduce a calculus which is a direct extension of both the
lambda and the pi calculi. We give a simple type system for it, that
encompasses both Curry's type inference for the lambda-calculus,
and Milner's sorting for the pi-calculus as particular cases of
typing. We observe that the various continuation passing style
transformations for lambda-terms, written in our calculus, actually
correspond to encodings already given by Milner and others
for evaluation strategies of lambda-terms into the pi-calculus. Furthermore,
the associated sortings correspond to well-known
double negation translations on types. Finally we provide an
adequate cps transform from our calculus to the pi-calculus.

This shows that the latter may be regarded as an "assembly
language", while our calculus seems to provide a better
programming
notation for higher-order concurrency.

a.k.a. Blue Calculus

By Andris Birkmanis at 2005-01-29 18:15 | Lambda Calculus | other blogs | 14265 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

And even more "direct"

The Deep Blue Calculus
We develop a calculus which is a "direct" descendant of the blue calculus of Boudol [Bou97]. This calculus is both an extension of Abadi & Cardelli's &-calculus [AC96] and the Milner's pi-calculus [Mil93]. We give a simple type system that is a direct extension of any type fragment considered in [AC96] encodable into the pi-calculus. The type system enjoys Subject Reduction. We provide finally an adequate CPS transform from our calculus to the blue calculus. This transform shows that the latter can be seen as a "target language", while our calculus provide a very expressive and promising notation for higher-order object-oriented concurrent programming languages.

Should I start googling for even deeper blues??!

By Andris Birkmanis at Sat, 2005-01-29 21:23 | login or register to post comments

Review

Just several points that I brought home:
  1. Application of call-by-name lambda is broken down to two constructs (def and application) of name-passing lambda - so can be used as a syntactic sugar thereafter (page 1)
  2. def is broken down to three constructs (restriction, parallel, and decl) of blue calculus - so can be used as a syntactic sugar thereafter (page 2)
  3. the resulted calculus directly subsumes both CBN lambda and pi (that was actually a disappointment to understand that CBV does not play so nice - but I might got it wrong - still have to grok CPS section which I skipped on the first reading)
  4. declared references are suggested to be separated from abstracted variables (pages 11-12)
While not unifying CBV and CBN directly, this calculus seems as a good start point for a small (or big) concurrent PL.

Also, it was a pleasure to see how presenting complex constructs in terms of simpler ("big" application via "small" application and def, then def via nu, par, and decl) allowed a more flexible and expressive structure where it's needed, while preserving simplicity where it was enough.

I will be glad to hear objections (especially from Derek, as he probably was right about CPS after all).

By Andris Birkmanis at Mon, 2005-02-21 08:31 | login or register to post comments