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

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

\begin{document}
\input{common-post}

\input{lecture-post}
\newcommand{\dateoflecture}{25 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{Today's plan}

  \vspring

  \begin{itemize}
  \item exercises from last week

  \vspring

  \item data structures

  \vspring

  \item coding definitions in terms of replication

  \vspring

  \item bisimulation theorems

  \end{itemize}

  \vspring
\end{slide}

\begin{slide}
  \slidehead{Adding sum}

  \vspring

  \begin{center}
    \begin{tabular}{>{$}l<{$}@{}>{$}l<{$}!{\qquad}l}
      P ::= {}
      & M & sum \\
      & P \parp P   & parallel (par) \\
      & \newp x P   & restriction (new)  \text{($x$ binds in $P$)} \\
      & \bangp P    & replication (bang) \\
      M ::= {}
      & \outp x y P & output \\
      & \inp x y P  & input \text{($y$ binds in $P$)} \\
      & M + M & sum \\
      & \zerop
    \end{tabular}
  \end{center}

  \vspring

  Changes:
  \begin{itemize}
  \item structural congruence: $+$ is associative and
    commutative with identity $\zerop$.
    
  \item reduction: $(\outp x y P + M) \parp (\inp x u Q + N)
    \red{} P \parp \sub u y Q$.

  \item labelled transition:
    $ M + \outp x y P + N \red{\outlab x y} P $ \\
    $ M + \inp x y P + N \red{\inlab x z} \sub y z P$
  \end{itemize}

  \vspring

\end{slide}

\begin{slide}
  \slidehead{Process abstractions}

  \vspring

  We don't need CCS-style ``definitions'' for infinite behaviour since
  we have replication, $\bangp P$, as shown later. Nonetheless, they
  are convenient.  In \pic, we call them \myemph{process
    abstractions}:
  % 
  \begin{gather*}
    F = \pabs {u_1, ..., u_k} P
  \end{gather*}
  Instantiation takes an abstraction and a vector of names and gives
  back a process:
  \begin{gather*}
    \pconcr F {x_1, ..., x_k} = \multisub{\sublet{x_1}{u_1},...,\sublet{x_k}{u_k}} P
  \end{gather*}

  \vspring

\end{slide}


\begin{slide}
  \slidehead{Booleans}

  \vspring
  In Ocaml,

\begin{alltt}
type bool = True | False;;
let cases b t f = match b with True -> t | False -> f;;
let not b = cases b False True;;
\end{alltt}

  In \pic,
  \begin{align*}
    \PTrue  &= \pabs l {\polyinp l {t,f} {\zoutact t }} \\
    \PFalse &= \pabs l {\polyinp l {t,f} {\zoutact f }} \\
     \Pboolcases P Q &= \pabs l {
       \newp t {\newp f {\polyoutp l {t,f}
           {(\zinp t P + \zinp f Q)}}}} \\
     \Pnot &= \pabs {l,k} {\pconcr {\Pboolcases {\pconcr \PFalse k} {\pconcr \PTrue k}} l}
  \end{align*}
  Example: show that
  \vspring
  \begin{gather*}
    \newp l {(\pconcr \PTrue l \parp \pconcr \Pnot {l,k})} \redstar{}
    \pconcr \PFalse k
  \end{gather*}

  \vspring

\end{slide}


\begin{slide}
  \slidehead{From linear to replicated data}

  \vspring

  Can we reuse a boolean? No...

  \vspring
  Example: show that we don't have
  \begin{gather*}
    \newp l {(\pconcr \PTrue l \parp \pconcr \Pnot {l, k_0} \parp
      \pconcr \Pnot {l,k_1})}
    \redstar{} \pconcr \PFalse {k_0} \parp \pconcr \PFalse {k_1}
  \end{gather*}

  \vspring

  Why? After we use $\pconcr \PTrue l$ once, we ``exhaust'' it. The solution is
  to use replication:

  \begin{align*}
    \PTruebang &= \pabs l {\bangp {\polyinp l {t,f} {\zoutact t }}} \\
    \PFalsebang &= \pabs l {\bangp {\polyinp l {t,f} {\zoutact f }}}
  \end{align*}

  \vspring

\end{slide}


\begin{slide}
  \slidehead{Lists}

  \vspring

  In Ocaml,

\begin{alltt}
type 'a list = Nil | Cons of 'a * 'a list;;
let cases xs n c =
  match xs with Nil -> n | Cons (y, ys) -> c y ys;;
\end{alltt}

  In \pic,
  % 
  \begin{align*}
    \PNil &= \pabs l {\bangp {\polyinp l {n,c} {\zoutact n}}} \\
    \PCons H T &= \pabs l {
      \newp {h,t} {(
        \bangp {\polyinp l {n,c} {\polyoutact c {h,t}}}
        \parp \pconcr H h 
        \parp \pconcr T t %
        )}}
    \\
    \Plistcases P F &= \pabs l {
      \newp {n,c} {(\polyoutact l {n,c} \parp (\zinp n P + \polyinp c
        {h,t} {\pconcr F {h,t}} ) })}
   \\
    \Plistcopy & = \pabs {l,m} {
      \Plistcasesmlconcr
      {\pconcr \PNil m}
      {\pabs {h,t} {
          \newp {t'} {(
            \bangp {\polyinp m {n,c} { \polyoutact c {h, t'} }}
            \parp \pconcr \Plistcopy {t,t'} 
          }
          )}}
      l
    }
  \end{align*}

  \vspring

  Example: show that for all lists $L$ made from $\PNil$ and $\PCons
  {-} {-}$, %CHECK
  % 
  \begin{gather*}
    \newp l (\pconcr L l \parp \pconcr \Plistcopy {l,m}) \weakbisim %
    \pconcr L m 
  \end{gather*}
  % 
  Note that it's cheating to use $\Plistcopy$ recursively...

  \vspring
\end{slide}

\begin{slide}
  \slidehead{Interlude: encoding recursive definitions in terms of
    replication}

  \vspring 

  Consider the recursive abstraction (``definition'' in CCS):
  % 
  \begin{gather*}
    F = \pabs {\xvec} P
  \end{gather*}
  % 
  where $P$ may well contain recursive calls to $F$ of the form
  $\pconcr F {\zvec}$.

  \vspring

  We can replace the RHS with the following process abstraction
  containing no mention of $F$:
  \begin{gather*}
    \pabs {\xvec} {\newp f {(\polyoutact f {\xvec} \parp \bangp {\polyinp f {\xvec} {\sub
            {\zoutact f} {F} P}})}}
  \end{gather*}
  provided that $f$ is fresh.
  \vspring

  Example: compare the transitions of $\pconcr F {u,v}$, where $F = \pabs
  {x,y} {\outp x y  {\pconcr F {y,x}}}$ to those of its encoding.
  Notice the extra $\tau$ steps. %CHECK

  \vspring
  
\end{slide}


\begin{slide}
  \slidehead{List append}
  
  \vspring

\begin{alltt}
let rec append xs zs =
  cases xs zs (fun y -> fun ys -> Cons(y, append ys zs));;
\end{alltt}

  \vspring

  \begin{gather*}
    \Plistappend  = \pabs {k,l,m} {
      \Plistcasesmlconcr
       {\pconcr \Plistcopy {l,m}}
       {\pabs {h,t} {
           \newp {t'} {(
             \bangp {\polyinp m {n,c} { \polyoutact c {h, t'} }}
             \parp \pconcr \Plistappend {t,l,t'} 
           }
           )}
       }
      k}
  \end{gather*}

  \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 $\bn \alpha \cap \fn Q = \emptyset$,
  there exists $Q'$ such that $Q \red{\alpha} Q'$ and $(P',Q') \in
  \RR$, and symmetrically.
  
  \vspring


   \begin{gather*}
     \begin{mygraph}
      !s{3}{1}
       [] ([] {P}="0"        [r] {P'}="1" )
      [d] ([] {Q}="4"        [r] {Q'}="5" )
      % 
      "0" (:@[|1.159pt]"1" ^{\alpha} , :@[|1.159pt]@{-}"4"_{\RR})
      "1" (:@[|1.159pt]@{--}"5" ^{\RR})
      "4" (:@[|1.159pt]@{-->}"5" ^{\alpha})        
     \end{mygraph}
  \end{gather*}

  \vspring

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

  \vspring

\end{slide}

\begin{slide}
  \slidehead{Bisimulation proofs}

  \vspring

  \emph{Theorem:} $P \streq Q$ implies $P \strongbisim Q$.

  \vspring

  Can you think of a counterexample to the converse?
  
  \vspring
  \vspring

  Some easy results:

  \vspring

  \begin{enumerate}
  \item $P \parp \zerop \strongbisim P$

  \item $\outp x y {\newp z P} \strongbisim \newp z {\outp x y P}$, if $z
    \notin \{x,y\}$
    %CHECK

  \item $\inp x y {\newp z P} \strongbisim \newp z {\inp x y P}$, if $z
    \notin \{x,y\}$
    %CHECK

  \item $\bangp {\newp z P} \notstrongbisim \newp z {\bangp P}$ for some $P$
    %CHECK
    %

  \end{enumerate}
  
  \vspring  \vspring

  More difficult:

  \vspring

  \begin{enumerate}
  \item $\newp x P \parp Q \strongbisim \newp x {(P\parp Q)}$, for $x
    \notin  \fn Q$
  \item $P \strongbisim Q$ implies $P \parp S \strongbisim Q \parp S$
  \item $\bangp P \parp \bangp P \strongbisim \bangp P$
  \item $\bangp {\bangp P} \strongbisim \bangp P$

  \end{enumerate}

  \vspring

\end{slide}

\begin{slide}
  \slidehead{Congruence with respect to parallel}

  \vspring

  Theorem: $P \strongbisim Q$ implies %
  $P \parp S \strongbisim Q \parp S$

  \vspring

  Proof: Consider $\RR = \{ (P \parp S, Q \parp S) \setst P
  \strongbisim Q \}$. If we can show $\RR \subseteq {\strongbisim}$
  then we're done: if $P \strongbisim Q$, then $(P \parp S,  Q \parp
  S) \in \RR$, thus $P \parp S \strongbisim Q \parp S$.

  \vspring

  Claim: $\RR$ is a bisimulation. Suppose $P \strongbisim Q$ and $P
  \parp S \red{\alpha} P_0$, where $\bn \alpha  \cap \fn {Q \parp S} =
  \emptyset$.

  \vspring

  What are the cases to consider?

  \vspring

\end{slide}

\newcommand{\trickycongcase}{%
  $P \red{\inlab x y} P'$ and %
  $S \red{\boutlab x y} S'$ and %
  $P_0 = \newp y {(P' \parp S')}$ and %
  $\alpha = \tau$ and %
  $y \notin \fn P$}

\begin{slide}

  \slidehead{Congruence with respect to parallel: case analysis}

  \vspring

  $P$ is solely responsible:
  % 
  \begin{itemize}
  \item $P \red{\alpha} P'$ and $P_0 = P' \parp S$ and %
    $\bn \alpha \cap \fn S = \emptyset$
  \end{itemize}
  
  \vspring

  $S$ is solely responsible:
  % 
  \begin{itemize}
  \item $S \red{\alpha} S'$ and $P_0 = P \parp S'$ and %
    $\bn \alpha \cap \fn P = \emptyset$
  \end{itemize}
  
  \vspring

  $P$ and $S$ are jointly responsible:
  \begin{itemize}
  \item $P \red{\outlab x y} P'$ and $S \red{\inlab x y} S'$
    and $P_0 = P' \parp S'$ and $\alpha = \tau$
  \item $P \red{\inlab x y} P'$ and $S \red{\outlab x y} S'$
    and $P_0 = P' \parp S'$ and $\alpha = \tau$
  \item $P \red{\boutlab x y} P'$ and $S \red{\inlab x y} S'$ and $P_0
    = \newp y {(P' \parp S')}$ and $\alpha = \tau$ %
    and $y \notin \fn S$
  \item \trickycongcase: careful!
  \end{itemize}
  
  \vspring

\end{slide}

\begin{slide}
  \slidehead{Congruence with respect to parallel: the tricky case}

  \vspring

  Case: \trickycongcase.   The following lemmas can help:
  \begin{enumerate}
  \item If $P \red{\inlab x y} P'$ and $y \notin \fn P$ then %
    $P \red{\inlab x {y'}} \sub {y'} y P'$.

  \item If $S \red{\boutlab x y} S'$ and $y' \notin \fn S$ then %
    $S \red{\boutlab x {y'}} \sub {y'} y S'$.
  \end{enumerate}
  
  \vspring

  Now,  \tcR{let $y'$ be fresh}. We can apply both lemmas. %
  By alpha-conversion, $P_0 = \newp {y'} {(\sub {y'} y P' \parp
    \sub {y'} y S')}$

  \vspring

  Since $P \strongbisim Q$, there exists $Q''$ such that $Q
  \red{\inlab x {y'}} Q''$ and $\sub {y'} y P' \strongbisim Q''$.
  \tcR{Since $y'$ is fresh,}
  % 
  \begin{gather*}
    Q \parp S \red{\tau} \newp {y'} {(Q'' \parp \sub {y'} y S')}
  \end{gather*}

  \vspring

  Our bisimulation isn't big enough! Take instead: %
  %
  \begin{gather*}
    \RR = \{ %
    (\newp {\zvec} {(P \parp S)}, %
    \newp {\zvec} {(Q \parp S)}) %
    \setst P \strongbisim Q \}
  \end{gather*}
\vspring

\end{slide}

\slidehead{Exercises for next lecture}

\vspring

\begin{enumerate}
  
\item I gave an imprecise argument that $\bangp {\newp z P}
  \strongbisim \newp z {\bangp P}$ is not generally true.

  \begin{enumerate}
    
  \item Make the argument precise by giving a concrete process $P$
    and a sequence of labelled transitions showing that bisimulation
    doesn't hold.
    
    % Answer: Take P = x-z | z-.  Then
    % !new z.P -{x-z}-> z- | !new z.P which is only able to output
    % on z once.  The other can output twice.
    
  \item Let us say that a process $Q$ \myemph{has a weak barb} $b$,
    written $Q \wbarb b$ if $Q$ is eventually able to output on $b$,
    \ie there exists $Q_0$, $Q_1$, and $\yvec$ such that $Q \redstar{}
    \newp {\yvec} {(\outp b u {Q_0} \parp Q_1)}$ with $b \notin
    \yvec$.

    Find a context $C$ that can distinguish the two processes above,
    \ie such that $C[\newp z {\bangp P}] \wbarb b$ but not $C[\bangp
    {\newp z P}] \wbarb b$.

    % C = - | x(z).(z-.z-.b-)
    
  \item Give an example of a general class of processes $P$ for which
    the bisimulation would hold?

    % Answer: z \notin \fn P
  \end{enumerate}

\vspring
\newpage

\item Recall the encoding of recursive abstractions in terms of
  replication.

  \begin{enumerate}

  \item  Write the process $\pconcr F {x,y}$ in terms of replication,
    where the abstraction $F$ is defined as follows:
  % 
    \begin{gather*}
      F = \pabs {u,v} {\zinp u {\pconcr F {u,v}}}
    \end{gather*}
 
  \item Consider the pair of mutually recursive definition
    %
    \begin{gather*}
      G = \pabs {u,v} {(\zinp u {\pconcr H {u,v}}  \parp \zinp k {\pconcr H {u,v}})} \\
      H = \pabs {u,v} {\zinp v {\pconcr G {u,v}}} 
    \end{gather*}
    Write the process $\pconcr G {x,y}$ in terms of replication.
    (Note that we didn't discuss the coding of mutually recursive
    definitions so you have to invent the technique yourself!)
  \end{enumerate}

\newpage

\item Help the lecturer to get his lists right! Fix my broken result
  about lists (corrected in the slides) by showing:
    \begin{gather*}
      \newp l (\pconcr L l \parp \pconcr \Plistcopy {l,m}) \weakbisim %
      \pconcr L m 
    \end{gather*}

\item Write a process abstraction $\Plistrev$ such that %
  $\pconcr \Plistrev {l,m}$ takes the list located at $l$ and produces
  a new list at $m$ with the elements reversed.  It may help to
  consider the definition of \texttt{rev} (and that of the auxiliary
  function \texttt{rev'}) in Ocaml:
  % 
\begin{alltt}
let rec rev' xs ys =
  match ys with Nil -> xs
      | Cons (z,zs) -> rev' (Cons (z,xs)) zs;;
let rev ys = rev' Nil ys;;
\end{alltt}

\newpage

\item Prove $\bangp P \parp \bangp P \strongbisim \bangp P$.  To make
  the problem easier, replace the labelled transition rule for
  replication by the following ones that make the analysis much
  easier:

  \begin{gather*}
    \infer
    {P \red{\alpha} P'}{\bangp P \red{\alpha} P' \parp \bangp P}%
    \text{if $\bn \alpha \cap \fn P = \emptyset$}
    \quad\maketag{lab-bang-simple}
    \\[0 pt plus 1fill]
    \infer
    {P \red{\outlab x y } P' \qquad P \red{\inlab x y } P''}%
    {\bangp P \red{\tau} (P' \parp P'') \parp \bangp P}
    \quad\maketag{lab-bang-comm}
    \\[0 pt plus 1fill]
    \infer{P \red{\boutlab x y } P' \qquad P \red{\inlab x y } P''}%
    {\bangp P \red{\tau} \newp y {(P' \parp P'')} \parp \bangp P}%
    \text{if $y \notin \fn P$}
    \quad\maketag{lab-bang-close}
  \end{gather*}

  Furthermore, feel free to use structural congruence (\eg %
  $\bangp P \streq P \parp \bangp P$) instead of process equality
  anywhere you need it in the proof.

\end{enumerate}

\end{document}

%% Local IspellDict: british

%% Local Variables:
%% time-stamp-line-limit: 100
%% time-stamp-format: "%04Y/%02m/%02d %02H:%02M:%02S %u"
%% time-stamp-time-zone: "GMT"
%% End:
