\documentclass[runningheads]{llncs}
\usepackage{hyperref,latexsym,underscore,breakurl}
\catcode`~=11 % make LaTeX treat tilde (~) like a normal character
\newcommand{\urltilde}{\kern -.15em\lower .7ex\hbox{\texttt{~}}\kern -.04em}
\catcode`~=13 % revert back to treating tilde (~) as an active character
\usepackage[shortlabels]{enumitem}
\newcommand{\weg}[1]{}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\makeatletter
\newif\if@qeded
\global\@qededtrue
\def\qed{\hfill$\Box$\global\@qededtrue}
\def\qedneeded{\global\@qededfalse}
\def\qedifneeded{\if@qeded\else\qed\fi}
\makeatother
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%% Theorem-like environments %%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newtheorem{defi}{Definition}
\newtheorem{theo}{Theorem}
\newtheorem{prop}{Proposition}
\newtheorem{lemm}{Lemma}
\newtheorem{coro}{Corollary}
\newtheorem{exam}{Example}
\newtheorem{obse}{Observation}
\newtheorem{post}{Postulate}
\renewenvironment{definition}[1]{\begin{defi} \rm \label{df:#1} }{\end{defi}}
\newenvironment{definitionc}[2]{\begin{defi}[#2] \rm \label{df:#1} }{\end{defi}}
\renewenvironment{theorem}[1]{\begin{theo} \rm \label{thm:#1} }{\end{theo}}
\newenvironment{theoremc}[2]{\begin{theo}[#2] \rm \label{thm:#1} }{\end{theo}}
\renewenvironment{proposition}[1]{\begin{prop} \rm \label{pr:#1} }{\end{prop}}
\newenvironment{propositionc}[2]{\begin{prop}[#2] \rm \label{pr:#1} }{\end{prop}}
\renewenvironment{lemma}[1]{\begin{lemm} \rm \label{lem:#1} }{\end{lemm}}
\renewenvironment{corollary}[1]{\begin{coro} \rm \label{cor:#1} }{\end{coro}}
\renewenvironment{example}[1]{\begin{exam} \rm \label{ex:#1} }{\end{exam}}
\newenvironment{observation}[1]{\begin{obse} \rm \label{obs:#1} }{\end{obse}}
\newenvironment{postulate}[1]{\begin{post} \rm \label{post:#1} }{\end{post}}
\newenvironment{postulatec}[2]{\begin{post}[#2] \rm \label{post:#1} }{\end{post}}
\renewenvironment{proof}{\qedneeded\begin{trivlist} \item[\hspace{\labelsep}\bf Proof:]}
{\qedifneeded\end{trivlist}}
\newcommand{\df}[1]{Def.~\ref{df:#1}}
\newcommand{\thm}[1]{Thm.~\ref{thm:#1}}
\newcommand{\pr}[1]{Prop.~\ref{pr:#1}}
\newcommand{\lem}[1]{Lemma~\ref{lem:#1}}
\newcommand{\cor}[1]{Cor.~\ref{cor:#1}}
\newcommand{\ex}[1]{Example~\ref{ex:#1}}
\newcommand{\obs}[1]{Obs.~\ref{obs:#1}}
\newcommand{\sect}[1]{Sect.~\ref{sec:#1}}
\newcommand{\tab}[1]{Table~\ref{tab:#1}}
\newcommand{\pos}[1]{Postulate~\ref{post:#1}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%% Less space in lists %%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\makeatletter
\def\@listi{\leftmargin\leftmargini
\parsep 0\p@ \@plus1.5\p@ \@minus0\p@
\topsep 1\p@ \@plus2\p@ \@minus2\p@
\itemsep0\p@ \@plus1.5\p@ \@minus0\p@}
\let\@listI\@listi
\@listi
\def\@listii {\leftmargin\leftmarginii
\labelwidth\leftmarginii
\advance\labelwidth-\labelsep
\topsep 1\p@ \@plus\p@ \@minus\p@
\parsep 1\p@ \@plus\p@ \@minus\p@
\itemsep \parsep}
\def\@listiii{\leftmargin\leftmarginiii
\labelwidth\leftmarginiii
\advance\labelwidth-\labelsep
\topsep \z@
\parsep \z@
\itemsep \topsep}
\makeatother
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\DeclareSymbolFont{cmi} {OT1}{cmr}{m}{it}
\DeclareMathSymbol\val {\mathord}{cmi}{118} % value
\DeclareMathSymbol\wal {\mathord}{cmi}{119} % value
\newfont{\bbb}{bbm10 scaled 1100} % blackboard bold
\newcommand{\denote}[1]{\mbox{\bbb [}#1\mbox{\bbb ]}} % denotation
\newcommand{\IN}{\bbbn} % set of natural numbers
\newcommand{\INs}{\bbbn} % small set of natural numbers
\newcommand{\IT}{\mbox{\bbb T}} % set of valid expressions / terms
\newcommand{\T}{{\rm T}} % set of closed terms
\newcommand{\D}{{\cal D}} % set of denotable elements
\newcommand{\fL}{{\cal L}} % a language
\newcommand{\fT}{{\cal T}} % a translation
\newcommand{\bR}{\mathrel{\bf R}} % semantic translation
\newcommand{\bT}{{\bf T}} % translation of semantic domains
\newcommand{\bU}{{\bf U}} % semantic domain of interpretation
\newcommand{\bV}{{\bf V}} % semantic domain of interpretation
\newcommand{\bW}{{\bf W}} % semantic domain of interpretation
\newcommand{\bZ}{{\bf Z}} % semantic domain of interpretation
\newcommand{\E}{E} % an expression
\newcommand{\p}{P} % a closed expression
\newcommand{\V}{\mathcal{X}} % set of process variables
\newcommand{\n}{{\sf n}} % set of names
\newcommand{\bn}{{\sf bn}} % set of bound names
\newcommand{\fv}{{\it fv}} % set of free variables
\newcommand{\dom}{{\it dom}} % domain
\newcommand{\eqa}{\mathrel{\plat{$\stackrel{\alpha}=$}}} % same up to alpha-conversion
\newcommand{\N} {{\cal N}} % set of (free) names
\newcommand{\asim}{\mathrel{\mbox{${\scriptscriptstyle\bullet}\hspace{-1.5ex}\sim$}}}
\newcommand{\subs}[2]{\{\mathord{\raisebox{2pt}[0pt]{$#1$}\!/\!#2}\}} % substitution {w/z}
\newcommand{\sbarb}[2]{#1{\downarrow_{#2}}}
\newcommand{\wbarb}[2]{#1{\Downarrow_{#2}}}
\newcommand{\nwbarb}[2]{#1{\not\Downarrow_{#2}}}
\newcommand{\wbb}{\stackrel{\raisebox{-1pt}[0pt][0pt]{$\scriptscriptstyle \bullet$}}{\approx}}
\newcommand{\plat}[1]{\raisebox{0pt}[0pt][0pt]{#1}} % no vertical space
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\titlerunning{A Theory of Encodings and Expressiveness}
\authorrunning{R.J. van Glabbeek}
\title{A Theory of Encodings and Expressiveness \texorpdfstring{{\\[-4pt]\normalsize (extended abstract)}}{}}
\author{
Rob van Glabbeek \inst{1,2}
}
\institute{
Data61, CSIRO, Sydney, Australia
\and
Comput. Sci. and Engineering, University of New South Wales, Sydney, Australia
}
\begin{document}
\maketitle
\setcounter{footnote}{0}
\begin{abstract}
This paper proposes a definition of what it means for one system
description language to encode another one, thereby enabling an ordering
of system description languages with respect to expressive power.
I compare the proposed definition with other definitions of encoding and
expressiveness found in the literature, and illustrate it on a well-known
case study: the encoding of the synchronous in the asynchronous $\pi$-calculus.
\end{abstract}
\section{Introduction}
This paper, like \cite{Gorla10a,vG12}, aims at answering the question what it means for one language to
encode another one, and making the resulting definition applicable to order system description
languages like CCS, CSP and the $\pi$-calculus with respect to their expressive power.
To this end it proposes a unifying concept of valid translation between two languages
\emph{up to} a semantic equivalence or preorder.
It applies to languages whose semantics interprets the operators and recursion
constructs as operations on a set of values, called a \emph{domain}.
Languages can be partially ordered by their expressiveness up to the chosen equivalence or preorder
according to the existence of valid translations between them.
The concept of a [valid] translation between system description languages (or \emph{process
calculi}) was first formally defined by Boudol \cite{Bo85}. There, and in most other
related work in this area, the domain in which a system description language is
interpreted consists of the closed expressions from the language itself. In \cite{vG94a} I
have reformulated Boudol's definition, while dropping the requirement that the domain of
interpretation is the set of closed terms. This allows (but does not
enforce) a clear separation of syntax and semantics, in the tradition of universal
algebra. Nevertheless, the definition employed in \cite{vG94a} only deals with the case
that all (relevant) elements in the domain are denotable as the interpretations of closed
terms. In \cite{vG12} situations are described where such a restriction is undesirable.
In addition, both \cite{Bo85} and \cite{vG94a} require the semantic equivalence $\sim$ under
which two languages are compared to be a congruence for both of them.
This is too severe a restriction to capture many recent encodings
\cite{San93,Boreale98,Nestmann00,NestmannP00,CarboneM03,BPV05,PalamidessiSVV06,PN12}.
In \cite{vG12} I alleviated these two restrictions by proposing two notions of encoding:
\emph{correct} and \emph{valid} translations up to $\sim$. Each of them generalises the
proposals of \cite{Bo85} and \cite{vG94a}. The former drops the
restriction on denotability as well as $\sim$ being a congruence for the whole target language,
but it requires $\sim$ to be a congruence for the source language, as well as for the source's
image within the target. The latter drops both congruence requirements (and allows $\sim$ to be a
preorder rather than an equivalence), but at the expense of requiring denotability by closed terms.
In situations where $\sim$ is a congruence for the source language's image within the target
language \emph{and} all semantic values are denotable, the two notions agree.
The current paper further generalises the work of \cite{vG12} by proposing a new notion of a valid
translation that incorporates the correct and valid translations of \cite{vG12} as special cases.
It drops the congruence requirements as well as the restriction on denotability.
As in \cite{vG12}, my aim is to generalise the concept of a valid translation as much as possible,
so that it is uniformly applicable in many situations, and not just in the world of process
calculi. Also, it needs to be equally applicable to encodability and separation results,
the latter saying that an encoding of one language in another does not exists.
At the same time, I try to derive this concept from a unifying principle,
rather than collecting a set of criteria that justify a number of known
encodability and separation results that are intuitively justified.
\paragraph{Overview of the paper}
\sect{validity} defines my new concept of a valid translation up to a semantic equivalence or
preorder $\asim$.
Roughly, a valid translation \weg{up to $\asim$ }of one language into another is
a mapping from the expressions in the first language to those in the second
that preserves their meaning, i.e.\ such that the meaning of a translated expression
is semantically equivalent to the meaning of the original. % expression being translated.
\sect{valid-correct} shows that this concept generalises the notion of a correct translation from \cite{vG12}:
a translation is correct up to a semantic equivalence $\sim$ iff it is valid up to $\sim$ and $\sim$
is a congruence for the source language as well as for the image of the source language within the
target language.
Likewise, \cite{translations}---the full version of this paper---establishes the coincidence of my
validity-based notion of expressiveness with the one from \cite{vG12} when applying both to
languages for which all semantic values are denotable by closed terms.
One language is said to be at least as expressive as another up to $\asim$
iff there exists a valid translation up to $\asim$ of the latter language into the former.
\sect{hierarchy} shows that \weg{the relation }``being at least as expressive as'' is a
preorder on languages. This expressiveness preorder depends on the choice of $\asim$, and
a coarser choice (making less \weg{semantic }distinctions) yields a richer preorder of expressiveness
inclusions.
\sect{asynpi} illustrates the framework on a well-known
case study: the encoding of the synchronous in the asynchronous $\pi$-calculus.
\sect{congruence closure} discusses the \emph{congruence closure} of a semantic
equivalence for a given language, and remarks that in the presence of operators with infinite arity
it is not always a congruence.
\sect{ccproperty} states a useful congruence closure property for valid translations:
if a translation between two languages exists that is valid up a semantic equivalence $\sim$,
then it is even valid up to an equivalence that
{\leftmargini 12pt
\begin{itemize}
\item on the source language coincides with the congruence closure of $\sim$
\item on the image of the source within the target language also coincides with the congruence closure of $\sim$%
\item melts each equivalence class of the source with exactly one of the target\weg{, and vice versa}.
\end{itemize}}
\sect{integrating} concludes that the framework established thus far is great for comparing the
expressiveness of languages, but falls short for the purpose of combining language features.
This requires a congruence reflection theorem, provided in \sect{compositionality}, for languages satisfying
postulates formulated in Sects.~\ref{sec:closed-term},~\ref{sec:standard heads} and~\ref{sec:invariance}.
\sect{compositionality} defines when a translation is \emph{compositional}, and shows that any
valid translation up to $\asim$ can be modified into a compositional translation valid up to
$\asim$. This requires restricting attention to languages and preorders $\asim$ that satisfy
some mild sanity requirements---the postulates of Sects.~\ref{sec:standard heads} and~\ref{sec:invariance}.
Hence, for the purpose of comparing the expressive power of languages,
valid translations between them may be presumed compositional.
\sect{related} compares my approach with the one of Gorla~\cite{Gorla10a}, and concludes.
Omitted proofs and counterexamples (marked by \P) can be found in \cite{translations}.
\section{Languages, \weg{correct and }valid translations, and expressiveness}\label{sec:validity}
A language consists of \emph{syntax} and \emph{semantics}.
The syntax determines the valid expressions in the language.
The semantics is given by a mapping $\denote{\ \ }$ that associates
with each valid expression its meaning, which can for instance be an
object, concept or statement.
Following \cite{vG12}, I represent a language $\fL$ as a pair
$(\IT_{\fL},\denote{\ \ }_\fL)$ of a set $\IT_{\fL}$ of valid expressions in
$\fL$ and a mapping $\denote{\ \ }_\fL:\IT_\fL\rightarrow \D_\fL$
from $\IT_\fL$ in some set of meanings $\D_\fL$.
\begin{definitionc}{translation}{\cite{vG12}}
A \emph{translation} from a language $\fL$ into a language $\fL'$ is a
mapping $\fT: \IT_\fL \rightarrow \IT_{\fL'}$.
\end{definitionc}
In this paper, I consider single-sorted languages $\fL$ in which
\emph{expressions} or \emph{terms} are built from variables (taken
from a set $\V$) by means of operators (including constants) and
possibly recursion constructs. For such languages the meaning $\denote{\E}_\fL$
of an $\fL$-expression $\E$ is a function of type
$(\V\mathbin{\rightarrow}\bV)\mathbin{\rightarrow}\bV$ for a given sets of \emph{values} $\bV$.
It associates a value $\denote{E}_\fL(\rho) \mathbin\in\bV$ to $E$ that depends on
the choice of a \emph{valuation} $\rho\!:\V\!\!\!\rightarrow\!\bV$. The
valuation associates a value from $\bV$ with each variable.
Since normally the names of variables are irrelevant and the
cardinality of the set of variables satisfies only the requirement
that it is ``sufficiently large'', no generality is lost by insisting
that two (system description) languages whose expressiveness is being
compared employ the same set of (process) variables.\linebreak[2]
On the other hand, two languages $\fL$ and $\fL'$ may be interpreted in
different domains of values $\bV$ and $\bV'\!$.
Let $\fL$ and $\fL'$ be languages as considered above, with semantic mappings\\[1ex]
\mbox{}\hfill
$\denote{\ \ }_{\fL}:\IT_{\fL} \rightarrow ((\V\rightarrow\bV)\rightarrow\bV)$
\hfill
and
\hfill
$\denote{\ \ }_{\fL'}:\IT_{\fL'} \rightarrow ((\V\rightarrow\bV')\rightarrow\bV')$.
\hfill\mbox{}\\[1ex]
In order to compare these languages
w.r.t.\ their expressive power I need a semantic equivalence or
preorder $\asim$ that is defined on a unifying domain of interpretation $\bZ$,
with $\bV,\bV' \subseteq\bZ$.\footnote{I will be chiefly interested in the case that $\asim$ is an
equivalence---hence the choice of a symbol that looks like $\sim$. However, to establish
\obs{identity} and \thm{composition} below, it suffices to know that $\asim$ is reflexive and
transitive. My convention is that the dotted end of \mbox{$\asim$} points to a translation
and the other end to an original---without offering an intuition for the possible asymmetry.}
Intuitively, $\val'\asim \val$ with $\val\in\bV$ and $\val'\in\bV'$ means that values $\val$ and
$\val'$ are sufficiently alike for our purposes,\pagebreak[4] so that one can accept a translation of an
expression with meaning $\val$ into an expression with meaning $\val'$.
Below, target values of a translation (in $\bV'$) are written on the left.
\emph{Correct} and a \emph{valid} translations up to a semantic equivalence or preorder
$\asim$ were introduced in \cite{vG12}. Here I redefine these concepts in terms of a new concept of
\emph{correctness w.r.t.\ a semantic translation}.
\begin{definition}{semantic translation}
Let $\bV$ and $\bV'$ be domains of values in which two languages $\fL$ and $\fL'$ are interpreted.
A \emph{semantic translation} from $\bV$ into $\bV'$ is a relation $\mathord{\bR}\subseteq\bV'\times\bV$
such that $\forall \val\in\bV.\,\exists \val'\in\bV'.\,\val'\bR \val$.
\end{definition}
Thus every semantic value in $\bV$ needs to have a counterpart in $\bV'$---possibly multiple ones.
For valuations $\eta:\V\rightarrow\bV'$, $\rho:\V\rightarrow\bV$ I write $\eta\bR\rho$ iff
$\eta(X)\bR\rho(X)$ for each $X\in \V$.
\begin{definition}{correct R}
A translation $\fT:\IT_\fL\rightarrow\IT_{\fL'}$ is \emph{correct} w.r.t.\ a semantic translation $\bR$
if $\denote{\fT(\E)}_{\fL'}(\eta) \bR \denote{\E}_\fL(\rho)$ for all expressions $\E\in \IT_\fL$
and all valuations $\eta:\V\rightarrow\bV'$ and $\rho:\V\rightarrow\bV$ with $\eta\bR\rho$.
\end{definition}
Thus $\fT$ is correct iff the meaning of the translation of an expression $E$ is a counterpart
of the meaning of $E$, no matter what values are filled in for the variables,
provided that the value filled in for a given variable $X$ occurring in the translation $\fT(E)$ is
a counterpart of the value filled in for $X$ in $E$.
\begin{definition}{correct}
A translation $\fT:\IT_\fL\rightarrow\IT_{\fL'}$ is \emph{correct} up to $\asim$ iff
$\asim$ is an equivalence, the restriction $\bR$ of $\asim$ to $\bV'\times\bV$ is a semantic
translation, and $\fT$ is correct w.r.t.\ $\bR$.
\end{definition}
\begin{definition}{valid}
A translation $\fT$ is \emph{valid} up to $\asim$ iff
it is correct w.r.t.\ some semantic translation $\mathord{\bR} \subseteq \mathord{\asim}$.
Language $\fL'$ is at least as \emph{expressive} as $\fL$ up to $\asim$ if a
translation valid up to $\asim$ from $\fL$ into $\fL'$ exists.
\end{definition}
Example 4 in \cite{translations} illustrates both notions and shows their difference.
\section{Correct = valid + congruence}\label{sec:valid-correct}
In \cite{vG12} the concept of a correct translation up to $\sim$ was defined, for
$\sim$ a semantic equivalence on $\bZ$.\linebreak[3]
Here two valuations $\eta,\rho:\V\rightarrow\bZ$ are called \emph{$\sim$-equivalent},
$\eta\sim\rho$, if $\eta(X)\sim\rho(X)$ for each $X\in \V$.
In case there exists a $\val\in \bV$ for which there is no
$\sim$-equivalent $\val'\in \bV'$, there is no correct translation from
$\fL$ into $\fL'$ up to $\sim$. Namely, the semantics of $\fL$
describes, among others, how any $\fL$-operator evaluates the argument
value $\val$, and this aspect of the language has no counterpart in $\fL'$.
Therefore, \cite{vG12} requires\vspace{-1.5ex}
\begin{equation}\label{related}
\forall \val\in \bV.~ \exists \val'\in \bV'.~ \val'\sim \val.
\vspace{-1ex}
\end{equation}
This implies that for any valuation $\rho\,{:}\,\V\rightarrow\bV$ there is an
\weg{valuation }$\eta\,{:}\,\V\rightarrow\bV'$ with $\eta\sim\rho$.
\begin{definitionc}{correct translation}{\cite{vG12}}
A translation $\fT$ from $\fL$ into $\fL'$ is \emph{correct up to $\sim$} iff
(\ref{related}) holds and $\denote{\fT(\E)}_{\fL'}(\eta) \sim \denote{\E}_\fL(\rho)$ for all
$\E\in \IT_\fL$ and all valuations $\eta:\V\rightarrow\bV'$ and $\rho:\V\rightarrow\bV$ with
$\eta\sim\rho$.
\end{definitionc}
Note that this definition agrees completely with \df{correct}.
Requirement (\ref{related}) above corresponds to $\bR$ being a semantic translation in \df{correct}.
If a correct translation up to $\sim$ from $\fL$ into $\fL'$ exists, then $\sim$ must be a
congruence for $\fL$.
\begin{definition}{congruence}
An equivalence relation $\sim$ is a \emph{congruence} for a language
$\fL$ interpreted in a semantic domain $\bV$ if
$\denote{E}_\fL(\nu)\sim\denote{E}_\fL(\rho)$
for any $\fL$-expression $E$ and any valuations
$\nu,\rho\!:\V\rightarrow \bV$ with $\nu \sim \rho$.\footnote{This is called a \emph{lean}
congruence in \cite{vG17b}; in the presence of recursion, stricter congruence requirements are common.
Those are not needed in this paper.}
\end{definition}
\begin{propositionc}{congruence}{\cite{vG12}}
$\!$If $\fT\!\!$ is a correct translation up to $\sim$ from $\fL$ into $\fL'\!\!$,
% If a correct translation up to $\sim$ from $\fL$ into $\fL'$ exists,
then $\sim$ is a congruence for $\fL\!\!$.
\end{propositionc}
% \begin{proof}
% Let $\fT$ be a correct translation up to $\sim$ from $\fL$ into $\fL'$.
% Let $E\in\IT_\fL$ and let $\nu,\rho:\V\!\rightarrow\bV$ with $\nu\mathord\sim\rho$.
% By (\ref{related}) there is a valuation $\eta\!:\!\V\!\!\rightarrow\!\bV'$ with $\eta\mathbin\sim\nu$.
% Hence $\denote{\E}_{\fL}(\nu) \mathbin\sim \denote{\fT(\E)}_{\fL'}(\eta) \mathbin\sim \denote{\E}_\fL(\rho)$.%
% \end{proof}
The existence of a correct translation up to $\sim$ from $\fL$ into $\fL'$ does not imply
that $\sim$ is a congruence for $\fL'$. However, $\sim$ has the properties of a congruence for
those expressions of $\fL'$ that arise as translations of expressions of $\fL$, when
restricting attention to valuations into $\bU:=\{\val\in\bV'\mid \exists \val\in \bV.~\val'\sim \val\}$.
In \cite{vG12} this called a \emph{congruence for} $\fT(\fL)$.%
\begin{definition}{weak congruence}
Let $\fT: \IT_\fL \rightarrow \IT_{\fL'}$ be a translation from $\fL$ into $\fL'$.
An equivalence $\sim$ on $\bV'$ is a \emph{congruence for} $\fT(\fL)$
if $\denote{\fT(E)}_{\fL'}(\theta)\mathbin\sim\denote{\fT(E)}_{\fL'}(\eta)$
for any $E\mathbin\in\IT_\fL$ and $\theta,\eta\!:\!\V\!\!\!\rightarrow \!\bU$ with $\theta \mathbin\sim \eta$.%
\end{definition}
\begin{propositionc}{weak congruence}{\cite{vG12}}
If $\fT$ is a correct translation up to $\sim$ from $\fL$ into $\fL'$, then $\sim$ is a
congruence for $\fT(\fL)$.
\end{propositionc}
% \begin{proof}
% Let $\fT$ be correct up to $\sim$ from $\fL$ into $\fL'$.
% Let $E\in\IT_\fL$ and let $\nu,\eta:\V\rightarrow\bU$ with $\nu\sim\eta$.
% By definition of $\bU$ there is a $\rho:\V\rightarrow\bV$ with $\rho\sim\nu$.
% Hence $\denote{\fT(\E)}_{\fL'}(\nu) \sim \denote{\E}_\fL(\rho) \sim\denote{\fT(\E)}_{\fL'}(\eta)$.
% \end{proof}
The following theorem tells that the notion of validity proposed in \sect{validity} can be seen as a
generalisation of the notion of correctness from \cite{vG12} that applies to
equivalences (and preorders) $\asim$ that need not be congruences for $\fL$ or $\fT(\fL)$.
\begin{theorem}{valid correct}
A translation $\fT$ from $\fL$ into $\fL'$ is correct up to a semantic equivalence $\sim$ iff
it is valid up to $\sim$ and $\sim$ is a congruence for $\fT(\fL)$.
\hfill\P
\end{theorem}
\weg{
\begin{proof}
By Definitions~\ref{df:correct} and ~\ref{df:valid} any translation that is correct up to $\sim$
is surely valid up to $\sim$.
Suppose $\fT$ is valid up to $\sim$ and $\sim$ is a congruence for $\fT(\fL)$.
Then there is a semantic translation $\mathord{\bR}\subseteq \bV' \times \bV$ such that
$\mathord{\bR} \subseteq \mathord{\sim}$ and $\fT$ is correct w.r.t.\ $\bR$.
To establish that $\fT$ is correct up to $\sim$,
let $\E\in \IT_\fL$ and let $\eta:\V\rightarrow\bV'$ and $\rho:\V\rightarrow \bV$ be
valuations with $\eta\sim\rho$.
Let $\theta:\V\rightarrow\bV'$ be a valuation with $\theta \bR \rho$---it exists since $\bR$ is a
semantic translation.
Now $\theta \sim \rho \sim \eta$, using that $\mathord{\bR} \subseteq \mathord{\sim}$, so
$\theta,\eta:\V\rightarrow\bU$ and $\theta\sim\eta$. Hence
$\denote{\fT(\E)}_{\fL'}(\eta) \sim \denote{\fT(\E)}_{\fL'}(\theta) \sim \denote{\E}_\fL(\rho)$,
using that $\sim$ is a congruence for $\fT(\fL)$ and that $\bT$ is correct w.r.t.\ $\bR$.
\end{proof}
}
\section{A hierarchy of expressiveness preorders}\label{sec:hierarchy}
An equivalence or preorder $\asim$ on a class $\bZ$ is said to be \emph{finer},
\emph{stronger}, or \emph{more discriminating} than another equivalence or
preorder \mbox{${\scriptscriptstyle\bullet}\hspace{-1.45ex}\approx$} on $\bZ$ if $\val \asim \wal
\Rightarrow \val \mathrel{\mbox{${\scriptscriptstyle\bullet}\hspace{-1.45ex}\approx$}} \wal$ for all $\val,\wal\in\bZ$.
\begin{observation}{hierarchy}
Let $\fT: \IT_\fL \rightarrow \IT_{\fL'}$ be a translation from $\fL$ into $\fL'$, and let
$\asim$ be finer than \mbox{${\scriptscriptstyle\bullet}\hspace{-1.45ex}\approx$}.
If $\fT$ is valid up to $\asim$, then it is also valid up to
\mbox{${\scriptscriptstyle\bullet}\hspace{-1.45ex}\approx$}.
\end{observation}
The quality of a translation depends on the choice of the equivalence or
preorder up to which it is valid. Any two languages are equally expressive up to
the universal equivalence, relating any two processes.
Hence, the equivalence or preorder needs to be chosen carefully to match the
intended applications of the languages under comparison. In general,
as shown by \obs{hierarchy}, using a finer equivalence or preorder yields a
stronger claim that one language can be encoded in another.
On the other hand, when separating two languages $\fL$ and $\fL'$ by
showing that $\fL$ \emph{cannot} be encoded in $\fL'$, a coarser
equivalence \weg{or preorder }yields a stronger claim.
\begin{observation}{identity}
The identity is a valid translation up to any preorder from any
language into itself.
\end{observation}
\begin{theorem}{composition}
If valid translations up to $\asim$ exists from $\fL_1$ into $\fL_2$ and from $\fL_2$
into $\fL_3$, then there is a valid translation up to $\asim$ from $\fL_1$ into $\fL_3$.
\hfill\P
\end{theorem}
\weg{
\begin{proof}
For $i=1,2,3$ let $\denote{\ \ }_{\fL_i}:\IT_{\fL_i} \rightarrow ((\V\rightarrow\bV_i)\rightarrow\bV_i)$,
and for $k=1,2$ let $\fT_k:\IT_{\fL_k}\rightarrow\IT_{\fL_{k+1}}$ be valid translations up to
$\asim$ from $\fL_k$ to $\fL_{k+1}$, based on semantic translations
$\mathbin{\bR_k}\subseteq \bV_{\fL_{k+1}}\times\bV_{\fL_{k}}$. I will show that the translation
$\fT_2\circ\fT_1:\IT_{\fL_1}\rightarrow\IT_{\fL_3}$ from $\fL_1$ into $\fL_3$,
given by $\fT_2\circ\fT_1(E)=\fT_2(\fT_1(E))$, is valid up to $\asim$.
To this end, let $\mathord{\bR_2\circ\bR_1}\subseteq \bV_3\times\bV_1$ be the relation
given by $\val_3 \bR_2\circ\bR_1 \val_1$ iff \mbox{$\exists \val_2: \val_3 \bR_2 \val_2 \wedge \val_2
\bR_1 \val_1$}---\linebreak[1]it is again a semantic translation, and satisfies
$\mathord{\bR_2\circ\bR_1}\subseteq\mathord{\asim}$, using the transitivity of $\asim$.
Now let $\E\in \IT_{\fL_1}$, $\rho:\V\rightarrow\bV_1$ and $\theta:\V\rightarrow\bV_3$, with $\theta\bR_2\circ\bR_1\rho$.
Then there is a valuation $\eta:\V\rightarrow\bV_2$ with $\theta\bR_2\eta\bR_1\rho$.
Hence $\denote{\fT_2(\fT_1(\E))}_{\fL_3}(\theta) \asim
\denote{\fT_1(\E)}_{\fL_2}(\eta) \asim \denote{\E}_{\fL_1}(\rho)$,
so $\fT_2\circ\fT_1$ is correct w.r.t.\ $\bR_2\circ\bR_1$.
\end{proof}
}\thm{composition} and \obs{identity} show that the relation
``being at least as expressive as up to $\asim$'' is a preorder on languages.
\section{Closed-term languages}\label{sec:closed-term}
The languages considered in this paper feature \emph{variables}, \emph{operators} of \emph{arity}
$n\mathbin\in\IN$, and/or other constructs. The set $\IT_\fL$ of $\fL$-expressions is inductively defined by:
\begin{itemize}
\item $X\in\IT_\fL$ for each variable $X\in\V$,
\item $f(E_1,\ldots,E_n)\in\IT_\fL$ for each $n$-ary operator $f$ and expressions $E_i\in\IT_\fL$\weg{ for $i=1,\ldots,n$},
\item and clauses for the other constructs, if any.
\end{itemize}
Examples of other constructs are the infinite summation operator $\sum_{i\in I}E_i$ of CCS, which
takes arbitrary many arguments, or the recursion construct $\mu X.E$, that has one argument, but
\emph{binds} all occurrences of $X$ in that argument.
In general a construct has a number (possibly infinite) of argument expressions and it may bind
certain variables within some of its arguments---the \emph{scope} of the binding.
An occurrence of a variable $X$ in an expression is \emph{bound} if it occurs within the scope of a
construct that binds $X$, and \emph{free} otherwise.
The semantics of such a language is given, in part, by a domain of
values $\bV$, and an interpretation of each $n$-ary operator $f$ of
$\fL$ as an $n$-ary operation $f^\bV: \bV^n\rightarrow \bV$ on $\bV$.
Using the equations $$\denote{X}_\fL(\rho) = \rho(X) \quad \mbox{and} \quad
\denote{f(E_1,\ldots,E_n)}_\fL(\rho) = f^\bV(\denote{E_1}_\fL(\rho),\ldots,\denote{E_n}_\fL(\rho))$$
this allows an inductive definition of the meaning $\denote{\E}_\fL$
of an $\fL$-expression $\E$.
Moreover, $\denote{E}_\fL(\rho)$ only depends on the restriction of $\rho$ to
the set $\fv(E)$ of variables occurring free in $\E$.
The set $\T_\fL \subseteq \IT_\fL$ of \emph{closed terms} of $\fL$ consists of those $\fL$-expressions $E\in\IT_\fL$
with $\fv(E)=\emptyset$. If $P\in\T_\fL$ and $\bV\neq\emptyset$ then $\denote{P}_\fL(\rho)$ is
independent of the choice of $\rho:\V\rightarrow\bV$, and therefore denoted $\denote{P}_\fL$.
\begin{definition}{substitution}
A \emph{substitution} in $\fL$ is a partial function $\sigma:\V\rightharpoonup\IT_\fL$ from the
variables to the $\fL$-expressions. For a given $\fL$-expression $E\in\IT_\fL$,
$E[\sigma]\in\IT_\fL$ denotes the $\fL$-expression $E$ in which each free occurrence of a
variable $X\in\dom(\sigma)$ is replaced by $\sigma(X)$, while renaming bound variables in $E$
so as to avoid a free variable $Y$ occurring in an expression $\sigma(X)$ ending up being
bound in $E[\sigma]$.
A substitution is \emph{closed} if it has the form $\sigma:\V\rightarrow\T_\fL$.
\end{definition}
An important class of languages used in concurrency theory are the ones
where the distinction between syntax and semantic is effectively dropped by taking $\bV=\T_\fL$,
i.e.\ where the domain of values where the language is interpreted in consists of the closed terms
of the language. Here a valuation is the same as a closed substitution, and $\denote{E}_\fL(\rho)$
for $E\in\IT_\fL$ and $\rho:\V\rightarrow \T_\fL$ is defined to be $E[\rho]\in\T_\fL$.
I will call such languages \emph{closed-term} languages.
\section[Translating a synchronous into an asynchronous pi-calculus]
{Translating a synchronous into an asynchronous $\pi$\weg{-calculus}}\label{sec:asynpi}
As an illustration of the concepts introduced above, consider the $\pi$-calculus as presented in
\cite{Mi92}, i.e., the one of \cite{SW01book} without matching, $\tau$-prefixing, and choice.
Given a set of \emph{names } $\N$, the set $\IT_\pi$ of \emph{process expressions} or \emph{terms} $E$
of the calculus is given by $$E ::= X ~~\mid~~ \textbf{0} ~~\mid~~ \bar xy.E ~~\mid~~ x(z).E ~~\mid~~ E|E' ~~\mid~~ (\nu z)E ~~\mid~~ !E$$
with $x,y,z$ ranging over $\N$, and $X$ over $\V$, the set of \emph{process variables}.
Process variables are not considered in \cite{SW01book}, although they are common in languages like
CCS \cite{Mi90ccs} that feature a recursion construct. Since process variables form a central part
of my notion of a valid or correct translation, here they have simply been added. This works generally.
In \sect{compositionality} I show that for the purpose of accessing whether one language is as
expressive as another, translations between them can be assumed to be compositional.
This important result would be lost if process variables were dropped from the language.
In that case compositionality would need to be stated as a separate requirement for valid translations.
Closed process expressions are called \emph{processes}.
The $\pi$-calculus is usually presented as a closed-term language, in that the semantic value
associated with a closed term is simply itself. Yet, the real semantics is given by a reduction
relation between processes, defined below.
\begin{definition}{structural congruence}
An occurrence of a name $z$ in $\pi$-calculus process $P\in\T_\pi$ is \emph{bound} if it occurs
within a subexpression $x(z).P'$ or $(\nu z)P'$ of $P$; otherwise it is \emph{free}.
Let $\n(P)$ (resp.\ $\bn(P)$) be the set of names occurring (bound) in $P\in \T_\pi$.
\emph{Structural congruence}, $\equiv$, is the smallest congruence relation on processes satisfying
\[
\begin{array}[b]{r@{~\equiv~}l@{\hspace{-2ex}}r@{~\equiv~}l@{}r@{~\equiv~}l}
P_1 | (P_2 | P_3) & (P_1 | P_2) | P_3 &
!P & P | !P &
(\nu w) (P | Q) & P | (\nu w)Q \\
P_1 | P_2 & P_2 | P_1 &
(\nu z) \textbf{0} & \textbf{0} &
x(z).P & x(w).P\subs{w}{z} \\
P | \textbf{0} & P &
(\nu z)(\nu w)P & (\nu w)(\nu z) P &
(\nu z)P & (\nu w)P\subs{w}{z}\\
\end{array}.
\]
Here the rightmost column only holds when $w\notin\n(P)$,
and $P\subs{w}{z}$ denotes the process obtained by replacing each
free occurrence of $z$ in $P$ by $w$.
% The last two conversions in the right column constitute \emph{$\alpha$-conversion} (renaming of bound names).
% In case $w \in\n(P)$, $P\subs{w}{z}$ denotes $Q\subs{w}{z}$ for some process $Q$ obtained from $P$
% by means of $\alpha$-conversion, such that $z$ does not occur within subexpressions $x(w).Q'$ or $(\nu w)Q'$ of $Q$.
\end{definition}
\begin{definition}{reduction}
The \emph{reduction relation}, ${\rightarrow}\subseteq \T_\pi \times \T_\pi$, is generated by the
following rules.\vspace{-2ex}
\[
\frac{}{\bar xz.P | x(y).Q \rightarrow P|Q\subs{z}{y}} ~ (z\notin\bn(Q)) \qquad
\]
\[
\frac{P \rightarrow P'}{P|Q \rightarrow P'|Q} \qquad
\frac{P \rightarrow P'}{(\nu z)P \rightarrow (\nu z)P'} \qquad
\frac{Q \equiv P \quad P \rightarrow P' \quad P' \equiv Q'}{Q \rightarrow Q'}
\]
\end{definition}
Let $\Longrightarrow$ be the reflexive and transitive closure of $\rightarrow$.
The observable behaviour of $\pi$-calculus processes is often stated in terms of the outputs
they can produce (abstracting from the value communicated on an output channel).
\begin{definition}{barbs}
Let $x\in\N$. A process $P$ has a \emph{strong output barb} on $x$, notation $\sbarb{P}{\bar x}$, if
$P$ can perform an output action $\bar xz$. This is defined inductively:
\[
\sbarb{(\bar xz.(P))}{\bar x} \qquad
\frac{\sbarb{P}{\bar x}}{\sbarb{(P|Q)}{\bar x}} \qquad
\frac{\sbarb{Q}{\bar x}}{\sbarb{(P|Q)}{\bar x}} \qquad
\frac{\sbarb{P}{\bar x} \quad x\neq z}{\sbarb{((\nu z)P)}{\bar x}} \qquad
\frac{\sbarb{P}{\bar x}}{\sbarb{(!P)}{\bar x}}
\]
A process $P$ has a \emph{weak output barb} on $x$, \weg{notation }$\wbarb{P}{\bar x}$, if
there is a $P'$ with $P \Longrightarrow \wbarb{P'}{\bar x}$.
\end{definition}
A common semantic equivalence applied in the $\pi$-calculus is \emph{weak barbed congruence} \cite{MilS92,SW01book}.
\begin{definition}{barbed congruence}
\emph{Weak (output) barbed bisimilarity} is the largest symmetric relation ${\wbb}\subseteq \T_\pi \times \T_\pi$
such that
\begin{itemize}
\item $P \wbb Q$ and $\sbarb{P}{\bar x}$ implies $\wbarb{Q}{\bar x}$, and
\item $P \wbb Q$ and $P \Longrightarrow P'$ implies $Q \Longrightarrow Q'$ for some $Q'$ with $P' \wbb Q'$.
\end{itemize}
\emph{Weak barbed congruence}, $\cong^c$, is the largest congruence included in $\wbb$.
\end{definition}
Often \emph{input barbs}, defined similarly, are included in the definition of weak barbed bisimilarity \cite{SW01book}.
This is known to induce the same notion of weak barbed congruence \cite{SW01book}.
Another technique for defining weak barbed congruence is to use a barb, or set of barbs, external to
the language under investigation, that are added to the language as constants \cite{Gorla10a},
similar to the theory of testing of \cite{DH84}. This method is useful for
languages with a reduction semantics that do not feature a clear notion of barb, or where there
is ambiguity in which barbs should be\linebreak[3] counted and which not, or for comparing languages
with different kinds of barb.
\begin{example}{asynchronous congruence}
$\bar x z.\textbf{0} \not\cong^c (\nu u)(\bar x u .\textbf{0}| u(v). \bar v z. \textbf{0})$.\\
For let $E := X | x(u).\bar u v.\textbf{0}$ with $\rho(X)=\bar x z.\textbf{0}$ and
$\zeta(X)=(\nu u)(\bar x u.\textbf{0} | u(v). \bar v z. \textbf{0})$.\\
Then $E[\zeta] \rightarrow (\nu u)\big(u(v). \bar v z. \textbf{0} | \bar u v.\textbf{0}\big) \rightarrow \sbarb{(\bar v z. \textbf{0})}{\bar v}$
but $\nwbarb{(E[\rho])}{\bar v}$.
\end{example}
\noindent
The asynchronous $\pi$-calculus, as introduced by Honda \& Tokoro in \cite{HT91} and by Boudol in
\cite{Bo92}, is the sublanguage $\rm a\pi$ of the fragment $\pi$ of the $\pi$-calculus presented above where all
subexpressions $\bar x y.E$ have the form $\bar x y.\textbf{0}$. \emph{Asynchronous barbed congruence},
$\cong^c_{\rm a}$, is the largest congruence \emph{for the asynchronous $\pi$-calculus} included in $\wbb$.
Since $a\pi$ is a sublanguage of $\pi$, $\cong^c_{\rm a}$ is at least as coarse an equivalence as $\cong^c$,
i.e.\ ${\cong^c} \subseteq {\cong^c_{\rm a}}$. The inclusion is strict, since
$!x(z).\bar x z.\textbf{0} \cong^c_{\rm a} \textbf{0}$, yet $!x(z).\bar x z.\textbf{0} \not\cong^c \textbf{0}$ \cite{SW01book}.
Since all expressions used in \ex{asynchronous congruence} belong to $\rm a\pi$, one even has
$\bar x z.\textbf{0} \not\cong^c_{\rm a} (\nu u)(\bar x u .\textbf{0}| u(v). \bar v z. \textbf{0})$.
Boudol \cite{Bo92} defined a translation $\fT$ from $\pi$ to $\rm a\pi$ inductively as follows:
\[
\begin{array}{rcll}
\fT(X) &=& X & \mbox{for}~X\in\V\\
\fT(\textbf{0}) &=& \textbf{0} \\
\fT(\bar{x}z.P) &=& (u)(\bar{x}u | u(v).(\bar{v}z | \fT(P))) & \mbox{choosing}~u,v \notin\n(P),~ u\neq v\\
\fT(x(y).P) &=& x(u).(v)(\bar{u}v | v(y).\fT(P)) & \mbox{choosing}~u,v \notin\n(P),~ u\neq v \\
\fT(P | Q) &=& (\fT(P) | \fT(Q)) \\
\fT(!P) &=& \ ! \fT(P) \\
\fT((\nu x) P) &=& (\nu x) \fT(P)
\end{array}
\]
\ex{asynchronous congruence} shows that $\fT$ is not valid up to $\cong^c$.
In fact, it is not even valid up to $\cong^c_{\rm a}$.
However, as shown in \cite{LMGG18}, it is valid up to $\wbb$.
Since $\wbb$ is not a congruence (for $\pi$ or $\rm a\pi$) it is not correct up to $\wbb$.
\section{Congruence closure}\label{sec:congruence closure}
\begin{definition}{1-hole congruence}
An equivalence relation $\sim$ is a \emph{1-hole congruence} for a language
$\fL$ interpreted in a semantic domain $\bV$ if
$\denote{E}_\fL(\nu)\sim\denote{E}_\fL(\rho)$
for any $\fL$-expression $E$ and any valuations
$\nu,\rho:\V\rightarrow \bV$ with $\nu \sim^1 \rho$.
Here $\nu,\rho$ are \emph{$\sim^1$-equivalent}, $\nu\mathbin\sim^1\rho$,
if $\nu(X)\mathbin\sim\rho(X)$ for some $X\mathbin\in \V$ and $\nu(Y)\mathbin=\rho(Y)$ for all variables $Y\mathbin{\neq} X$.
\end{definition}
An \emph{$n$-hole congruence} for any finite $n\in\IN$ can be defined in the same vain, and it is
well known and easy to check that a 1-hole congruence $\sim$ is also an $n$-hole congruence, for any $n\in\IN$.
However, in the presence of operators with infinitely many arguments, a 1-hole congruence need not
be a congruence.
\begin{example}{1-hole congruence}
Let $\bV$ be $(\IN\times\IN) \cup\{\infty\}$, with the well-order $\leq$ on $\bV$ inherited lexicographically from the default
order on $\IN$ and $\infty$ the largest element. So $(n,m) \leq (n',m')$ iff $n\leq n' \vee (n=m \wedge m\leq m')$. Consider the
language $\fL$ with constants $0$, $1$ and $(1)$, interpreted in $\bV$ as $(0,0)$, $(1,0)$ and
$(0,1)$, respectively, the binary operator $+$, interpreted by $(n_1,m_1) +^{\!\bV} (n_2,m_2) =
(n_1\mathord+n_2,m_1\mathord+m_2)$ and $\infty+E=E+\infty=\infty$,
and the construct $\sup (E_i)_{i\in I}$ that takes any number of arguments (dependent on the set of
the index sets $I$). The interpretation of $\sup$ in $\bV$ is to take the supremum of its
arguments w.r.t.\ the well-order $\leq$. In case $\sup$ is given finitely many arguments, it
simply returns the largest. However $\sup((n,i))_{i\in\INs}=(n\mathord+1,0)$.
Now let the equivalence relation $\sim$ on $\bV$ be defined by $(n,m)\sim(n',m')$ iff $n=n'$,
leaving $\infty$ in an equivalence class of its own.
This relation is a 1-hole congruence on $\fL$. Hence, it is also a 2-hole congruence, so one has\vspace{-3pt}
{\small
$$\big((n_1,m_1)\mathbin\sim (n_1',m_1') \mathrel\wedge (n_2,m_2)\mathbin\sim (n_2',m_2')\big) \Rightarrow
(n_1,m_1)+ (n_2,m_2) \sim (n'_1,m'_1)+ (n'_2,m'_2).$$}
Yet it fails to be a congruence: $(n,i) \sim (n,0)$ for all $i\in\IN$, but
$$(n\mathord+1,0)=\sup((n,i))_{i\in\INs}\not\sim \sup((n,0))_{i\in\INs}=(n,0).$$
\end{example}
It is well known and easy to check that the collection of equivalence relations on any domain $\bV$, ordered by
inclusion, forms a complete lattice---namely the intersection of arbitrary many equivalence
relations is again an equivalence relation. Likewise, the collection of 1-hole congruences for $\fL$
is also a complete lattice, and moreover a complete sublattice of the complete lattice of
equivalence relations on $\bV$. The latter implies that for any collection $C$ of 1-hole congruence
relations, the least equivalence relation that contains all elements of $C$ (exists and) happens to
be a 1-hole congruence relation. Again, this is a property that is well known \cite{Gr10} and easy
to prove. It follows that for any equivalence relation $\sim$ there exists a largest 1-hole
congruence for $\fL$ contained in $\sim$. I will denote this 1-hole congruence by $\sim^{1c}_\fL $,
and call it the \emph{congruence closure} of $\sim$ w.r.t.\ $\fL$.
One has $\val_1\sim^{1c}_\fL\val_2$ for $\val_1,\val_2\in\bV$ iff
$\denote{E}_\fL(\nu)\sim\denote{E}_\fL(\rho)$
for any $\fL$-expression $E$ and any valuations
$\nu,\rho:\V\rightarrow \bV$ with
$\nu(X)\mathbin=\val_1$ and $\rho(X)\mathbin=\val_2$ for some $X\in \V$ and $\nu(Y)\mathbin=\rho(Y)$ for all \weg{variables }$Y\mathbin{\neq} X$.
Such results do not generally hold for congruences.
\begin{example}{no largest congruence}
Continue \ex{1-hole congruence}, but skipping the operator $+$.
Let $\sim_k$ be the equivalence on $\bV$ defined by $(n,m)\sim_k(n',m')$ iff $n=n' \wedge (m=m' \vee m,m'\leq k)$.
It is easy to check that all $\sim_k$ for $k\in\IN$ are congruences on the reduced $\fL$, and
contained in $\sim$. Yet their least upper bound (in the lattice of equivalence relations on $\bV$)
is $\sim$, which is not a congruence itself. In particular, there is no largest congruence contained in $\sim$.
\end{example}
When dealing with languages $\fL$ in which all operators and other constructs have a finite arity, so that
each $E\in\IT_\fL$ contains only finitely many variables, there is no difference between a
congruence and a 1-hole congruence, and thus $\sim^{1c}_\fL$ is a congruence relation for any equivalence $\sim$.
I will apply the theory of expressiveness presented in this paper also to languages like CCS that
have operators (such as $\sum_{i\in I}E_i$) of infinite arity. However, in all such cases I'm
currently aware of, the relevant choices of $\fL$ and $\sim$ have the property that $\sim^{1c}_\fL$ is
in fact a congruence relation. As an example, consider weak bisimilarity \cite{Mi90ccs}. This equivalence relation
fails to be a congruence for $\sum$. However, the coarsest 1-hole congruence contained in this
relation, often called \emph{rooted} weak bisimilarity, happens to be a congruence. In fact, when
congruence-closing weak bisimilarity w.r.t.\ the binary sum, the result \cite{vG05e} is also a
congruence for the infinitary sum, as well as for all other operators of CCS \cite{Mi90ccs}.
\pagebreak[3]
\begin{definition}{1-hole congruence for image}
Let $\fT$ be a translation from $\fL$ into $\fL'$.
A subset $\bW$ of $\bV'$ is \emph{closed} under $\fT(\fL)$ if $\denote{\fT(E)}(\eta) \in \bW$
for any expression $E\in\IT_\fL$ and valuation $\eta:\V \rightarrow \bW$.
An equivalence $\sim$ on $\bW$ is a \emph{congruence} (respectively \emph{1-hole congruence})
for $\fT(\fL)$ on $\bW$ if for any $E\in\IT_\fL$ and $\theta,\eta:\V\rightarrow \bW$ with $\theta
\sim \eta$ (respectively $\theta\sim^1\eta$) one has
$\denote{\fT(E)}_{\fL'}(\theta)\sim\denote{\fT(E)}_{\fL'}(\eta)$.
\end{definition}
\begin{proposition}{closed}
Let $\fT$ be a translation from $\fL$ into $\fL'$ that is correct w.r.t.\ a semantic translation
$\mathord{\bR}\subseteq\bV'\times\bV$. Let $\mathord{\bR}(\bV):=\{\val'\in\bV' \mid \exists \val\in\bV.~\val'\bR \val\}$.
Then $\mathord{\bR}(\bV)$ is closed under $\fT(\fL)$.
\end{proposition}
\begin{proof}
Let $E\in\IT_\fL$ and $\eta:\V \rightarrow \mathord{\bR}(\bV)$. Take $\rho:\V \rightarrow\bV$ with
$\rho \bR \eta$. Then $\denote{\fT(\E)}_{\fL'}(\eta) \bR \denote{\E}_\fL(\rho)$.
Since $\denote{\E}_\fL(\rho)\in\bV$ one has $\denote{\fT(\E)}_{\fL'}(\eta)\in\mathord{\bR}(\bV)$.
\end{proof}
\begin{proposition}{1-hole congruence for image}
Let the translation $\fT$ from $\fL$ into $\fL'$ be correct w.r.t.\ the semantic translation
$\mathord{\bR}\subseteq\mathord{\sim}$.
Then $\sim$ is a (1-hole) congruence for $\fL$ iff it is a (1-hole) congruence for $\fT(\fL)$ on $\mathord{\bR}(\bV)$.
\end{proposition}
\begin{proof}
First suppose $\sim$ is a congruence for $\fL$.
Let $E\mathbin\in\IT_\fL$ and $\theta,\eta:\V\rightarrow \mathord{\bR}(\bV)$ with $\theta \sim \eta$.
By the definition of $\mathord{\bR}(\bV)$ there are valuations $\nu,\rho:\V\rightarrow\bV$ with
$\theta \bR \nu$ and $\eta \bR \rho$. Now $\nu\sim\theta\sim\eta\sim\rho$, so
$$\denote{\fT(E)}_{\fL'}(\theta) \bR \denote{\E}_\fL(\nu) \sim
\denote{\E}_\fL(\rho) \bR^{-1} \denote{\fT(E)}_{\fL'}(\eta)$$
and hence $\denote{\fT(E)}_{\fL'}(\theta) \sim \denote{\fT(E)}_{\fL'}(\eta)$.
The other direction proceeds in the same way.
Now suppose $\sim$ is a 1-hole congruence for $\fL$.
Let $E\mathbin\in\IT_\fL$ and $\theta,\eta:\V\rightarrow \mathord{\bR}(\bV)$ with $\theta \sim^1 \eta$.
Then $\theta(X)\sim\eta(X)$ for some $X\in\V$ and $\theta(Y)=\eta(Y)$ for all $Y\neq X$.
So there must be $\nu,\rho:\V\rightarrow\bV$ with $\theta \bR \nu$, $\eta \bR \rho$ and
$\nu(Y)=\rho(Y)$ for all $Y\neq X$. Since $\nu(X)\sim\theta(X)\sim\eta(X)\sim\rho(X)$ it follows
that $\nu\sim^1\rho$. The conclusion proceeds as above, and the other direction goes likewise.
\end{proof}
The requirement of being a congruence for $\fT(\fL)$ on $\mathord{\bR}(\bV)$ is slightly weaker than that of
being a congruence for $\fT(\fL)$---cf.\ \df{weak congruence}---for it proceeds by restricting
attention to valuations into $\mathord{\bR}(\bV)\subseteq \bU$.
\hfill\P
\weg{
\begin{example}{congruence on T(L)}
Let $\fL$ be a language with two constants \textbf{Yes} and \textbf{No} and a unary operator $\neg$.
Its semantics is given by $\bV=\{0,1\}$, $\textbf{Yes}^\bV=1$, $\textbf{No}^\bV=0$ and $\neg^\bV(b)=1{-}b$.
Let $\fL'$ be the extension of $\fL$ with the constant $\top$ and the semantic value $\top$---so
$\bV'=\{0,1,\top\}$---with $\top^{\bV'}=\top$ and $\neg^{\bV'}(\top)=\top$.
Let $\sim$ be the semantic equivalence on $\bV' \supseteq \bV$ given by $0\not\sim 1 \sim \top$.
Then the identity function $\cal I$ is a translation from $\fL$ into $\fL'$ that is valid up to $\sim$.
This is witnessed by the semantic translation ${\bR} :=\{(0,0),(1,1)\} \subseteq {\sim}$.
The relation $\sim$ is a congruence for $\fL$. In line with \pr{1-hole congruence for image} it also
is a congruence for ${\cal I}(\fL)$ on ${\bR}(\bV)=\{0,1\}$. However it fails to be a congruence
for ${\cal I}(\fL)$ (on $\bU=\{0,1,\top\}$). So by \pr{weak congruence} the transition $\cal I$ is not correct up
to $\sim$. Indeed, for $\rho:\V\rightarrow\bV$ a valuation that sends $X\in \V$ to $1$ and
$\eta:\V\rightarrow\bV'$ a valuation that sends $X$ to $\top$, assuming $\rho(Y)=\eta(Y)$ for other
variables $Y$, one has $\rho \sim \eta$, yet
$\denote{{\cal I}(\neg X)}_{\fL'}(\eta) = \denote{\neg X}_{\fL'}(\eta) = \neg^{\bV'}(\eta(X)) = \top
\not\sim 0 = \neg^{\bV}(\rho(X)) =\denote{\neg X}_{\fL}(\rho)$.
\end{example}
}
\section{A congruence closure property for valid translations}\label{sec:ccproperty}
In many applications, semantic values in the domain of interpretation of a language $\fL$ are only
meaningful up to a semantic equivalence $\sim^c$, and the intended semantic domain could just as
well be seen as the set of $\sim^c$-equivalence classes of values. For this purpose it is essential
that $\sim^c$ is a congruence for $\fL$. Often $\sim^c$ is the congruence closure of a coarser semantic
equivalence $\sim$, so that two values end up being identified iff they are $\sim$-equivalent in
every context. An example of this occurred in \sect{asynpi}, with $\wbb$ in the r\^ole of $\sim$ and
$\cong^c$ in the r\^ole of $\sim^c$. Now \thm{congruence closure of translation}, contributed in
this section, says that if a translation from $\fL$ into $\fL'$ is valid up to $\sim$, then it is
even valid up to an equivalence \plat{$\sim^{1c}_{\fL\!,\bR}$} that extends $\sim^c$ from $\bV$ to a
subdomain $\bW$ of $\bV'$ that suffices for the interpretation of translated expressions from $\fL$.
This equivalence \plat{$\sim^{1c}_{\fL\!,\bR}$}
coincides with the congruence closure of $\sim$ on $\fL$, as well as on $\fT(\fL)$,
and melts each equivalence class of $\bV$ with exactly one of $\bW$, and vice versa.
\\[1ex]
Let $\fL$ and $\fL'$ be languages with
$\denote{\ \ }_{\fL}:\IT_{\fL} \rightarrow ((\V\rightarrow\bV)\rightarrow\bV)$
and
$\denote{\ \ }_{\fL'}:\IT_{\fL'} \rightarrow ((\V\rightarrow\bV')\rightarrow\bV')$.
In this section I assume that $\bV\cap\bV'=\emptyset$. To apply the results to the general case,
just adapt $\fL'$ by using a copy of $\bV'$---any preorder $\asim$ on $\bV\cup\bV'$ extends to this
copy by considering each copied element $\asim$-equivalent to the original.
\begin{definition}{canonical equivalence}
Given any semantic translation $\bR$, let $\mathord{\equiv_{\bR}} \subseteq (\bV\cup\bV')^2$
be the smallest equivalence relation on $\bV\cup\bV'$ containing $\bR$.
\end{definition}
\begin{theorem}{canonical equivalence}
If a translation $\fT$ is correct w.r.t.\ the semantic translation $\bR$, then $\equiv_{\bR}$
is a 1-hole congruence for $\fL$.
\hfill\P
\end{theorem}
\weg{
\begin{proof}
Let $E\in\IT_\fL$ and $\nu,\rho:\V\rightarrow\bV$ with $\nu\equiv_{\bR}^1\rho$.
I have to show that $\denote{E}_\fL(\nu)\equiv_{\bR}\denote{E}_\fL(\rho)$.
Let $X\in\V$ be such that $\nu(X)\equiv_{\bR}\rho(X)$ and $\nu(Y)=\rho(Y)$ for all $Y\neq X$.
Then, for some $n\geq 0$ there are $\val_0,\ldots,\val_n\in\bV$ and $\wal_1,\ldots,\wal_n\in\bV'$ with
$\nu(X)=\val_0 \bR^{-1} \wal_1 \bR \val_1 \bR^{-1} \wal_2 \bR \val_2
\bR^{-1} \ldots \bR \val_n = \rho(X)$.
For $i=0,\ldots,n$ let $\rho_i:\V\rightarrow\bV$ be given by $\rho_i(X)=\val_i$ and $\rho_i(Y)=\rho(Y)$ for $Y\neq X$,
and for $i=1,\ldots,n$ let $\eta_i:\V\rightarrow\bV'$ be given by $\eta_i(X)=\wal_i$ and
$\eta_i(Y)=\eta(Y)$ for $Y\neq X$, for some $\eta:\V\rightarrow\bV'$ with $\eta\bR\rho$.
Then $\nu=\rho_0 \bR^{-1} \eta_1 \bR \rho_1 \bR^{-1}
\eta_2 \bR \rho_2 \bR^{-1} \ldots \bR \rho_n = \rho$.
Hence $\denote{E}_\fL(\rho_0) \bR^{-1} \denote{\fT(\E)}_{\fL'}(\eta_1)
\bR \denote{E}_\fL(\rho_1) \bR^{-1} \denote{\fT(\E)}_{\fL'}(\eta_2) \bR
\denote{E}_\fL(\rho_2) \bR^{-1} \cdots \bR \denote{E}_\fL(\rho_n)$.
Thus $\denote{E}_\fL(\nu)\equiv_{\bR}\denote{E}_\fL(\rho)$.
\end{proof}
}By \pr{1-hole congruence for image} $\equiv_{\bR}$
also is a 1-hole congruence for $\fT(\fL)$ on $\mathord{\bR}(\bV)$.
Only the subset $\mathord{\bR}(\bV)$ of $\bV'$ matters for the purpose
of translating $\fL$ into $\fL'$. On $\bV'\setminus\mathord{\bR}(\bV)$ the equivalence
$\equiv_{\bR}$ is the identity.
\begin{theorem}{congruence closure of translation}
Let $\fT$ be a translation from a language $\fL$, with semantic domain $\bV$,
into a language $\fL'$, with domain $\bV'$, that is valid up to a semantic equivalence $\sim$.
Then $\fT$ is even valid up to a semantic equivalence \plat{$\sim^{1c}_{\fL\!,\bR}$}, contained in $\sim$, such that
(1) the restriction of \plat{$\sim^{1c}_{\fL\!,\bR}$} to $\bV$ is the largest 1-hole congruence for $\fL$ contained in $\sim$,
(2) the set $\bW := \{\val\in\bV'\mid \exists \val\in\bV.~\val'\sim^{1c}_{\fL\!,\bR} \val\}$ is closed under $\fT(\fL)$,
and (3) the restriction of \plat{$\sim^{1c}_{\fL\!,\bR}$} to $\bW$
is the largest 1-hole congruence for $\fT(\fL)$ on $\bW$ that is contained in $\sim$.
\hfill\P
\end{theorem}
\weg{
\begin{proof}
By assumption the translation $\fT$ from $\fL$ into $\fL'$
is correct w.r.t.\ a semantic translation $\mathord{\bR} \subseteq \mathord{\sim}$.
Let $\sim^{1c}_{\fL\!,\bR}$, the \emph{congruence closure} of $\sim$ w.r.t.\ $\fL$ and $\bR$, be
the binary relation on $\bV \cup \bV'$ defined by \plat{$\wal_1 \sim^{1c}_{\fL\!,\bR} \wal_2$} iff
\plat{$\wal_1 \equiv_{\bR} \val_1 \sim^{1c}_\fL \val_2 \equiv_{\bR} \wal_2$} for some $\val_1,\val_2\in\bV$.
Here \plat{$\sim^{1c}_\fL$} is the largest 1-hole congruence for $\fL$, defined on $\bV$, that is contained in $\sim$.
Since $\mathord{\equiv_{\bR}}$ is a 1-hole congruence for $\fL$
contained in $\sim$ (by \thm{canonical equivalence}), and $\sim^{1c}_\fL$ is the
largest 1-hole congruence for $\fL$ contained in $\sim$,
one has $\val \equiv_{\bR} \wal\Rightarrow \val \sim^{1c}_\fL \wal$ for all $\val,\wal\in\bV$.
From this it follows that $\sim^{1c}_{\fL\!,\bR}$ is transitive. As $\equiv_{\bR}$ and
\plat{$\sim^{1c}_\fL$} are reflexive and symmetric, so is \plat{$\sim^{1c}_{\fL\!,\bR}$}. Thus, \plat{$\sim^{1c}_{\fL\!,\bR}$}
is an equivalence relation.
Since \plat{$\sim^{1c}_\fL$} and $\bR$, and hence also $\equiv_{\bR}$, are contained in $\sim$, so is $\sim^{1c}_{\fL\!,\bR}$.
Moreover, \plat{$\mathord{\bR} \subseteq \mathord{\equiv_{\bR}} \subseteq \mathord{\sim^{1c}_{\fL\!,\bR}}$},
so $\fT$ is valid up to \plat{$\sim^{1c}_{\fL\!,\bR}$}.
% , and $\fL'$ is at least as expressive as $\fL$ up to \plat{$\sim^{1c}_{\fL\!,\bR}$}.
It remains to check properties (1)--(3).
Let $E\in \IT_\fL$ be an $\fL$-expression and $\nu,\rho:\V\rightarrow \bV$ be valuations with
$\nu\sim^1 \rho$. Then there are valuations $\nu',\rho':\V\rightarrow\bV$ with
\plat{$\nu \equiv_{\bR}^1 \nu' \mathrel{(\sim^{1c}_\fL)^1} \rho' \equiv_{\bR}^1 \rho$}.
Since $\equiv_{\bR}$ and $\sim^{1c}_\fL$ are 1-hole congruences, it follows that
$\denote{E}_\fL(\nu)\equiv_{\bR}\denote{E}_\fL(\nu')\sim^{1c}_\fL\denote{E}_\fL(\rho')\equiv_{\bR}
\denote{E}_\fL(\rho)$, so $\denote{E}_\fL(\nu)\sim^{1c}_{\fL\!,\bR}\denote{E}_\fL(\rho)$. Thus
\plat{$\sim^{1c}_{\fL\!,\bR}$} is a 1-hole congruence for $\fL$ on $\bV$. Since \plat{$\sim^{1c}_\fL$} is the
largest 1-hole congruence for $\fL$ contained in $\sim$, it follows that, restricted to $\bV$,
${\sim^{1c}_{\fL\!,\bR}} \subseteq {\sim^{1c}_\fL}$. By the reflexivity of $\equiv_{\bR}$ one moreover has
${\sim^{1c}_{\fL}} \subseteq {\sim^{1c}_{\fL\!,\bR}}$, so \plat{${\sim^{1c}_{\fL\!,\bR}} = {\sim^{1c}_\fL}$},
i.e.\ (1) holds.
Let $\bW := \{\wal\in\bV'\mid \exists \val\in\bV.~\wal\sim^{1c}_{\fL\!,\bR} \val\}$.
By definition, $\bW = {\bR}(\bV)$. So by \pr{closed} $\bW$ is closed under $\fT(\fL)$,
i.e.\ (2) holds.
By \pr{1-hole congruence for image} \plat{$\sim^{1c}_{\fL\!,\bR}$}
is a 1-hole congruence for $\fT(\fL)$ on $\bW = \mathord{\bR}(\bV)$, contained in $\sim$.
Let $\approx$ be any other 1-hole congruence on $\bW$ contained in $\sim$.
Define the relation $\approx_{\bR}$ on $\bV\cup\bW$ by \plat{$\val_1 \approx_{\bR} \val_2$} iff
\plat{$\val_1 \equiv_{\bR} \wal_1 \approx \wal_2 \equiv_{\bR} \val_2$} for some
$\wal_1,\wal_2\in{\bW}$, and let $\approx_{\bR}^*$ be its transitive closure.
Then $\approx_{\bR}^*$ is an equivalence relation on $\bV\cup\bW$.
Since $\equiv_{\bR}$ and $\approx$ are 1-hole congruences for $\fT(\fL)$ on $\bW$, by the same
reasoning as above also \plat{$\approx_{\bR}^*$} is a 1-hole congruence for $\fT(\fL)$ on $\bW$.
As \plat{$\mathord{\bR} \subseteq \mathord{\equiv_{\bR}} \subseteq {\approx_{\bR}^*}$},
by \pr{1-hole congruence for image}, \plat{$\approx_{\bR}^*$} is a 1-hole congruence for $\fL$.
Since \plat{$\sim^{1c}_\fL$} is the largest 1-hole congruence for $\fL$ contained in $\sim$, it
follows that, restricted to $\bV$, ${\approx_{\bR}^*} \subseteq {\sim^{1c}_\fL}$.
For each $\wal_1,\wal_2\in\bW$ with $\wal_1 \approx \wal_2$ there are $\val_1,\val_2\in\bV$ with
\plat{$\val_1 \equiv_{\bR} \wal_1 \approx \wal_2 \equiv_{\bR} \val_2$}. So $\val_1 \approx_{\bR} \val_2$
and hence $\val_1 \sim^{1c}_\fL \val_2$, and thus \plat{$\wal_1 \sim^{1c}_{\fL\!,\bR} \wal_2$}, by definition.
So ${\approx} \subseteq {\sim^{1c}_{\fL\!,\bR}}$ and (3) holds.
\end{proof}
}Note that each equivalence class of \plat{$\sim^{1c}_{\fL\!,\bR}$} on $\bV \cup \bW$ melts an equivalence
class of $\sim^{1c}_{\fL\!,\bR}$ on $\bV$ with one of \plat{$\sim^{1c}_{\fL\!,\bR}$} on $\bW$.
Moreover, on $\bV$ the relation is completely determined by $\fL$ and $\sim$.
% The following example shows that
However, in general the whole relation \plat{$\sim^{1c}_{\fL\!,\bR}$} is not
completely determined by $\fL$ and $\sim$.
\hfill\P
\weg{
\begin{example}{congruence closure not determined by L and sim}
Let $\fL$ be a language with two constants \textbf{Yes} and \textbf{No} and a binary operator \textbf{same}.
Its semantics is given by $\bV=\{0,1,\top,\bot\}$, $\textbf{Yes}^\bV=1$, $\textbf{No}^\bV=0$ and
$\textbf{same}^\bV(x,y)=1$ if $x=y$, while $\textbf{same}^\bV(x,y)=0$ if $x\neq y$.
The semantic values $\top$ and $\bot$ are not denotable as the interpretation of closed terms.
Let $\fL'$ be an exact copy of $\fL$, except that the semantic values are primed.
Let $\sim$ be the semantic equivalence on $\bV \cup \bV'$ given by
$0 \sim 0' \not\sim 1 \sim 1' \not\sim \top \sim \top' \sim \bot \sim \bot'$.
Then the identity function $\cal I$ is a translation from $\fL$ into $\fL'$ that is valid up to $\sim$.
This is witnessed by the semantic translation ${\bR}^\dagger :=\{(0',0),(1',1),(\top',\bot),(\bot',\top)\} \subseteq {\sim}$,
or, alternatively, by the semantic translation ${\bR} :=\{(0',0),(1',1),(\top',\top),(\bot',\bot)\} \subseteq {\sim}$.
Upon taking the congruence closure $\sim^1_\fL$, the four semantic values of $\bV$ become
inequivalent. Yet, there are two candidates for \plat{$\sim^{1c}_{\fL\!,\bR}$}, namely $\bR^\dagger$ and $\bR$.
\end{example}
}
\begin{corollary}{congruence closure of translation}
Let $\fT$ be a translation from a language $\fL$, with semantic domain $\bV$,
into a language $\fL'$, with domain $\bV'$, valid up to a semantic equivalence $\sim$,
and suppose the congruence closure $\sim_\fL^1$ of $\sim$ w.r.t.\ $\fL$ is in fact a congruence.
Then $\fT$ is correct up to the equivalence \plat{$\sim^{1c}_{\fL\!,\bR}$} described in
\thm{congruence closure of translation}.
\hfill\P
\end{corollary}
\weg{
\begin{proof}
By the proof of \thm{congruence closure of translation} $\fT$ is correct w.r.t.\ the semantic
translation \plat{${\bR} \subseteq {\sim^{1c}_{\fL\!,\bR}}$}, the restriction of \plat{$\sim^{1c}_{\fL\!,\bR}$} to $\bV$
equals $\sim_\fL^1$, and ${\bR}(\bV)=\bW$. Using that $\sim_\fL^1$ is a congruence for $\fL$, by
\pr{1-hole congruence for image} \plat{$\sim^{1c}_{\fL\!,\bR}$} is a congruence for $\fT(\fL)$ on ${\bR}(\bV)$.
Since ${\bR}(\bV)=\bW$, which for \plat{$\sim^{1c}_{\fL\!,\bR}$} is the $\bU$ used in \df{weak congruence},
\plat{$\sim^{1c}_{\fL\!,\bR}$} is a congruence for $\fT(\fL)$.
So by \thm{valid correct}, $\fT$ is correct up to \plat{$\sim^{1c}_{\fL\!,\bR}$}.
\end{proof}
}
The languages $\pi$ and $\rm a\pi$ of \sect{asynpi} do not feature operators (or other constructs)
of infinite arity. Hence the congruence closure $\sim_\pi^{1c}$ or $\sim_{\rm a\pi}^{1c}$ of an
equivalence $\sim$ on $\pi$ or $\rm a\pi$ is always a congruence.
So by \cor{congruence closure of translation} Boudol's translation $\fT$ is correct up to an equivalence \plat{$\wbb_{\pi,{\bR}}^c$},
defined on the disjoint union of the domains $\T_\pi$ and $\T_{\rm a\pi}$ on which the two languages are
interpreted. This equivalence is contained in $\wbb$, and on the source domain $\T_\pi$ coincides
with $\cong^c$. By \thm{congruence closure of translation}, the restriction of $\wbb_{\pi,{\bR}}^c$
to a subdomain $\bW\subseteq \T_{\rm a\pi}$ is the largest congruence for $\fT(\pi)$ on $\bW$ that is contained in $\sim$.
As $\cong^c_{\rm a}$ is a congruence for all of $\rm a\pi$ on all of $\T_{\rm a\pi}$, and contained
in \plat{$\wbb$}, it is certainly a congruence for $\fT(\pi)$ on $\bW$, and thus contained in \plat{$\wbb_{\pi,{\bR}}^c$}.
This inclusion turns out to be strict.
As an illustration of that, note that $\bar x z.\textbf{0} | \bar x z.\textbf{0} \cong^c \bar xz.\bar x z \textbf{0}$.
(This follows since these processes are strong (early) bisimilar \cite{SW01book} and thus strong
full bisimilar by \cite[Def. 2.2.2]{SW01book}.)
Consequently, their translations must be related by \plat{$\wbb_{\pi,{\bR}}^c$}. So, for distinct
$u,v,y,w,x,z \in\N$,\vspace{-13.6pt}
{\small
$$(u)(\bar{x}u | u(v).(\bar{v}z | \textbf{0})) \big| (u)(\bar{x}u | u(v).(\bar{v}z | \textbf{0})) \wbb_{\pi,{\bR}}^c
(y)(\bar{x}y | u(w).(\bar{w}z | (u)(\bar{x}u | u(v).(\bar{v}z | \textbf{0})) )). $$}%
Yet, these processes are not $\cong^c_{\rm a}$-equivalent, as can be seen by putting them in a
context $x(y).x(y).\bar r(s) | X$. \weg{In this context,}There, only the left-hand side has a weak barb
$\Downarrow_{\bar r}$.
\section{Integrating language features through translations}\label{sec:integrating}
The results of the previous section show how valid translations are satisfactory for comparing the
expressiveness of languages. If there is a valid translation $\fT$ from $\fL$ to $\fL'$ up to $\sim$,
and (as usual) $\sim^{1c}_\fL$ is a congruence, then all truths that can be expressed in terms of
$\fL$ can be mimicked in $\fL'$. For the congruence classes of $\sim^{1c}_\fL$ translate bijectively
to congruence classes of an induced equivalence relation on the domain of $\fT(\fL)$ (within the
domain of $\fL'$), and all operations on those congruence classes that can be performed by contexts of
$\fL$ have a perfect counterpart in terms of contexts of $\fT(\fL)$. This state of affairs was
illustrated on Boudol's translation from a synchronous to an asynchronous $\pi$-calculus.
There is however one desirable property of translations between languages that has not yet been
achieved, namely to combine the powers of two languages into one unified language.
If both languages $\fL_1$ and $\fL_2$ have valid translations into a language $\fL'$,
then all that can be done with $\fL_1$ can be mimicked in a fragment of $\fL'$, and
all that can be done with $\fL_2$ can be mimicked in another fragment of $\fL'$.
In order for these two fragments to combine, one would like to employ a single congruence relation
on $\fL'$ that specialises to congruence relations for $\fT_1(\fL_1)$ and $\fT_2(\fL_2)$,
which form the counterparts of relevant congruence relations for the source languages
$\fL_1$ and $\fL_2$.
In terms of the translation $\fT$ from $\pi$ to $\rm a\pi$, the equivalence $\cong^c_{\rm a}$ on
$\T_{\rm a\pi}$ would be the right congruence relation to consider for $\rm a\pi$.
Ideally, this congruence would extend to an equivalence $\cong^c_{\pi,\rm a\pi}$ on the disjoint
union $\T_\pi \uplus \T_{a\pi}$, such that the restriction of $\cong^c_{\pi,\rm a\pi}$ to $\T_\pi$
is a congruence for $\pi$. Necessarily, this congruence on $\T_\pi$ would have to distinguish the
terms $\bar x z.\textbf{0} | \bar x z.\textbf{0}$ and $\bar xz.\bar x z \textbf{0}$, since their
translations are distinguished by $\cong^c_{\rm a}$. One therefore expects $\cong^c_{\pi,\rm a\pi}$
on $\T_\pi$ to be strictly finer than $\cong^c$. Here it is important that the union
of $\T_\pi$ and $\T_{a\pi}$ on which this congruence is defined is required to be disjoint.
For if one considers $\T_{a\pi}$ as a subset of $\T_\pi$, then we obtain that the restriction of
$\cong^c_{\pi,\rm a\pi}$ to that subset (1) coincides with $\cong^c_{\rm a}$ and (2) is strictly
finer than $\cong^c$. This contradicts the fact that $\cong^c$ is strictly finer than $\cong^c_{\rm a}$.
In \sect{compositionality} I will show that such a congruence $\cong^c_{\pi,\rm a\pi}$ indeed exists.
In fact, under a few very mild conditions this result holds generally, provided that the source
language $\fL$ is a closed-term language.
\hfill\P
\weg{The following example illustrated why that restriction needs to be imposed.
\begin{example}{reflection}
Let $\fL$ be a language with three constants $\top$, \textbf{Yes} and \textbf{No}.
Its semantics is given by $\bV=\{+,-\}$, $\top^\bV =\textbf{Yes}^\bV=+$ and $\textbf{No}^\bV=-$.
Let $\fL'$ be a language with the same three constants and a unary operator \textbf{next}.
Its semantics is given by $\bV'=\{0,1,2\}$ with $\top^{\bV'}=2$, $\textbf{Yes}^{\bV'}=1$ and
$\textbf{No}^{\bV'}=0$, while $\textbf{next}^{\bV'}(n)=(n+1) \textsf{mod}\,3$.
Let $\sim$ be the semantic equivalence on $\bV' \cup \bV$ given by $- \sim 0 \not\sim 1 \sim 2 \sim +$.
Then the identity function $\cal I$ is a translation from $\fL$ into $\fL'$ that is valid up to $\sim$.
This is witnessed by the semantic translation ${\bR} :=\{(0,-),(1,+),(2,+)\} \subseteq {\sim}$.
The congruence closure of $\sim$ on $\bV'$ is the identify relation. This relation cannot be
extended to $\bV \cup \bV'$ in such a way that $\fT$ remains valid. For $1$ and $2$ need to be
different; yet to make $\fT$ valid both need to be related to $+$.
\end{example}
}
\section{A unique decomposition of terms}\label{sec:standard heads}
The results of \sect{compositionality} apply only to languages satisfying
two postulates, formulated below, and to preorders $\asim$ that ``respect $\eqa$'', defined in \sect{invariance}.
% Below and in \sect{invariance} I formulate these postulates.
\begin{definition}{alpha}
\emph{$\alpha$-conversion} is the act of renaming all occurrences of a bound variable $X$ within the
scope of its binding into another variable, say $Y$, while avoiding capture of free variables. Here
one speaks of \emph{capture} when a free occurrence of $Y$ turns into a bound one.
Write $E \eqa F$ if expression $E$ can be converted into $F$ by \weg{multiple }acts of $\alpha$-conversion.
\end{definition}
In languages where there are multiple types of bound variables, $\eqa$ allows conversion of all of them.
In a $\pi$-calculus with recursion, for instance, there could be bound process variables $X\mathbin\in\V$ as well
as bound names $x\mathbin\in\N$.
The last two conversions in the right column of \df{structural congruence} define $\alpha$-conversion for \weg{$\pi$-calculus }names.
\begin{postulatec}{standard head}{\cite{vG12}, paraphrased}
There exists a class of expressions called \emph{standard heads}, and a class of substitutions
called \emph{standard substitutions}, such that for each expression $E$, if not a variable, there
are unique standard heads $H$ and substitutions $\sigma$ such that $E \eqa H[\sigma]$.
\end{postulatec}
A term $f(c,g(c))$, for instance, can be written as $H[\sigma]$ where $H=f(X_1,X_2)$ is a head, and
$\sigma:\{X_1,X_2\}\rightarrow\IT_\fL$ is given by $\sigma(X_1)=c$ and $\sigma(X_2)=g(c)$. The head $H$ is
standardised by means of a particular (arbitrary) choice for its argument variables $X_1$ and $X_2$.
$\sigma$ is standardised through a particular choice of the bound variables that may occur in the
expressions $\sigma(X)$.
A head for a recursive expression $\mu X.f(g(c),g(g(X)))$ is $\mu X.f(Y,g(g(X)))$.
See \cite{vG12} for further detail.
This postulate is easy to show for each common type of system description language, and I am not
aware of any counterexamples. However, while striving for maximal generality, I consider
languages with (recursion-like) constructs that are yet to be invented, and in view of
those, this principle has to be postulated rather than derived.
\section[Invariance of meaning under alpha-conversion]
{Invariance of meaning under $\alpha$-conversion}\label{sec:invariance}
Write $\val \eqa_{\fL} \wal$, with $\val,\wal\in \bV$, iff there are terms $E,F\in\IT_\fL$ with $E\eqa F$, and a valuation
$\zeta:\V\rightarrow\bV$ such that $\denote{E}_\fL(\zeta)=\val$ and $\denote{F}_\fL(\zeta)=\wal$.
This relation is reflexive and symmetric.
In \cite{vG12} I limited attention to languages satisfying\vspace{-1ex}
\begin{equation}\label{alpha}\textit{
if $E\eqa F$ then $\denote{E}_\fL=\denote{F}_\fL$.}\vspace{-1ex}
\end{equation}
This postulate says that the meaning of an expression is invariant under $\alpha$-conversion.
% This postulate was used only twice in \cite{vG12}, namely implicitly the statement of
% (\ref{inductive meaning}) and in the last line of the proof of Theorem 3.
It can be reformulated as the requirement that $\eqa_{\fL}$ is the identity relation.
This postulate is satisfied by all my intended applications, except for the important class
of closed-term languages.
Languages like CCS and the $\pi$-calculus can be regarded as falling
in this class (although it is also possible to declare the meaning of a term under a valuation to be
an $\eqa$-equivalence class of closed terms).
To bring this type of application within the scope of my theory, here
I weaken this postulate by requiring merely that $\eqa_{\fL}$ is an equivalence.
\begin{postulate}{alpha}
$\eqa_\fL$ is an equivalence relation.\pagebreak[3]
\end{postulate}
This postulate is needed in \sect{compositionality}.
I also need to restrict attention to preorders $\asim$ with $\mathord{\eqa_\fL} \subseteq \mathord{\asim}$.
When that holds I say that the preorder $\asim$ \emph{respects} $\eqa_\fL$.
If (\ref{alpha}) holds---which strengthens of \pos{alpha}---then \emph{any} preorder respects $\eqa_\fL$.
\section{Compositionality}\label{sec:compositionality}
An important property of translations, defined below, is \emph{compositionality}.
In this section show I that any valid translation up to a preorder $\asim$ can be modified into such
a translation that moreover is compositional, provided one restricts attention to languages
that satisfy Postulates~\ref{post:standard head} and~\ref{post:alpha}, and preorders $\asim$ that respect $\eqa$.
\begin{definition}{compositionality}
A translation $\fT$ from $\fL$ into $\fL'$ is \emph{compositional} if
\begin{enumerate}[(1)]
\item\label{comp1}
$\fT(E[\sigma])\eqa \fT(E)[\fT\circ\sigma]$ for each $E\in\IT_\fL$ and $\sigma:\fv(E)\rightarrow\IT_\fL$,
\item\label{comp2}
$E\eqa F$ implies $\fT(E) \eqa \fT(F)$ for all $E,F\in\IT_\fL$,
\item\label{comp3}
and moreover $\fT(X)=X$ for each $X\in\V$.
\end{enumerate}
\end{definition}
In case $E=f(t_1,\ldots,t_n)$ for certain $t_i\in\IT_\fL$ this amounts to
$\fT(f(t_1,\ldots,t_n)) \eqa E_f(\fT(t_1),\ldots,\fT(t_n))$,
where $E_f:=\fT(f(X_1,\ldots,X_n))$ and $E_f(u_1,\ldots,u_n)$ denotes the result of the simultaneous
substitution in this expression of the terms $u_i\in\IT_{\fL'}$ for the free variables $X_i$,
for $i=1,\ldots,n$. The first requirement of \df{compositionality} is more general and covers
language constructs other than functions, such as recursion. Requiring equality rather than $\eqa$
is too demanding.
\hfill\P
\weg{, as the following example illustrates.
\begin{example}{alpha compositionality}
Take a source language $\fL$ that features an unary replication operator $!$, as in the
$\pi$-calculus, and a target language $\fL'$ that instead has a recursion construct $\mu X.E$,
as in CCS; both languages have a constant $0$. A suitable translation $\fT$ satisfies
$\fT(!X_1) = \mu X. (X|X_1)$ and $\fT(0)\mathbin=0$.
Applying \df{compositionality} with $\sigma(X_1)=0$ gives $\fT(!0) \eqa \mu X. (X|0)$, whereas
applying it with $\sigma(X_1)=X$ gives $\fT(!X) \eqa \mu Y. (Y|X)$.
Here the bound variable $X$ needed to be renamed (into $Y$) to avoid capture of the free
variable $X$ that is substituted for $X_1$. Furthermore, applying \df{compositionality} on
$\fT(!X) \eqa \mu Y. (Y|X)$ with $\sigma(X)=0$ gives $\fT(!0) \eqa \mu Y. (Y|0)$. Since $X\neq Y$,
this shows that $\eqa$ cannot consistently be replaced by $=$.
\end{example}
}
\begin{lemma}{composition is compositional}
If $\fT_1:\IT_{\fL_1} \rightarrow \IT_{\fL_2}$ and $\fT_2:\IT_{\fL_2} \rightarrow \IT_{\fL_3}$ are
compositional translations, then so is their composition
$\fT_2\circ\fT_1:\IT_{\fL_1}\rightarrow\IT_{\fL_3}$, defined by
$\fT_2\circ\fT_1(E):=\fT_2(\fT_1(E))$ for all $E\in\fL_1$.
\end{lemma}
\begin{proof}
(1) $\fT_2(\fT_1(E[\sigma]))\eqa \fT_2(\fT_1(E)[\fT_1\circ\sigma]) \eqa
\fT_2(\fT_1(E))[\fT_2\circ\fT_1\circ\sigma])$ for each $\sigma:\V\rightharpoonup\IT_{\fL_1}$ and $E\in\IT_{\fL_1}$.
Here the derivation of the first $\eqa$ uses Property \ref{comp2} of \df{compositionality}---and
this is the reason for requiring that property.
(2) $E\mathbin{\eqa} F$ implies $\fT_1(E) \mathbin{\eqa} \fT_1(F)$ and $\fT_2(\fT_1(E)) \eqa \fT_2(\fT_1(F))$ for
all $E,F\mathbin\in\IT_\fL$.
(3) $\fT_2(\fT_1(X)) = \fT_2(X)=X$ for each $X\in\V$.
\end{proof}
\begin{theorem}{compositionality}
Let $\fL$ and $\fL'$ be languages that satisfy Postulates~\ref{post:standard head} and~\ref{post:alpha},
and $\asim$ a preorder that respects $\eqa_\fL$ and $\eqa_{\fL'}$.
If any valid (or correct) translation from $\fL$ into $\fL'$ up to $\asim$ exists,
then there exists a compositional translation that is valid (or correct) up to $\asim$.
\hfill\P
\end{theorem}
Hence, for the purpose of comparing the expressive power of languages,
valid translations between them can be assumed to be compositional.
For correct translations this was already established in \cite{vG12}, but assuming (\ref{alpha}),
a stronger version of \pos{alpha}.
I can now establish the theorem promised in \sect{integrating}.
In view of \thm{compositionality}, no great sacrifices are made by assuming that the translation
$\fT$ is compositional. Other ``mild conditions'' needed are
\pos{alpha} for $\fL'$ and $\approx$ respecting $\eqa_{\fL'}$.
\begin{theorem}{pulling back congruences}
Let $\fL$ be a closed-term language and $\fL'$ a language that satisfies \pos{alpha}.
Let $\fT$ be a compositional translation from $\fL$ into $\fL'$ that is valid up to $\sim$.
Let $\approx$ be any congruence for $\fL'$ containing $\eqa_{\fL'}$ and contained in $\sim$.
Then $\fT$ is correct up to an equivalence $\approx_{\fT}$ on $\bV \cup \bV'$, contained in
$\sim$, that on $\bV'$ coincides with $\approx$.
\hfill\P
\end{theorem}
\weg{
\begin{proof}
Let $\equiv_{\fT}$ be the smallest equivalence relation on $\bV \cup \bV'$ such that
$\denote{\fT(p)}_{\fL'} \equiv_{\fT} \denote{p}_\fL$ for all $p\in\T_\fL$.
Since $\fT$ is valid up to $\sim$ there must be a semantic translation ${\bR}\subseteq{\sim}$ such
that $\denote{\fT(p)}_{\fL'} \bR \denote{p}_\fL$ for all $p\in\T_\fL$. Hence ${\equiv_{\fT}} \subseteq {\sim}$.
Define $\approx_{\fT}$ on $\bV \cup \bV'$ by \plat{$\val_1 \approx_{\fT} \val_2$} iff
\plat{$\val_1 \equiv_{\fT} \wal_1 \approx \wal_2 \equiv_{\fT} \val_2$} for some $\wal_1,\wal_2\in{\bV'}$.
Then ${\approx_{\fT}} \subseteq {\sim}$.
Since $\fL$ is a closed-term language, for each $\val \in \bV$ there is exactly one $p\in \T_\fL$ with $\denote{p}_\fL=\val$.
Hence, each $\equiv_{\fT}$-equivalence class on $\bV \cup \bV'$ contains exactly one element of $\bV'$.
It follows that $\approx_{\fT}$ is transitive, and hence an equivalence relation. Moreover, on $\bV'$
it coincides with $\approx$. It remains to show that $\fT$ is valid up to $\approx_{\fT}$.
For then \thm{valid correct} implies that $\fT$ is correct up to $\approx_{\fT}$.
Let $\bR_\fT := \{(\denote{\fT(p)}_{\fL'},\denote{p}_\fL) \mid p \in\T_\fL\}$.
Then $\bR_\fT$, and hence $\bR_\fT^\alpha$, is a semantic translation.\vspace{1pt}
I claim that ${\bR_\fT^\alpha} \subseteq {\approx_\fT}$.
For if $\val_1 \eqa \val_2 \bR_\fT \wal_2 \eqa \wal_1$ then there are terms $E,F \in\IT_\fL$ with $E \eqa F$
and a valuation $\zeta:\V \rightarrow\bV$ such that $\denote{E}_\fL(\zeta)=\val_1$ and $\denote{F}_\fL(\zeta)=\val_2$.
Let $\sigma:\V \rightarrow \T_\fL$ be the unique substitution such that $\zeta(X)=\denote{\sigma(X)}_\fL$ for all $X\in \V$,
i.e.\ $\zeta=\denote{\sigma}_\fL$. Then
$\val_1=\denote{E}_\fL(\denote{\sigma}_\fL)=\denote{E[\sigma]}_\fL$, using (\ref{inductive meaning}),
and likewise $\val_2=\denote{F[\sigma]}_\fL$. So $\wal_2=\denote{\fT(F[\sigma])}_{\fL'}$.
Since $E\eqa F$, also $E[\sigma] \eqa F[\sigma]$, and hence $\fT(E[\sigma]) \eqa \fT(F[\sigma])$ by compositionality.
Thus $\val_1 =\denote{E[\sigma]}_\fL \equiv_\fT \denote{\fT(E[\sigma])}_{\fT'} \eqa \denote{\fT(F[\sigma])}_{\fL'} = \wal_2 \eqa \wal_1$,
and hence $\val_1 \approx_\fT \wal_1$.
To show validity of $\fT$ up to $\approx_{\fT}$ it suffices to establish that $\fT$ is correct w.r.t.\ $\bR_\fT^\alpha$.
So let $E\in\IT_\fL$ and let $\eta,\bar\eta:\V\!\rightarrow\bV'$ and $\bar\rho,\rho:\V\! \rightarrow \bV$
be valuations with $\eta \eqa \bar\eta \bR_\fT \bar\rho \eqa \rho$.
I have to show that $\denote{\fT(\E)}_{\fL'}(\eta) \bR_\fT \denote{\E}_\fL(\rho)$.
Let \mbox{$\sigma:\V\rightarrow \T_\fL$} be the unique substitution such that
$\bar\rho(X)=\denote{\sigma(X)}_\fL$ for all $X\in \V$, and define \mbox{$\sigma':\V\rightarrow \T_{\fL'}$} by
$\sigma'(X)=\fT(\sigma(X))$, i.e., $\sigma'=\fT\circ\sigma$.\vspace{1pt} Then $\bar\eta(X)=\denote{\sigma'(X)}$
for all $X$, i.e., $\bar\eta=\denote{\sigma'}_{\fL'}$, and thus $\eta\eqa\denote{\fT\circ\sigma}_{\fL'}$.
So, using \lem{alpha congruence}, (\ref{inductive meaning}) and compositionality,
\[\denote{\fT(\E)}_{\fL'}(\eta) \eqa \denote{\fT(\E)}_{\fL'}(\denote{\fT\circ\sigma}_{\fL'}) \eqa
\denote{\fT(\E)[\fT\circ\sigma])}_{\fL'} \eqa {}\]
\hfill ~~~~$\denote{\fT(\E[\sigma])}_{\fL'} \bR_\fT \denote{\E[\sigma]}_\fL \eqa
\denote{\E}_\fL(\denote{\sigma}_{\fL}) = \denote{\E}_\fL(\bar\rho) \eqa \denote{\E}_\fL(\rho)$.
\end{proof}
}
\section{Related work}\label{sec:related}
\newcommand{\So}{{\rm S}}
\newcommand{\Ta}{{\rm T}}
The concept of \emph{full abstraction} stems from Milner \cite{Mi75}. It indicates a satisfactory connection
between a denotational and an operational semantics of a language.
Riecke \cite{Rie91} and Shapiro \cite{Sha91} adapt this notion to translations between languages.
\begin{definition}{Full Abstraction}
A translation $ \fT \!: \IT_{\fL_\So} \rightarrow \IT_{\fL_\Ta} $ is \emph{fully abstract} w.r.t.\ the equivalences
$ {\sim_\So} \mathbin\subseteq \T_{\fL_\So}^2 $ and $ {\sim_\Ta} \mathbin\subseteq \T_{\fL_\Ta}^2 $ if, for all
$ \p, Q \in \T_{\fL_\So} $,
$ \p \sim_\So Q \Leftrightarrow \fT(\p) \sim_\Ta \fT(Q).$
\end{definition}
In \cite{Rie91,Sha91}, $\sim_\So$ and $\sim_\Ta$ are required to be congruence closures---see
\cite{translations} for more detail. The simplified definition above was used in \cite{NestmannP00,Nestmann00,BPV05}.
Fu~\cite{Fu16} bases a theory of expressiveness on full abstraction, with a
divergence-preserving form of barbed branching bisimilarity \cite{GLT09b} in the r\^ole of $\sim_\So$ and $\sim_\Ta$.
A comparison of full abstraction with the approach of the present paper appears in \cite{translations}.
In the last twenty years, a great number of encodability and separation results have
appeared, comparing CCS, Mobile Ambients, and several versions of the $\pi$-calculus (with
and without recursion; with mixed choice, separated choice or asynchronous)
\cite{%
San93,% % encoding (barbed congruence)
%Jen94,% % encoding priority
Boreale98,% % encoding (barbed eq.)
Parrow00,% % encoding (weak bis)
NestmannP00,% % border between encoding (coupled) and separation, following separation of Palamidessi03
Palamidessi03,% % separation (asyn pi and full pi; pi and CCS (any reasonble equiv.))
Nestmann00,% % border between encoding and separation, following separation of Palamidessi03
CardelliG00,% % expressiveness not the main issue
%CardelliGG02,% % expressiveness not the main issue
BusiGZ09,% % separation and encoding (weak bis); stated to contain BusiGZ03 and 04
CarboneM03,% % encoding and separation
%BPV04,% % encoding (may testing)
BPV05,% % encoding (may testing)
%Palamidessi05,% % border between encoding and separation; recursion; overview
PalamidessiSVV06,% % encoding (weak bis) and separation
PV06,% % separation
%CCP07,% % separation (a\pi versus \pi; must testing; conflicts with Lippert13?)
VPP07,% % separation (overview with unified approach)
CCAV08,% % separation (testing, contrast with PalaSVV06)
%HMP08,% % separation (following CarboneM03)
%PV08,% % separation
%VBG09,% % separation - extended version of VBG07
%LPSS10,% % encoding
%PSN11,% % separation (acc. Gorla + causality)
PN12,% % border between encoding and separation, following separation of Palamidessi03
PNG13,% % causality
%EPTCS160.2}% % encoding with strong operational correspondence
EPTCS190.5,% % CCS vs CSP; Gorla but not compositional
GW14,% % separation
EPTCS160.4,% % separation
EPTCS189.9,% % encoding/separation
%GWL16,% % encoding/separation
PN16% % encoding/separation
%PP16% % separation
}; see
\cite{Gorla10b}, \cite{Gorla10a} for an overview. Many of these results employ different and
somewhat ad-hoc criteria on what constitutes a valid encoding, and thus are hard to
compare with each other.
Several of these criteria are discussed and compared in \cite{Parrow08} and \cite{Peters12}.
Gorla \cite{Gorla10a} collected some essential features of
these approaches and integrated them in a proposal for a valid encoding that justifies
most encodings and some separation results from the literature.
Like Boudol \cite{Bo85} and the present paper, Gorla requires a compositionality condition
for encodings. However, his criterion is weaker than mine (cf.\ \df{compositionality}) in
that the expression $E_f$ encoding an operator $f$ may be dependent on the set of names
occurring freely in the expressions given as arguments of $f$. This issue is further discussed in \cite{vG12}.
It is an interesting topic for future research to see if there are any valid encodability
results \`a la \cite{Gorla10a} that suffer from my proposed strengthening of compositionality.
The second criterion of \cite{Gorla10a} is a form of invariance under name-substitution.
It serves to partially undo the effect of making the compositionality requirement
name-dependent. In my setting I have not yet found the need for such a condition.
In \cite{vG12} I argue that this criterion as formalised in \cite{Gorla10a} is too restrictive.
The remaining three requirements of Gorla (the `semantic' requirements) are very close to an instantiation of mine with a particular
preorder $\asim$. If one takes $\asim$ to be weak barbed bisimilarity with explicit divergence
(i.e.\ relating divergent states with divergent states only), using barbs external to the language,
as discussed in \sect{asynpi}, then an valid translation in my sense satisfies Gorla's semantic
criteria, provided that the equivalence $\equiv$ on the target language that acts as a parameter in
Gorla's third criterion is also taken to be weak barbed bisimilarity with explicit divergence.
The precise relationships between the proposals of \cite{vG12} and \cite{Gorla10a} are further
discussed in \cite{EPTCS190.4}.
Further work is needed to sort out to what extent the two approaches have
relevant differences when evaluating encoding and separation results from the literature.
Another topic for future work is to sort out how dependent known encoding and separation
results are on the chosen equivalence or preorder.
\providecommand{\doi}[1]{doi:\href{http://dx.doi.org/#1}{#1}}
\renewcommand{\url}[1]{\href{#1}{#1}}
\bibliographystyle{eptcs}
\bibliography{fossacs}
\end{document}
Notation:
\IT set of open terms
\T set of closed terms
\fL language
\fT translation
\D set of denotable objects
E,F,G expression or open term
t_i,u_i more open terms
f operator in a language
n arity of f
i typical index
\val,\wal value in domain of interpretation
X,Y variables
\V set of variables
C collection of congruences
P (closed) process expression
\bR semantic translation
\bT semantic counterpart of a translation
\bU common subdomain
\bV domain of values
\bW subdomain
\bZ unifying domain
\rho,\nu,\zeta: \V->\bV
\eta,\theta: \V->\bU,\bV'
\sigma,\xi(,\nu): \V->\T_\fL
p,q elements of \bZ
________From encodings________
\bD (quotient) domain
\bC (quotient) domain
\bW domain of values
G process graph
G_P process graph of P
S set of states
Act alphabet of actions