Encoding Choice and Replication in \(\mathtt{\textbf{roll}}\text {-}\pi \)
摘要
Reversible process calculi, such as \(\mathtt{\textbf{roll}}\text {-}\pi \) , can accommodate fault-tolerant communication protocols. However, untyped process calculi cannot guarantee desirable behavioural properties such as deadlock-freedom. Concomitantly, Multiparty Session Types (MPST) can provide such guarantees by construction, but often do not consider failures. This suggests that, by leveraging both MPST and \(\mathtt{\textbf{roll}}\text {-}\pi \) , we can facilitate the representation of failures without requiring a significant extension to the MPST theory. However, \(\mathtt{\textbf{roll}}\text {-}\pi \) lacks choice and replication primitives, which are key features for an MPST-based type system. Nonetheless, its expressiveness allows these constructs to be encoded directly. In this paper, we introduce \(\mathtt{\textbf{roll}}\text {-}\pi !\oplus \) , a variant of \(\mathtt{\textbf{roll}}\text {-}\pi \) that incorporates choice and replication, and outline its encoding in \(\mathtt{\textbf{roll}}\text {-}\pi \) . This extension lays the foundation for integrating \(\mathtt{\textbf{roll}}\text {-}\pi \) with MPST.