# reperiendi

## Polyadic asynchronous asymmetric pi calculus

Posted in Programming by Mike Stay on 2008 January 2

$\begin{array}{rll} P :=\\& \mbox{send } \langle y_1, \ldots, y_n\rangle \mbox{ on } \bar{x}. & |\\& \mbox{receive } \langle y_1, \ldots, y_n\rangle \mbox{ on } x; P &|\\& (P|P) &|\\& \mbox{new }y; P & |\\& !P\end{array}$

where $y$ is either an input channel $x$ or an output channel $\bar{x},$ and $x$ is taken from a countably infinite set.

Structural congruence:

• $\mbox{new } y; P \equiv \mbox{new } y'; P'$ [with $y'$ replacing $y$] if $y'$ does not appear in $P.$ (alpha conversion)
• $(P|P') \equiv (P'|P)$ (parallel processes)
• $((P|P')|P'') \equiv (P|(P'|P''))$ (association)
• $\mbox{new } y; \mbox{new } y'; P \equiv \mbox{new } y'; \mbox{new } y; P$ (restriction)
• $!P \equiv (P|!P)$ (replication)
• $\mbox{new } y; (P|P') \equiv \mbox{new } y; P|P'$ if $y$ is not free in $P'.$

Reduction rules:

• $(\mbox{send } \langle y_1, \ldots, y_n \rangle \mbox{ on } \bar{x}. | \mbox{ receive } \langle y'_1, \ldots, y'_n \rangle\mbox{ on } x; P) \to P$ [with $y_i$ replacing $y'_i$]
• If $P_1 \to P_2$ then $(P_1|P_3) \to (P_2|P_3)$
• If $P_1 \to P_2$ then $\mbox{new } y; P_1 \to \mbox{new } y; P_2$
• If $P_1 \equiv P_2, \; P_2 \to P_3,$ and $P_3 \equiv P_4,$ then $P_1 \to P_4$