Understanding Pi Calculus
2023-09-06
Synopsis
Introduction
introduce
Syntax
Symbol
\[x ::= \mathtt{a} \hspace{.3em} | \hspace{.3em} \mathtt{b} \hspace{.3em} | \hspace{.3em} \ldots \hspace{.3em} | \hspace{.3em} \mathtt{aa} \hspace{.3em} | \hspace{.3em} \mathtt{ab} \hspace{.3em} | \hspace{.3em} \ldots\]
Action
\[\begin{split}\begin{array}{rl}
a := & (\mathbf{send} \hspace{.3em} x \hspace{.3em} x) \\
| & (\mathbf{recv} \hspace{.3em} x \hspace{.3em} x) \\
| & \tau
\end{array}\end{split}\]
Process
\[\begin{split}\begin{array}{rl}
p ::= & 0 \\
| & (+ \hspace{.3em} (\mathbf{sync} \hspace{.3em} a \hspace{.3em} p) \hspace{.3em} \ldots) \\
| & (+_! \hspace{.3em} (\mathbf{sync} \hspace{.3em} a \hspace{.3em} p) \hspace{.3em} \ldots) \\
| & (| \hspace{.3em} p \hspace{.3em} \ldots) \\
\end{array}\end{split}\]
Evaluation Context
\[\begin{split}\begin{array}{rl}
E ::= & [] \\
| & (+ \hspace{.3em} (\mathbf{sync} \hspace{.3em} a \hspace{.3em} p) \hspace{.3em} \ldots \hspace{.3em} (\mathbf{sync} \hspace{.3em} a \hspace{.3em} E) \hspace{.3em} \hspace{.3em} (\mathbf{sync} \hspace{.3em} a \hspace{.3em} p) \hspace{.3em} \ldots) \\ | & (+_! \hspace{.3em} (\mathbf{sync} \hspace{.3em} a \hspace{.3em} p) \hspace{.3em} \ldots \hspace{.3em} (\mathbf{sync} \hspace{.3em} a \hspace{.3em} E) \hspace{.3em} \hspace{.3em} (\mathbf{sync} \hspace{.3em} a \hspace{.3em} p) \hspace{.3em} \ldots) \\
| & (| \hspace{.3em} p \hspace{.3em} \ldots \hspace{.3em} E \hspace{.3em} \hspace{.3em} p \hspace{.3em} \ldots) \\
\end{array}\end{split}\]
Syntactic Sugar
Base Process
Synchronization
Choice
Composition
Restriction
Replication
Reduction
\[(recv \tau p_1) \cdot p_1\]