\documentclass[5p]{elsarticle}
\usepackage{hyperref,breakurl}             % Not needed if you use pdflatex only.
\usepackage{bm}
\usepackage{stmaryrd}
\usepackage{amssymb}
\usepackage{amsmath}
\usepackage{amsthm}
\usepackage{mathrsfs}
\usepackage{tabularx}
\usepackage{multirow}
\usepackage{tikz}
\usepackage{pifont}
\usepackage{xspace}
\usepackage[inference]{semantic}
\usepackage{enumerate}
\makeatletter
\def\ps@pprintTitle{%
     \let\@oddhead\@empty
     \let\@evenhead\@empty
     \let\@oddfoot\@empty
     \let\@evenfoot\@oddfoot}
\makeatother
\newfont{\bbb}{bbm10}        % blackboard bold

\usetikzlibrary{arrows,automata,chains,matrix,positioning,scopes,calc,decorations.pathmorphing,shapes.misc}

\tikzset{drbox/.style={
  rounded rectangle,
  minimum size=2mm,
  very thick,draw=black!50,
  top color=white,bottom color=black!20,
  font=\ttfamily}}
\tikzset{prbox/.style={
  rounded rectangle,
  minimum size=2mm,
  very thick,draw=white,
  top color=white,bottom color=white,
  font=\ttfamily}}
\tikzset{mode/.style={font=\scriptsize,execute at begin node=$,execute
    at end node=$}}

\usepackage{macros}

\theoremstyle{plain}
\newtheorem{proposition}{Proposition}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{corollary}{Corollary}

\theoremstyle{remark}
\newtheorem{remark}{Remark}
\newtheorem{observation}{Observation}

\theoremstyle{definition}
\newtheorem{definition}{Definition}

\title{A Case Study on Evaluating Encodings Between Process Calculi\textsuperscript{\sep$\ast$}}
\author[tubs]{Christopher Lippert}
\ead{kris.lippert@web.de}

\author[tubs]{Stephan Mennicke}
\ead{mennicke@ips.cs.tu-bs.de}

\author[csiro,nsw]{Rob J. van Glabbeek}
\ead{rvg@cs.stanford.edu}

\author[tubs]{Ursula Goltz}
\ead{goltz@ips.cs.tu-bs.de}

\address[csiro]{Data61, CSIRO, Sydney, Australia}
\address[nsw]{School of Computer Science and Engineering, University of New South Wales, Sydney, Australia}
\address[tubs]{Institute for Programming and Reactive Systems, TU Braunschweig, Germany}

\cortext[dfg]{This work was partially supported by the DFG (German Research Foundation).}

\begin{document}

\begin{abstract}
Two process calculi may be compared in their expressive power using encodings between them.
Not every such translation is meaningful and therefore quality criteria are necessary.
There are several frameworks to assess the quality of encodings.
A rather prominent approach consists of five criteria for valid encodings collected by Gorla.
An alternative notion of validity up to a semantic equivalence was proposed by one of the authors.
Here the quality of the encoding is measured by the strength of the semantic equivalence that makes it valid.

In this paper we analyse two well-known translations from the synchronous into the asynchronous \piCal, both meeting Gorla's criteria,
and evaluate the encodings' validity up to different semantic equivalences.

While Honda and Tokoro's translation is valid only for the weakest of
the considered behavioural equivalences, Boudol's encoding also respects stronger ones. 
One could hence argue that Boudol's translation is more faithful.
\end{abstract}

\begin{keyword}
process calculi \sep quality criteria for encodings \sep \ensuremath{\pi}-calculus
\end{keyword}

\maketitle

\section{Introduction}

\noindent
Since the late 1970s, a large number of process calculi has been invented and studied, see \eg\cite{Baeten05}.
The need for new process calculi emerged with different requirements for analysability and applicability.
Due to the significant number of process calculi, techniques to bring order into the process calculi landscape are highly useful.
One of those techniques consists of the comparison of the expressive power of process languages.
A well-established way of doing this is based on the existence of convincing translations between them.

Translations between process calculi help us understand their differences and commonalities.  A translation
may also be useful to make existing tools for the target language available for the source language.

A calculus $\sB$ is at least as expressive as $\sA$ if there exists a 
translation, mapping every $\sA$ expression to an expression of $\sB$ 
such that certain criteria are met.
The criteria are necessary, because not every translation is suitable or meaningful. 
The literature provides a wide variety of translations between process calculi 
for which the authors often establish their own criteria satisfied by
their translation, cf.~\cite{gorla:unified}.
Unfortunately, due to the very different criteria, it is hard to compare two translations with each other.
To obtain formal arguments comparing two translations, a unified set of quality criteria is required.
Gorla proposes a set of five criteria to assess process calculi encodings\footnote{We use the terms
  {\em encodings} and {\em translations} synonymously.}~\cite{gorla:unified}.
A different approach for assessing the quality of encodings, also applicable to languages other than process calculi, is
proposed by one of the authors in \cite{gla:musings}. There,
the concept of a \emph{valid} encoding up to some semantic equivalence $\sim$ is
defined, demanding that the meaning of an expression and its
translation are equivalent.
This criterion has already been used to compare Milner's CCS with Hoare's CSP~\cite{gla:musings}.

In this paper we analyse the validity, in the sense of~\cite{gla:musings}, of two translations from a synchronous into an
asyn\-chro\-nous variant of the \piCal. Both are known to satisfy Gorla's criteria \cite{vG18a}.
One encoding is given by Boudol~\cite{boudol:async}, the other by Honda and Tokoro~\cite{ht:objectcalculus}.
Although source and target language are very similar, the encodings use different ideas to encode synchrony by asynchronous primitives.
Hence, the encodings serve as perfect candidates for a case study on the concept of validity introduced in \cite{gla:musings}.
We find an answer to the questions to what extent the validity of both
encodings depends on the choice of the equivalence, and if there is any difference in the translations' quality.
In Gorla's framework both translations have equally good properties, \ie all five of Gorla's criteria are met \cite{vG18a}.

We choose several semantic equivalences under which we evaluate the validity of the encodings.
For each translation we find equivalences up to which they 
are valid and some for which we disprove validity.
Moreover, we find a potential difference in the quality of the translations by 
presenting equivalences for which Boudol's encoding is valid, but 
Honda and Tokoro's encoding is not.
Conversely, we conjecture that there is no natural equivalence for which Honda and Tokoro's encoding is valid, but Boudol's is not.

In Sect.~\ref{sec:preliminaries}, we give preliminary definitions.
Sect.~\ref{sec:processcalculi} defines syntax and semantics of our variants of the 
synchronous and asynchronous \piCal.
Furthermore, we introduce the equivalence notions employed in this paper.
In Sect.~\ref{sec:boudol}, we present Boudol's translation and discuss up to which equivalences it is valid.
Analogously, we discuss Honda and Tokoro's encoding in Sect.~\ref{sec:honda}.
Sect.~\ref{sec:conclusion} concludes.

\section{Valid Translations between Languages}\label{sec:preliminaries}

\noindent
In this section, we introduce the notions of language, translation and validity of a translation according to \cite{gla:musings}.
The definitions may be applied to arbitrary translations between formal languages.
However, the focus of this paper is on process calculi.

\begin{definition}
Let $\sD_{\sL}$ be a set.
A {\em language} is a pair $\sL = ( \bbT_{\sL}, \llbracket \, \rrbracket_{\sL} )$ where $\bbT_{\sL}$ is the set of all valid expressions and
$\llbracket \, \rrbracket_{\sL} : \bbT_{\sL} \rightarrow \sD_{\sL}$ is a function which associates with each expression $P \in \bbT_{\sL}$
its meaning $\llbracket P \rrbracket_{\sL} \in \sD_{\sL}$.
\end{definition}

\noindent
$\sD_{\sL}$ is called the {\em semantic domain of $( \bbT_{\sL}, \sem{\,}{\sL} )$}.
If $\sD_{\sL}$ is the set of all labelled transition systems, then $\sem{\,}{\sL}$ may be the
function mapping each $\sL$-term $T \in \bbT_{\sL}$ to its transition system $\sem{T}{\sL}$ given by
some structural operational semantics.

In \cite{gla:musings} languages $\sL$ with process variables are
considered, drawn from a set $\sX$, and accordingly $\sD_\sL$ is of
type $(\sX \rightarrow \bV) \rightarrow \bV$ for some set of
values $\bV$. Here an element of $\sX \rightarrow \bV$ is a
\emph{valuation}, associating a value from $\bV$ with each process
variable, and the meaning of an expression is a value that depends on
the choice of such a valuation. Since in this paper we deal with
languages without process variables, we can instead take $\sD_\sL$
to be $\bV$.

\begin{definition}
Let $\sL_1, \sL_2$ be languages.
A {\em translation from $\sL_1$ to $\sL_2$} is a function $\sI : \bbT_{\sL_1} \rightarrow \bbT_{\sL_2}$.
\end{definition}

\noindent
We call $\sL_1$ the {\em source language} and $\sL_2$ the {\em target language} of $\sI$.
We require the behaviour encoded by a source term
$P \in \bbT_{\sL_1}$ to be preserved by its translation $\sI(P)$.

\begin{definition}
Let $\sL_i$ ($i = 1, 2$) be languages with semantic domains $\sD_{\sL_i}$ and
let $\sim$ be an equivalence on $\sD_{\sL_1} \cup \sD_{\sL_2}$.
A translation $\sI : \bbT_{\sL_1} \rightarrow \bbT_{\sL_2}$ is {\em valid
up to $\sim$} iff $\sI$ is compositional and
$\llbracket \sI(P) \rrbracket_{\sL_2} \sim \llbracket P \rrbracket_{\sL_1}$
for all $P \in \bbT_{\sL_1}$.
\end{definition}

\noindent
Here a translation $\sI$ is called \emph{compositional} if for every $n$-ary operator $f$ in the source language one has $$\sI(f(P_1,\ldots,P_n)) \stackrel\alpha=  C_f(\sI(P_1),\ldots,\sI(P_n))\vspace{-3pt}$$ for some $n$-hole context $C_f$.
Here $\stackrel\alpha=$ denotes equivalence up to \emph{$\alpha$-conversion}, i.e., renaming of bound names.
The definition in \cite{gla:musings} is more general, because it also covers language constructs such as recursion; this generality is not needed here.
In \cite{gla:musings} the use of the above definition is restricted to languages in which all semantic values are denotable by closed terms; this condition is trivially fulfilled for the languages considered here.
In fact, formally the semantic domain $\sD_{\sL}$ of the languages $\sL$ occurring in this paper consists of the (closed) terms of $\sL$ up to $\alpha$-conversion---the real semantics is given by an appropriate equivalence relation on these expressions.
In addition, since in this paper we investigate languages that make no use of process variables, the translations under investigation are automatically what is called ``fvr-translations'' in \cite{gla:musings}.

In \cite{gla:musings}, besides the notion of a valid translation, also
the concept of a \emph{correct} translation up to an equivalence
$\sim$ is introduced. This definition requires $\sim$ to be a
congruence for the source language. As this condition is not met
by the semantic equivalences of this paper, we will not apply the
notion of a correct translation here.

\section{Process Calculi}\label{sec:processcalculi}

\noindent
In this section we introduce two versions of the \piCal, namely a
subset $\pims$ of the (synchronous) \piCal and an asynchronous \piCal $\pima$.
We specify syntax and semantics, and we list semantic equivalences under
which we will compare processes of the source language $\pims$
with translated processes of the target language $\pima$.

\subsection[A Synchronous pi-Calculus]{A Synchronous \ensuremath{\pi}-Calculus}

\noindent
The (synchronous) $\pi$-calculus was first introduced by Milner, Parrow
and Walker~\cite{mpw:mobileprocessesi}.
Here we use a subset of their operators that was first employed in \cite{milner:functions}.

\begin{definition}
Let $\mathcal N$ be a set of {\em names}.
The syntax of the {\em synchronous mini-\piCal}, $\pims$, is defined
by the grammar\\[3pt]
\centerline{
$P ::= \bm{0} ~\big|~ \bar{x}z.P ~\big|~  x(y).P
~\big|~  P|P ~\big|~ (y)P ~\big|~  !P$\vspace{3pt}
}
where $x, y, z \in \mathcal N$.
\end{definition}

\noindent
$\bm{0}$ denotes the empty process.
$\bar{x}z$ stands for an output guard that sends the name $z$ along the channel $x$.
$x(y)$ denotes an input guard that waits for a name to be transmitted along the channel named $x$.
Upon receipt, the name is substituted for $y$ in the subsequent process.
$P|Q$ ($P, Q \in \pims$) denotes a parallel composition between $P$ and $Q$.
$!P$ is the replication construct and $(y)P$ restricts the scope of name $y$ to $P$.

The input construct $x(y).P$ binds the name $y$ in $P$; similarly the
restriction $(y)Q$ binds $y$ in $Q$.
We denote the bound names of $P$ by $\bn(P)$, free names by $\fn(P)$,
and define $\n(P) := \bn(P) \cup \fn(P)$.
With $P\subs{w}{y}$ we denote the result of substituting $w$ for all free occurrences of $y$ in $P$, with change of bound names to avoid name captures.

Following \cite{mpw:mobileprocessesii,milner:functions}, we give two semantics
of $\pims$: a labelled transition semantics and a reduction semantics.
The labels of the former are drawn from
a set of actions $\Act := \{ \bar x y, x(y), \bar x(y) \,|\, x, y \in \mathcal N \} \cup \{ \tau \}$.
We define free and bound names on transition labels:\vspace{-4ex}

\begin{align*}
\fn(\tau)       &= \emptyset &\bn(\tau)       &= \emptyset \\[-3pt]
\fn(\bar{x}z)   &= \{x,z\}   &\bn(\bar{x}z)   &= \emptyset \\[-3pt]
\fn(x(y))       &= \{x\}     &\bn(x(y))       &= \{y\} \\[-3pt]
\fn(\bar{x}(y)) &= \{x\}    &\bn(\bar{x}(y)) &= \{y\}
\end{align*}
For $\alpha\in\Act$ we define $\n(\alpha) := \bn(\alpha) \cup \fn(\alpha)$.\

\begin{definition}\label{def:syncltssemantics}
The {\em labelled transition relation of $\pims$} is the
smallest relation $\mathord{\longrightarrow} \subseteq \bbT_{\pims} \times \Act \times \bbT_{\pims}$,
satisfying the rules of Fig.~\ref{tab:pisyncsemantics}.
\end{definition}

{\renewcommand*\arraystretch{3}%
\begin{figure}[ht]
\centering
\vspace{-4ex}%
\begin{center}
\begin{tabular}{@{}c@{}}
\inference[(OUTPUT-ACT)~]
{~}
{\bar{x}z.P\stackrel{\bar{x}z}{\longrightarrow}P}
\\
\inference[(INPUT-ACT)~]
{w\not\in\fn((y)P)}
{x(y).P\stackrel{x(w)}{\longrightarrow}P\subs{w}{y}}
\\

\inference[(PAR)~]
{P \stackrel{\alpha}{\longrightarrow} P' & \bn(a) \cap \fn(Q) = \emptyset}
{P|Q \stackrel{\alpha}{\longrightarrow} P'|Q}
\\

\inference[(COM)~]
{P\stackrel{\bar{x}z}{\longrightarrow}P' & Q\stackrel{x(y)}{\longrightarrow} Q'}
{P|Q \stackrel{\tau}{\longrightarrow}P'|Q'\subs{z}{y}}
\\
\inference[(CLOSE)~]
{P\stackrel{\bar{x}(w)}{\longrightarrow}P' & Q\stackrel{x(w)}{\longrightarrow}Q'}
{P|Q\stackrel{\tau}{\longrightarrow}(w)(P'|Q')}
\\
\inference[(RES)~]
{P \stackrel{\alpha}{\longrightarrow}P' & y \not\in \n(a)}
{(y)P\stackrel{\alpha}{\longrightarrow}(y)P'}
\\
\inference[(OPEN)~]
{P \stackrel{\bar{x}y}{\longrightarrow} P' & y \neq x & w \not\in \fn((y)P')}
{(y)P \stackrel{\bar{x}(w)}{\longrightarrow}P'\subs{w}{y}}
\\
\inference[(REP-ACT)~]
{P \stackrel{\alpha}{\longrightarrow} P'}
{!P \stackrel{\alpha}{\longrightarrow} P'| !P}
\\
\inference[(REP-COMM)~]
{P \stackrel{\bar x z}{\longrightarrow} P' & P \stackrel{x(y)}{\longrightarrow} P''}
{!P \stackrel{\tau}{\longrightarrow} ( P' | P''\subs{z}{y} ) | !P}
\\
\inference[(REP-CLOSE)~]
{P \stackrel{\bar x(w)}{\longrightarrow} P' & P \stackrel{x(w)}{\longrightarrow} P''}
{!P \stackrel{\tau}{\longrightarrow} ( (w)( P'|P'' ) ) | !P}
\end{tabular}
\end{center}
\caption{SOS rules for the synchronous mini-\piCal.
PAR, COM and CLOSE also have symmetric rules.}
\label{tab:pisyncsemantics}
\end{figure}

\noindent
Another common way to describe the behaviour of a process is a reduction
semantics \cite{milner:functions}.
Instead of taking each label into account, here we are only interested in the actual communication steps a $\pims$ process may perform.
A crucial part of this type of semantics is handled by {\em structural congruence} $\equred$, the smallest congruence relation on $\bbT_{\pims}$ satisfying the following five rules:
\begin{enumerate}[1.]
\item Processes that only differ in the
choice of bound names are identified; this is known as $\alpha$-conversion.
\item $(\bbT_{\pims}/\mathord\equred, |, \bm{0})$ is an Abelian monoid, \ie
(i) $\bm{0} | P \equred P$,
(ii) $( P | Q ) | R \equred P | ( Q | R )$ and
(iii) $P|Q \equred Q|P$, for all $P, Q, R \in \bbT_{\pi}$.
\item $!P \equred P|!P$.
\item $(x)\bm{0} \equred \bm{0}$, $(x)(y)P \equred (y)(x)P$.
\item If $x \notin \fn(P)$, then $(x)(P|Q) \equred P|(x)Q$.
\pagebreak[3]
\end{enumerate}

\begin{definition}\label{reduction}
The {\em reduction relation} $\mapsto \ \subseteq \bbT_{\pims} \times
\bbT_{\pims}$ is the smallest relation satisfying the rules of Fig.~2.
\vspace{-2ex}
\end{definition}
%
{\centering
\begin{tabular}{cc}
\multicolumn{2}{c}{\inference[(COM)~]
{~}
{\bar x z . P | x(y) . Q \mapsto P|Q\subs{z}{y}}}
\\
\inference[(PAR)~]
{P \mapsto P'}
{P|Q \mapsto P'|Q}
&
\inference[(RES)~]
{P \mapsto P'}
{(y) P \mapsto (y) P'}
\\
\multicolumn{2}{c}{\inference[(STRUCT)~]
{Q \equred P & P \mapsto P' & P' \equred Q'}
{Q \mapsto Q'}}
\end{tabular}}
\begin{center}
{\footnotesize Figure 2: Reduction semantics of the mini-$\pi$-calculus.}
\refstepcounter{figure}
\end{center}
\label{tab:piredsemantics}
}
\vspace{2ex}

\noindent
The following results show (1) that the labelled transition relations are invariant under structural congruence ($\equred$), and (2)
that the closure under structural congruence of the
labelled transition relation restricted to $\tau$-steps coincides with
the reduction relation --- (2) stems from Milner~\cite{milner:functions}.
\begin{lemma} {\rm (Harmony Lemma \cite[Lemma 1.4.15]{Sangiorgi2001})}\label{harmony}
\begin{enumerate}
\vspace{-1ex}
\item If $P \stackrel{\alpha}{\longrightarrow} P'$ and $P\equred Q$ then $\exists Q'. Q \stackrel{\alpha}{\longrightarrow} Q' \equred P'$%.
\vspace{-1ex}
\item $P \mapsto P'$ iff $\exists P''. P \stackrel{\tau}{\longrightarrow} P'' \equred P'$.
\vspace{-1ex}
\end{enumerate}
\end{lemma}

\subsection[The Asynchronous pi-Calculus]{The Asynchronous \ensuremath{\pi}-Calculus}

\noindent
A characteristic of synchronous communication, as used in $\pims$,
is that sending a message synchronises with receiving it, so that
a process sending a message can only proceed after another party has
received it. In the asynchronous {\piCal} this feature is dropped, as
it is not possible to specify any behaviour scheduled after a send action.

\begin{definition}[\cite{boudol:async}]
The {\em asynchronous mini-\piCal}, $\pima$, consists of all processes
in $\pims$ such that in each sub-term of the form $\bar x y . P$,
$P = \bm{0}$.
\end{definition}

\noindent
Instead of $\bar x y . \bm{0}$, we just write $\bar x y$.
Since the asynchronous mini-\piCal is a subset of the synchronous one,
we simply reuse the semantics defined above.
$\pima$ is closed under
structural congruence ($\equred$), labelled transitions, as well as reductions.

\subsection{Equivalences}

\noindent
Here we present six behavioural equivalences for $\pims$ and $\pima$
We start with the standard notion of {\em early weak bisimulation} for labelled transition systems~\cite{Sangiorgi2001}.

\begin{definition}\label{def:WB}
A symmetric binary relation \mrel on $\pi$-pro\-cesses $P,Q$ is a {\em early weak
bisimulation} iff $P \mrel Q$ implies
\begin{enumerate}
\vspace{-1ex}
\item if $P \mathbin{\stackrel{\tau}{\longrightarrow}} P'\hspace{-.3pt}$ then a $Q'\hspace{-1pt}$ exists with
  $Q \mathop{\stackrel{\tau}{\longrightarrow}^{\!*}}\! Q'\hspace{-1pt}$ and $P'\mathop{\mrel} Q'\!$,%
\vspace{-1ex}
\item if $P \stackrel{\alpha}{\longrightarrow} P'$ where $\alpha\mathbin= \bar{x}z$ or
  $\bar{x}(y)$  with $y \mathbin{\notin} \n(P)\cup\n(Q)$
  then a $Q'$ exists with
  $Q \mathbin{\stackrel{\tau}{\longrightarrow}^* \stackrel{\alpha}{\longrightarrow} \stackrel{\tau}{\longrightarrow}^*} Q'$ and $P' \mathop{\mrel} Q'$,%
\vspace{-1ex}
\item if $P \stackrel{x(y)}{\longrightarrow} P'$ with $y \notin \n(P)\cup\n(Q)$\vspace{-2pt} then for all $w$ a $Q'$
exists with $Q \mathbin{\stackrel{\tau}{\longrightarrow\!\!}^* \stackrel{x(y)}{\longrightarrow\!\!}
\stackrel{\tau}{\longrightarrow}^*} Q'$ and  $P'\subs{w}{y} \mathop{\mrel} Q'\subs{w}{y}$.%
\vspace{-1ex}
\end{enumerate}
We denote the largest early weak bisimulation by $\wesim$.
\end{definition}

\noindent
Here $y \notin \n(P)\cup\n(Q)$ merely ensures the usage of fresh names.
A \emph{late} weak bisimulation is obtained by requiring in Clause 3 above that the choice of
$Q'$ is independent of $w$; this gives rise to a slightly finer equivalence relation.\pagebreak[3]

{\leftmargini 20pt
A weaker approach does not compare all the transitions with
  visible labels, for these are merely \emph{potential} transitions,
  that can occur only in certain contexts. Instead it just compares
  internal transitions, together with the information whether a state
  has the potential to perform an input or output over a certain channel.
We treat the capability
to read or write over a channel as a predicate of a process.
Such predicates are called {\em barbs} \cite{milner:poly}.

\begin{definition}
Let $x, z \in \mathcal N$.\vspace{1pt}
A process $P$ has a {\em strong barb on $x$}, $P \sbarb x$, iff there
is a $P'$ with \plat{$P \stackrel{x(z)}{\longrightarrow} P'$}.
It has a {\em strong barb on $\bar x$}, $P \sbarb {\bar x}$, iff there\vspace{1pt}
is a $P'$ with \plat{$P \stackrel{\bar x z}{\longrightarrow} P'$} or
\plat{$P \stackrel{\bar x(z)}{\longrightarrow} P'$}.
A process $P$ has a \mbox{\em weak barb on $a$}
($a \in \{ x, \bar x \,|\, x \in \mathcal N \}$), $P \ocomm a$, iff
there is a $P'$ such that \plat{$P \stackrel{\tau}{\longrightarrow}^* P'$} and
$P' \sbarb a$.
\end{definition}

\noindent
Combining the notion of barbs
with the transfer property of classical bisimulation for internal actions only
yields {\em weak barbed bisimulation} \cite{milner:poly}.
Here, two related processes simulate each other's internal transitions and
furthermore have the same weak barbs.

\begin{definition}\label{def:WBB}
A symmetric relation \mrel on $\pi$-terms is a {\em weak barbed bisimulation}
iff $P \mrel Q$ implies
\begin{enumerate}
\vspace{-1ex}
\item if $P \scomm a$ with $a \in \{ x, \bar x \,|\, x \in \mathcal N \}$ then $Q \ocomm a$ and
\vspace{-1ex}
\item if $P \stackrel{\tau}{\longrightarrow} P'\hspace{-1pt}$ then a $Q'\hspace{-1pt}$ exists with
  $Q \mathop{\stackrel{\tau}{\longrightarrow}^{\!*}}\! Q'\hspace{-1pt}$ and $P'\mathop{\mrel} Q'\!$.%
\vspace{-1ex}
\end{enumerate}
The largest weak barbed bisimulation is denoted by $\wbb$.
\end{definition}

\noindent
By Lemma~\ref{harmony} this definition can equivalently be stated with $\mapsto$ in the role of $\stackrel{\tau}{\longrightarrow}$.

In {\em asynchronous weak barbed bisimulation} \cite{acs:asynchronous},
only the names of output channels are observed.
Input barbs are ignored here, as it is assumed that an environment
is able to observe output messages, but not (missing) inputs.

\begin{definition}
A symmetric relation $S$ on $\pi$-terms is an {\em asynchronous weak barbed bisimulation}
iff $P\mrel Q$ implies
\begin{enumerate}
\vspace{-1ex}
\item if $P \scomm {\bar{x}}$, then $Q \wcomm {\bar{x}}$, and
\vspace{-1ex}
\item if $P \stackrel{\tau}{\longrightarrow} P'\hspace{-1pt}$ then a $Q'\hspace{-1pt}$ exists with
  $Q \mathop{\stackrel{\tau}{\longrightarrow}^{\!*}}\! Q'\hspace{-1pt}$ and $P'\mathop{\mrel} Q'\!$.%
\vspace{-1ex}
\end{enumerate}
The largest asynchronous weak barbed bisimulation is denoted by $\wbbisim$.
\end{definition}

\noindent
We obtain a stronger equivalence if we consider not only
output channels but also the messages sent along them.

\begin{definition}[\cite{acs:asynchronous}]
A symmetric relation \mrel on $\pi$-terms is a {\em weak $o\tau$-bisimulation}
if \mrel meets Clauses 1 and 2 (but not necessarily 3) from Definition~\ref{def:WB}.
The largest weak $o\tau$-bisimulation is denoted by $\wotau$.
\end{definition}

\noindent
Amadio \etal\ strengthen this equivalence by adding a further constraint
for input transitions.

\begin{definition}[\cite{acs:asynchronous}]
A relation \mrel is a {\em weak asynchronous bisimulation} iff \mrel is a
weak $o\tau$-bisimulation\vspace{1pt} such that \mbox{$P\mrel Q$} and
\plat{$P \stackrel{\tau}{\longrightarrow}^* \stackrel{x(y)}{\longrightarrow}
\stackrel{\tau}{\longrightarrow}^* P'$} implies
\begin{itemize}
\vspace{-1ex}
\item either a $Q'$ exists satisfying a condition akin to Clause 3 of
 Definition~\ref{def:WB}~\cite{acs:asynchronous},
or\vspace{-1ex}
\vspace{-1ex}
\item a $Q'$ exists such that $Q \stackrel{\tau}{\longrightarrow}^* Q'$ and
$P'\mrel (Q'|\bar{x}y)$.
\vspace{-1ex}
\end{itemize}
The largest weak asynchronous bisimulation is denoted by $\wab$.
\end{definition}

\noindent
As a last equivalence we introduce an even weaker equivalence than weak barbed bisimulation, that does not distinguish between input and output channels.

\begin{definition}
A process $P$ {\em can perform an action on channel $x$},
$P \!\ascomm x$, if $P \stackrel{\alpha}{\longrightarrow} P'$,
for some $P'$, where $\alpha$ has the form $\bar{x}y$, $\bar{x}(y)$ or $x(y)$.
We write $P\acomm x$ when a $P'$ exists with $P \stackrel{\tau}{\longrightarrow}^* P'$
and $P' \!\ascomm x$.

A symmetric relation \mrel on $\pi$-terms is a {\em weak channel bisimulation}
if $P\mrel Q$ implies
\begin{enumerate}
\vspace{-1ex}
\item if $P \ascomm x$ then $Q \acomm x$ and
\vspace{-1ex}
\item if $P \stackrel{\tau}{\longrightarrow} P'\hspace{-1pt}$ then a $Q'\hspace{-1pt}$ exists with
  $Q \mathop{\stackrel{\tau}{\longrightarrow}^{\!*}}\! Q'\hspace{-1pt}$ and $P'\mathop{\mrel} Q'\!$.%
\vspace{-1ex}
\end{enumerate}
The largest weak channel bisimulation is denoted $\wlbsim$.
\end{definition}

\noindent
We thereby obtain the following hierarchy of equivalence relations on \piCal processes (\cf Fig.~\ref{fig:semeq_hier}).}
\begin{figure}[ht]
\centering
%
\begin{tikzpicture}[font=\small]

\node[circle,inner sep=.2em,fill=black,label=below:EWB] (ewb) at (12em,0) {};
\node[circle,inner sep=.2em,fill=black,label=above:WAB] (wab) at (8em,3em) {};
\node[rotate=-35] (wab2ewb) at (10em,1.5em) {$\supset$};

\node[circle,inner sep=.2em,fill=black,label=above:Wo$\tau$] (wot) at (4em,3em) {};
\node (wot2wab) at (6em,3em) {$\supset$};

\node[circle,inner sep=.2em,fill=black,label=below:WBB] (wbb) at (0,0) {};
\node (wbb2ewb) at (6em,0) {$\supset$};

\node (awbb2wot) at (1em,3em) {$\supset$};

\node[circle,inner sep=.2em,fill=black,label=above:AWBB] (awbb) at (-4em,3em) {};
\node[rotate=-35] (awbb2wbb) at (-2em,1.5em) {$\supset$};

\node[circle,inner sep=.2em,fill=black,label=below:WCB] (wcb) at (-8em,0) {};
\node (wcb2wbb) at (-4em,0) {$\supset$};

\draw[semithick] (wab) to (wab2ewb) to (ewb);
\draw[semithick] (wot) to (wot2wab) to (wab);
\draw[semithick] (wbb) to (wbb2ewb) to (ewb);
\draw[semithick] (awbb) to (awbb2wbb) to (wbb);
\draw[semithick] (awbb) to (awbb2wot) to (wot);
\draw[semithick] (wcb) to (wcb2wbb) to (wbb);

\draw[thick] (-6em,4em) -- (-6em,-4em);
\draw[thick] (2em,4em) -- (2em,-4em);
\end{tikzpicture}
\caption{A hierarchy on semantic equivalence relations for \piCal processes,
with separation lines indicating
where the encodings discussed in this paper pass and fail validity.}
\label{fig:semeq_hier}
\end{figure}

\section{Boudol's Translation}\label{sec:boudol}

\renewcommand{\sI}{\mathscr{T}^{}_{\!\scriptscriptstyle \rm B}}
\noindent
In the previous section, we introduced syntax and semantics of the
synchronous as well as of the asynchronous \piCal.
Furthermore, we picked several behavioural equivalences under which we
want to assess two translations between these process calculi.
Boudol's translation  $\sI : \bbT_{\pims} \rightarrow \bbT_{\pima}$ shall be the first~\cite{boudol:async}.
The crucial task is to implement synchronous communication in the asynchronous calculus.

Suppose there is a $\pims$-process able to perform a
communication, for example $\bar{x}z.P|x(y\hspace{-.6pt}).Q$.
In the asynchronous variant of the \piCal, there is no continuation process after an output operation.
Hence, a translation into the asynchronous \piCal has to reflect the communication on channel $x$ as well as the guarding role of $\bar x z$ for $P$ in the synchronous \piCal.
The idea of Boudol's encoding is to assign a guard to $P$ such that this process must receive an {\em acknowledgement message} confirming the receipt of $z$.
We write the sender as
$P' \mathbin= (\bar{x}z|u(v).P)$
where $u,v \mathbin{\not\in} \fn(P)$.
Symmetrically, the receiver must send the acknowledgement, \ie
$Q' = x(y).(\bar{u}v|Q)$.
Unfortunately, this simple transformation is not applicable in every
case, because the protocol does not protect the channel $u$.
$u$ should be known to sender and receiver only, otherwise the
communication may be interrupted by the environment.
Therefore, we restrict the scope of $u$, and start by sending this
private channel to the receiver. The actual message $z$ is now send in
a second stage, over a channel $v$, which is also made into a
private channel between the two processes.
The crucial observation is that in
$(u)(\bar{x}u|u(v).P^*)$,
the subprocess $P^*=\bar{v}z | P$ may only continue after
$\bar{x}u$ was accepted by some receiver, and this receiver has
  acknowledged this by transmitting another channel name $v$ on the
  private channel $u$.
Boudol's translation from $\pims$ to $\pima$ is defined by the following
function (where $u\neq v$):
\begin{align*}
\sI(\bm{0})       &= \bm{0} \\
\sI(\bar{x}z.P)   &= (u)(\bar{x}u | u(v).(\bar{v}z | \sI(P))) &\hspace{-2pt}\mbox{\small$u,v\mathbin{\notin}\fn(P){\cup}\{x,z\}$} \\
\sI(x(y).P)       &= x(u).(v)(\bar{u}v | v(y).\sI(P)) &\hspace{-2pt}\mbox{\small$u,v\mathbin{\notin}\fn(P){\cup}\{x\}$} \\
\sI(P | Q)        &= (\sI(P) | \sI(Q)) \\
\sI(!P)           &= \ ! \sI(P) \\
\sI((x) P)        &= (x) \sI(P)
\end{align*}
In the original definition, Boudol observed that $\bm{0}$ could be
dropped from the syntax of $\pima$ in favour of the constant
$\bar{x}z$, and accordingly used $\sI(\bm{0}) = (x)(z)\bar{x}z$.

The following lemma guarantees that the names $u$ and $v$ used above do not occur in the
translated terms $\sI(P)$ and $\sI(Q)$ either.
\begin{lemma}\label{free vars}\label{sbst}
Let $P\mathbin\in\bbT_{\pims}$. Then $\fn(\sI(P))=\fn(P)$.\\
Moreover, $\sI(P)\subs{z}{y} = \sI(P\subs{z}{y})$ for any $z,y\in\mathcal N$.
\end{lemma}
\begin{proof}
A straightforward structural induction on $P$.
\end{proof}

\noindent
By construction, the encoding of Boudol is compositional.
As it makes use of intermediate steps (namely the acknowledgement protocol), we must fail proving validity of the encoding up to semantics based on action labels, \eg early weak bisimulation.

\begin{theorem}\label{the:boudolwesim}
$\sI$ is not valid up to $\wesim$.
\end{theorem}

\begin{proof}
Let $P = \bar{x}z.\bm{0}$ and $\sI(P) = (u)(\bar{x}u|u(v).(\bar{v}z|\bm{0}))$.
We present the relevant parts of the labelled transition semantics:
\vspace{-2ex}
%
\begin{center}
\begin{tikzpicture}[shorten >=1 pt,>=latex',scale=1.0]
  \node(b0) at(0,3){$\bar{x}z.\bm{0}$};
  \node(b1) at(0,1.5){$\bm{0}$};
    \draw[->](b0)--node[mode,right]{\bar{x}z}(b1);
  \node(b0) at(4.5,4.5){$(u)(\bar{x}u|u(v).(\bar{v}z|\bm{0}))$};
  \node(b1) at(4.5,3){$(u)(\bm{0}|c(v).(\bar{v}z|\bm{0}))$};
  \node(b2) at(4.5,1.5){$(u)(\bm{0}|(\bar{d}z|\bm{0}))$};
  \node(b3) at(4.5,0){$(u)(\bm{0}|(\bm{0}|\bm{0}))$};
    \draw[->](b0)--node[mode,right]{\bar{x}(c)}(b1);
    \draw[->](b1)--node[mode,right]{c(d)}(b2);
    \draw[->](b2)--node[mode,right]{\bar{d}z}(b3);
\end{tikzpicture}
\end{center}
%
Here,\vspace{1pt} the translated term may perform an input transition \plat{$\stackrel{c(d)}{\longrightarrow}$} the source term is not capable of.
Hence, the processes are not equivalent up to early weak bisimulation.
\end{proof}

\noindent
Early weak bisimulation is too strong to prove the translation
valid, as intermediate steps are taken into account by the equivalence.
Weaker equivalences such as weak barbed bisimulation only compare
the barbs of a process.
Fortunately, Boudol's encoding keeps the original
channel names of a sending or receiving process invariant.
Hence, a translated term does exhibit the same barbs as the source term.
\begin{lemma}\label{barbs}
Let $P \in \bbT_{\pims}$ and $a \in \{ x, \bar x \,|\, x \in \mathcal N \}$.
Then $P \scomm a$ iff $\sI(P) \scomm a$.
\end{lemma}
\begin{trivlist}\item[\hspace{4pt}\textit{Proof.}]
With structural induction on $P$.
\leftmargini 20pt
\begin{itemize}
\vspace{-1ex}
\item $\bm{0}$ and $\sI(\bm{0})$ have the same strong barbs, namely none.%
\vspace{-1ex}
\item $\bar xz.P$ and $\sI(\bar xz.P)$ both have only the strong barb $\bar x$.%
\vspace{-1ex}
\item $x(y).P$ and $\sI(x(y).P)$ both have only strong barb $x$.%
\vspace{-1ex}
\item The strong barbs of $P|Q$ are the union of the ones of $P$ and $Q$.
  Using this, the case $P|Q$ follows by induction.%
\vspace{-1ex}
\item The strong barbs of $!P$ are the ones of $P$.
  Using this, the case $!P$ follows by induction.
\vspace{-1ex}
\item The strong barbs of $(x)P$ are ones of $P$ except $x$ and $\bar x$.
  Using this, the case $(x)P$ follows by induction.
\qed
\vspace{-1ex}
\end{itemize}
\end{trivlist}

\noindent
Before we prove validity of Boudol's translation up to weak barbed bisimulation, we further investigate the protocol steps established by Boudol's encoding.
Let $P'\mathbin=\bar{x}z.P$ and $Q'\mathbin=x(y).Q$. Pick $u,v$ not free in $P$ and $Q$, with
$u\mathbin{\neq} v$. Write $P^*\mathbin{:=}\bar{v}z | \sI(P)$ and $Q^*\mathbin{:=}v(y).\sI(Q)$. Then
\[\begin{array}{rcl}\sI(P'|Q') &=& (u)(\bar{x}u | u(v).P^*) ~|~ x(u).(v)(\bar{u}v | Q^*)\\
&\mapsto& (u)\big(u(v).P^* ~|~ (v)(\bar{u}v | Q^*)\big)\\
&\mapsto& (v)(P^* | Q^*)\\
&\mapsto& \sI(P) | (\sI(Q)\subs{z}{y})\;.
\end{array}\]
Here structural congruence is applied in omitting parallel components $\bm{0}$ and empty binders
$(u)$ and $(v)$. Now the crucial idea in our proof is that the last two reductions are \emph{inert},
in that set of the potential behaviours of a process is not diminished by doing (internal) steps of
this kind. The first reduction above in general is not inert, as it creates a commitment between a
sender and a receiver to communicate, and this commitment goes at the expense of the potential of
one of the two parties to do this communication with another partner.
We employ a relation that captures these inert reductions in a context.

\newcommand{\XX}{P}
\newcommand{\YY}{Q}
\begin{definition}[\cite{vG18a}]\label{def:cool-rel}
Let $\equiv\!\Rrightarrow$ be the smallest relation on $\bbT_{\pima}$ such that
\begin{enumerate}
\vspace{-5pt}
\item $(v)(\bar vy | \XX | v(z).\YY) \equiv\!\Rrightarrow \XX|(\YY\subs{y}{z})$,
\vspace{-3pt}
\item if $\XX \equiv\!\Rrightarrow \YY$ then $\XX|C \equiv\!\Rrightarrow \YY|C$,
\vspace{-3pt}
\item if $\XX \equiv\!\Rrightarrow \YY$ then $(w) \XX \equiv\!\Rrightarrow (w) \YY$,
\vspace{-3pt}
\item if $\XX \equred \XX' \equiv\!\Rrightarrow \YY' \equred \YY$ then $\XX \equiv\!\Rrightarrow \YY$,
\vspace{-6pt}
\end{enumerate}
where
$v \not\in \fn(\XX) \cup \fn(\YY\subs{y}{z})$.
\end{definition}

\noindent
First of all observe that whenever two processes are related by $\equiv\!\Rrightarrow$, an actual
reduction takes place.

\begin{lemma}[\cite{vG18a}]\label{lem1}
If $P \equiv\!\Rrightarrow Q$ then $P \longmapsto Q$.
\end{lemma}

\noindent
The next two lemmas confirm that inert reductions do not diminish the
potential behaviour of a process.
\begin{lemma}[\cite{vG18a}]\label{lem2}
If $P \equiv\!\Rrightarrow Q$ and $P \longmapsto P'$ with $P'\not\equred Q$
then there is a $Q'$ with $Q \longmapsto Q'$ and $P' \equiv\!\Rrightarrow Q'$.
\end{lemma}
\begin{corollary}\label{lem2 transitive}
If $P \equiv\!\Rrightarrow^* Q$ and $P \mapsto P'$
then either $P'\mathbin{\equiv\!\Rrightarrow^*} Q$ or there is a $Q'$ with $Q \mapsto Q'$ and $P' \equiv\!\Rrightarrow^* Q'$.
\end{corollary}
\begin{proof}
By repeated application of Lemma~\ref{lem2}.
\end{proof}

\begin{lemma}\label{postponed barbs}
If $P \equiv\!\Rrightarrow Q$ and $P \scomm a$ for $a \in \{ x, \bar x \,|\, x \in \mathcal N \}$
then $Q \scomm a$.
\end{lemma}
\begin{proof}
\newcommand{\rn}{z}
\newcommand{\un}{y}
Let $(\tilde w)P$ for $\tilde w \mathbin=\{w_1,\dots,w_n\}\mathbin\subseteq \mathcal{N}$
with $n\mathbin\in\mbox{\bbb N}$ denote $(w_1)\cdots(w_n)P$ for some
arbitrary order of the $(w_i)$.
Using a trivial variant of Lemma 1.2.20 in \cite{Sangiorgi2001},
there are
$\tilde w \subseteq\mathcal{N}$, $x,\un,\rn\mathbin\in\mathcal{N}$
and $R,C\mathbin\in\bbT_{\pima}$, such that $x\in\tilde w$ and
$P \mathbin{\equred} (\tilde w)((\bar x \un | x(\rn) . R) | C ) \mathbin{\longmapsto}
(\tilde w)(( \bm{0} | R\subs{\un}{\rn}) | C ) \mathbin{\equred} Q$.
Since $P{\sbarb{a}}$, it must be that $a{=}x$ or $\bar x$ with $x\notin\tilde w$, and
$C{\sbarb{a}}$. Hence $Q{\sbarb{a}}$.
\end{proof}

\noindent
The following lemma states, in terms of Gorla's framework, {\em operational completeness}~\cite{gorla:unified}:
if a source term is able to make a step, then its translation is able to simulate that step by protocol steps.

\begin{lemma}[\cite{vG18a}]\label{lem5}
Let $P,P' \mathbin\in \bbT_{\pims}$.
If $P \mapsto P'$ then $\sI(P) \mapsto^* \sI(P')$.
\end{lemma}

\noindent
Finally, the next lemma was a crucial step in establishing \emph{operational soundness}~\cite{gorla:unified}.

\begin{lemma}[\cite{vG18a}]\label{lem6}
Let $P \mathbin\in \bbT_{\pims}\!$ and $Q \mathbin\in \bbT_{\pima}\!$.
If $\sI(P) \mathbin{\longmapsto} Q$ then there is a $P'$ with $P \longmapsto P'$
and $Q\equiv\!\Rrightarrow^* \sI(P')$.
\end{lemma}

\noindent
Using these lemmas, we prove the validity of Boudol's encoding up to weak reduction bisimulation.

\begin{theorem}\label{theo:boudolwrequ}
Boudol's encoding is valid up to $\wbb$.
\end{theorem}

\newcommand{\rel}{\mrel}
\begin{proof}
Define the relation $\rel$ by $P\rel Q$ iff $Q \mathrel{\equiv\!\Rrightarrow^*} \sI(P)$.
It suffices to show that the symmetric closure of $\rel$ is a weak barbed bisimulation.

To show that $\rel$ satisfies Clause 1 of Def.~\ref{def:WBB},
suppose $P \rel Q$ and $P \scomm a$ for $a \in \{ x, \bar x \,|\, x \in \mathcal N \}$.
Then $\sI(P) \scomm a$ by Lemma~\ref{barbs}.
Since  $Q \mathrel{\equiv\!\Rrightarrow^*} \sI(P)$, we obtain $Q \mapsto^* \sI(P)$ by Lemma~\ref{lem1}, and
thus $Q \wcomm a$.\pagebreak[3]

To show that $\rel$ also satisfies Clause 2,
suppose $P \rel Q$ and $P \mapsto P'$. Since $Q \mathrel{\equiv\!\Rrightarrow^*} \sI(P)$, by
Lemmas~\ref{lem1} and \ref{lem5} we have $Q \mathbin{\mapsto^*} \sI(P) \mathbin{\mapsto^*} \sI(P')$, and also $P' \rel \sI(P')$.

To show that $\rel^{-1}$ satisfies Clause 1, suppose $P \rel Q$ and $Q \scomm a$.
Since $Q \mathrel{\equiv\!\Rrightarrow^*} \sI(P)$, Lemma~\ref{postponed barbs} yields \mbox{$\sI(P) \scomm a$},
and Lemma~\ref{barbs} gives $P \scomm a$, which implies $P \wcomm a$.

To show that $\rel^{-1}$ satisfies Clause 2, suppose
$P \rel Q$ and $Q \mapsto Q'$. Since $Q \mathrel{\equiv\!\Rrightarrow^*}\!\! \sI(P)$, by
Corollary~\ref{lem2 transitive} either $Q' \mathbin{\equiv\!\Rrightarrow^*}\!\!\sI(P)$
or there is a $Q''$ with $\sI(P) \mathbin{\mapsto} Q''$ and $Q' \mathbin{\equiv\!\Rrightarrow^*} Q''\!$.
In the first case $P \rel Q'$, so taking $P':=P$ we are done.
In the second case, by Lemma~\ref{lem6} there is a $P'$ with $P \mapsto P'$ and $Q'' \equiv\!\Rrightarrow^* \sI(P')$.
We thus have $P' \rel Q'$.
\end{proof}

\noindent
Since $\wbbisim$ and $\wlbsim$ are weaker equivalences than $\wbb$, we obtain
the following:

\begin{corollary}
Boudol's translation is valid up to $\wbbisim$ and up to $\wlbsim$.
\end{corollary}

\noindent
We now know that Boudol's translation is valid up to $\wbbisim$, but
not up to $\wesim$.
A natural step is to narrow down this gap by considering equivalences in between.

\begin{theorem}
Boudol's translation $\sI : \bbT_{\pims} \rightarrow \bbT_{\pima}$ is
not valid up to $\wotau$, and not not up to $\wab$.
\end{theorem}

\begin{proof}
Consider the proof of Theorem~\ref{the:boudolwesim}.
$\bar{x}z.\bm{0}$ sends a free name along $x$ while $(u)(\bar{x}u|u(v).(\bar{v}z|\bm{0}))$ sends a bound name along the same channel.
Since $\wotau$ differentiates between free and bound names, the transition systems of $\bar{x}z$ and its translation are not $\wotau$-equivalent.
\end{proof}

\section{Honda and Tokoro's Translation}\label{sec:honda}

\renewcommand{\sI}{\mathscr{T}_{\rm HT}}
\noindent
Honda and Tokoro translate between the same languages as 
Boudol does~\cite{ht:objectcalculus}.
Unlike Boudol's translation, communication
takes place directly after synchronising along the private channel $u$.
The synchronisation occurs in the reverse direction, because sending
and receiving messages alternate, meaning that the sending process 
$\bar{x}z.Q$ is translated into a process that receives a message 
on channel $x$ and the receiving process $x(y).R$ is translated into a 
process passing a message on $x$.
%
\begin{align*}
\sI(\bm{0})       &= \bm{0} \\
\sI(\bar{x}z.P)   &= x(u).(\bar{u}z | \sI(P) ) &\mbox{\small$u\mathbin{\notin}\fn(P){\cup}\{x,z\}$} \\
\sI(x(y).P)       &= (u)(\bar{x}u | u(y).\sI(P)) &\mbox{\small$u\mathbin{\notin}\fn(P){\cup}\{x\}$} \\
\sI(P | Q)        &= (\sI(P) | \sI(Q)) \\
\sI(!P)           &= \ ! \sI(P) \\
\sI((x) P)        &= (x) \sI(P) 
\end{align*}
%
Again, this translation is compositional.
As in the case of Boudol's translation, Honda and Tokoro's translation
is not valid up to equivalences based on action labels:

\begin{theorem}
Honda and Tokoro's translation $\sI$
is not valid up to $\wotau$, $\wab$ or  $\wesim$.
\end{theorem}
\begin{proof}
By the counterexample $\bar xz.\bm{0}$, as for Theorem~\ref{the:boudolwesim}.
\end{proof}

\noindent
So again we have to use variants of barbed bisimilarity.
However, the choices of $\wbbisim$ or $\wbb$, that worked for Boudol's translation,
bear no fruit here.

\begin{theorem}
Honda and Tokoro's translation $\sI$ is not valid up to $\wbbisim$, and thus not up to $\wbb$.
\end{theorem}

\begin{proof}
Let $P = \bar{x}z.\bm{0}$.
Then $P \scomm {\bar{x}}$.
The translation is $\sI(P) = x(u).(\bar{u}z|\bm{0})$ and
$\sI(P) {\not\!\wcomm {\bar{x}}}$.
\end{proof}

\noindent
One equivalence remains, namely weak channel bisimulation which does not 
distinguish between input and output channels.
Actually, we introduced $\wlbsim$ as 
a rather weak equivalence after we had proven that Honda and Tokoro's 
encoding is not valid up to one of the original equivalences.

\begin{theorem}
Honda and Tokoro's translation $\sI$
is valid up to $\wlbsim$.
\end{theorem}

\noindent
The proof is similar to the one of Theorem \ref{theo:boudolwrequ}.
Here we use that Lemmas~\ref{lem5} and ~\ref{lem6} also apply to $\sI$ \cite{vG18a}
and Lemma~\ref{barbs} now holds with $\ascomm{x}$ in the role of $\scomm{a}$.

\section{Conclusion}\label{sec:conclusion}

\noindent
We evaluated the concept of a valid translation between two languages, introduced by one of the authors~\cite{gla:musings}.
The two translations we examined were developed by Boudol and by Honda and Tokoro.
Both translate from the synchronous into the asynchronous mini-\piCal.
Honda and Tokoro translate an output action into a construct that first performs an input action on
the same channel and vice versa, while Boudol's encoding leaves the roles of sender and receiver
names untouched.

We instantiated the concept of validity from~\cite{gla:musings} with six behavioural equivalences.
Fig.~\ref{fig:semeq_hier} summarises the results.

In order to prove the validity of Honda and Tokoro's translation, we
had to use the novel weak channel bisimulation that does not distinguish between input and output channels.
Boudol's encoding withstands a stronger equivalence, namely weak barbed bisimilarity.
Hence, Honda and Tokoro's encoding can be regarded as weaker than the one of Boudol.
Whether Boudol's encoding is to be preferred, because it meets stronger
requirements/equivalences, is a decision that should be driven by
the requirements of an application the encoding is used for.

We only used weak equivalences, abstracting from $\tau$-steps.
The reason is that both translations implement a protocol with additional transitions,
and thus are not valid up to strong equivalences.

A translation for further study would be Nestmann's encoding of
the \piCal with separate choice into the asynchronous \piCal~\cite{nestmann:guarded}.
One could also try to state Palamidessi's separation result~\cite{pala:expressive}
in the current framework.
It states that the \piCal with mixed choice is strictly more expressive
than the one with separate choice.
After choosing an appropriate weak equivalence, it must
be proven that there is no valid encoding from $\pi$ with mixed choice into
the \piCal with separate choice.

Finally, we remark that translations are only comparable if their
correctness or validity is proven using the same criteria.
It is not useful to establish a specific set of criteria for each translation.
Consequently, the use of general approaches like the ones by Gorla or
the one used here leads to comparable results on expressiveness of process
calculi, positive as well as negative ones.


\bibliographystyle{eptcs}
\bibliography{generic}
\end{document}