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

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

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

\input{lecture-post}
\newcommand{\dateoflecture}{9 December 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 review: barbed bisimilarity
    
    \vspring

  \item two natural congruences

    \vspring

  \item a family portrait
    
    \vspring

  \item weak barbed congruence and weak labelled bisimilarity correspond

    \vspring

%   \item higher-order \pic
  
%     \vspring
    
%  \item encoding \lac
  \end{itemize}

  \vspring
\end{slide}

\begin{slide}
  \slidehead{Weak barbed bisimulation}

  \vspring

  Recall that a process $P$ has a \myemph{strong barb} $x$, written %
  $P \barb x$ iff there exists $P_0$, $P_1$, and $\yvec$ such that %
  $P \streq \newp {\yvec} {(\outp x u {P_0} \parp P_1)}$ and %
  $x \not\in \yvec$.

  \vspring

  A process $P$ has a \myemph{weak barb} $x$, written %
  $P \wbarb x$ iff there exists $P'$ such that $P \redstar{} P'$ and
  $P' \barb x$.

  \vspring

  A relation $\RR$ is a \myemph{weak barbed bisimulation} if it is
  symmetric and for all $(P,Q) \in \RR$ %
  \begin{itemize}
  \item if $P \red{} P'$, there exists $Q'$
    such that $Q \redstar{} Q'$ and $(P',Q') \in \RR$;

  \item if $P \barb x$ then $Q \wbarb x$.
  \end{itemize}


  \vspring
  \myemph{Weak barbed bisimilarity}, written $\weakbbisim$, is the
  largest such relation.

  \vspring
\end{slide}


\begin{slide}

  \slidehead{Two possible equivalences (non-input congruences)}

  \vspring
  We write ``equivalence'' for ``non input-prefixing congruence''.

  Clearly $\weakbbisim$ isn't an equivalence: %
  $\outact x y \weakbbisim \outact x z$ but %
  $- \parp \inp x u {\outact u w}$ can distinguish them.
  There  are two ways of building an equivalence:

  \vspring

  \begin{itemize}

  \item Close up at the end: \myemph{weak barbed equivalence},
    $\weakbequiv$, is the largest equivalence included in
    $\weakbbisim$.
%
    % exists? yes, take any two congs included in weakbbism RR1 and
    % RR2.  then RR1 cup RR2 is a cong and is included.
%
    Concretely, $P \weakbequiv Q$ iff for all contexts $C \in \EvalCxt$ we have
    $C[P] \weakbbisim C[Q]$. Check!

    % congruence: let P \weakbcong Q. let C. then C[P] \weakbcong C[Q]
    % if for all C', C'CP \weakbcong C'CQ, which follows by the defi
    % of P weakbcong Q.

    % inclusio:. let P weakbcong Q. then by def (taking the empty
    % cxt), P weakbbisim Q.

    % largest: suppose RR is a congruence in weakbbisim. 
    \vspring
    
  \item Close up at every step: \myemph{weak barbed reduction
      equivalence}, $\weakredbequiv$, is the largest relation $\RR$ such
    that $\RR$ is a weak barbed bisimulation and an equivalence.
%    
    Concretely, $\weakredbequiv$ is the largest symmetric relation
    $\RR$ such that for all $(P,Q) \in \RR$,

    \begin{itemize}

    \item if $P \red{} P'$, there exists $Q'$ such that $Q \redstar{}
      Q'$ and $(P',Q') \in \RR$;

    \item if $P \barb x$ then $Q \wbarb x$;

    \item for all $C\in \EvalCxt$, we have $(C[P], C[Q]) \in \RR$.

    \end{itemize}
  
    Check!

  \end{itemize}
  
  \vspring

\end{slide}


\begin{slide}

  \slidehead{An extended family portrait}

  \vspring

%  \sizes
  \begin{center}
  \begin{tabular}{|l|c|c|}
    \hline
    & \multicolumn{2}{|c|}{strong} \\
    & labelled & barbed \\
    \hline
    not an equivalence
    &
    & ``bisimilarity'' $\strongbbisim$
    \\ \hline
    equivalence    
    & ``bisimilarity'' $\strongbisim$ 
    &
    \begin{tabular}{@{}l@{}}
      ``equivalence'' $\strongbequiv$ \\
      ``reduction equivalence'' $\strongredbequiv$ 
    \end{tabular}
    \\ \hline
    congruence
    &  ``full bisimilarity'' $\fullstrongbisim$
    &
    \begin{tabular}{@{}l@{}}
      ``congruence'' $\strongbcong$ \\
      ``reduction congruence'' $\strongredbcong$ 
    \end{tabular}
    \\ \hline \hline
    & \multicolumn{2}{|c|}{weak} \\
    & labelled & barbed \\
    \hline
    not an equivalence
    &
    & ``bisimilarity'' $\weakbbisim$
    \\ \hline
    equivalence    
    & ``bisimilarity'' $\weakbisim$ 
    &
    \begin{tabular}{@{}l@{}}
      ``equivalence'' $\weakbequiv$ \\
      ``reduction equivalence'' $\weakredbequiv$ 
    \end{tabular}
    \\ \hline
    congruence
    &  ``full bisimilarity'' $\fullweakbisim$
    &
    \begin{tabular}{@{}l@{}}
      ``congruence'' $\weakbcong$ \\
      ``reduction congruence'' $\weakredbcong$ 
    \end{tabular}
    \\ \hline
  \end{tabular}
  \end{center}
  \vspring

\end{slide}

\begin{slide}
  \slidehead{A detailed family portrait}
  
  \newcommand{\nofbox}[1]{{#1}}

  \vspring
  \sizes
  \begin{center}
  \begin{tabular}{|l|l|l|l|}
    \hline
    &labelled & \multicolumn{2}{|c|}{barbed}
    \\ \hline
    \begin{tabular}{@{}l@{}}
      not an \\ equivalence
    \end{tabular}
    &
    & \multicolumn{2}{|c|}{%
      \nofbox{%
        \begin{tabular}{@{}l@{}}%
          \tcR{$\weakbbisim$}: largest $\RR$ st\\
          $
          \begin{mygraph}
            !s{2}{1}
            [] ([] {P}="0"    [r] {P'}="1" )
            [d] ([] {Q}="4"   [r] {Q'}="5" )
            % 
            "0" (:@[|1.159pt]"1" ^{} , :@[|1.159pt]@{-}"4"_{\RR})
            "1" (:@[|1.159pt]@{--}"5" ^{\RR})
            "4" (:@[|1.159pt]@{-->}"5" ^{*})        
          \end{mygraph}$
          \\ $P \barb x$ implies $Q \wbarb x$
        \end{tabular}%
      }%
    }
    \\ \hline
    equivalence
    &\nofbox{%
      \begin{tabular}{@{}l@{}}%
        \tcR{$\weakbisim$}: largest $\RR$ st\\
        $\begin{mygraph}
          !s{2}{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" ^{\tau^{*}\hat{\alpha}\tau^{*}})        
        \end{mygraph}$
      \end{tabular}%
    }
    &\nofbox{%
      \begin{tabular}{@{}l@{}}%
        \tcR{$\weakredbequiv$}: largest $\RR$ st\\
          $
          \begin{mygraph}
            !s{2}{1}
            [] ([] {P}="0"    [r] {P'}="1" )
            [d] ([] {Q}="4"   [r] {Q'}="5" )
            % 
            "0" (:@[|1.159pt]"1" ^{} , :@[|1.159pt]@{-}"4"_{\RR})
            "1" (:@[|1.159pt]@{--}"5" ^{\RR})
            "4" (:@[|1.159pt]@{-->}"5" ^{*})        
          \end{mygraph}$
          \\ $P \barb x$ implies $Q \wbarb x$
          \\ $\forall D\in\EvalCxt. (D[P],D[Q]) \in \RR$
      \end{tabular}%
    }      
    &\nofbox{%
      \begin{tabular}{@{}l@{}}%
        \tcR{$\weakbequiv$}: \\
        $\{(P,Q) \setst (\forall D\in\EvalCxt. D[P] \weakbbisim D[Q]\}$
      \end{tabular}%
    }
  \\ \hline
  \end{tabular}
  \end{center}

  \vspring  \vspring

\end{slide}

\begin{slide}
  \slidehead{What's the difference between $\weakredbequiv$ and $\weakbequiv$?}

  \vspring

   \begin{itemize}
    
   \item ${\weakredbequiv} \subseteq {\weakbequiv}$: Yes, trivially.

     \vspring

   \item ${\weakredbequiv} \supseteq {\weakbequiv}$: Not necessarily.

     Two difficult results due to C\'edric Fournet and Georges Gonthier.  ``A
  hierarchy of equivalences for asynchronous cacluli''. ICALP 1998. Journal version: \\
    {\sizess http://research.microsoft.com/$\sim$fournet/papers/a-hierarchy-of-equivalences-for-asynchronous-calculi.pdf}

    \vspring

  \begin{itemize}

  \item In general they're not the same.  $\weakbequiv$ is not
    even guaranteed to be a weak barbed bisimulation:
    \begin{gather*}
      \begin{mygraph}
        !s{1.7}{1.7}
        [] ([] {P}="10"   [r] {C[P]}="0" [r]       [r] {P'}="1" )
        [d] ([] {Q}="14"  [r] {C[Q]}="4" [r]       [r] {Q'}="5" )
        % 
        "10" (:@[|1.159pt]@{-}"14"_{\weakbequiv})
        "0" (:@[|1.159pt]"1" ^{} , :@[|1.159pt]@{-}"4"_{\weakbbisim})
        "1" (:@[|1.159pt]@{--}"5" ^{\weakbbisim})
        "4" (:@[|1.159pt]@{-->}"5" ^{*})        
      \end{mygraph}
    \end{gather*}

    \vspring

  \item But for \pic, they coincide.

  \end{itemize}
  \end{itemize}    

  \vspring 

\end{slide}

\begin{slide}
  \slidehead{Comparing labels and barbs}

  \vspring

  \begin{itemize}
    \item ${\weakbisim} \subseteq {\weakredbequiv}$: Yes, easy.

    \item ${\weakbisim} \supseteq {\weakredbequiv}$: Yes, provided we
      have name matching.  The result is subtle.
  \end{itemize}

  \vspring

\end{slide}

\begin{slide}
  \slidehead{Name matching}

  \vspring

  Motivation: Which context can detect that $P \red{\outlab x y} P'$?
  It's easy to tell $P$ can output on $x$; we just check $P\barb
  x$. If we want to test that this transition leads to $P'$, we
  can take the context %
  $C= -\parp \inp x u {\zinact k} \parp \zoutact k $ for $k$ fresh.
  Now %
    \[C[P] \red{} \red{} P'\] where $P' \nbarb k$.

  \vspring

  But how do we detect that the message is $y$?  We could try %
  \[C= -\parp \inp x u {(\zoutact u \parp \zinp y {\zinact k})} \parp
  \zoutact k\] but this risks having the $\zoutact u$ and the
  $\zinact y$ interact with the process in the hole.

  \vspring

  Thus, we introduce a simple new construct called \myemph{name matching}:
  % 
  \begin{center}
    \begin{tabular}{>{$}l<{$}@{}>{$}l<{$}!{\qquad}l}
      P ::= {}
      & ...  & \\
      & \matchp x y P \\
    \end{tabular}
  \end{center}
  
  \vspring

  Reductions: $\matchp x x P \red{} P$

  \vspring

  Labelled transitions:  $\matchp x x P \red{\tau} P$

  \vspring

\end{slide}

\begin{slide}

  \slidehead{Barbed equivalence is a weak labelled bisimulation}
  
  \vspring
  Theorem: ${\weakbisim} \supseteq {\weakredbequiv}$.

  \vspring
  Proof:   Consider $P \weakredbequiv Q$ and suppose $P \red{\alpha} P'$.
  (For simplicity, ignore structural congruence.)

  \vspring

  \begin{description}
  \item[case $\alpha=\tau$:] Then $P \red{} P'$. By definition, there
    exists $Q'$ such that $Q \redstar{} Q'$ and $P' \weakredbequiv
    Q'$.  Thus $Q \redstar{\tau} Q'$ as desired.

    \vspring

  \item[case $\alpha=\inlab x y$:] Let %
    $C = - \parp \outp x y {\zinact k} \parp \zoutact k$, where $k$ is
    fresh.  Then $C[P] \red{}\red{} P'$. Therefore, there exists $Q$
    such that %
    $C[Q] \redstar{} Q'$ and $P' \weakredbequiv Q'$.  Since $P'
    \nwbarb k$, we have $Q' \nwbarb k$, therefore %
    $Q \redstar{\tau}\red{\inlab x y}\redstar{\tau} Q'$, as desired.

  \end{description}

  \vspring

\end{slide}

\newcommand{\myanswer}[1]{#1}

\begin{slide}

  \vspring

  \begin{description}
  \item[case $\alpha=\outlab x y$:] Let %
    $C=-\parp \inp x u {\matchp u y {\zinact k}} \parp \zoutact k$,
    where $k$ is fresh. Then $C[P] \red{}\red{}\red{} P'$.  Therefore,
    there exists $Q$ such that $C[Q] \redstar{} Q'$ and $P'
    \weakredbequiv Q'$.  Since $P' \nwbarb k$, we have $Q' \nwbarb k$,
    therefore %
    $Q \redstar{\tau}\red{\outlab x y}\redstar{\tau} Q'$, as desired.

    \vspring

  \item[case $\alpha=\boutlab x y$ and $y \notin \fn Q$:] Let %
    \[\textstyle C=-\parp \inp x u {\left(\outact z u \parp \zinact k
        \parp \prod _{w \in \fn P} \matchp u w {\zoutact k}\right)}
    \parp \zoutact k\]
    where $k$ and $z$ are fresh.
    % 
    Then $C[P] \red{}\red{} H_{z,y}[P']$ where %
    \[H_{z,y} = \newp y {(\outact z y \parp -)}\] %
    Therefore, there exists $Q''$ such that $C[Q] \redstar{} Q''$ and
    $H_{z,y}[P'] \weakredbequiv Q''$.  Since $H_{z,y}[P'] \nwbarb k$, we have
    $Q'' \nwbarb k$.  Thus there exists $Q'$ such that $Q'' \streq
    C'[Q']$ and $Q \redstar{\tau}\red{\boutlab x y} \redstar{\tau} Q'$.
    Do we know $P' \weakredbequiv Q'$?

  \end{description}
  
  \vspring

\end{slide}

  \slidehead{Exercises for next lecture}
  
  \begin{enumerate}
  \item Since the last lecture, the proof has been fixed by using
    $\nwbarb k$ everywhere.  Prove from the definition of
    $\weakredbequiv$ that for $P\weakredbequiv Q$ if $P \wbarb x$
    then $Q \wbarb x$, and thus the contrapositive: if $Q \nwbarb x$
    then $P \nwbarb x$.

    \myanswer{ \sizess Answer: %
      Suppose $P \weakredbequiv Q$. If $P \wbarb x$ then there exists
      $P'$ such that $P \redstar{} P'$ and $P' \barb x$.  Thus there
      exists $Q'$ such that $Q \redstar{} Q'$ and $P' \weakredbequiv
      Q'$. Since $P' \barb x$, we have $Q'\wbarb x$.  Hence there
      exists $Q''$ such that $Q' \redstar{} Q''$ and $Q''\barb x$.
      Thus $Q\wbarb x$, as desired.  }

    \newpage

  \item The last case of the proof relies on the following lemma:
    $H_{z,y}[P] \weakredbequiv H_{z,y}[Q]$ implies $P  \weakredbequiv
    Q$, where $z \notin {\fn P} \cup {\fn Q}$.  In the updated version of
    the proof you will find the definition %
    $H_{z,y} = \newp y {(\outact z y \parp -)}$. %
      
    Hints...

    In order to prove this, consider \[\RR = \{(P,Q) \setst z \notin
    {\fn P} \cup {\fn Q} \text{~and~} H_{z,y}[P] \weakredbequiv H_{z,y}[Q]
    \}\text{.}\] Our goal (as usual) is to prove that $\RR$ satisfies
    the same properties as $\weakredbequiv$, and thus deduce that $\RR
    \subseteq {\weakredbequiv}$. Assume $(P,Q) \in \RR$.

    \begin{itemize}
    \item \myemph{$\RR$ is a bisimulation}: Show that $P \red{} P'$
      implies that there exists $Q'$ such that $Q \redstar{} Q'$ and
      $(P',Q') \in \RR$.

      \myanswer{\sizess Answer: %
        Suppose $P \red{} P'$. Since $H_{z,y}$ is an evaluation
        context, $H_{z,y}[P] \red{} H_{z,y}[P']$. Since $H_{z,y}[P]
        \weakredbequiv H_{z,y}[Q]$, there exists $Q''$ such that %
        $H_{z,y}[Q] \redstar{} Q''$ and %
        $H_{z,y}[P'] \weakredbequiv Q''$.  Since %
        $z \notin \fn Q$, these reductions could not be due to any
        interaction between $H_{z,y}$ and $Q$, nor can $H_{z,y}$
        itself reduce, thus there exists $Q'$ such that $Q \redstar{}
        Q'$ and $Q'' \streq H_{z,y}[Q']$. Thus (ignoring structural
        congruence), $(P',Q') \in \RR$, as desired.}

      \item \myemph{$\RR$ preserves barbs}: Show that $P \barb w$
        implies $Q \wbarb w$.

        \myanswer{\sizess Answer: %
          Suppose $P \barb w$.  Since $z \notin \fn P$, we know that
          $w \neq z$. We distinguish two cases.

          \begin{description} 
          \item[case $w \neq y$:] We have $P\barb w$ implies %
            $H_{z,y}[P] \barb w$. Since %
            $H_{z,y}[P] \weakredbequiv H_{z,y}[Q]$, we have %
            $H_{z,y}[Q] \wbarb w$. Since there is no interaction
            between $H_{z,y}$ and $Q$ and the former can't be
            responsible for the barb because $w \neq z$, we have $Q
            \wbarb w$, as desired.

          \item[case $w = y$:] We don't have $H_{z,y}[P] \barb w$
            since the new binder in $H_{z,y}$ prevents the $w$ from
            being seen.  However, we can let %
            $C = \inp z u {\inp u v {\zoutact k }} \parp -$ where
            $u,k$ are fresh. By extrusion we can see %
            $C[H_{z,y}[P]] \wbarb k$. Since %
            $H_{z,y}[P] \weakredbequiv H_{z,y}[Q]$, we have
            $C[H_{z,y}[P]] \weakredbequiv C[H_{z,y}[Q]]$, thus
            $C[H_{z,y}[Q]] \wbarb k$. The only way this can be is if
            $Q\wbarb w$, as desired.
          \end{description}
        }

      \item \myemph{$\RR$ is an equivalence}: It is sufficient to show
        that $(C[P],C[Q]) \in \RR$ where %
        $C = \newp {\wvec} {(- \parp S)}$. Hint: try to find a context
        $C'$ such that $H_{z,y}[C[P]] \weakredbequiv C'[H_{z,y}[P]]$
        and the same for $Q$ (perhaps using a labelled bisimilarity
        since we know ${\weakbisim} \subseteq {\weakredbequiv}$).  You
        may have to distinguish between the cases $y \in \wvec$ and
        $y \notin \wvec$.

        \myanswer{ \sizess %
          Answer: We distinguish two cases:

          \begin{description}
          \item[case $y \in \wvec$:]
            We have that 

          \item[case $y \notin \wvec$:]
          \end{description}
          
        }
    \end{itemize}
    
  \end{enumerate}


% higher order?
% lambda calculus?
% ambients
% join patterns
% nomadic pict (location dependent comm)
% real issues: location dependence, failure, type compatability,
%           blocking system calls
% wanted: dea intern; transactions to acute

% \begin{slide}
%   \slidehead{A family portrait (strong)}

%   \vspring

%   \begin{tabular}{|l|l|}
%     \hline
%     strong bisimilarity ($\strongbisim$): largest s.t.\\
%     $\begin{mygraph}
%       !s{1.8}{1.8}
%       [] ([] {P}="0" [r]       [r] {P'}="1"  )
%       [d] ([] {Q}="4" [r]       [r] {Q'}="5"  )
%       % 
%       "0" (:@[|1.159pt]"1" ^{\alpha} , :@[|1.159pt]@{-}"4"_{\strongbisim})
%       "1" (:@[|1.159pt]@{--}"5" ^{\strongbisim})
%       "4" (:@[|1.159pt]@{-->}"5" ^{\alpha})        
%     \end{mygraph}$ &
%     strong barbed equivalence ($\strongbequiv$) \\

%   \end{tabular}

%   \vspring

% \end{slide}

\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:
