On the Expressiveness of Mixed Choice Sessions

09/06/2022
by   Kirstin Peters, et al.
0

Session types provide a flexible programming style for structuring interaction, and are used to guarantee a safe and consistent composition of distributed processes. Traditional session types include only one-directional input (external) and output (internal) guarded choices. This prevents the session-processes to explore the full expressive power of the pi-calculus where the mixed choices are proved more expressive than the (non-mixed) guarded choices. To account this issue, recently Casal, Mordido, and Vasconcelos proposed the binary session types with mixed choices (CMV+). This paper carries a surprising, unfortunate result on CMV+: in spite of an inclusion of unrestricted channels with mixed choice, CMV+'s mixed choice is rather separate and not mixed. We prove this negative result using two methodologies (using either the leader election problem or a synchronisation pattern as distinguishing feature), showing that there exists no good encoding from the pi-calculus into CMV+, preserving distribution. We then close their open problem on the encoding from CMV+ into CMV (without mixed choice), proving its soundness and thereby that the encoding is good up to coupled similarity.

READ FULL TEXT

Please sign up or login with your details

Forgot password? Click here to reset