\documentclass[11pt]{article}
%\usepackage{times}
\usepackage{amsmath}
\usepackage{array}



%\definecolor{darkyellow}{rgb}{1, 0.9, 0}


\newif\ifsolutions
\solutionstrue
%will be made false in the version without solutions

\ifsolutions
\newcommand{\solution}[1]{%
%  \psframebox*[fillcolor=darkyellow,linestyle=none]{%
  \begin{quote}%
    \textbf{Solution:}\ %
    #1%
  \end{quote}%
%}%
}
\else
\newcommand{\solution}[1]{}
\fi

\newcommand{\qhard}{\fbox{${*}{*}{*}$}\xspace}
\newcommand{\qmed}{\fbox{${*}{*}\phantom{*}$}\xspace}
\newcommand{\qeasy}{\fbox{${*}\phantom{*}\phantom{*}$}\xspace}

\newif\ifslidegeometry
\slidegeometryfalse
\input{../../pi/common.tex}
\let\redar=\red
\renewcommand{\sublab}{}
\newcommand{\sizes}{\small}

\usepackage{pstricks,pst-node}

%\usepackage{color}
%\usepackage{graphicx}
%\newcommand{\dotdia}[1]{\begingroup\input{#1.tex}\input{#1.pstex_t}\endgroup}

\usepackage{geometry}
\usepackage{fancyhdr}

\geometry{
  dvips,  
  a4paper,
  left=20mm, right=20mm,
  top=8mm, bottom=8mm,
  headheight=10mm, headsep=10mm,
  footskip=10mm
}

\renewcommand{\headrulewidth}{0mm}
\renewcommand{\footrulewidth}{0mm}
\lhead{}
\chead{}
\rhead{}
\lfoot{}
\cfoot{\thepage}
\rfoot{}
\pagestyle{fancy}
\setlength{\parskip}{1pt}

\begin{document}
\begin{center}
\Large
MPRI Concurrency (Cours 2-3) \\
Final exam, 2005-2006 \\
22 Feb 2006, 16.15--19.15 \\
James.Leifer@inria.fr \\
\end{center}

\psset{linecolor=darkgray,linewidth=0.5pt}


\emph{Question annotations:} \qeasy = easy; \qmed = medium; \qhard = hard

\begin{enumerate}
\item  Consider the term
  %
  $P =
  \newpp y {\inp x x {\inp x x {\outact x y }} }
  \parp
  \newpp y {\outp x y {\newpp x {\outp y x {\inact x x}}}}$ with
  $x \neq y$.

  \begin{enumerate}
  \item \qeasy What is the set of free names of $P$?
    \solution{%
      $\{x\}$.
    }
    
  \item \qeasy Define a process $P'$ that is $\alpha$-equivalent to $P$ and
    has all bound names distinct from each other and from all free
    names.
    \solution{%
      $P'=
      \newpp {\rnode[bc]{y1}{y_1}}
      {\inp x {\rnode[bc]{x1}{x_1}}
        {\inp {\rnode[bc]{x11}{x_1}} {\rnode[bc]{x2}{x_2}}
          {\outact {\rnode[bc]{x21}{x_2}}{\rnode[bc]{y11}{y_1}} }} }
      \parp
      \newpp {\rnode[bc]{y2}{y_2}}
      {\outp x {\rnode[bc]{y21}{y_2}} 
        {\newpp {\rnode[bc]{x3}{x_3}} 
          {\outp {\rnode[bc]{y22}{y_2}} {\rnode[bc]{x31}{x_3}}
            {\inact {\rnode[bc]{x32}{x_3}} {\rnode[bc]{x4}{x_4}}}}}}$\rnode[bc]{nil}{}.
      \nccurve[angleA=-30,angleB=-120]{->}{y1}{y11}
      \nccurve[angleA=-30,angleB=-120]{->}{x1}{x11}
      \nccurve[angleA=-30,angleB=-120]{->}{x2}{x21}
      \nccurve[angleA=-30,angleB=-120]{->}{y2}{y21}
      \nccurve[angleA=-30,angleB=-120]{->}{y2}{y22}
      \nccurve[angleA=-30,angleB=-120]{->}{x3}{x31}
      \nccurve[angleA=-30,angleB=-120]{->}{x3}{x32}
%      \nccurve[angleA=-30,angleB=-120]{->}{x4}{nil}
      \vspace*{4ex}
    }

  \item \qeasy What is the set of free names of $P'$?
    \solution{%
      $\{x\}$, since $\alpha$-conversion doesn't change the free names.
    }

  \item \qmed Show the sequence of three reduction steps ($\redar{}$) starting
    at $P'$, taking care to make explicit any scope
    extrusions you need (\ie use of \citetag{str-ex} in $\streq$).
    \solution{%
      \begin{mulprf}
        &P'\\
        \streq &
        \newpp {y_1,y_2} {\inp x {x_1} {\inp {x_1} {x_2}
            {\outact {x_2} {y_1} }}
          \parp
          \outp x {y_2} {\newpp {x_3} {\outp {y_2} {x_3} {\inact {x_3}
                {x_4}}}}}
        & extrusion of $y_2$
        \\
        \redar{}&
        \newpp {y_1,y_2} {\inp {y_2} {x_2}
            {\outact {x_2} {y_1} }
          \parp
          \newpp {x_3} {\outp {y_2} {x_3} {\inact {x_3} {x_4}}}}
        &communication on $x$
        \\
        \streq&
        \newpp {y_1,y_2,x_3} {\inp {y_2} {x_2}
            {\outact {x_2} {y_1} }
          \parp
          \outp {y_2} {x_3} {\inact {x_3} {x_4}}} & extrusion of $x_3$
        \\
        \redar{}&
        \newpp {y_1,y_2,x_3} { \outact {x_3} {y_1}
          \parp
          \inact {x_3} {x_4}} &communication on $y_2$
        \\
        \redar{}&
        \newpp {y_1,y_2,x_3} { \zerop \parp \zerop } &communication on $x_3$
      \end{mulprf}
    }

  \end{enumerate}
  
\item This question explores the relationship between name hiding and
  bisimulation in the core \pic{} (\ie the calculus on slide 3 with no
  extra features).

  \begin{enumerate}
  \item \qhard Prove that strong bisimilarity is closed by
  new binding, \ie $P \strongbisim Q$ implies %
  $\newp x P \strongbisim \newp x Q$.  You may only use the basic
  definitions of bisimulation and labelled transition (no ``up to''
  techniques).

  Hint: start with a relation %
  $\RR=\{ (\newp x P, \newp x Q ) \setst P \strongbisim Q \}$
  % 
  and try to show that $\RR$ is a strong bisimulation.  You may have
  to add some more pairs to $\RR$.

  \solution{%
    Take $\RR'=\RR \cup (\strongbisim)$. We aim to show that $\RR'$ is a
    bisimulation.  To do that we need to consider $(P_0,Q_0) \in
    \RR'$ and $P_0 \redar{\alpha} P'_0$ with %
    $\bn \alpha \cap \fn{Q_0} = \emptyset$.
    We distinguish two cases.

    \begin{description}
    \item[Case $P_0 \strongbisim Q_0$:] By definition of
      $\strongbisim$, there exists $Q'_0$ such that $Q_0 \redar{\alpha}
      Q'_0$ and $P'_0 \strongbisim Q'_0$, hence %
      $(P'_0,Q'_0) \in \RR'$, as desired.

    \item[Case $(P_0,Q_0) \in \RR$:] Then there exists $P$ and $Q$
      such that $P \strongbisim Q$ and %
      $P_0 = \newp x P$ and $Q_0 = \newp x Q$. We consider the two
      possible ways that the labelled transition %
      $P_0 \redar{\alpha} P'_0$ could have been derived.

      \begin{description}
      \item[Case \citetag{lab-new}:] Then there exists $P'$ such that
        $P \redar{\alpha} P'$ and $P'_0 = \newp x P'$ and %
        $x \notin \bn \alpha$.  By hypothesis, we also have %
        $\bn \alpha \cap \fn{Q_0} = \emptyset$, hence %
        $\bn \alpha \cap \fn Q = \emptyset$, thus it is safe to apply
        the definition of bisimulation to the hypothesis %
        $P \strongbisim Q$; hence there exists $Q'$ such that %
        $Q \redar{\alpha} Q'$ and $P' \strongbisim Q'$.  Let %
        $Q'_0=\newp x Q'$. Then by \citetag{lab-new}, %
        $Q_0 \redar{\alpha} Q'_0$. Finally, %
        $(P'_0,Q'_0) \in \RR \subseteq \RR'$, as desired.

      \item[Case \citetag{lab-open}:] Then there exists $P'$ and $w$
        such that $P \redar{\outlab w x} P'$ and $w \neq x$ and %
        $P'_0 = P'$ and $\alpha = \boutlab w x$. By hypothesis, %
        $P \strongbisim Q$, so there exists $Q'$ such that %
        $Q \redar{\outlab w x} Q'$ and $P' \strongbisim Q'$. Let %
        $Q'_0 = Q'$. By \citetag{lab-open}, $Q_0 \redar{\alpha} Q'_0$.
        Finally, $(P'_0,Q'_0) \in (\strongbisim) \subseteq \RR'$, as
        desired.
      \end{description}
    \end{description}

    Since $\RR'$ is a symmetric relation, we conclude that it is a
    bisimulation.  Hence for any $P \strongbisim Q$, we have %
    $(\newp x P,\newp x Q) \in \RR' \subseteq (\strongbisim)$, which
    completes the proof.
  }
  
\item \qeasy Give a counterexample to show that the converse is false, \ie
  $\newp x P \strongbisim \newp x Q$ does not imply %
  $P \strongbisim Q$.
  \solution{%
    Take $P=\outlab x y$ and $Q=\zerop$ with $x,y$ distinct.  Then
    $\newp x P \strongbisim \newp x Q$ since both sides are
    deadlocked. However $P \notstrongbisim Q$ since $P$ has the
    labelled transition $P \redar{\outlab x y}$ but $Q$ does not.
  }

\item \qmed However if we hide \emph{and then reveal} a name, then it is as
  if we never hid it!  Prove that %
  $\newpp x {\outact k x \parp P} %
  \strongbisim %
  \newpp x {\outact k x \parp Q}$ implies %
  $P \strongbisim Q$ for $k\notin \fn P \cup \fn Q \cup \{x\}$.

  Hint: There is no need to explicitly construct a bisimulation relation
  containing $(P,Q)$.  Instead consider the $\boutlab k x$ labelled
  transitions of %
  $\newpp x {\outact k x \parp P}$ and %
  $\newpp x {\outact k x \parp Q}$.  Take care to clearly write out
  any proof trees you use when deriving labelled transitions.
  \solution{%
    We can infer a bound output for %
    $\newpp x {\outact k x \parp P}$ by the following derivation:
    % 
    \begin{gather*}
      \infer{
        \infer
        {\infer{}{\outact k x \redar{\outlab k x} \zerop}\prftag{lab-out}}
        {\outact k x \parp P \redar{\outlab k x} \zerop \parp P}\prftag{lab-par-l}
      }{\newpp x {\outact k x \parp P} \redar{\boutlab k x} \zerop \parp P}
       k\neq x, \prftag{lab-open}
    \end{gather*}
    Since we have two bisimilar processes, %
    $\newpp x {\outact k x \parp P} %
    \strongbisim \newpp x {\outact k x \parp Q}$, and %
    $x \notin \fn{\newpp x {\outact k x \parp Q}}$, we know that the
    right-hand process must be able to match the transition we just
    derived, \ie there exits $Q''$ such that %
    $\zerop \parp P \strongbisim Q''$ and
    $\newpp x {\outact k x \parp Q} \redar{\boutlab k x} Q''$. There are
    only two possible rules that the this last labelled transition
    can be derived from, the first of which turns out to be impossible.
    % 
    \begin{description}
    \item[Case \citetag{lab-new}:] By the side condition for the rule,
      the only way it can be applied is if we do
      $\alpha$-conversion on $x$, \ie we have a derivation of the form:
      %
      \begin{gather*}
        \infer{\outact k {x'} \parp \sub {x'} x Q \redar{\boutlab k x}}%
        {\newpp {x'}
          {\outact k {x'}
            \parp \sub {x'} x Q} \redar{\boutlab k x} }
        \prftag{lab-new}
      \end{gather*}
      where $x'$ is fresh. Suppose, for contradition, that the
      premiss were derivable. By hypothesis, $k \notin \fn Q$, hence %
      $k \notin \fn {\sub {x'} x Q}$, therefore we cannot have %
      $\sub {x'} x Q \redar{\boutlab k x}$. Nor can %
      $\outact k x' \redar{\boutlab k x}$ since $x'$ is free here, 
      disallowing any bound output. Thus this case is impossible.

    \item[Case \citetag{lab-open}:] Then the premiss is %
      $\outact k x \parp Q \redar{\outlab k x} Q''$. Since %
      $k\notin \fn Q$, the output is due to %
      $\outact k x \redar{\outlab k x} \zerop$, thus %
      $Q'' = \zerop \parp Q$.  Finally, %
      $P \strongbisim \zerop \parp P %
      \strongbisim \zerop \parp Q \strongbisim Q$, as desired.
    \end{description}
  }
\end{enumerate}

\item This question addresses relationships between labelled
  transitions and barbs in the core \pic.

   \begin{enumerate}
   \item \qhard Prove that $P \redar{\outlab x y} P'$ implies $P\barb x$.
     Hint: induct on the derivation of $P \redar{\outlab x y} P'$.
     % 
     \solution{%
       According to the definition of $P \barb x$, we have to show
       that there exists $\zvec$, $w$, $P_0$, and $P_1$ such that %
       $P \streq \newpp \zvec { \outp x w {P_0} \parp {P_1} }$. In
       fact we can always use $w=y$, as we show in the following
       induction on the derivation of $P \redar{\outlab x y} P'$.
       % 
       \begin{description}
       \item[Case \citetag{lab-out}:] Then there exists $P_0$ such
         that $P = \outp x y {P_0}$. Take $P_1=\zerop$ and $\zvec$ to
         be the empty list of names. Then %
         $ P \streq \newpp \zvec { \outp x y {P_0} \parp {P_1} }$, as
         required.
         
       \item[Case \citetag{lab-par-l}:] Then there exists $P_2$ and
         $Q$ such that $P=P_2 \parp Q$ with the premiss %
         $P_2 \redar{\outlab x y}$. Applying the inductive hypothesis to
         the premiss, there exist $\zvec$, $P_0$, and $P_1$ such
         that %
         $P_2 \streq \newpp \zvec { \outp x y {P_0} \parp {P_1} }$.
         Without loss of generality, we may assume that %
         $\zvec \cap \fn Q = \emptyset$, hence %
         $P = P_2 \parp Q %
         \streq \newpp \zvec { \outp x y {P_0} \parp P_1 } \parp Q
         \streq \newpp \zvec { \outp x y {P_0} \parp (P_1  \parp Q)}$
         by scope extrusion, as required.

       \item[Case \citetag{lab-par-r}:] Symmetric to the previous
         case.

       \item[Case \citetag{lab-new}:] There exists $P_2$ and $u$ such
         that $P = \newp u {P_2}$ and $u\notin\{x,y\}$, with the
         premiss $P_2 \redar{\outlab x y}$. Applying the inductive hypothesis to
         the premiss, there exist $\zvec$, $P_0$, and $P_1$ such
         that %
         $P_2 \streq \newpp \zvec { \outp x y {P_0} \parp {P_1} }$.
         Hence %
         $P = \newp u P_2 %
         \streq \newpp {u} {\newpp \zvec { \outp x y {P_0} \parp P_1  }}$,
         as required.
       \end{description}
     }

  \item \qeasy Give an example to show that the converse is not true,
    \ie find a $P$ such that $P\barb x$ but not $P \redar{\outlab x y}$.
    \solution{%
      Take $P=\newp y {\outact x y}$.  Then $P \barb x$ but $P$ can
      only do a \emph{bound output} on $x$, \ie $P \redar{\boutlab x y} \zerop$.
    }
  \end{enumerate}
\end{enumerate}

\end{document}

