Abstract:
The 
-calculus with synchronous output and mixed-guarded
choices is strictly more expressive than the -calculus with asynchronous
output and no choice. As a corollary, Palamidessi recently proved that there
is no fully compositional encoding from the former into the latter that
preserves divergence-freedom and symmetries. This paper shows that there are
nevertheless `good' encodings between these calculi.
In detail, we present a series of encodings for languages with (1) input-guarded choice, (2) both input- and output-guarded choice, and (3) mixed-guarded choice, and investigate them with respect to compositionality and divergence-freedom. The first and second encoding satisfy all of the above criteria, but various `good' candidates for the third encoding|inspired by an existing distributed implementation|invalidate one or the other criterion. While essentially confirming Palamidessi's result, our study suggests that the combination of strong compositionality and divergence-freedom is too strong for more practical purposes
Available as PostScript, PDF, DVI.