Minimality and separation results on asynchronous mobile processes – representability theorems by concurrent combinators

AbstractIn Honda and Yoshida (TACS’94, Lecture Notes in Computer Science, vol. 789, Springer, Berlin, 1994, pp. 786–805; POPL’94, ACM Press, New York, 1994, pp. 348–360) we presented a theory of concurrent combinators for the asynchronous monadic π-calculus without match or summation operator. The system of concurrent combinators is based on a finite number of atoms and fixed interaction rules, but is as expressive as the original calculus, so that it can represent diverse interaction structures, including polyadic synchronous name passing and input guarded summations. The present paper shows that each of the five basic combinators introduced in Honda and Yoshida (POPL’94, ACM Press, New York, 1994, pp. 348–360) is indispensable to represent the whole computation, i.e. if one of the combinators is missing, we can no longer express the original calculus up to semantic equalities. Expressive power of several interesting subsystems of the asynchronous π-calculus is also measured by using appropriate subsets of the combinators and their variants. Finally, as an application of the main result, we show there is no semantically sound encoding of the calculus into its proper subsystem under a certain condition