Separation and Encodability in Mixed Choice Multiparty Sessions (Technical Report)

TL;DR

This work extends multiparty session types with mixed choice (MCMP), develops a general typing system guaranteeing communication safety and deadlock-freedom, and establishes a comprehensive expressiveness hierarchy among MCMP subcalculi and CMV$^+$ variants. By constructing good encodings and separations (e.g., via M and star synchronization patterns and leader election), the authors show MCMP strictly outperforms classical MP in expressive power and that mixed choice at the multiparty level yields richer interaction patterns than binary mixed-choice settings. The results reveal that while some binary encodings preserve expressiveness across related calculi, the top-layer MCMP capabilities can not be emulated by bottom-layer calculi, underscoring the practical impact of allowing mixed choice across multiple participants. The paper also demonstrates how to encode between many of the calculi, preserving safety, deadlock-freedom, and distributability, and it sets the stage for future work on more general features such as session delegation and global-type projections with flexible choices.

Abstract

Multiparty session types (MP) are a type discipline for enforcing the structured, deadlock-free communication of concurrent and message-passing programs. Traditional MP have a limited form of choice in which alternative communication possibilities are offered by a single participant and selected by another. Mixed choice multiparty session types (MCMP) extend the choice construct to include both selections and offers in the same choice. This paper first proposes a general typing system for a mixed choice synchronous multiparty session calculus, and prove type soundness, communication safety, and deadlock-freedom. Next we compare expressiveness of nine subcalcli of MCMP-calculus by examining their encodability (there exists a good encoding from one to another) and separation (there exists no good encoding from one calculus to another). We prove 8 new encodablity results and 20 new separation results. In summary, MCMP is strictly more expressive than classical multiparty sessions (MP) and mixed choice in mixed sessions. This contrasts earlier results where mixed sessions do not add any expressiveness to non-mixed fundamental sessions, shedding a light on expressiveness of multiparty mixed choice.

Figures (19)

• Figure 1: Hierarchy of $\pi$-like calculi PY2022
• Figure 2: Reduction and structure congruence of MCMP
• Figure 3: Labelled transition systems of types and contexts
• Figure 4: Typing rules for MCMP-calculus.
• Figure 5: Hierarchy of Session Calculi

Theorems & Definitions (134)

• Definition 2.1: syntax
• Definition 2.2: Family of MCMP
• Example 2.1: A Family of MCMP
• Example 2.2: Leader election protocol
• Definition 3.1: MCMP types and local contexts
• Definition 3.2: Subtyping
• Example 3.1: Mixed choice subtyping
• Proposition 3.1: Subtyping
• Remark 3.1: Subtyping
• Definition 3.3: Local context reductions