\documentclass[11pt]{article}
\newif\ifslidegeometry
\slidegeometrytrue

\input{lecture-pre}
\input{common}
\begin{document}

\input{lecture-post}
\newcommand{\dateoflecture}{16 November 2004}
\setfooters{\dateoflecture}

\begin{slide}

  \vspring
  \vspring

  \begin{center}
    \sizeb \tcR{\bf MPRI Concurrency (course number 2-3) 2004-2005:}\\
    \tcR{\bf \pic}
    \\
    \dateoflecture
    \\
    \vspring
    {\sizez http://pauillac.inria.fr/$\sim$leifer/teaching/mpri-concurrency-2004/ }
    \\
    \vspring
    James J. Leifer 
    \\
    INRIA Rocquencourt
    \\
    \vspring
    James.Leifer@inria.fr
    \\
  \end{center}

  \vspring
  \vspring
\end{slide}

\begin{slide}

  \slidehead{About the lectures}

  \vspring

  \begin{itemize}
  \item The MPRI represents a transition from \emph{student} to 
    \emph{researcher}. So...
  \vspring

%  \item Thus I'd like for us to work at this as researchers, if you're willing/able!
  \item Interrupting me with questions is good.

  \vspring

  \item Working through a problem without already knowing the answer
    is good.

  \vspring

  \item I'll make mistakes. 8-)
  \end{itemize}

  \vspring  \vspring

  \slidehead{About me}

  \vspring

  \begin{itemize}
  \item 1995--2001: Ph.D. student of Robin Milner's in Cambridge, UK

  \vspring

  \item 2001--2002: Postdoc in INRIA Rocquencourt, France 
  \vspring

  \item 2002--: Research scientist in INRIA Rocquencourt, France

  \item November 2004: voted against W (who, despite this, was
    elected for the first time)

  \end{itemize}

  \vspring

\end{slide}


\begin{slide}
  \slidehead{Books}
  \raggedright

  \begin{itemize}
  \item Robin Milner. \emph{Communicating and mobile systems: the
      $\pi$-calculus}. (Cambridge University Press, 1999).
  \item Robin Milner. \emph{Communication and concurrency}. (Prentice
    Hall, 1989).
  \item Davide Sangiorgi and David Walker. \emph{The $\pi$-calculus: a
      theory of mobile processes}. (Cambridge University Press, 2001).
  \end{itemize}

  \vspring

  \slidehead{Tutorials available online}

  \begin{itemize}
  \item Robin Milner. ``The polyadic pi-calculus: a tutorial''.
    Technical Report ECS-LFCS-91-180, University of Edinburgh. {\sizes
      http://www.lfcs.inf.ed.ac.uk/reports/91/ECS-LFCS-91-180/ECS-LFCS-91-180.ps}

  \item Joachim Parrow. ``An introduction to the pi-calculus''.
    {\sizes http://user.it.uu.se/$\sim$joachim/intro.ps}

  \item Peter Sewell. ``Applied pi --- a brief tutorial''. Technical
    Report 498, University of Cambridge. {\sizes
      http://www.cl.cam.ac.uk/users/pes20/apppi.ps}
  \end{itemize}


  \vspring
\end{slide}

\begin{slide}
  \slidehead{Today's plan}

  \vspring

  \begin{itemize}
    \item syntax

      \vspring

    \item reduction semantics and structural congruence

      \vspring

%    \item examples: polyadic into monadic, synchronous into
%      asynchronous, definitions into replication
%
%      \vspring

    \item labelled transitions 

      \vspring

    \item bisimulation
  \end{itemize}

  \vspring

\end{slide}

\begin{slide}

  \slidehead{Syntax}

  \vspring
  
  \begin{center}
    \begin{tabular}{>{$}l<{$}@{}>{$}l<{$}!{\qquad}l}
      P ::= {}
      & \outp x y P & output \\
      & \inp x y P  & input \tcR{($y$ binds in $P$)} \\
      & \newp x P    & restriction (new)  \tcR{($x$ binds in $P$)}\\
      & P \parp P   & parallel (par) \\
      & \zerop      & empty \\
      & \bangp P    & replication (bang) \\
      & ...         & \\
%      & \matchp x y P & match \\
%      & \mismatchp x y P & mismatch \\
    \end{tabular}
  \end{center}

  \vspring
  Significant difference from CCS: channels carry names.
  \vspring
\end{slide}

\begin{slide}
  \slidehead{Free names}

  \vspring

  The free names of $P$ are written $\fn P$.
  \vspring

  \emph{Example:}
  % 
  $\fn \zerop = \emptyset$;
  % 
  $\fn {\outp x y {\inp z y \zerop}} = \{x,y,z\}$.

  \vspring

  \emph{Exercise:} Calculate
  % 
  $\fn {\inp z y {\outp x y \zerop}}$;
  % 
  $\fn {\newp z {(\inp z y {\outact x y} )} \parp \outact y z}$.

  \vspring

  Formally:
  % 
  \[\sizes 
  \begin{array}{lcl}
    \fn {\outp x y P} & = & \{x,y\} \cup \fn P \\
    \fn {\inp x y P}  & = & \{x\} \cup (\fn P \setminus \{y\}) \\
    \fn {\newp x P}   & = & \fn P \setminus \{x\} \\
    \fn {P \parp P'}  & = & \fn P \cup \fn {P'} \\
    \fn {\zerop}      & = & \emptyset \\
    \fn {\bangp P}    & = & \fn P \\
  \end{array}\]

  \vspring
  \slidehead{Alpha-conversion}

  We consider processes up to alpha-conversion:   provided $y' \notin
  \fn P$, we have
  % 
  \begin{gather*}
    \inp x y P = \inp x {y'} {\sub {y'} y P} \\
    \newp y P = \newp {y'} {\sub {y'} y P}
  \end{gather*}
  % 

  \vspring
  \emph{Exercise:} Freshen all bound names:
  % 
  $\newp x {(\inp x x {\outact x x })} \parp \inact x x $

  \vspring
\end{slide}

\begin{slide}
  \slidehead{Reduction ($\red{}$)}

  \vspring

  We say that $P$ reduces to $P'$, written $P \red{} P'$, if this can
  be derived from the following rules:
  % 
  \begin{gather*}
    \outp x y P \parp \inp x u Q \red{} P \parp \sub y u Q
    \eqtag{red-comm}
    \\
    \infer{P \red{} P'}{P \parp Q \red{} P' \parp Q}
    \eqtag{red-par}
    \\
    \infer{P \red{} P'}{\newp x P \red{} \newp x P'}
    \eqtag{red-new}
  \end{gather*}

  \vspring

  \emph{Example:} %
  $\newp x {(\outact x y \parp \inp x u {\outact u z})} \red{} %
   \newp x {(\zerop \parp \outact y z)}
  $

  \vspring

  As currently defined, reduction is too limited:
  \begin{gather*}
    (\outact x y \parp \zerop) \parp \inact x u \nored{}
    \\
    \newp w {\outact x y} \parp \inact x u \nored{}
  \end{gather*}

  \vspring
\end{slide}

\begin{slide}
  \slidehead{Structural congruence ($\streq$)}

  \begin{gather*}
    P \parp (Q \parp S) \streq (P \parp Q) \parp S \eqtag{str-assoc}
    \\
    P \parp Q \streq Q \parp P \eqtag{str-commut}
    \\
    P \parp \zerop \streq P \eqtag{str-id}
    \\
    \newp x {\newp y P} \streq \newp y {\newp x P} \eqtag{str-swap}
    \\
    \newp x \zerop \streq \zerop \eqtag{str-zero}
    \\
    \newp x P \parp Q \streq \newp x {(P \parp Q)} %
    \qquad\text{if $x \notin \fn Q$} \eqtag{str-ex}
    \\
    \bangp P \streq P \parp \bangp P \eqtag{str-repl}
  \end{gather*}
  
  \vspring

  We close reduction by structural congruence:

  \begin{gather*}
    \infer{P \mathbin{{\streq} {\red{}} {\streq}} P'}{P \red{} P'}
    \eqtag{red-str}
  \end{gather*}
  
  \vspring

  \emph{Exercise:} Calculate the reductions of %
  $\newp y {(\outact x y \parp \inp y u {\outact u z})} \parp \inp x w {\outact w
    v}$ and \\%
  $ \outact x y \parp \newp y {(\inp x u {\outact u w} \parp \inact y
    v)}$

  \vspring
\end{slide}

\begin{slide}
  \slidehead{Application of new binding: from polyadic to monadic channels}

  \vspring

  Let us extend our notion of \emph{monadic} channels, which carry
  exactly one name, to \emph{polyadic} channels, which carry a vector
  of names, \ie
  % 
  \vspring
  % 
  \begin{center}
    \begin{tabular}{>{$}l<{$}@{}>{$}l<{$}!{\qquad}l}
      P ::= {}
      & \polyoutp x {y_1,...,y_n} P & output \\
      & \polyinp x {y_1,...,y_n} P  & input \tcR{($y_1,...,y_n$ bind in $P$)}
    \end{tabular}
  \end{center}

  \vspring

  Is there an encoding from polyadic to monadic channels?  We might
  try:
  % 
  \begin{gather*}
    \trans{\polyoutp x {y_1,...,y_n} P} = \outp x {y_1} {... \outp x
      {y_n} {\trans{P}}} \\
    \trans{\polyinp x {y_1,...,y_n} P} = \inp x {y_1} {... \inp x
      {y_n} {\trans{P}}}
  \end{gather*}
  % 
  but this is broken! Can you see why? The right approach is use new
  binding:
  % 
  \begin{gather*}
    \trans{\polyoutp x {y_1,...,y_n} P}
    = \newp z {(\outp x z {\outp z {y_1} {... \outp z {y_n} {\trans{P}}}})} \\
    \trans{\polyinp x {y_1,...,y_n} P}
    = \inp x z {\inp z {y_1} {... \inp z {y_n} {\trans{P}}}}
  \end{gather*}
  % 
  where $z \notin \fn P$ in both cases.  (We also need some
  well-sorted assumptions.)

  \vspring  

\end{slide}

\begin{slide}
  \slidehead{Application of new binding: from synchronous to asynchronous ouput}

  \vspring In distributed computing, sending and receiving messages
  may be asymmetric: we clearly know when we have received a message
  but not necessarily when a message we sent has been
  delivered. (Think of email.)
  % 
  \begin{center}
    \begin{tabular}{>{$}l<{$}@{}>{$}l<{$}!{\qquad}l}
      P ::= {}
      & \outact x y & output \\
      & \inp x y P  & input \tcR{($y$ binds in $P$)}
    \end{tabular}
  \end{center}  
  %

  Nonetheless, one can always achieve synchronous sends by using an
  \emph{acknowledgement} protocol:
  % 
  \begin{gather*}
    \trans{\outp x y P}
    = \newp z {(\polyoutact x {y,z} \parp \polyinp z {} {\trans{P}} )} \\
    \trans{\inp x y P}
    = \polyinp x {y,z} {(\polyoutact z {} \parp \trans{P})}
  \end{gather*}
  %
  provided $z \notin \fn P$ in both cases.

  \vspring

\end{slide}

\begin{slide}
  \slidehead{Labels}

  \vspring

  The labels $\alpha$ are of the form:
  
  \vspring

  \begin{center}
    \begin{tabular}{>{$}l<{$}@{}>{$}l<{$}!{\qquad}l}
      \alpha ::= {}
      & \outlab x y & output \\
      & \boutlab x y & bound output \\
      & \inlab  x y & input \\
      & \tau         & silent \\
    \end{tabular}
  \end{center}    
  
  \vspring  \vspring

  The free names $\fn \alpha$ and bound names $\bn \alpha$ are defined as follows:

  \vspring

  \begin{gather*}
    \begin{array}{r|cccc}
      \alpha &  \outlab x y & \boutlab x y & \inlab x y & \tau \\
      \hline
      \fn \alpha & \{x,y\}   & \{x\}  &  \{x,y\}  & \emptyset \\
      \bn \alpha & \emptyset & \{y\}  & \emptyset & \emptyset 
      \end{array}
  \end{gather*}

  \vspring
\end{slide}

\begin{slide}
  \slidehead{Labelled transitions ($P \red{\alpha} P'$)}

  \vspring

  Labelled transitions are of the form $P \red{\alpha} P'$ and are
  generated by:

  \vspring
  \begingroup
  \sizes

  \begin{gather*}
    \outp x y P \red{\outlab x y} P \quad\maketag{lab-out}
    % 
    \qquad\qquad
    \inp x y P \red{\inlab x z} \sub z y P \quad\maketag{lab-in}
    \\[0 pt plus 1fill]
    % 
    \infer{P \red{\alpha} P'}{P \parp Q \red{\alpha} P' \parp Q}
    \text{if $\bn \alpha \cap \fn Q = \emptyset$} %
    \quad\maketag{lab-par-l}
    \qquad\qquad
    \\[0 pt plus 1fill]
    \infer{P \red{\alpha} P'}{\newp y P \red{\alpha} \newp y P'}
    \text{if $y \notin \fn \alpha \cup \bn \alpha$}
    \quad\maketag{lab-new}
    \qquad\qquad
    % 
    \infer{P \red{\outlab x y} P'}{\newp y P \red{\boutlab x y}  P'}
    \text{if $y \neq x$}
    \quad\maketag{lab-open}    
    \\[0 pt plus 1fill]
    \infer%
    {P \red{\outlab x y} P' \qquad Q \red{\inlab x y} Q'}%
    {P \parp Q \red{\tau} P' \parp Q'} %
    \quad\maketag{lab-comm-l}
    % 
    \qquad
    \infer
    {P \red{\boutlab x y} P' \qquad Q \red{\inlab x y} Q'}%
    {P \parp Q \red{\tau} \newp y{(P' \parp Q')}} %
    \text{if $y \notin \fn Q$}%
    \quad\maketag{lab-close-l}
    \\[0 pt plus 1fill]
    \infer
    {P \parp \bangp P \red{\alpha} P'}{\bangp P \red{\alpha} P'}
    \quad\maketag{lab-bang}
  \end{gather*}
  \endgroup

  \vspring

  plus symmetric rules \maketag{lab-par-r}, \maketag{lab-comm-r},
  \maketag{lab-close-r}.

  \vspring
  
\end{slide}

\begin{slide}
  \slidehead{Labelled transitions and structural congruence}

  \vspring

  \emph{Theorem:}

  \begin{enumerate}
  \item $P \red{} P'$ iff $ P \mathbin{{\red{\tau}}{\streq}} P'$.
  \item $P \mathbin{{\streq}{\red{\alpha}}} P'$ implies  $P \mathbin{{\red{\alpha}{\streq}}} P'$
  \end{enumerate}
    
  \vspring

  \emph{Exercise:} Why does the converse of the second not hold?

  \vspring

  \emph{Exercise:} Show that the following pair of processes are both
  in $(\red{})$ and $(\red{\tau}\streq)$: 
  % 
  \begin{gather*}
    \newp z {\outact x z} \parp \inp x u {\outact y u} %
    \qquad
    \newp z {\outact y z}
  \end{gather*}

  \vspring
  
  \slidehead{Fun with side conditions}

  \emph{Exercise:} Show that the side condition on \maketag{lab-par-l}
  is necessary by considering the process $\newp y {(\outp x y {\inact
      y u}) \parp \outact z v} $ and an alpha variant.

  \vspring


\end{slide}

\begin{slide}
  \slidehead{Strong bisimulation}

  \vspring 

  A relation $\RR$ is a strong bisimulation if for all $(P,Q) \in \RR$
  and $P \red{\alpha} P'$, where \tcR{$\bn \alpha \cap \fn Q = \emptyset$},
  there exists $Q'$ such that $Q \red{\alpha} Q'$ and $(P',Q') \in
  \RR$, and symmetrically.
  
  \vspring

  Strong bisimilarity $\strongbisim$ is the largest strong
  bisimulation.

  \vspring

\end{slide}

\end{document}
