In Milner's Pi Calculus, what are the evaluation semantics when multiple processes read from the same channel?

Question

In Milner's Pi Calculus, what are the evaluation semantics when multiple processes read from the same channel?

The rules say that

!x(a). P | ?x(b) Q ~> P | Q[a/b]

but what about situations like

!x(a). P | ?x(b) Q | ?x(c) R

?

Answer 1

I know this question is somewhat old, but for the sake of the next person to come searching for an answer, I'll attempt one.

The answer is: it's nondeterministic. The Pi calculus process:

?x(b).Q | ?x(c).R

Says "Either accept input on x then proceed as Q, or accept input on x and proceed as R". Both executions are valid with respect to this process. You can consider the labelled transition system associated with those process --- it will be branching, as you would expect.

It is precisely this kind of nondeterminism that makes process calculi (like Pi calculus and friends) "special", and different from things like the lambda calculus, where it doesn't matter in what order you evaluate things (you will reach the same result). Pi calculus has all this machinery like bisimulation and transition system semantics precisely so that it can capture these sorts of situations and make them amenable to analysis.