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
Advertisements

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: