\documentstyle[hyperref]{article}
\def\titlesize{\setlength{\baselineskip}{18pt}\xviipt}
\def\ninesize{\setlength{\baselineskip}{10pt}\ixpt}
\def\normalsize{\setlength{\baselineskip}{11pt}\xpt}
\textwidth 342 pt
\textheight 46 pc
\unitlength 1 mm % This is used in pictures
\pagestyle{myheadings} % Headers slanted lowercase
\markboth{On the Expressiveness of ACP}{} % Title on the left
\newcommand{\msection}[1]{\section[#1]{\setlength % and sections on the right
{\baselineskip}{16pt}#1}\markright{\thesection\hspace{1em}#1}\normalsize}
\renewenvironment{abstract}{\begin{list}{\hspace{\labelsep}}
{\rightmargin\leftmargin
\listparindent 1.5em
\parsep 0pt plus 1pt}
\ninesize\item}{\end{list}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%% Theorem-like environments %%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newtheorem{defi}{Definition}
\newtheorem{theo}{Theorem}
\newtheorem{prop}{Proposition}
\newtheorem{lemm}{Lemma}
\newtheorem{coro}{Corollary}
\newtheorem{exam}{Example}
\newenvironment{definition}[1]{\begin{defi} \rm \label{df-#1} }{\end{defi}}
\newenvironment{theorem}[1]{\begin{theo} \rm \label{th-#1} }{\end{theo}}
\newenvironment{proposition}[1]{\begin{prop} \rm \label{pr-#1} }{\end{prop}}
\newenvironment{lemma}[1]{\begin{lemm} \rm \label{lem-#1} }{\end{lemm}}
\newenvironment{corollary}[1]{\begin{coro} \rm \label{cor-#1} }{\end{coro}}
\newenvironment{example}[1]{\begin{exam} \rm \label{ex-#1} }{\end{exam}}
\newenvironment{proof}{\begin{trivlist} \item[\hspace{\labelsep}\bf Proof:]}{\hfill $\Box$\end{trivlist}}
\newenvironment{itemise}{\begin{list}{$\bullet$}{\leftmargin 18pt
\labelwidth 12pt \topsep 4pt \itemsep 2pt \parsep 2pt}}{\end{list}}
\newcommand{\df}[1]{Definition~\ref{df-#1}}
\newcommand{\th}[1]{Theorem~\ref{th-#1}}
\newcommand{\pr}[1]{Proposition~\ref{pr-#1}}
\newcommand{\lem}[1]{Lemma~\ref{lem-#1}}
\newcommand{\cor}[1]{Corollary~\ref{cor-#1}}
\newcommand{\ex}[1]{Example~\ref{ex-#1}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\dcup}{\stackrel{\mbox{\huge .}}{\cup}} % disjoint union
\newcommand{\dl}[1]{\mbox{\rm I\hspace{-0.45ex}#1}} % openface letter
\newcommand{\dc}[1]{\mbox{\rm {\raisebox{.4ex}{\makebox % openface character
[0pt][l]{\hspace{.2em}\scriptsize $\mid$}}}#1}}
\newcommand{\IT}{\mbox{\sf T\hspace{-1.1ex}T}} % openface T (terms)
% Alternative for those who have font msbm10:
\newfont{\open}{msbm10} % Remone these two lines if you don't have font msbm10
\renewcommand{\IT}{\mbox{\open T}} % this one too. % Open terms as in Fokkink
\newcommand{\plat}[1]{\raisebox{0pt}[0pt][0pt]{$#1$}} % no vertical space
\newcommand{\Id}[1]{[\hspace{-1.4pt}[#1]\hspace{-1.4pt}]} % denotation
\newcommand{\In}[1]{\plat{ % notation
\stackrel{\mbox{\tiny $/\hspace{-2.1pt}/$}}
{\raisebox{-.3ex}[.3ex]{\tiny $\backslash
\hspace{-2.1pt}\backslash$}}\!\!#1\!\!
\stackrel{\mbox{\tiny $\backslash\hspace{-1.8pt}\backslash$}}
{\raisebox{-.3ex}[.3ex]{\tiny $/\hspace{-1.8pt}/$}} }}
\newcommand{\rec}[1]{\plat{ % recursion
\stackrel{\mbox{\tiny $/$}}
{\raisebox{-.3ex}[.3ex]{\tiny $\backslash$}}
\!\!#1\!\!
\stackrel{\mbox{\tiny $\backslash$}}
{\raisebox{-.3ex}[.3ex]{\tiny $/$}} }}
\newcommand{\goto}[1]{\stackrel{#1}{\longrightarrow}} % transition
\newcommand{\gonotto}[1]{\hspace{4pt}\not\hspace{-4pt} % no transition
\stackrel{#1\ }{\longrightarrow}}
\newcommand{\bis}[1]{ \; % bisimulation
\raisebox{.3ex}{$\underline{\makebox[.7em]{$\leftrightarrow$}}$}
\,_{#1}\,}
\newcommand{\obis}[2]{\;_{#1} % bisimulation
\raisebox{.3ex}{$\underline{\makebox[.7em]{$\leftrightarrow$}}$}
\,_{#2}\,}
\newcommand{\nobis}[1]{\mbox{$\,\not\hspace{-2.5pt} % no bisimulation
\raisebox{.3ex}{$\underline{\makebox[.7em]{$\leftrightarrow$}}$}
\,_{#1}\,$}}
\newcommand{\pf}{\noindent {\bf Proof:\ }} % beginning of proof
\newcommand{\lmerge}{\mbox{$\,\|\hspace{-1.1ex}
\raisebox{-1.2ex}[0pt][0pt]{$-\!\!\!-\!\!$}$}} % left-merge
\newcommand{\rest}{ % restriction operator
\begin{picture}(2.16,3.2)
\thinlines
\put(1.12,-0.48){\line(0,1){3.52}}
\put(0.8,1.6){\tiny $\backslash$}
\end{picture} }
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%% Abbreviations %%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\IN}{\dl{N}} % natural numbers
\newcommand{\IC}{\dc{C}} % configuration structures
\newcommand{\IE}{\dl{E}} % event structures
\newcommand{\ID}{\dl{D}} % a domain
\newcommand{\IG}{\dc{G}} % graphs
\newcommand{\IP}{\dl{P}} % transition space
\newcommand{\fC}{{\cal C}} % function into \IC
\newcommand{\fE}{{\cal E}} % function into \IE
\newcommand{\fG}{{\cal G}} % function into \IG
\newcommand{\eC}{{\rm C}} % conf. structure
\newcommand{\eD}{{\rm D}} % conf. structure
\newcommand{\eE}{{\rm E}} % event structure
\newcommand{\eF}{{\rm F}} % event structure
\newcommand{\eG}{{\rm G}} % process graph
\newcommand{\eH}{{\rm H}} % process graph
\newcommand{\eP}{{\rm P}} % process expression
\newcommand{\eS}{{\rm S}} % ST-structure
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\title{\vspace{-3pc}\titlesize\bf On the Expressiveness of ACP\\[5pt]
\normalsize \bf (extended abstract)\thanks{\baselineskip 9pt To appear
in A. Ponse, C. Verhoef \& S.F.M. van Vlijmen, editors:
Proceedings ACP94, Workshop on Algebra of Communicating
Processes, Utrecht, The Netherlands, May 1994, {\sl Workshops in
Computing}, Springer-Verlag, 1994.}}
\author{\large Rob van Glabbeek\thanks{This work was supported by ONR
under grant number N00014-92-J-1974.}\\
\normalsize Computer Science Department, Stanford University\\
\normalsize Stanford, CA 94305, USA\\[-1pt]
\normalsize \tt rvg@cs.stanford.edu \date{}}
\begin{document}
\bibliographystyle{plain} % Actually the vG-style is used here
\maketitle\vspace{-8pt}
\begin{abstract}{\sc De Simone} showed that a wide class of languages,
including CCS, SCCS, CSP and ACP, are expressible up to strong
bisimulation equivalence in {\sc Meije}. He also showed that every
recursively enumerable process graph is representable by a {\sc Meije}
expression. {\sc Meije} in turn is expressible in aprACP (ACP with
action prefixing instead of sequential composition).
{\sc Vaandrager} established that both results crucially depend on
the use of unguarded recursion, and its noncomputable consequences.
{\em Effective} versions of CCS, SCCS, {\sc Meije} and ACP, not
using unguarded recursion, are incapable of expressing all
effective De Simone languages. And no effective language can denote
all computable process graphs.
In this paper I recreate De Simone's results in aprACP without using
unguarded recursion. The price to be payed for this is the use of a
partial recursive communication function and---for the second
result---a single constant denoting a simple infinitely branching
process. Due to the noncomputable communication function, the version
of aprACP employed is still not effective.
However, I also define a wide class of De Simone languages that are
expressible in an effective version of aprACP. This class includes
the effective versions of CCS, SCCS, ACP, {\sc Meije} and most other
languages proposed in the literature, but not CSP. An even wider
class, including CSP, turns out to be expressible in an effective
version of aprACP to which an effective relational renaming
operator has been added.
\end{abstract}
\msection{Introduction}
{\renewcommand{\thepage}{} % First page unnumbered
In the early 1980's several languages for the description of
communicating processes were introduced, most notably CCS \cite{Mi80},
SCCS \cite{Mi83}, CSP \cite{BHR84} and ACP \cite{BK84}. Using these
languages for purposes of specification and verification showed the
necessity, or at least the convenience, of adding many additional
constructs tailored to specific applications. In foundational
research however, for instance when proving a property by structural
induction, it is more convenient to have a fixed and well-defined set
of operators. This consideration gives rise to the task of finding a
basic language in which all or most useful operators can be expressed.
Although the languages CCS and SCCS were designed with this goal in
mind, the language {\sc Meije}, proposed by {\sc Austry \& Boudol}
\cite{AB84}, was the first result of a systematic analysis of
expressiveness issues. In \cite{dS85}, {\sc Robert de Simone} observed
that all constructs of the languages CCS, SCCS, CSP and ACP, and most
constructs that are used in specific applications, can be defined in a
particular way---namely by structural operational rules that fit in
what is now known as the {\em De Simone format}---and showed that any
operator that can so be defined is expressible in {\sc Meije}, up to
strong bisimulation equivalence. I will refer to a language all of
whose constructs can so be defined as a {\em De Simone language}.
The interleaving semantics of CCS-like languages is most conveniently
described in terms of {\em process graphs} or {\em labelled transition
systems}. Depending on how constructive one wants the theory to be,
several classes of graphs or transition systems can be considered, as
indicated in Figure~\ref{classes}.}
\begin{figure}[htb]
\begin{center}
\begin{minipage}{2in}
\begin{center}\small
\begin{picture}(20,70)(0,-20)
\put(10,50){\makebox[0pt]{$\kappa$-bounded}} \put(10,49){\line(0,-1){6}}
\put(10,40){\makebox[0pt]{countable}} \put(8,39){\line(-1,-1){7}}
\put(0,30){\makebox[0pt]{rec.\ enumerable}} \put(12,39){\line(2,-3){7.4}}
\put(0,20){\makebox[0pt]{decidable}} \put(0,29){\line(0,-1){6}}
\put(20,25){\makebox[0pt]{finitely branching}} \put(20,24){\line(-2,-3){7.4}}
\put(10,10){\makebox[0pt]{computable}} \put(1,19){\line(1,-1){6}}
\put(10,0){\makebox[0pt]{primitive recursive}} \put(10,9){\line(0,-1){6}}
\put(10,-10){\makebox[0pt]{regular}} \put(10,-1){\line(0,-1){6}}
\put(10,-20){\makebox[0pt]{finite \& acyclic}} \put(10,-11){\line(0,-1){6}}
\end{picture}
\end{center}
\end{minipage}
\hfill
\begin{minipage}{2in}
\begin{center}\small
\begin{picture}(20,70)(0,-20) \put(16,29){\line(-2,-1){12}}
\put(10,50){\makebox[0pt]{$\kappa$-bounded}} \put(10,49){\line(0,-1){6}}
\put(10,40){\makebox[0pt]{countable}} \put(8,39){\line(-1,-1){7}}
\put(0,30){\makebox[0pt]{rec.\ enumerable}} \put(12,39){\line(1,-1){7}}
\put(0,20){\makebox[0pt]{decidable}} \put(0,29){\line(0,-1){6}}
\put(20,30){\makebox[0pt]{guarded}} \put(20,29){\line(0,-1){6}}
\put(20,20){\makebox[0pt]{bounded}} \put(20,19){\line(-1,-1){6}}
\put(10,10){\makebox[0pt]{effective}} \put(1,19){\line(1,-1){6}}
\put(10,0){\makebox[0pt]{primitive effective}} \put(10,9){\line(0,-1){6}}
\put(10,-10){\makebox[0pt]{regular}} \put(10,-1){\line(0,-1){6}}
\put(10,-20){\makebox[0pt]{recursion-free}} \put(10,-11){\line(0,-1){6}}
\end{picture}
\end{center}
\end{minipage}
\end{center}
\caption[Classes]{Classes of process graphs\label{classes}
\makebox[2.6in]{\hfill\hfill$\ldots$ and process expressions\hfill}}
\end{figure}
For any uncountable cardinal $\kappa$ one can define the {\em
$\kappa$-bounded} process graphs to be the ones with less than
$\kappa$ (reachable) nodes (states) and edges (transitions),
or---clearly equivalent---the ones in which every node has less than
$\kappa$ outgoing edges. For $\kappa=\aleph_0$, however, these
definitions would not be equivalent. The {\em regular} process graphs
(having a finite set of states and transitions) form a strictly
smaller class than the {\em finitely branching} ones. Additionally one
can consider the {\em recursively enumerable} graphs, whose nodes form
a recursive set (such as the natural numbers), and whose edges form a
recursively enumerable set. If, moreover, it is decidable whether a
prospective edge is present or not, such a graph is {\em decidable}.
Furthermore, a {\em computable} process graph is one for which there
exists a terminating algorithm that, when given a node, produces as
output the finite set of its outgoing edges. This notion was
introduced in {\sc Baeten, Bergstra \& Klop} \cite{BBK87a}. Note that
it is a stronger requirement than ``decidable and finitely
branching''. Finally, in {\sc Ponse} \cite{Po92} a graph is called
{\em primitive recursive} if it is computable by means of a primitive
recursive algorithm.
In this paper I propose a similar classification for (expressions in)
De Simone languages. For each class of process graphs in
Figure~\ref{classes} I introduce a class of (process) expressions that
are guaranteed to denote graphs from that class only. The classes of
process expressions are displayed in the second part of
Figure~\ref{classes}. The notions of {\em recursion-free}, {\em
regular}, and {\em $\kappa$-bounded} expressions are just mentioned
for the sake of completeness, and are defined for CCS-like languages
only. The {\em countable} process expressions are the ones in which
all operators, not counting recursion, have finite arities. Except in
the section on $\kappa$-bounded expressions, I presume this to be the
default. The concepts {\em bounded} and {\em effective} are due to
{\sc Vaandrager} \cite{Va93}. These two general but simple
restrictions ensure that the effected expressions only denote,
respectively, finitely branching and computable process graphs.
Applied to CCS-like languages boundedness reduces to guardedness of
recursive specifications. The notion of effectivity is also applied
to languages as a whole. In that case it presupposes a decidable set
of closed terms, and requires the interpretation which maps closed
terms to descriptions of computable process graphs to be computable as
well.
Whereas for languages like ACP and CCS one can define a
$\kappa$-bounded version (containing only $\kappa$-bounded
expressions), a recursively enumerable version, an effective version,
etc., the language {\sc Meije} was designed in such a way that all its
constructs, except for recursion, are intrinsically effective.
Nevertheless, as shown in {\sc De Simone}
\cite{dS84a}, many undecidable and infinitely branching processes can
be specified by {\sc Meije}-expressions. The expressive power needed
to do so can only originate from the use of unguarded recursion. It
follows that the restriction to guarded recursion must be a
prerequisite in the definitions of decidable and bounded expressions.
This is indicated in Figure~\ref{classes}. The language {\sc Meije}
with unguarded recursion falls in the class of recursively enumerable
languages. In {\sc Meije} only finite recursion is used.
In \cite{dS85}, {\sc De Simone} shows that {\sc Meije} is universal in
two different ways. It is universal among the De Simone languages, and
it has a universal power to specify process graphs. Namely, any
finitary recursively enumerable De Simone language is expressible in
{\sc Meije}, and any recursively enumerable process graph is
representable by a {\sc Meije} expression. Here {\em finitariness} is
a syntactic restriction that is met by virtually all De Simone
languages encountered in practice. Both expressiveness results hold up
to bisimulation equivalence.
{\sc Vaandrager} \cite{Va93} investigates whether similar
expressiveness results can be obtained for effective languages, and
comes up with two negative results. First of all he points out that no
effective language is capable of denoting all computable process
graphs. This had been shown already by {\sc Baeten, Bergstra \& Klop}
\cite{BBK87a} up to strong bisimulation equivalence, but Vaandrager
sharpens the result to hold for the coarser notion of trace
equivalence as well. Secondly he defines a finitary effective De
Simone language PC that cannot be translated in any effective version
of {\sc Meije}, CCS, SCCS or ACP with only finite guarded recursion.
The culprit is a {\em relational renaming operator} that occurs in
this language. By means of this operator a primitive recursive graph
can be specified that is not specifiable in the mentioned languages.
The main contributions of the present paper are two effective versions
of De Simone's first expressivity result. As unguarded recursion
violates effectivity, its use must be eliminated from De Simone's
construction. But {\sc Meije} appears to lose most of its power when
unguarded recursion is gone. Therefore I will use a variant of
ACP \cite{BK84}, called aprACP$_F$. aprACP$_F$ is a parametrised
language, of which an instantiation is obtained by selecting a set $A$
of {\em actions} and a partial binary {\em communication function} on
$A$. One particular choice of the communication function yields an
extension of {\sc Meije}. Thus all expressiveness results
obtained for {\sc Meije} hold for aprACP$_F$ as well. However,
thanks to the possibility of other communication functions, aprACP$_F$
is more flexible, and potentially more expressive.
In Section~\ref{semantics} I propose a definition of what it
means for one language to be expressible in another. This definition
agrees with the notion of a {\em translation} from {\sc Boudol}
\cite{Bo85}. I also introduce (annotated) signatures to
determine the syntax of a language and review the method of
structural operational semantics for interpreting the closed
expressions in a language as (equivalence classes of) process graphs.
In Section~\ref{acp} I introduce the language aprACP$_F$, and indicate
how it relates to ACP, CCS and {\sc Meije}. In short, it is a
sublanguage of ACP---thus ``apr'' (for {\em action prefix})---to which
renaming operations have been added---thus the subscript $F$ (for {\em
functional renaming}). CCS as well as {\sc Meije} are obtained as
sublanguages of aprACP$_F$ under particular instantiations of the
parameters. I show that several operators, such as the {\em
left-merge}, the {\em communication merge} and the {\em alternative
composition}, that play a r\^ole in ACP, are expressible in terms of
the other operators, and hence need not to be introduced as
primitives. I also show that one can benefit from all
choices of communication functions at the same time. There is namely
one canonical instantiation of aprACP$_F$ in which any other
instantiation with the same set of actions can be expressed.
In Section~\ref{specifying} I define the classification of
aprACP$_F$-expressions of Figure~\ref{classes}. When possible, I make
these classes of expressions large enough to denote every graph in the
corresponding class. Only in case of the decidable
aprACP$_F$-expressions I do not succeed in this. In particular, each
computable process graph can be represented by an effective
expression. This had been shown earlier by {\sc Ponse} \cite{Po92} for
the language $\mu$CRL. However, it is not possible to combine enough
such expressions in one effective language, as follows from the first
negative expressiveness result mentioned above. When one tries to do
this, the set of closed terms of the language becomes undecidable. For
the same reason I couldn't find a canonical candidate for an effective
version of aprACP$_F$, in which all other (finitary) effective
versions of aprACP$_F$ can be expressed. This leaves not much hope
for expressing all finitary effective De Simone languages in
aprACP$_F$.
Therefore I settle for the {\em primitive effective} De Simone
languages, denoting only primitive recursive graphs. By means of a
trivial construction, every such graph can be denoted in a single
primitive effective version of aprACP$_F$. As the construction uses
infinite---but primitive recursive---guarded recursion, this is still
not a primitive effective version of De Simone's second expressiveness
result. The same can be said for a more disciplined construction by
{\sc Ponse} \cite{Po92}.
In Section~\ref{dS} I extend the classification of
Figure~\ref{classes}, or actually the part between ``countable'' and
``primitive effective'', to arbitrary De Simone languages. Subsequently
I state the expressiveness results that I obtained, but in this
extended abstract the proofs are not included.
Vaandrager's counterexample-language PC needs only primitive
recursion, so not all finitary primitive effective De Simone
languages translate in aprACP$_F$ with finite guarded recursion.
Therefore I isolate a class that do. These are the {\em functional}
finitary primitive effective De Simone languages. They include the
primitive effective versions of CCS, SCCS, ACP and {\sc Meije}. The
restriction to primitive recursion is probably not so bad, as I am not
aware of any use of effective but not primitive effective De Simone
languages. However, the requirement of functionality rules out CSP
and Vaandrager's PC. This is solved by adding the relational
renaming operator of PC---which to a great extent also occurs as the {\em
(inverse) image operator} in CSP---to aprACP$_F$, thereby obtaining
aprACP$_R$. All finitary primitive effective De Simone languages are
expressible in the primitive recursive version of aprACP$_R$ using
only finite guarded recursion. I do not know if these results carry
over to {\sc Meije}. They do not carry over to CCS, CSP or PC.
Besides these main contributions I establish similar results for the
countable De Simone languages and the bounded ones. Again, I use only
aprACP$_R$ with finite guarded recursion. Similarly, I recreate De
Simone's first expressiveness result for aprACP$_R$, without using
unguarded recursion. For this, an undecidable communication function is
used.
All results announced above are also generalised to
non-finitary De Simone languages. This necessitates the use of
infinite, but still guarded, recursion.
{\sc Vaandrager} \cite{Va93} established that any finite effective De
Simone language is expressible in a finite version of PC. Here {\em
finite} means specified by means of a finite number of De Simone rules.
Such languages only denote graphs with a finite set of actions.
It should be noted that any finite De Simone language with guarded
recursion is functional, finitary and primitive effective. Finite
guarded De Simone languages can also be expressed in aprACP$_F$ and
{\sc Meije}.
As far as the power to specify process graphs
goes, I recreate De Simone's result while using only finite
guarded recursion. For this purpose I use a version of aprACP$_F$ with
a partial recursive (but undecidable) communication function, to which
a single constant $U$ has been added denoting a simple infinitely
branching process. Without adding $U$ no infinitely branching
processes can be specified in aprACP$_F$ with guarded recursion. This
result did not extend to other classes of process graphs/expressions.
\msection{Syntax, Semantics and Expressibility}\label{semantics}
In this section I propose a definition of what it means for one
language to be expressible in another. In order for such a notion of
expressibility to be meaningful, a language is understood to combine
syntax and semantics.
First I will introduce the syntax of a language through the notion of
a {\em annotated signature}. The annotated signature determines what
are the valid expressions of the language. I will define a signature
as a set of function declarations, thus omitting the possibility of
predicates. These do not occur in the languages I want to study. The
annotation specifies to what extent recursion is incorporated in the
language.
The semantics of a language is given through an interpretation of the
(closed) terms in a domain of values. Such an interpretation should be
{\em compositional} and satisfy a few other requirements. My notion
of a compositional semantics generalises notions of {\em denotational
semantics}, namely by not insisting that the meaning of recursive
expressions is obtained by order-theoretic methods. Thus my concept of
expressiveness applies to languages with a denotational semantics as
well.
Subsequently I treat the notion of Structural Operational Semantics in
{\sc Plotkin}'s style \cite{Pl81}\hspace{-1.17989pt}.\hspace{-1pt} The
languages considered in this paper will all be equipped with a
structural operational semantics. Such an operational semantics
associates in a standard way a {\em process graph} to every closed
process expression.
On process graphs, I divide out {\em bisimulation equivalence},
which is among the finest congruence relations available. All my
expressibility results will be established up to bisimulation
equivalence. They will then also hold for most other---less
fine---equivalences.
\subsection{Syntax}\label{syntax}
In this paper $V$ is an infinite set of {\em variables}, ranged over
by $X,X_i,x,y,x'$ etc.
\begin{definition}{signatures} ({\em Signatures}).
A {\em function declaration} is a pair $(f,n)$ of a {\em function
symbol} $f\not\in V$ and an {\em arity} $n \in \IN$. A function
declaration $(c,0)$ is also called a {\em constant declaration}.
A {\em signature} is a set of function declarations. The set
$\IT^r(\Sigma)$ of {\em terms with recursion} over a signature $\Sigma$
is defined inductively by:
\begin{itemize}
\item $V \subseteq \IT^r(\Sigma)$,
\item if $(f,n) \in \Sigma$ and $t_1,\ldots,t_n \in \IT^r(\Sigma)$ then
$f(t_1,\ldots,t_n) \in \IT^r(\Sigma)$,
\item If $V_S \subseteq V$, $S:V_S \rightarrow \IT^r(\Sigma)$ and $X\in V_S$,
then $\rec{X|S}\in \IT^r(\Sigma)$.
\end{itemize}
A term $c()$ is often abbreviated as $c$. A function $S$ as appears in
the last clause is called a {\em recursive specification}. A
recursive specification $S$ is often displayed as $\{X=S_X \mid X \in V_S\}$.
An occurrence of a variable $y$ in a term $t$ is {\em free} if it does not
occur in a subterm of the form $\rec{X|S}$ with $y \in V_S$. A term
is {\em closed} if it contains no free occurrences of variables. Let
$T^r(\Sigma)$ be the set of closed terms over $\Sigma$. The
sets $\IT(\Sigma)$ and $T(\Sigma)$ of open and closed terms over
$\Sigma$ without recursion are defined likewise, but without the last clause.
\end{definition}
The syntax of a language can be given as a signature together with an
annotation which places some restrictions on the use of recursion.
These can be:\\
\begin{tabular}{@{}l@{ }l@{}}
$\kappa$-bounded: & the sets $S$ should have cardinality less than $\kappa$,\\
countable: & the sets $S$ should be countable,\\
enumerable: & the functions $S$ should be partial recursive,\\
computable: & the sets $V_S$ should be decidable and the functions $S$
recursive,\\
primitive: & as above, but using only primitive recursion,\\
finite: & the sets $S$ should be finite,\\
guarded: & the sets of equations $S$ should satisfy a syntactic
criterion that\\ &\small ensures that they have unique
solutions under a given interpretation,
\end{tabular}\\
or no recursion.
\begin{definition}{substitutions}({\em Substitutions}).
A {\em $\Sigma$-substitution} $\sigma$ is a partial function from $V$
to \plat{\IT^r(\Sigma)}. If $\sigma$ is a substitution and $t$ a term, then
$t[\sigma]$ denotes the term obtained from $t$ by replacing, for $x$
in the domain of $\sigma$, every free occurrence of $x$ in $t$ by
$\sigma(x)$, while renaming bound variables if necessary to prevent
name-clashes. In that case $t[\sigma]$ is called a {\em substitution
instance} of $t$. A substitution instance $t[\sigma]$ where $\sigma$
is given by $\sigma(x_i)=s_i$ for $i\in I$ is denoted as
$t[s_i/x_i]_{i\in I}$. These notions extend to syntactic objects containing
terms, with the understanding that such an object is a substitution
instance of another one only if the same substitution has been applied
to each of its constituent terms.
\end{definition}
\subsection{Expressibility}\label{expressibility}
A {\em language} can be given by an annotated signature, specifying its syntax,
and an {\em interpretation}, assigning to every (closed) term $t$ its
meaning $\Id{t}$. The meaning of a closed term can simply be a {\em
value} chosen from a set of values $\ID$, which is called a {\em domain}.
Usually interpretations are required to satisfy some sanity
requirements. One of them is that the meaning of a term $\rec{X|S}$ is
the $X$-component of a solution of $S$. To be precise:
$$\Id{\rec{X|S}}=\Id{S_X[\rec{Y|S}/Y]_{Y\in V_S}}.$$
Other requirements are {\em compositionality} and {\em invariance
under $\alpha$-recursion}. Compositionality demands that the meaning of a
term is completely determined by the meaning of its components.
This means that for functions $(f,n)\in \Sigma$ and for recursive
specifications $S$ and $S'$ with $X\in V_S = V_{S'}$ we have
$$\Id{t_i}=\Id{t'_i} ~(i=1,...,n) ~~\Rightarrow~~
\Id{f(t_1,...,t_n)} = \Id{f(t'_1,...,t'_n)}$$ $$\mbox{and}~
\Id{S_Y} = \Id{S'_Y} ~(Y\in V_S)
~~\Rightarrow~~ \Id{\rec{X|S}} = \Id{\rec{X|S'}}.$$
Invariance demands that the meaning of a term is
independent of the names of its bound variables, i.e.\
for any injective substitution $\alpha:V_S \rightarrow V$
$$\Id{\rec{\alpha(X) | S[\alpha]}} = \Id{\rec{X|S}}.$$
In order for language $L_1$ to be expressible in language $L_2$, I
require that for every closed $L_1$-term $t$ there exists a closed
$L_2$-term $\tilde{t}$ denoting the same value. Usually this can only
be the case if the domain $\ID_1$ in which $L_1$-expressions are
interpreted is included in the domain $\ID_2$ of $L_2$.
The requirement on closed terms is not sufficient. It says that every
value denotable by language $L_1$ can also be denoted by language $L_2$.
In addition I want that every {\em operation} of $L_1$ can be mimicked
in $L_2$. This has to do with the meaning of open terms. For every open
term in \plat{\IT^r(\Sigma_1)} I want to find a term in \plat{\IT^r(\Sigma_2)}
with the same meaning.
A common approach to open terms is to reduce them to the collection of
their closed substitution instances. In this view there is no need to
extend the interpretation $\Id{\cdot}$ explicitly to open terms. The
preconditions $\Id{S_Y}=\Id{S_Y'}$ of the second compositionality
requirement are simply read as ``$\Id{S_Y[\sigma]}=\Id{S_Y'[\sigma]}$ for
each closed substitution $\sigma:V \rightarrow T^r(\Sigma)$''. This
approach is often taken when generalising an equivalence relation on
closed terms to an equivalence on open terms (over the same
signature). Two open terms are then declared equivalent if for every
closed substitution the corresponding substitution instances are
equivalent.
It is slightly more difficult to employ this approach in defining
expressibility. The problem is that open terms over different
signatures are compared, so that it is impossible to employ the same
substitution at both sides. This is solved as follows:
\begin{definition}{closed-expressibility}({\em Expressibility})
Let $L_i$ ($i=1,2$) be two languages, given as an annotated signature
$\Sigma_i$ and an interpretation $\Id{\cdot}_i:T^r(\Sigma_i)
\rightarrow \ID_i$. $L_1$ is said to be {\em expressible} in $L_2$ if
there is a translation $\tilde{\cdot}:\IT^r(\Sigma_1)\rightarrow
\IT^r(\Sigma_2)$ such that for all $t \in \IT^r(\Sigma_1)$ with free
variables $x_1,...,x_n$ and for all $t_1,...,t_n \in T^r(\Sigma)$
$$\Id{t[t_i/x_i]_{i=1}^n}_1 = \Id{\tilde{t}[\tilde{t}_i/x_i]_{i=1}^n}_2.$$
\end{definition}
This will be my definition of expressibility for now. In the full
version of this paper, however, I plan to be a bit more
ambitious. An open term with $n$ free variables is interpreted as an
$n$-ary operator on the domain $\ID$, and for $L_1$ to be expressible
in $L_2$ I require that for every $L_1$-term $t$ there is an
$L_2$-term $\tilde{t}$, such that $t$ and $\tilde{t}$ denote the same
operator, at least when applied to values from the domain of $L_1$.
If $L_1$ can be expressed into $L_2$ in that sense, it can certainly
be done in the sense of \df{closed-expressibility}.
\subsection{Quotient domains}
Let $\sim$ be an equivalence relation on a domain $\ID$.
An interpretation $\Id{\cdot}$ in $\ID$ is {\em compositional up to
$\sim$} if it satisfies the requirements for compositionality, but
with ``$=$'' replaced by ``$\sim$''.
The first requirement for instance reads
$$\Id{t_i}\sim\Id{t'_i} ~(i=1,...,n) ~~\Rightarrow~~
\Id{f(t_1,...,t_n)} \sim \Id{f(t'_1,...,t'_n)}.$$
In the same way the other sanity requirements, as well as the notion
of expressibility, can be defined {\em up to $\sim$}. In the case of
expressibility, however, it is necessary that $\sim$ is defined on
$\ID_1 \cup \ID_2$.
Given a domain $\ID$ for interpreting languages and an equivalence
relation $\sim$, the {\em quotient domain} $\ID/_\sim$ consists of the
$\sim$-equivalence classes of elements of $\ID$. An interpretation
$\Id{\cdot}: T^R(\Sigma) \rightarrow \ID$ of the closed terms of a
language in $\ID$, is turned into the {\em quotient interpretation}
$\Id{\cdot}_\sim: T^R(\Sigma) \rightarrow \ID/_\sim$ of these terms by
letting $\Id{t}_\sim$ be the equivalence class containing $\Id{t}$.
This quotient interpretation satisfies the sanity requirements of
Section~\ref{expressibility} iff the original interpretation satisfies
them up to $\sim$. Likewise, one language is expressible in another
under a quotient interpretation obtained by dividing out the same
equivalence $\sim$ on their domains of interpretation, iff, under the
original interpretation, this language is expressible in the other up
to $\sim$.
\subsection{Process Graphs}
When the expressions in a language are meant to represent processes,
they are called {\em process expressions}, and the language a {\em
process description language}.
Suitable domains for interpreting process description languages are
the class of {\em process graphs} and its quotients. In such {\em
graph domains} a process is represented by either a process graph, or
an equivalence class of process graphs. Process graphs are also known
as {\em state-transition diagrams} or {\em automata}. They are {\em
labelled transition systems} equipped with an initial state.
\begin{definition}{graphs}({\em Process graphs})
A {\em process graph}, labelled over a set $A$ of actions, is a
triple $G=(S,T,I)$ with
\begin{itemise}
\item[\bf --] $S$ a set of {\em nodes} or {\em states},
\item[\bf --] $T \subseteq S \times A \times S$ a set of {\em edges}
or {\em transitions},
\item[\bf --] and $I \in S$ the {\em root} or {\em initial} state.
\end{itemise}
Let $\IG(A)$ be the domain of process graphs labelled over $A$.
\end{definition}
Virtually all so-called {\em interleaving models} for the
representation of processes are isomorphic to graph models. The {\em
failure sets} for instance that represent expressions in the process
description language CSP \cite{BHR84} can easily be exchanged for
equivalence classes of graphs, under a suitable equivalence.
In \cite{BK84} the language ACP is equipped with a process graph
semantics, and the semantics of CCS, SCCS and {\sc Meije} given in
\cite{Mi80,Mi83,AB84,dS85} are operational ones, which, as I will
show below, induce a process graph semantics.
Usually the parts of a graph that cannot be reached from the initial
state by following a finite path of transitions are considered
meaningless for the description of processes. This means that one is
only interested in process graphs as a model of system behaviour up to
some equivalence, and this equivalence identifies at least graphs with
the same reachable parts. Likewise, the particular identity of the
states in a process graph is normally not of any importance. Two
graphs that only differ in the naming of their states are called {\em
isomorphic} and also isomorphic graphs are semantically identified.
\begin{definition}{reachability}({\em Reachability}).
Let $G=(S,T,I)$ be a process graph. A {\em path} is an alternating
sequence $s_0, a_1, s_1, a_2, s_2, \ldots , s_{n-1}, a_n, s_n$ of
states and actions, such that \plat{s_{i-1}\goto{a_i}s_i} for
$i=1,...,n$. Here \plat{s_{i-1}\goto{a_i}s_i} is an abbreviation for
$(s_{i-1},a_i,s_i)\in T$. Such a path is said {\em to go from $s_0$ to
$s_n$}. A state $s'$ is {\em reachable} from a state $s$ if there is a
path from $s$ to $s'$. The {\em reachable part} of $G$ is the graph
$(S^R,T^R,I)$ with $S^R \subseteq S$ the set of states reachable from
the initial state $I$, and $T^R = T \cap (S^R\times A \times S^R)$.
%\end{definition}
%\begin{definition}{isomorphism}
({\em Isomorphism}).
Two process graphs $G=(S,T,I)$ and $H=(S',T',I')$ are {\em isomorphic}
if there exists a bijection $f:S \rightarrow S'$---called an {\em
isomorphism}---with $f(I)=I'$ and $(s,a,t) \in T \Leftrightarrow
(f(s),a,f(t))\in T'$.
Write $G\cong H$ if the reachable parts of $G$ and $H$ are isomorphic.
\end{definition}
Thus $\cong$ may be considered the finest equivalence (the one
with the fewest identifications, and the smallest equivalence
classes) on $\IG$ that makes $\IG/_{\cong}$ in a reasonable model of
concurrency. However, some languages (interpretations) encountered in
this paper fail to be compositional up to $\cong$. Also several
expressiveness results will not hold up to $\cong$. Therefore a
coarser equivalence (identifying more, and having larger equivalence
classes) should be divided out on $\IG$. In the literature many
equivalences have been proposed. The finest of those is (strong)
bisimulation equivalence, due to {\sc Milner} \cite{Mi80,Mi83}.
\begin{definition}{bisimulation}({\em Bisimulation equivalence}).
Two process graphs $G$ and $H$ are {\em bisimulation
equivalent}---notation $G \bis{} H$---if there exists a
binary relation $R$---called a {\em bisimulation}---between their
states, such that
\begin{itemise}
\item[\bf --] the initial states of $G$ and $H$ are related,
\item[\bf --] if $sRt$ and $s \goto{a} s'$ then $H$ has a state $t'$
with $t\goto{a}t'$ and $s'Rt'$,
\item[\bf --] if $sRt$ and $t \goto{a} t'$ then $G$ has a state $s'$
with $s\goto{a}s'$ and $s'Rt'$.
\end{itemise}
\end{definition}
All languages mentioned in this paper satisfy the sanity requirements
of Section~\ref{expressibility} up to $\bis{}$. The expressiveness
results of this paper will also be established up to bisimulation
equivalence. This means that they surely hold for the (coarser)
equivalences used elsewhere in the literature, such as {\em weak
bisimulation equivalence}---the standard equivalence of CCS
\cite{Mi80}---and (weak) failures equivalence---the standard semantics
of CSP \cite{BHR84}.
\subsection{Operational Semantics}
In this section I present {\sc Plotkin}'s method of {\em Structural
Operational Semantics} \cite{Pl81} for interpreting expressions as
process graphs or labelled transition systems.
\begin{definition}{TSS} ({\em Transition system specifications;}
{\sc Groote \& Vaandrager} \cite{GrV92})\hspace{-1.01157pt}.\linebreak[2]
Let $\Sigma$ be an annotated signature and $A$ a set (of {\em
actions}). A {\em (positive) $(\Sigma,A)$-literal} is an expression
\plat{t \goto{a} t'} with \plat{t,t'\in \IT^r(\Sigma)} and $a \in A$.
An {\em action rule} over $(\Sigma,A)$ is an expression of the
form \plat{\frac{H}{\alpha}} with $H$ a set of $(\Sigma,A)$-literals (the {\em
premises} of the the rule) and $\alpha$ a $(\Sigma,A)$-literal (the
{\em conclusion}). A rule \plat{\frac{H}{\alpha}} with $H=\emptyset$ is
also written $\alpha$. A {\em transition system
specification (TSS)} is a triple $(\Sigma,A,R)$ with $\Sigma$ a signature
and $R$ a set of action rules over $(\Sigma,A)$.
\end{definition}
The following definition tells when a transition is provable from a
TSS. It generalises the standard definition (see e.g.\ \cite{GrV92})
by (also) allowing the derivation of rules. The
derivation of a transition \plat{t\goto{a}t'} corresponds to the
derivation of the rule $\frac{H}{t\goto{a}t'}$ with $H=\emptyset$.
The case $H \neq \emptyset$ corresponds to the derivation of
\plat{t\goto{a}t'} under the assumptions $H$.
\begin{definition}{proof}({\em Proof\/}).
Let $P=(\Sigma,R)$ be a TSS. A {\em proof} of an action rule
\plat{\frac{H}{\alpha}} from $P$ is a well-founded, upwardly
branching tree of which the nodes are labelled by $\Sigma$-literals,
such that:
\begin{itemize}\vspace{-1ex}
\item the root is labelled by $\alpha$, and\vspace{-1ex}
\item if $\beta$ is the label of a node $q$ and $K$ is the set of
labels of the nodes directly above $q$, then
\begin{itemize}\vspace{-1ex}
\item either $K=\emptyset$ and $\beta \in H$,
\item or $\frac{K}{\beta}$ is a substitution instance of a rule from $R$.
\vspace{-1ex}\end{itemize}
\end{itemize}
If a proof of $\frac{H}{\alpha}$ from $P$ exists, then
$\frac{H}{\alpha}$ is {\em provable} from $P$, notation $P \vdash
\frac{H}{\alpha}$.
\end{definition}
Transition system specifications often contain infinitely many rules,
yet are presented finitely by giving {\em rule schemata}, each of
which codifies a large set of rules. This practice is formalised in
part by the notion of an abstract TSS.
\begin{definition}{abstract}({\em Abstract TSSs}).
An {\em abstract $\Sigma$-literal} is an expression $t \goto{} t'$
with $t,t'\in \IT(\Sigma)$.
An {\em abstract action rule} over $(\Sigma,A)$ is an expression of
the form $\frac{H,~Pr}{\alpha}$ with $H$ a set of abstract
$(\Sigma,A)$-literals, $Pr \subseteq A^H \times A$, and $\alpha$ an
abstract $\Sigma$-literal. An {\em abstract TSS} is a triple
$(\Sigma,A,R)$ with $\Sigma$ a signature and $R$ a set of abstract
action rules over $(\Sigma,A)$.
An abstract TSS $(\Sigma,A,R)$ {\em determines} the (concrete) TSS
$(\Sigma,A,R')$ with
$$R'=\left\{\frac{\{t_i \goto{a_i}t'_i \mid i\in I\}}{t\goto{b}t'}
~\left|~
\frac{\{t_i \goto{}t'_i \mid i\in I\},~Pr}{t\goto{}t'} \in R \wedge
Pr(\vec{a},b) \right.\right\}.$$
\end{definition}
Finally I will show how the operational semantics of a language, given as
a TSS, induces a process graph semantics.
\begin{definition}{interpreting}\hspace{-0.12048pt}({\em Interpreting
the closed expressions in a TSS as process graphs}).
Let $P=(\Sigma,A,R)$ be a TSS and $t \in T(\Sigma)$. Then $\Id{t}$ is
defined to be the reachable part of the process graph $(T^r(\Sigma),T,t)$
with $T$ the set of transitions provable from $P$.
\end{definition}
\msection{Prefix ACP with Relational Renaming}\label{acp}
The language that I will use for my expressiveness results is a
variant of ACP \cite{BK84} that could be called {\em prefix ACP with
relational renaming}. Like ACP this language has two parameters: an alphabet
$A$ of $actions$ and a partial {\em communication function} $| :A^2
\rightarrow A$, which is commutative and associative, i.e.\
\begin{itemise}\vspace{-3pt}
\item $a|b=b|a~~~\mbox{(commutativity)}$\vspace{-3pt}
\item $(a|b)|c=a|(b|c)~~~\mbox{(associativity)}$\vspace{-3pt}
\end{itemise}
for all $a,b,c \in A$ (and each side of these equations is defined
just when the other side is). I will denote this language as aprACP$_R(A,|)$.
Its signature contains a constant $0$ denoting inaction, two binary
operators $+$ and $\|$ denoting {\em alternative} and {\em parallel
composition} respectively, a unary operator $a$ for any action $a\in
A$, a unary {\em encapsulation} operator $\partial_H$ for any $H
\subseteq A$ and a {\em relational renaming} operator $\rho_R$ for any
binary relation $R \subseteq A \times A$.
$p \| q$ represents the independent execution of the processes $p$ and
$q$, partly synchronised by the communication function $|$. If $a|b$
is defined, an occurrence of $a$ in $p$ can synchronise with an
occurrence of $b$ in $q$ into a communication action $a|b$ between $p$
and $q$. If $a|b$ is not defined, no such communication is possible.
The action $a$ of $p$ can, instead of synchronising with an action of
$q$, (also) appear independent of $q$, and likewise can $b$ occur
independently of $p$.
The process $ap$ first performs the action $a \in A$ and then behaves
like $p$. $\partial_H(p)$ behaves like $p$, but without the
possibility of performing actions from $H$. The operator $\rho_R$ is a
slight generalisation of the relabelling and (inverse) image operators
of CCS and CSP. Process $\rho_R(p)$ behaves just like process $p$,
except that if $p$ has the possibility of doing an $a$, $\rho_R(p)$
can do any one action $b$ that is related to $a$ via $R$.
In aprACP$_R(A,|)$-expressions brackets are omitted under the
convention that $a$ binds strongest and $+$ weakest. Besides aprACP
with relation renaming I also consider aprACP with functional renaming,
denoted aprACP$_F(A,|)$. This is the same language, but with a renaming
operator $\rho_f$ only for every {\em function} $f:A \rightarrow A$
instead of for every relation.
The action rules for aprACP$_R(A,|)$ are given in Table~\ref{pracp},
thereby completing the formalisation of this language as a TSS. These
rules determine an interpretation of the aprACP$_R(A,|)$-expressions in
$\IG(A)$. This interpretation agrees, up to bisimulation equivalence,
with the more denotational interpretation of ACP$(A,|)$ in $\IG(A)$
given in {\sc [Baeten,] Bergstra \& Klop} \cite{BK84,BBK87a}.
\begin{table}[htb]
\begin{center}
\framebox{$\begin{array}{ccc}
ax \goto{a} x & \displaystyle\frac{x \goto{a} x'}{x+y \goto{a} x'} &
\displaystyle\frac{y \goto{a} y'}{x+y \goto{a} y'}\\[4ex]
\displaystyle\frac{x\goto{a} x'}{x\| y \goto{a} x'\| y} &
\displaystyle\frac{x\goto{a} x' ,~ y \goto{b} y' , ~a|b=c}
{x\| y \goto{c} x'\| y'} &
\displaystyle\frac{y \goto{a} y'}{x\| y \goto{a} x\| y'}\\[4ex]
\displaystyle\frac{x \goto{a} x', ~a\not\in H}{\partial_H(x) \goto{a}
\partial_H(x')} &
\displaystyle\frac{S_x[\rec{Y|S}/Y]_{Y\in V_S} \goto{a} z}{\rec{X|S}\goto{a}z}&
\displaystyle\frac{x \goto{a} x' ,~R(a,b)}{\rho_R(x) \goto{b} \rho_R(x')}
\end{array}$}
\end{center}
\caption{aprACP$_R$\label{pracp}}
\end{table}
It is common to regard the entries in tables like \ref{pracp} as
schemata, each of which denotes a rule for any proper instantiation of
the metavariables $a,b,c$ by real actions from $A$. Thus in case $A$
is infinite, there are infinitely many rules for every operator. In an
\vspace{-2pt}
attempt at ``finitisation'' I will in this paper regard each of the
first six entries as single rules of an abstract TSS. The
rule\vspace{-1.3ex} $\displaystyle\frac{x\goto{a} x'}{x\| y \goto{a}
x'\| y}$ for instance, should be read as $\displaystyle\frac{x\goto{}
x',~Id}{x\| y \goto{} x'\| y}$ where $Id \subseteq A\times A$ is the
identity relation on $A$. In the rules were $Pr$ is not the identity,
it is explicitly given. The last three entries in Table~\ref{pracp}
remain schemata even when interpreted as abstract action rules. There
is namely one rule for every encapsulation operator, one for every
relational renaming, and one for every pair $\rec{X|S}$ with $S$ a
recursive specification and $X \in V_S$. But at least there are now
finitely many rules for every operator, even if $A$ is infinite. This
will turn out to be a useful property.
\subsection{CCS}
{\sc Milner}'s Calculus of Communicating Systems (CCS) \cite{Mi80} can
be regarded as (a sublanguage of) an instantiation of aprACP with
functional renaming.
CCS is parametrised with a set ${\cal A}$ of {\em names}. The set
$\bar{\cal A}$ of {\em co-names} is given by $\bar{\cal A}=\{\bar{a}
\mid a\in {\cal A}\}$, and ${\cal L}={\cal A} \cup \bar{\cal A}$ is
the set of {\em labels}. The function $\bar{\cdot}$ is extended to
$\cal L$ by declaring $\bar{\bar{a}}=a$. Finally \plat{Act = L \dcup
\{\tau\}} is the set of {\em actions}. CCS can now be presented as
aprACP$(Act,|)$, where $|$ is the partial function on $Act$ given by
$a|\bar{a} = \tau$.
In CCS there is a renaming operator only for every function
$f: Act \rightarrow Act$ that satisfies $f(\bar{a})=\overline{f(a)}$ and
$f(\tau)=\tau$. This operator (applied on a process $p$) is written
$p[f]$ and called {\em relabelling}. Also there is an encapsulation
operator $\partial_H$ only when $H=A\cup\bar{A}$ with $A\subseteq
\cal A$. This operator is called {\em restriction} and is written
$p\backslash A$. Parallel composition is written $|$ instead of $\|$,
but there is no further difference between CCS and aprACP$_F(Act,|)$.
\subsection{ACP}
There are many methodological differences between the ACP approach to
{\em process algebra} and the CCS approach. I will not address these
here. As a language,
ACP can be regarded as a modification of CCS in four directions.
\begin{itemise}
\item First of all, ACP makes a distinction between deadlock and
successful termination. As a consequence, action prefixing can be
replaced by action constants and a general sequential composition.
\item ACP adds two auxiliary operators, the {\em left merge} and the
{\em communication merge}, denoted $\lmerge$ and $|$, to enable a
finite equational axiomatisation of the parallel composition.
\item Whereas CCS combines communication and abstraction from internal
actions in one operator, in ACP these activities are separated. In CCS
the result of any communication is the unobservable action $\tau$. In
ACP it is an observable action, from which (in the extended language
ACP$_\tau$) one can abstract by applying an {\em abstraction}
operator, renaming designated actions into $\tau$.
\item CCS adheres to a specific communication format, admitting
only handshaking communication, whereas ACP allows a variety of
communication paradigms, including ternary communication, through the
choice of the communication function $|$.
\end{itemise}
In this paper only the last feature of ACP is of importance. I don't
distinguish observable and unobservable actions and therefore work
with ACP rather than ACP$_\tau$. As I also don't deal with the
distinction between deadlock and successful termination, I restrict
attention to the sublanguage aprACP of ACP that doesn't make this
distinction and consequently supports prefixing only. Whereas in the
original papers on ACP the set $A$ of action constants was required to
be finite, I allow it to be infinite. I add the subscript $R$ (or $F$)
to indicate the addition of (functional) renaming operators, which
were not included in the syntax of ACP. Subsequently I drop the
auxiliary operators $\lmerge$ and $|$ from the language, since these
can be expressed in the other operators of aprACP$_F$, as I will show
in Section~\ref{left}.
The resulting language extends CCS in only one essential way,
namely through the general communication format. This generality
greatly enhances the expressiveness of the language.
\subsection{Meije}\label{meije}
Like CCS, also {\sc Boudol}'s language {\sc Meije} \cite{AB84,Bo85,dS85}
can be regarded as (a sublanguage of) an instantiation of aprACP with
functional renaming. {\sc Meije} is parametrised with a set ${\cal
A}$ of {\em atomic actions} and a set $\cal S$ of {\em signals}. The set
$Act$ of {\em actions} is a commutative monoid, namely the free
commutative product of the free commutative monoid generated by $\cal
A$ and the free commutative group generated by $\cal S$. This means that
the elements of $Act$ are a kind of multisets over $\cal A$ and $\cal
S$ with the stipulation that elements of $\cal S$ may also have negative
multiplicities. These can also be seen as ordinary multisets over
$\cal A$, $\cal S$ and ${\cal S}^{-1} = \{s^{-1} \mid s\in {\cal S}\}$
in which $s$ and $s^{-1}$ cancel. A typical element of $Act$ is denoted as
$a^5b^2s^3t^{-1}$. The product operation $.$ on $Act$ is such that
$a^5b^2s^3t^{-1} . a^2c^4s^{-3}t^3u^{-3} = a^7b^2c^4t^2u^{-3}$.
{\sc Meije} can now be presented as a sublanguage of aprACP$_F(Act,.)$.
In {\sc Meije} there are two kind of renaming operators. There is a
renaming operator $\rho_{\Phi}$, written $\rec{\Phi}(p)$, for any {\em
morphism} $\Phi: Act \rightarrow Act$. Here a morphism is a function
satisfying $\Phi(a.b)=\Phi(a).\Phi(b)$ for $a,b \in Act$. In addition
there is a renaming operator $s*p$, called {\em ticking}, for any
signal $s \in S$. This operator renames any action $a$ into $s.a$.
The only type of encapsulation operators permitted in {\sc Meije} are
the restriction operators $p\backslash s$ for any signal $s \in S$.
$p\backslash s$ is $\partial_H(p)$ for $H$ the set of all actions
containing $s$, i.e.\ all ``multisets'' in which $s$ has a positive or
negative multiplicity. {\sc Meije} also has an operator {\em
triggering} which is expressible in the others, and it lacks the
operator $+$, because, as explained in Section~\ref{choice}, that
operator is expressible in the others as well, but there is no further
difference between {\sc Meije} and aprACP$_F(Act,.)$.
\subsection{A Decidable Signature for aprACP}\label{decidable}
The language aprACP$_R(A,|)$ defined so far has an uncountable
signature if $A$ is infinite. There are namely uncountably many
encapsulation and renaming operators. Computationally it makes sense
to restrict attention to a fragment of aprACP$_R$ with a decidable
signature. This can be achieved by requiring the set of actions $A$ to
be decidable, and by restricting the permitted encapsulation and
renaming operators $\partial_H$ and $\rho_R$ to the ones where $A-H$
and $R$ are recursively enumerable sets. Such sets can be represented by
the code of a Turing machine that enumerates them, and it is decidable
whether an arbitrary piece of text is the code of a Turing machine
enumerating a recursive enumerable set. This makes the signature
decidable. As a consequence the set of recursion-free terms will be
decidable too.
I could have chosen $H$ to be enumerable instead of its complement
$A-H$. However, the choice above has the advantage that the
encapsulation operators can (in an obvious way) be regarded as special
relational renamings, so that one has one kind of operator less to be
concerned about. A more compelling argument will be presented in
Section~\ref{enumerable}.
In order to ensure that the set of recursive terms is decidable as
well, I have to require recursive specifications, seen as sets of
equations, to be recursively enumerable at least. This makes the set of
open terms decidable. However, it remains undecidable whether a
term is closed. The set of closed terms is not even enumerable.
Therefore one may wish to insist that in terms of the form $\rec{X|S}$
the set of recursion variables $V_S$ is decidable as well. This makes
$S$ computable. However, it is undecidable whether a piece of text is
the code of a Turing machine deciding membership of a set. Thus with
computable recursion even the set of open terms becomes undecidable
again.
Hence an even more restrictive requirement on the desired kind of
recursion is in order. Here I require $S$ to be primitive decidable.
This means that there is a primitive recursive function deciding
membership of $V_S$, and in case of a variable $X\in V_S$ returning
the term $S_X$. It is decidable whether a piece of text is the source
of a primitive recursive function, thus with this restriction the
signature as well as the sets of open and closed terms are decidable.
If moreover the communication function is required to be partial
recursive, the resulting variant of aprACP$_R$ will be denoted
aprACP$_R^{\rm r.e.}$. The other languages I mentioned can be
adapted in the same way. In aprACP$^{\rm r.e.}_F$ I have to allow
partial recursive renaming functions. In the original version of
aprACP$_F$, these where expressible in terms of total renamings and
encapsulation.
\subsection{Expressing the Left- and Communication Merge}\label{left}
The language ACP has two operators, $\lmerge$ and $|$, that I didn't
include in the syntax of aprACP$_F$. The reason is that these
operators can be expressed in the other operators of the language, and
thus need not be introduced as primitives. Here I show how.
\begin{table}[htb]
\begin{center}
\framebox{$\begin{array}{cc}
\displaystyle\frac{x\goto{a} x'}{x\lmerge y \goto{a} x'\| y} &
\displaystyle\frac{x\goto{a} x' ,~ y \goto{b} y' , ~a|b=c}
{x \mid y \goto{c} x'\| y'}
\end{array}$}
\end{center}
\caption{The left- and communication merge of ACP\label{aux}}
\end{table}
Table~\ref{aux} shows the action rules for the two operators.
\linebreak[3]
The left merge, $\lmerge$, behaves exactly like the {\em merge} or
parallel composition, $\|$, except that the first action is required
to come from its leftmost argument. The communication merge, $|$,
behaves exactly like $\|$, except that its first action is required to
be a communication between its two arguments. The operators' most
crucial use is in
the axiom CM1 $$x \| y = x \lmerge y + y \lmerge x + x \mid y$$
that plays an essential r\^ole in axiomatising ACP with bisimulation
semantics.
Note that the symbol $|$ is used for the communication function as
well as the communication merge. This overloading is intentional, as
the communication merge can be thought of as an extension of the
communication function, which is defined on actions only. The
vertical bar in the middle of an expression $\rec{X|S}$ is pronounced
{\em where}---and sometimes even written that way---and has nothing to
do with the communication function and merge. The vertical bar in a
set expression like $\{n\in \IN \mid n > 5\}$ is also pronounced {\em
where} and constitutes a fourth use of this symbol. Finally $|$ is
used to denote parallel composition in CCS. It is generally
easy to determine from the context which $|$ is meant.
In order to express $\lmerge$ and $|$ in aprACP$_F(A,|)$ I assume that
the set of actions $A$ is divided into a set $A_0$ of actions that may
be encountered in applications, and the remainder $H_0 = A-A_0$, which
is used as a working space for implementing useful operators, such as
$\lmerge$ and $|$. On $A_0$ the communication function is
dictated by the applications, but on $H_0$ I can choose it in any way
that suits me. The cardinality of $A_0$ should be infinite, and equal
to the cardinality of $A$.
For today's implementation I assume that $H_0$ contains actions {\tt
skip}, {\tt first}, {\tt next}, $a_{\tt first}$ and $a_{\tt next}$
(for $a \in A_0$). The communication function given on $A_0$ is
extended to these actions as indicated below (applying the convention
that if $a|b$ is not defined it is undefined).
%\begin{table}[h]
\begin{center}
$\begin{array}{|lr|}
\hline
a \mid {\tt first} = a_{\tt first} & (a\in A_0) \\
a \mid {\tt next} = a_{\tt next} & (a\in A_0) \\
a_{\tt first} \mid b_{\tt first} = a\mid b & (a,b\in A_0) \\
a \mid {\tt skip} = a & (a\in A_0) \\
\hline
\end{array}$
\end{center}
%\caption{\label{}}
%\end{table}
Let $H_1= A_0 \cup \{{\tt first}, {\tt
next}\}$. I will use a renaming operator $f_1$ that satisfies
$f_1(a_{\tt next}) = a$, $f_1(a_{\tt first}) = a_{\tt first}$
and $f_1(a)=a$ for $a \in A_0$.
Let me first introduce the notation $a^\infty$ to denote a process
that perpetually performs the action $a$. This process is obtained as
$a^{\infty} = \rec{X\mid X= aX}$. Now suppose $p$ is a process that
can do actions from $A_0$ only. Then $$\partial_{H_1}(p \| {\tt first}
({\tt next}^{\infty}))$$ is a process that behaves exactly like $p$,
except that every initial action has a tag (subscript) {\tt first}, and
every non-initial action has a tag {\tt next}. Thus
$\rho_{f_1}(\partial_{H_1}[p \| {\tt first} ({\tt next}^{\infty})])$ is
a process that behaves exactly like $p$, except that the initial
actions are tagged {\tt first}. It follows that for any two processes
$p$ and $q$ with actions from $A_0$ only $$p\mid q \bis{}\partial_{H_0}
\left( \rho_{f_1}(\partial_{H_1}[p \| {\tt first} ({\tt next}^{\infty})])
\mbox{\Large $\|$} \rho_{f_1}(\partial_{H_1}[q \| {\tt first} ({\tt
next}^{\infty})])\right).$$
In order to extend this result to processes with actions outside $A_0$
I use a bijective renaming $f_0:A \rightarrow A_0$ and its inverse
$f_0^{-1}$. The communication merge is expressed in aprACP$_F(A,|)$,
up to bisimulation equivalence, by
$$x\mid y \bis{} \rho_{f_0^{-1}}\left(\partial_{H_0}\left(\rho_{f_1}
(\partial_{H_1}[\rho_{f_0}(x) \| {\tt first} ({\tt next}^{\infty})])
\mbox{\Large $\|$}\rho_{f_1}(\partial_{H_1}[\rho_{f_0}(y) \| \cdots
])\right)\right).$$
Finally the left merge is expressed in terms of the communication merge
through $$x\lmerge y\bis{}\rho_{f_0^{-1}}({\tt skip}(\rho_{f_0}(y))
\mid\rho_{f_0}(x)).$$
\subsection{Expressing Choice}\label{choice}
As remarked in Section~\ref{meije}, the language {\sc Meije} lacks the
choice operator $+$ of CCS and ACP. The reason this operator was
omitted from the syntax of {\sc Meije} was that it can be expressed in
terms of the other operators. This is true in the setting of aprACP$_F$ as
well, so if one likes, this operator can be skipped from the signature.
For the implementation of choice, $A$ is again divided in $A_0$ and
$H_0$ and in $H_0$ we put the same actions as in the previous section,
together with the action {\tt choose}. The communication function also
works as before, except that there is no communication possible
between actions of the form $a_{\tt first}$ and $b_{\tt first}$. (So
maybe one wants to use a different action {\tt first}.) Instead one
has the communication ${\tt choose}\mid a_{\tt first} = a$ for $a \in
A_0$. Recall that for $p$ a process that can do actions from $A_0$
only, $\rho_{f_1}(\partial_{H_1}[p \| {\tt first} ({\tt
next}^{\infty})])$ is the same process in which the initial actions
are tagged with a subscript {\tt first}. This, by the way, is an
implementation of the operator {\em triggering} of {\sc Meije}.
It follows that $$p+q \bis{}\partial_{H_0}
\left( \rho_{f_1}(\partial_{H_1}[p \| {\tt first} ({\tt next}^{\infty})])
\mbox{\Large $\|$} {\tt choose} \mbox{\Large $\|$} \rho_{f_1}
(\partial_{H_1}[q \| {\tt first} ({\tt next}^{\infty})])\right)$$
since in the expression on the right {\tt choose} can communicate with
an initial action from only one of $p$ or $q$, so that the other one
is blocked forever. Using the renamings $\rho_{f_0}$ and its inverse,
just as in the previous section, $+$ is expressed in the rest of
aprACP$_F$.
\subsection{Expressing the Communication Function}\label{canonical}
It may be felt as a drawback that the language (apr)ACP, unlike CCS, is
parametrised by the choice of a communication function (besides the
choice of a set of actions). This, one could argue, makes it into a
collection of languages rather then a single one. Personally I do not
share this concern. If in different applications different
communication functions are used, they can, when desired, all be
regarded as different fragments of the same communication function,
each considered on only a small subset of the set of actions $A$. At
any given time there is no need to know all actions and the entire
communication function to be used in all further applications.
Alternatively one may argue that there are many parallel compositions
possible in ACP, namely one for every choice of a communication
function. Here I will present one instantiation of aprACP$_F(A,|)$, such
that for every other choice of a communication function the resulting
parallel composition is expressible in this language.
Let, as in the previous section, $A_0 \subseteq A$ be the actions that
are used in applications and $H_0=A-A_0$ the working space. I fix a
bijection $f_0:A \rightarrow A_0$ and abbreviate $\rho_{f_0}$ by
$\rho_0$. For this implementation, $H_0$ should contain the actions
$(a,b)$ for every $a,b \in A_0$, as well as an action $\delta$
denoting deadlock. The communication function $|$ is
defined by $a|b = (a,b)$ for $a,b \in A_0$ (thus undefined outside
$A_0$). Now for any other communication function $\gamma: A^2
\rightarrow A$ let $\bar{\gamma}:A\rightarrow A$ be a renaming satisfying
$\bar{\gamma}((\rho_0(a),\rho_0(b))) = c$ for those $a,b,c \in A$ with
$\gamma(a,b)=c$, and $\bar{\gamma}(a)=f_0^{-1}(a)$ for $a\in A_0$.
Furthermore, let $H$ be $\{(a,b)\in A_0\times A_0 \mid \gamma(a,b)
\mbox{ undefined} \}$.
Then the associated parallel composition $\|_\gamma$ is expressible in
aprACP$_F(A,|)$ by $$x \|_\gamma y \bis{}
\rho_{\bar{\gamma}}(\partial_H(\rho_0(x)\|\rho_0(y))).$$
\subsection{Expressing Renaming and Encapsulation}\label{renaming}
The syntax of aprACP$_F^{\rm r.e.}$ allows for a multitude of renaming
operators. Here I show that one needs only two, namely the operator
$\rho_0$, introduced earlier, which bijectively maps every action to
one in the subset $A_0$ of $A$, and the {\em universal renaming
operator} $\rho_F$. Every other functional renaming is then expressible.
To this end I introduce an action $\bar{f}\in H_0=A-A_0$ for every
partial recursive renaming function $f:A\rightarrow A$. I also
introduce an action $(\bar{f},a)\in H_0$ for every such $f$ and every
$a\in A_0$. The communication function is enriched by $\bar{f}\mid a =
(\bar{f},a)$ for $a \in A_0$ and the universal renaming $F$ should
satisfy $F((\bar{f},\rho_0(a)))=f(a)$. Let $H_1=A_0 \cup \{\bar{f}
\mid f:A\rightarrow A\}$. Then $\partial_{H_1} (\bar{f}^\infty\|
\rho_0(x))$ is a process that behaves exactly like $x$, except that
every action $a$ is renamed in $(\bar{f},\rho_0(a))$. Hence $\rho_f$
is expressible through $\rho_f(x)\bis{}\rho_F(\partial_{H_1}
(\bar{f}^\infty\| \rho_0(x)))$.
Note that every co-enumerable encapsulation operator can be regarded
as a partial recursive renaming, so also all encapsulation operators
can be expressed in aprACP with $\rho_0$ and $\rho_F$. The
encapsulation $\partial_{H_1}$ used in the construction can be
incorporated in $\rho_F$ as well.
In exactly the same way every enumerable relational renaming operator
is expressible in aprACP with only $\rho_0$ and a {\em universal
relational renaming}.
In the preceding section I showed how all operators $\|_\gamma$ with
$\gamma$ a communication function could be expressed in a particular
instantiation of aprACP$_F$, using a multitude of renamings. Here I
showed how all renaming operators of aprACP$_F^{\rm r.e.}$ can
be expressed in only two of them, using a particular communication
function, and similarly for the encapsulations. It is an easy exercise
to combine these results, and express all partial recursive renaming
operators, all co-enumerable encapsulations, and all parallel
compositions $\|_\gamma$ with $\gamma$ a partial recursive
communication function in a particular instantiation of aprACP$^{\rm
r.e.}_F$, with only one communication function and two renamings.
One may wonder whether {\em all} renaming operators can be expressed
in apr\-ACP, i.e.\ if it is possible to get rid of the last two. In
general this is not possible. However, if one only cares about the
behaviour of all the derived operators on the relevant subset $A_0$ of
$A$, it is possible to omit the use of $\rho_0$ from all the
constructions, encode the universal renaming in the communication
function, and find for any derived operator (such as $\lmerge$ or a
renaming) an aprACP-expression with the same behaviour on $A_0$.
\subsection{A Finite Signature for aprACP}
Here I show how the syntax of aprACP$^{\rm r.e.}_R$ can be reduced from a
decidable one to a finite one. In the previous section the set of
renaming and encapsulation operators was cut down to two elements, so
we are left with an infinity of actions to get rid of.
As in aprACP$^{\rm r.e.}_R$ the set of actions is decidable, they can be
numbered $a_0, a_1, a_2, \ldots$, such that the function ${\tt succ}:A
\rightarrow A$ given by ${\tt succ}(a_i)=a_{i+1}$ is partial recursive
(even computable). Hence every action is expressible in terms of $a_0$
and the renaming operator $\rho_{\tt succ}$.
\subsection{Expressing Relational Renaming}\label{relational}
In order to express relational renamings in aprACP$_F$ one needs to add
just one constant (or a third renaming) to the signature. One has to
assume the existence of actions $[a,b]$ in $H_0$ for $a,b\in A_0$. The
desired constant is ${\tt all}=\Sigma_{a,b\in A_0}[a,b]0$. Here
$\Sigma_{i\in I}$ is an infinite version of choice, to be formally
introduced in Section~\ref{kappa}. $\Sigma_{i\in I}$ is not a standard
ingredient in the syntax of aprACP---if it were there would be no
reason to add {\tt all} as a constant. {\tt all} can be expressed as
$\rho_R(c0)$ where $c$ is an action chosen from $A$ and $R$ is the
relation $\{(c,[a,b]) \mid a,b \in A_0\}$.
Now ${\tt allever}=\rec{X \mid X = {\tt all} \lmerge X}$ is a process
that perpetually performs an action of the form $[a,b]$, and at each
step has the choice between all such actions. For any relation $R
\subseteq A\times A$ the process $\partial_{A\times A - R}({\tt
allever})$ has at each step the choice between executing one the
actions $[a,b]$ with $R(a,b)$. Let ${\tt copy}:A_0 \rightarrow A$ be a
renaming that sends each action $a \in A_0$ to the (new) action
$a_{\tt copy}$. Define the communication function on the new actions
by $a_{\tt copy} \mid [a,b] = b$. Then for $p$ a process that does
actions from $A_0$ only $$\rho_R(p) \bis{} \partial_{H_0}(\rho_{\tt
copy}(p) \| \partial_{A \times A - R}({\tt allever}))$$
Thus, by means of $\rho_0$ and its inverse to deal with action from
outside $A_0$, all relational renaming operators are expressible in
aprACP$_F$ with {\tt all}.
{\tt all} can also be expressed in aprACP$_F$ using so-called {\em
unguarded recursion} (Section~\ref{guarded}) as ${\tt all} =
\rec{X\mid X= [a_0,a_0]0 + {\tt succ2}(X)}$ where ${\tt succ2}$ is a
renaming function enumerating the elements of $A\times A$. Thus, as
long as unguarded recursion is permitted, aprACP$_F$ is equally
expressive as aprACP$_R$. When unguarded recursion is banned, however,
aprACP$_R$ turns out to be more expressive.
\msection{Specifying Process Graphs}\label{specifying}
In this section I will isolate, for each of the classes of process
graphs mentioned in the introduction, a corresponding class of
process expressions that denote only graphs from that class. When
possible, I make these classes of expressions so large that every
graph of the appropriate kind can be denoted by an expression in the
corresponding class.
\begin{definition}{kinds}({\em Kinds of graphs}).
A process graph $G=(S,T,I) \in \IG(A)$ is
\begin{itemise}
\item {\em $\kappa$-bounded} (for an uncountable cardinal $\kappa$) if
for every state $s\in S$ there are less than $\kappa$ outgoing
transitions \plat{s \goto{a} s'},
\item {\em countable} if for every state $s\in S$ there are
at most countably many outgoing transitions \plat{s \goto{a} s'},
\item {\em finitely branching} if for every state $s\in S$ there are
only finitely many outgoing transitions \plat{s \goto{a} s'},
\item {\em recursively enumerable} if there exists an algorithm
enumerating all transitions $s\goto{a} s'$,
\item {\em decidable} if there exists an algorithm that, when given a
triple $(s,a,s') \in S\times A \times S$, determines whether this is a
transition from $T$,
\item {\em computable} if there exists an algorithm
that, when given a state $s\in S$, returns the complete finite
list of outgoing transitions \plat{s \goto{a} s'} and indicates when
the list is complete,
\item {\em primitive recursive} if there is such an algorithm that
is primitive recursive,
\item and {\em regular} if it has only finitely many states and
transitions.
\end{itemise}
\end{definition}
The class of all expressions defined so far will be the class of
countable process expressions. The $\kappa$-bounded process
expressions are obtained by enlarging the signature, whereas the other
classes of Figure~\ref{classes} are obtained by means of restriction.
\subsection[The k-bounded Process Expression]
{The $\kappa$-bounded Process Expressions}\label{kappa}
In order to define the $\kappa$-bounded process expressions I have to
generalise the syntax of aprACP$_R$, even beyond the boundaries imposed
by \df{signatures}. Whenever $I$ is an index set
and $p_i$ are process
expressions for $i\in I$, $\Sigma_{i\in I} p_i$ is now a process
expression too. It represents a choice between the processes $p_i$
($i\in I$). Since choice is associative and commutative for virtually
every semantics proposed in the literature, $I$ may be chosen to
range over sets rather than sequences. The corresponding action rules
(one abstract rule for every index set $I$ and index $j\in I$) are
$$\frac{x_j \goto{a} y}{\Sigma_{i\in I} x_i \goto{a} y}.$$ For this
purpose the set of variables should at least have cardinality
$\kappa$. The expression $p_1 + p_2$ can now be regarded as an
abbreviation for $\Sigma_{i=1,2}p_i$ and $0$ as the summation over an
empty index set. In the same fashion it is possible to introduce
infinitary parallel compositions.
Now the {\em $\kappa$-bounded process expressions} can be defined as
the ones in which all index sets, as well as the sets $V_S$ in
recursive specifications $S$, have cardinality less than $\kappa$.
Also, for every relational renaming $\rho_R$ and $a \in A$, the set $\{b
\mid R(a,b)\}$ should have less than $\kappa$ elements. It is
straightforward to prove that process graphs associated to
$\kappa$-bounded process expressions are $\kappa$-bounded. The
converse is true as well:
\begin{proposition}{kappa}
Every $\kappa$-bounded process graph can up to isomorphism be denoted
by a $\kappa$-bounded process expression.
\end{proposition}
\begin{proof}
Let $G=(S,T,I)$ be a $\kappa$-bounded process graph. Take a variable
$X_s$ for every state $s \in S$ and let \plat{\widetilde{G}} be the
recursive specification $\{X_s = \Sigma_{(s\goto{a}t)\in T} aX_t \mid
s \in S\}$. Now \plat{\rec{X_I | \widetilde{G}}} is a closed process
expression with \plat{\Id{\rec{X_I | \widetilde{G}}} \cong G}.
\end{proof}
\subsection{The Countable Process Expressions}\label{countable}
In the special case of the countable process expressions ($\kappa =
\aleph_1$) one allows countable alternative and parallel compositions
and countable recursion. However,
countable compositions can be expressed in terms of binary
compositions and countable unguarded recursion. Namely $$\Sigma_{i\in
\mbox{\scriptsize \IN}} p_i = \rec{X_0 \mid \{X_i = p_i + X_{i+1} \mid
i\in \IN\}}.$$ Thus the countable process expressions can be redefined to
be the ones with countable recursion but only binary alternative and
parallel composition.
Continuing from that perspective it can be observed that the addition
of arbitrary infinite recursion does not add to the expressive power
of the language, since in any expression $\rec{X|S}$ only countably
many variables are reachable from $X$. Thus the countable process
expressions can again be redefined to be exactly the ones introduced
in Section~\ref{acp}. It follows that
\begin{proposition}{countable}
Countable process expressions yield countable process
graphs and every countable process graph is denoted
by a countable process expression.
\end{proposition}
\subsection{The Bounded Process Expressions}\label{guarded}
The notion of guardedness was proposed in {\sc Milner} \cite{Mi80} to
syntactically isolate a class of recursive specifications that have
unique solutions. The definition below stems from {\sc Baeten,
Bergstra \& Klop} \cite{BBK87a}.
\begin{definition}{guardedness}({\em Guardedness}).
A free occurrence of a variable in a process expression $t$ is
{\em unguarded} if it does not occur in a subterm of the form $at'$.
Let $S$ be a recursive specification. The relation
\plat{\goto{u} \subseteq V_S \times V_S} is given by
\plat{X \goto{u} Y} iff $Y$ occurs unguarded in $S_X$.
$S$ is {\em guarded} if the relation \plat{\goto{u}} is well-founded.
\end{definition}
Besides ensuring unique solutions, the same requirement also helps to
keep the denoted process graphs finitely branching. Let a process
expression be {\em guarded} if in all its subexpressions $\rec{X|S}$
the recursive specification $S$ is guarded.
\begin{proposition}{guarded}
Guarded expressions in the languages (apr)ACP$_F$, CCS, SCCS and {\sc
Meije} denote finitely branching process graphs. Moreover, every
finitely branching process graph is denoted by a guarded process
expression.
\end{proposition}
\begin{proof}
The first statement follows with a straightforward induction on the
structure of terms, with in the case of recursion a nested induction
on the length of chains \plat{X_1 \goto{u} X_2 \goto{u} \cdots}.
The second statement follows immediately from the proof of \pr{kappa},
considering that unguarded recursion wasn't used there. In
\pr{countable} unguarded recursion has to be used to replace infinite
alternative compositions, but in order to denote finitely branching
graphs this is unnecessary.
\end{proof}
Due to the relational renaming (or inverse image) operator this
proposition does not hold for aprACP$_R$ and CSP. In case the set $\{b
\mid R(a,b)\}$ is infinite, $\rho_R(a)$ denotes an infinitely branching
process graph.
Let a relation $R \subseteq A \times A$ be {\em image-finite} if
$\forall a\in A: \{b \mid R(a,b)\}$ is finite. Then the {\em bounded}
process expressions can be defined as the ones with only guarded
recursion and image-finite renaming operators. It follows that the
bounded process expressions denote only finitely branching graphs.
\subsection{The Recursive Enumerable Process Expressions}
\label{enumerable}
The {\em recursively enumerable} process expressions are the ones
that appear in the language aprACP$^{\rm r.e.}_R(A,|)$. This is the
variant of aprACP$_R$ with a decidable signature, introduced in
Section~\ref{decidable}. $A$ has to be decidable and $|$ a partial
recursive function. Moreover, only encapsulation operators
$\partial_H$ with $H$ co-r.e. are allowed (i.e.\ the complement of $H$
should be enumerable), and only renaming operators $\rho_R$ with $R$
enumerable. Finally recursive specifications $S$ are required to be
primitive recursive.
\begin{proposition}{enumerable}
Any process $\Sigma_{i\in I}p_i$ with $\{p_i\mid i\in I\}$ a recursive
enumerable set of recursive enumerable process expressions is
expressible in aprACP$^{\rm r.e.}_R$.
\end{proposition}
\begin{proof}
A classic recursion theoretic theorem states that any non-empty
r.e.\ set can be obtained as the image of a primitive
recursive function. See e.g.\ Corollary 4.18 in {\sc Manin}
\cite{Ma77}. It follows that $\Id{\Sigma_{i\in I}p_i}\bis{}
\Id{\Sigma_{i\in \rm I\hspace{-0.55mm}N}p(n)}$ for certain primitive
recursive function $p:\IN\rightarrow ($the closed aprACP$^{\rm
r.e.}_R$-expressions). Now use the construction from
Section~\ref{countable}.
\end{proof}
\begin{proposition}{r.e.}
The r.e.\ process expressions denote exactly the r.e.\ graphs.
\end{proposition}
\begin{proof}
It is straightforward to enumerate (recursively) the valid proofs of
transitions between aprACP$^{\rm r.e.}_R$ expressions, and hence the
transitions themselves. Note that for this to be true one needs the
complement of $H$ in $\partial_H$ to be enumerable rather than $H$
itself. This is the argument promised in Section~\ref{decidable}.
The other direction follows immediately from the proof of \pr{kappa},
using \pr{enumerable}.
\end{proof}
{\sc De Simone} \cite {dS85} proved that in order to denote every
r.e.\ process graph it is sufficient to use finite recursion only.
However, whereas the Propositions \ref{pr-kappa}--\ref{pr-r.e.} are
rather trivial and only use inaction, action prefix, choice and
recursion, De Simone's construction is more intricate and uses the
entire syntax of {\sc Meije}.
\begin{theorem}{dS2}
Let $A$ be an decidable set of actions. There exists an decidable set of
signals $S$, such that for every r.e.\ process graph $G \in \IG(A)$
there exists a closed r.e.\ expression $t$ with finite recursion in
{\sc Meije}$(A,S)$ for which $\Id{t}\bis{} G$.
\end{theorem}
As {\sc Meije} can be implemented in aprACP$_F$, this theorem implies that
for every decidable set $A$ there is a decidable set $A' \supseteq A$ and a
r.e.\ communication function $|$ on $A'$, such that every r.e.\
process graph can, up to bisimulation, be denoted by an expression in
aprACP$_F^{\rm r.e.}(A',|)$ with only finite recursion.
It follows immediately from \pr{guarded} that the use of unguarded
recursion is unavoidable in De Simone's result. Still, it is possible
to limit such use to a minimum. Suppose $A$ contains actions $a_i$ and
$b_i$ for $i\in \IN$. The process $\Sigma_{i\in \rm
I\hspace{-0.55mm}N}a_i b_i 0$ can be obtained with unguarded recursion
as $\rec{X|X\!=\!a_0 b_0 0 + \rho_f(X)}$ in which $f$ is the renaming
with $f(a_i) = a_{i+1}$ and $f(b_i) = b_{i+1}$ for $i\in \IN$. Adding
this process as a constant $U$ to the language aprACP$_F$---thereby
obtaining aprACP$_U$---makes it possible to recreate De Simone's result
without using unguarded recursion.
\begin{theorem}{universal}
Let $A$ be a decidable set of actions. There exists an decidable set of
actions $A'$ and a partial recursive communication function $|$ on $A'$,
such that for every r.e.\ process graph $G \in \IG(A)$ there exists a
closed expression $t$ with finite guarded recursion in the language
aprACP$_U^{\rm r.e.}(A',|)$ for which $\Id{t}\bis{}G$.
\end{theorem}
\begin{proof}
The proof is a variation on the one of De Simone.
Consider the r.e.\ process graphs over $A$ with as nodes the natural
numbers. Since I consider graphs up to bisimulation equivalence, I may
assume that there is at most one edge between every two nodes. Such a
graph $G$ can be represented by an algorithm $g$ that, when given a pair
of nodes $(i,j)$, runs for some time and returns $a$ in case there is
a transition $(i,a,j)$. In case there is no transition from $i$ to $j$
it returns the value $\delta$ or runs forever.
Now let $A'$ be the set of all such algorithms $g$, together with $A$,
a special symbol $\delta$ denoting (dead)lock, and the actions {\tt
to}$_i$ and {\tt from}$_i$ for $i\in \IN$. Note that the set of
algorithms (in a particular form, such as Turing machine code) of
partial recursive functions is decidable, i.e.\ it is decidable
whether an arbitrary piece of text constitutes such an algorithm, and
hence an element of $A'$. Let the communication function $|$ be given
by $g \mid {\tt from}_i \mid {\tt to}_j = g(i,j)$. [To be precise, in
order to implement this in the ACP communication format I also need
actions of the form ${\tt fromto}_{ij}$, $g(i,\cdot)$ and
$g(\cdot,j)$].
The next thing I need is the {\em left merge} operator $\lmerge$ from
ACP, which, as we saw in Section~\ref{left}, can be expressed in
aprACP$_F$. By means of a renaming, the new constant $U$ can be turned
into ${\tt flow} = \Sigma_{i\in \rm I\hspace{-0.55mm}N}{\tt to}_i {\tt
from}_i 0$. This process describes the flow of control through an
arbitrary state. It says that when one enters state $i$, the next
thing to do is leaving the same state. Using only guarded recursion I
subsequently define the process ${\tt control} = {\tt flow} \lmerge
{\tt control}$. This process will be put in a context where in each
step a {\tt from} action and a {\tt to} action synchronise. As a
result, when the $n^{th}$ synchronisation involves a {\tt to}$_i$
action, denoting the arrival in state $i$, the next synchronisation
involves a {\tt from}$_i$, denoting departure from the same state.
The choice of the {\tt to} action is not restricted (by the {\tt
control} process). In order to initialise the process properly, and to
allow a first synchronisation, I use the initialised control $C = {\tt
from}_0 \| {\tt control}$, in which $0$ is supposed to be the initial
state.
Now a graph $G$ is represented by the expression
$\partial_H(g^{\infty} \| C)$. Here $g^{\infty}$ is a shorthand for
$\rec{X \mid X=gX}$, i.e.\ the process that repeatedly performs the
action $g$, and $H = A'-A$. It is easy to see that
$\Id{\partial_H(g^{\infty} \| C)} \cong G$.
\end{proof}
\begin{corollary}{universal}
Let $A$ be a countably infinite decidable set of actions. There exists
a partial recursive communication function $|$ on $A$, such that for
every r.e.\ process graph $G \in \IG(A)$ there exists a closed
expression $t$ with finite guarded recursion in the language
aprACP$_U^{\rm r.e.}(A,|)$ for which $\Id{t}\bis{}G$.
\end{corollary}
\begin{proof}
Partition $A$ into two infinite decidable subsets $A_0$ and $H_0$.
It suffices to prove the statement for $G\in \IG(A_0)$, since an
arbitrary r.e.\ process graph can be obtained as $\rho_f(G)$ for such
a $G$ with $f:A_0 \rightarrow A$ a bijective renaming.
By \th{universal} there is an extension $A'$ of $A_0$ and a partial
recursive communication function $|'$ on $A'$, such that for every
r.e.\ process graph $G \in \IG(A_0)$ there exists a closed expression
$t$ with finite guarded recursion in the language aprACP$^{\rm
r.e.}_U(A',|')$ for which $\Id{t}\bis{}G$. Let $h:A' \rightarrow A$ be
a recursive bijection with $h(a)=a$ for $a\in A_0$. Define the partial
recursive communication function $|:A^2 \rightarrow A$ by $h(a) \mid
h(b) = h(c)$. Let $\tilde{t}$ be the closed aprACP$^{\rm
r.e.}_U(A,|)$-expression obtained from $t$ by replacing all action
names $a$ by $h(a)$, including the action names in the subscripts of
encapsulation and renaming operators. Then $\Id{t}\bis{}G$ immediately
implies $\Id{\tilde{t}}\bis{}G$.
\end{proof}
\subsection{The Decidable and the Effective Expressions}
{\sc De Simone} \cite{dS84a} shows that with unguarded recursion it is
easy to specify undecidable processes. Therefore the first
requirement of a {\em decidable} process expression is that only
guarded recursion is permitted. In this setting there are already
three different variants of aprACP to consider: the language aprACP$_F$
with functional renaming, the language aprACP$_R$ with relational
renaming, and the language aprACP$_U$ with the constant $U$, introduced
in the previous section. The subscript $U$ reminds of {\em universal}
and is inspired by \th{universal}. Note that the guarded version of
aprACP$^{\rm r.e.}_U$ is at least as expressive as the guarded version
of aprACP$^{\rm r.e.}_R$. Namely, as $A$ is decidable, the constant
{\tt all} of Section~\ref{relational} can be obtained from $U$ by
means of encapsulation and renaming, and aprACP$^{\rm r.e.}_R$ turned
out to be guardedly expressible in terms of aprACP$^{\rm r.e.}_F$ with
{\tt all}. As long as unguarded recursion was allowed, the three
languages were equally expressive, but this is here no longer the
case.
A second requirement for decidable process expressions has to do with
the computable nature of the operators of the language. For the
relational renaming operators $\rho_R$ it is not sufficient to require
the relations $R$ to be decidable, as any recursively enumerable relation
can be obtained as the composition of two decidable ones.
In particular, the process $\Sigma_{a\in A} a0$ is surely decidable,
and can be obtained as the image of a single action under a suitable
decidable relational renaming. However, for any nonempty recursive
enumerable set of actions $B \subseteq A$, the (generally
undecidable) process $\Sigma_{b\in B}b0$ can be obtained as
$\rho_f(\Sigma_{a\in A} a0)$ with $f$ a primitive recursive function
(recalling that a primitive recursive function is a special total
recursive function, and any total recursive function, seen as a
relation, is decidable). This is Corollary 4.18 in {\sc Manin}
\cite{Ma77}.
A similar problem arises for the communication function. There are two
ways in which to strengthen the decidability requirement so as to avoid
these problems. The renaming operators as well as the communication
function should be either {\em effective} or {\em coeffective}.
The requirement of effectivity comes, in the more general setting of
De Simone languages, from {\sc Vaandrager} \cite{Va93}.
\begin{definition}{effective-pracp}({\em Decidable terms})
An aprACP$_R(A,|)$-expression is {\em effective} if
\begin{list}{\bf --}{\leftmargin 18pt
\labelwidth 12pt \topsep 0pt \itemsep 0pt \parsep 0pt}
\item $A$ is a decidable set,
\item $|$ is given as a total recursive function \plat{|:A^2
\rightarrow A \dcup \{\delta\}}\\
---$a|b=\delta$ means that $a$ and $b$ do not communicate,
\item it contains only computable guarded recursion,
\item it contains only encapsulation operators $\partial_H$ for which
$H$ is decidable
\item and only renamings $\rho_R$ for $R$ such that $\forall a\in A:
(\{b \mid R(a,b)\}$ is finite), and the total function which
yields for any $a\in A$ this finite set is recursive.
\end{list}
A aprACP$_U(A,|)$-expression is {\em coeffective} if
\begin{list}{\bf --}{\leftmargin 18pt
\labelwidth 12pt \topsep 0pt \itemsep 0pt \parsep 0pt}
\item $A$ is a decidable set,
\item $|$ satisfies $\forall c\in A: (\{(a,b) \mid a|b=c\}$ is finite),
and the total function which yields for any $c\in A$ this finite
set is recursive,
\item it contains only computable guarded recursion,
\item it contains only encapsulation operators $\partial_H$ for which
$H$ is decidable
\item and only renamings $\rho_R$ for $R$ such that $\forall b\in A:
(\{a \mid R(a,b)\}$ is finite), and the total function which
yields for any $b\in A$ this finite set is recursive.
\end{list}
A aprACP$_U(A,|)$ expression is {\em decidable} if it is either
effective and without the constant $U$ or coeffective.
\end{definition}
Note that, due to the use of countable recursion, the (co)effective
expressions are not a subclass of the enumerable ones. Using only
primitive recursive recursion would be a more serious restriction than
in the the previous section, as \pr{enumerable} crucially depends on
the use of unguarded recursion.
Mixing effective and coeffective ingredients in one process expression
leads in general to undecidable processes. As indicated above, adding
$U$ to the effective processes is already catastrophic.
\begin{proposition}{cfb}
Effective process expressions denote only computable graphs.
Decidable expressions denote only decidable graphs.
\end{proposition}
\begin{proof}
Two straightforward structural inductions.
\end{proof}
I have no idea how to represent {\em all} decidable graphs by
decidable process expressions. The proof strategy adopted for
\th{universal} makes use of a highly non-coeffective communication
function as well as the non-effective constant $U$. Similarly I don't
know if it is possible to represent all computable graphs by effective
process expressions with finite recursion. However, the same recipe as
used in the previous sections yields
\begin{proposition}{cfb-universal}
Every computable process graph is denoted by an effective process
expression, using only choice, (in)action and recursion.
\end{proposition}
\begin{proof}
If $G\in \IG(A)$ is computable it follows
immediately that the recursive specification \plat{\widetilde{G}}
constructed in the proof of \pr{kappa} is computable.
\end{proof}
In {\sc Ponse} \cite{Po92}, every computable graph is denoted by an
effective expression in the language $\mu$CRL. The trivial proof
above could be seen as a considerable simplification of his
construction. However, Ponse uses finite recursion schemata,
parametrised with recursive data parameters, whereas I use plain
infinite recursion.\\[2ex] It is interesting to compare this positive
result with the following negative one.
\begin{definition}{effective}({\em Effectivity})
An interpretation of a decidable language in a graph domain is {\em
effective} if it induces a total recursive function from the closed
terms to (descriptions of) computable process
graphs.
\end{definition}
The concept of an effective interpretation is due to {\sc
Vaandrager} \cite{Va93}. Let a language be {\em decidable} if its set
of closed terms is decidable (as in aprACP$^{\rm r.e.}_R$).
The following theorem stems from {\sc Baeten, Bergstra \& Klop}
\cite{BBK87a}. Is has been sharpened in {\sc Vaandrager} \cite{Va93},
who established it for the even coarser notion of trace equivalence.
\begin{theorem}{effective}
Let $A$ be a set of at least two actions. No decidable language with
an effective interpretation in $\IG(A)$ is able to denote all
computable process graphs, up to bisimulation equivalence.
\end{theorem}
If follows that the set of effective process expressions is not
decidable. This is due to the presence of computable recursion, which
was observed to make the language undecidable already in Section
\ref{decidable}. Similarly, the set of expressions in Ponse's language
is undecidable. It also follows that the decidability requirement in
the above theorem is essential.
\subsection{The Primitive Effective Process Expressions}
In Section~\ref{decidable} I proposed a variant aprACP$^{\rm r.e.}_R$ of
aprACP$_R$ with a decidable signature. In Section~\ref{enumerable}
this language turned out to denote only enumerable process graphs.
Furthermore in Section~\ref{canonical} there turned out to be a
{\em canonical} instantiation of this language, such that any other
instantiation (with a different communication function) is expressible
in it. Here I search for a similar variant of aprACP in which only
decidable graphs can be denoted.
The first idea could be to take the language of all effective process
expressions in aprACP$^{\rm r.e.}_U$ (or the coeffective ones or both).
However, such a language has an undecidable signature. To be precise,
as it is undecidable whether a piece of text is the code of a Turing
machine representing a total recursive function, the set of renaming
(and encapsulation) operators is undecidable.
Thus the collection of permitted encapsulation and renaming operators
has to be cut down until their codes form a decidable set. It is
tempting to think that Section~\ref{renaming} offers a solution, as it
allows all these operators to be expressed in only two of them.
However, the construction enabling this requires an action to be
introduced in $A$ for any renaming operator. This
only shifts the undecidable signature problem from the renaming
operators to the set of actions.
Another idea is allow any decidable selection of (co)effective renaming
operators to constitute a valid instantiation of the desired
language. This is basically what is done in {\sc Vaandrager}
\cite{Va93} for the recursive specifications. There only one
computable recursive specification is allowed. However, this violates
the desired property of canonicity, as one cannot express all
(co)effective renamings (or computable specifications) in one
decidable selection.
Hence a (complexity) class of such operators has to be found for which
it is decidable whether (a description of) an operator is in this
class. As in Section~\ref{decidable} I take the class of {\em
primitive recursive} operators. It should be admitted that many other
(complexity) classes would serve the purpose equally well.
In order to maintain the canonicity result of Section~\ref{canonical},
I also have to require primitive recursion for the communication
function, which in turn requires $A$ to be primitive decidable.
\begin{definition}{primitive}({\em Primitive})
An aprACP$_R(A,|)$-term is {\em primitive effective} if
\begin{list}{\bf --}{\leftmargin 18pt
\labelwidth 12pt \topsep 0pt \itemsep 0pt \parsep 0pt}
\item $A$ is a primitive decidable set,
\item $|$ is given as a primitive recursive function \plat{|:A^2
\rightarrow A \dcup \{\delta\}},
\item it contains only primitive recursive guarded recursion,
\item only encapsulation operators $\partial_H$ for which
$H$ is primitive decidable
\item and only renamings $\rho_R$ for $R$ such that $\forall a\in A:
(\{b \mid R(a,b)\}$ is finite), and the function which
yields for any $a\in A$ this finite set is primitive recursive.
\end{list}
A aprACP$_U(A,|)$-expression is {\em primitive coeffective} if
\begin{list}{\bf --}{\leftmargin 18pt
\labelwidth 12pt \topsep 0pt \itemsep 0pt \parsep 0pt}
\item $A$ is a primitive decidable set,
\item $|$ satisfies $\forall c\in A: (\{(a,b) \mid a|b=c\}$ is finite),
and the total function which yields for any $c\in A$ this finite
set is primitive recursive,
\item it contains only primitive recursive guarded recursion,
\item only encapsulation operators $\partial_H$ for which
$H$ is primitive decidable
\item and only renamings $\rho_R$ for $R$ such that $\forall b\in A:
(\{a \mid R(a,b)\}$ is finite), and the function which
yields for any $b\in A$ this finite set is primitive recursive.
\end{list}
A aprACP$_U(A,|)$ expression is {\em primitive decidable} if it is either
primitive effective and without the constant $U$ or primitive
coeffective.
\end{definition}
The languages of primitive (co)effective aprACP expressions will be
denoted aprACP$_R^{\rm p.e.}(A,|)$ and aprACP$_U^{\rm p.c.}(A,|)$.
It is easy to see that the signatures and sets of open and closed
terms of these languages are decidable. As it is very easy to
recognise the sources of primitive recursive functions, they are even
primitive decidable. Also the canonicity results of
Section~\ref{canonical}, as well as the expressibility results of
Sections \ref{left} and \ref{choice} apply to these variants of aprACP.
The {\em primitive decidable} process graphs are defined just like the
decidable ones (\df{kinds}), but with the additional requirement that
the involved algorithm uses only primitive recursion. Exactly as
before it follows that
\begin{proposition}{primitive}
Primitive effective process expressions denote only primitive
recursive process graphs. Primitive decidable
expressions denote only primitive decidable graphs.
Every primitive recursive process graph is denoted
by a primitive effective process expression.\hfill $\Box$
\end{proposition}
\subsection{The Regular and the Recursion-free Expressions}
Finally the {\em regular} process expressions are the ones with finite
guarded recursion, and no other operators than inaction, action prefix
and choice occurring in recursive specifications, whereas the
{\em recursion-free} ones obviously have no recursion at all.
It is easy to show that regular process expressions denote only
regular process graphs, and recursion-free expressions only finite and
acyclic process graphs. Conversely, every regular process graph is
denotable by a regular process expression, and every every finite and
acyclic process graph is, up to bisimulation equivalence, denotable by
a recursion-free expression.
\msection{De Simone Languages}\label{dS}
A {\em De Simone language} is a language of which the syntax is given
as an annotated signature, and the semantics as a TSS over that
signature of a particular form, known as the {\em De Simone} format.
\begin{definition}{simone}({\em The De Simone format}).
A TSS is in the {\em De Simone} format if for every recursive
specification $S$ and $X \in V_S$ it has a rule
$$\displaystyle\frac{S_x[\rec{Y|S}/Y]_{Y\in V_S} \goto{a}
z}{\rec{X|S}\goto{a}z}$$ and each of its other rules (the
{\em De Simone rules}) has the form
$$\frac{\{x_i\goto{a_i}y_i\mid i\in I\}}{f(x_1,\dots,x_n)\goto{a}t}$$
where $(f,n)\in \Sigma$, $I\subseteq \{1,\ldots,n\}$ and $t\in
\IT(\Sigma)$ is univariate recursion-free term containing no other
variables than $x_i$ ($1\leq x \leq n$ and $i\not\in I$) and $y_i$
($i\in I$). Here {\em univariate} means that
each variables occurs at most once.\\
In a rule of the above form, $(f,n)$ is the {\em type}, $a$ the
{\em action}, $t$ the {\em target}, and the tuple $(l_1,\ldots,l_n)$
with $l_i = a_i$ if $i\in I$ and $l_i=*$ otherwise, the {\em trigger}
\cite{Va93}.
\end{definition}
Most process description languages encountered in the literature,
including CCS, SCCS, CSP, ACP and {\sc Meije}, are De Simone
languages. De Simone languages are known to satisfy all the sanity
requirements of Section~\ref{expressibility} up to bisimulation
equivalence. Below I will generalise the classification of process
expressions in aprACP$_R$ to a classification of De Simone languages.
I will not consider the classes of finite, regular and
$\kappa$-bounded expressions. The De Simone languages from \df{simone}
are the countable ones.
\begin{definition}{guarded}({\em Guarded}).
Let $P=(\Sigma,A,R)$ be a TSS in De Simone format. For $(f,n)\in
\Sigma$ and $1\leq i \leq n$, the $i^{th}$ argument of $(f,n)$ is {\em
awake} if there is a rule in $R$ of type $(f,n)$ with $i$ in its index
set. For \plat{t \in \IT^r(\Sigma)} a free occurrence of a variable
in $t$ is {\em awake} or {\em unguarded} if for every subterm
$f(t_1,...,t_n)$ of $t$ such that the occurrence is in $t_i$, the
$i^{th}$ argument of $f$ is awake.
Let $S$ be a recursive specification. The relation
\plat{\goto{u} \subseteq V_S \times V_S} is given by
\plat{X \goto{u} Y} iff $Y$ is awake in $S_X$.
$S$ is {\em guarded} if the relation \plat{\goto{u}} is well-founded.
\end{definition}
This notion of guardedness is due to {\sc Vaandrager} \cite{Va93}.
Guarded recursive specifications in any De Simone language have unique
solutions.
\begin{definition}{dS-effective}
A TSS $P$ in De Simone format is said to be
\begin{itemise}\vspace{-1pt}
\item {\em (recursively) enumerable} if $\Sigma$ is decidable,
only primitive recursive recursion is allowed, and the set of
De Simone rules is r.e.\vspace{-1pt}
\item {\em bounded} \cite{Va93} if only guarded recursion is allowed
and for each type and trigger the set of rules involving that
type and trigger is finite.\vspace{-1pt}
\item {\em effective} \cite{Va93} if $\Sigma$ is decidable,
only computable guarded recursion is allowed, and there
exists a total recursive function associating with each type
and trigger the finite set of rules with that type and trigger.
\vspace{-1pt}
\item {\em coeffective} if $\Sigma$ is decidable,
only computable guarded recursion is allowed, and there
exists a total recursive function associating with each type,
action and target the finite set of corresponding rules.
\vspace{-1pt}
\item {\em primitive effective} if $\Sigma$ is primitive
decidable, only primitive recursive\linebreak guarded recursion
is allowed, and there exists a primitive recursive function
associating with each type and trigger the finite set of
corresponding rules.\vspace{-1pt}
\item {\em primitive coeffective} if $\Sigma$ is primitive
decidable, only primitive recursive guarded recursion is
used, and there is a primitive recursive function
giving for each type, action and target the finite set
of corresponding rules.
\vspace{-1pt}
\end{itemise}
\end{definition}
It is not difficult to apply these requirements to the De Simone
language aprACP$_U$ and verify that they coincide exactly with the ones
from Section~\ref{specifying}.
\begin{proposition}{effective}
Terms in a De Simone language with a property on the left
\begin{center}
\begin{tabular}{|l|l|}
\hline
countable & countable\\
bounded & finitely branching\\
recursively enumerable & recursively enumerable\\
effective & computable\\
coeffective & decidable\\
primitive effective & primitive recursive\\
primitive coeffective & primitive decidable\\
\hline
\end{tabular}
\end{center}
denote only process graphs satisfying the corresponding property on
the right.\\
\pf Straightforward.\hfill $\Box$
\pagebreak[3]
\end{proposition}
The main results announced in this extended abstract concern the
expressibility of arbitrary De Simone languages in aprACP$_R$.
In order to state which expressiveness results have been obtained,
more properties of De Simone languages need to be defined.
\begin{definition}{dependence}({\em Dependence of operators}).
Let $P=(\Sigma,A,R)$ be a TSS in De Simone format, then {\em
dependence} is the smallest transitive binary relation on $\Sigma$
such that $(f,n)$ {\em is dependent on} $(g,m)$ if there is a rule
with type $(f,n)$ and with $(g,m)$ occurring in its target.
\end{definition}
\begin{definition}{dS-finitary}
A TSS $P$ in De Simone format is said to be
\begin{itemise}\vspace{-1pt}
\item {\em width-finitary} if for each type there are only finitely many
targets (such that there is a rule with that type and target).
\vspace{-1pt}
\item {\em (primitive) width-effective} if there exists a (primitive)
recursive function giving for each type the finite set
of corresponding targets.\vspace{-1pt}
\item {\em finitary} if\vspace{-6pt}
\begin{itemise}
\item[\bf --] ({\em depth}:) each type is dependent on only
finitely many other types, \vspace{-4pt}
\item[\bf --] ({\em width}:) and for each type there are only
finitely many targets.
\end{itemise}\vspace{-1pt}
\item {\em image-finite} if for each type and trigger the
matching set of rules is finite.\vspace{-1pt}
\item {\em functional} if there exists a finite upperbound for
the number of rules with any given type and trigger.\vspace{-1pt}
\end{itemise}
\end{definition}
The first two properties can best be understood when viewing a De
Simone language as an abstract TSS. Width-finitariness is then the
property that for every type there are only finitely many abstract
rules. (Primitive) width-effectiveness moreover requires that there is
a (primitive) recursive function associating with each type the finite
set of abstract rules of that type. A language is finitary if the
behaviour of a finite term can be deduced by considering only finitely
many abstract rules. Thus a finitary De Simone language can be
obtained as the combination of a number of De Simone languages with
finitely many abstract rules, each of which is trivially primitive
width-effective. Boundedness is the combination of guarded- and
image-finiteness. As seen in Section~\ref{acp}, aprACP$_R$ is
width-finitary, and even primitive width-effective. As in aprACP$_R$
every type is dependent only on itself (at most), the language is
finitary as well. Image-finiteness for aprACP$_R$ reduces to
image-finiteness of the relational renamings, and functionality
corresponds with the restriction to aprACP$_F$.
The following table lists a number of {\em translatable properties} of
De Simone languages. Every translatable property consist of a full row
in the table, thus being the conjunction of a left and a right side.
For aprACP$_R$, in each property the left side is either always true or
implied by the right side.
\begin{table}[htb]
\centering{
\begin{tabular}{|l|l|}
\hline
width-finitary & with guarded recursion\\
width-effective & with computable guarded recursion\\
primitive width-effective & with prim. rec. guarded recursion\\
finitary & with finite guarded recursion\\
image-finite & with image-finite renaming\\
functional & with functional renaming\\
-- & recursively enumerable\\
primitive width-effective & primitive effective\\
\hline
\end{tabular}
}
\caption[Translatable properties]{\small Properties of De Simone
languages preserved under translation to aprACP$_R$\label{trans}}
\vspace{-1ex}\end{table}
\begin{theorem}{expressibility}
Any De Simone language satisfying certain translatable properties of
Table~\ref{trans} is expressible in the version of aprACP$_R$ with the
same properties.
\end{theorem}
\begin{proof}
To be supplied in the full version of this paper. My proof is an
adaptation of De Simone's construction, but avoids, when possible, the
use of unguarded recursion, by resorting to a richer synchronisation
algebra $(A,|)$. There is essentially only one construction,
translating any open term in any (countable) De Simone language into
aprACP$_R$. For any of the properties on the right in Table
\ref{trans}, I followed the construction backwards to see which
additional requirements on De Simone languages are needed to ensure
that the version of aprACP they are translated into meets that
property. This yielded the properties on the left.
\end{proof}
By taking the dependencies between the properties in Table~\ref{trans}
into account---finite recursion is surely primitive recursive,
primitive effectivity entails both image-finiteness and primitive
recursive guarded recursion, and with unguarded recursion aprACP$_F$ is
as good as aprACP$_R$---\th{expressibility} establishes 30
expressibility results. Since virtually all De Simone languages
encountered in practice are finitary, the most significant results are
\begin{enumerate}\vspace{-1ex}
\item Any finitary De Simone language is expressible in
aprACP$_R$ with finite guarded recursion.\vspace{-1ex}
\item Any finitary image-finite De Simone language is expressible in
aprACP$_R$ with finite guarded recursion and image-finite
renamings.\vspace{-1ex}
\item Any finitary functional De Simone language is expressible in
aprACP$_F$ with finite guarded recursion.\vspace{-1ex}
\item Any finitary enumerable De Simone language is
expressible in aprACP$^{\rm r.e.}_R$ with finite guarded recursion.
\vspace{-1ex}
\item Any finitary enumerable image-finite De Simone language
is expressible in aprACP$^{\rm r.e.}_R$ with finite guarded
recursion and image-finite renamings.\vspace{-1ex}
\item Any finitary enumerable functional De Simone language is
expressible in aprACP$^{\rm r.e.}_F$ with finite guarded recursion.
\vspace{-1ex}
\item Any finitary primitive effective De Simone language is
expressible in aprACP$^{\rm p.e.}_R$ with finite guarded recursion.
\vspace{-1ex}
\item Any finitary primitive effective functional De Simone language is
expressible in aprACP$^{\rm p.e.}_F$ with finite guarded recursion.
\end{enumerate}\vspace{-1ex}
In each of these results the De Simone languages are also assumed to
have finite guarded recursion only, but, by the compositionality of
recursion, the same results hold without requiring or getting
guardedness, finiteness or both.
Result 4 generalises the original theorem by De Simone, saying that any
finitary recursively enumerable De Simone language with finite recursion
is expressible in the recursively enumerable version of {\sc Meije} with
finite recursion. The generalisation is that, under the assumption
that the source languages have only guarded recursion, the target
language (now aprACP$_R$) can be required to use only guarded recursion
as well.
Using the constant $U$ yields an even stronger result for recursive
enumerable De Simone languages, namely by dispensing with
finitariness. This result has no effective counterpart.
\begin{theorem}{universal-expressibility}
Any recursively enumerable De Simone language is expressible in
aprACP$_U$ with finite guarded recursion.
\end{theorem}
\paragraph{Acknowledgments}
Many thanks to Hanna Wali\'nska and Anna Patterson for proofreading,
and to the editors and publisher of this proceeding for delaying
publication until my contribution was ready.
\begin{thebibliography}{10}
\vspace{-1ex}
\bibitem{AB84}
{\sc D.~Austry \& G.~Boudol} (1984):
\newblock {\em Alg\`{e}bre de processus et synchronisations.}
\newblock {TCS} 30(1), pp. 91--131. See
also \cite{Bo85}.\vspace{-1ex}
\bibitem{BBK87a}
{\sc J.C.M. Baeten, J.A. Bergstra \& J.W. Klop} (1987):
\newblock {\em On the consistency of {Koomen's} fair abstraction rule.}
\newblock {TCS} 51(1/2), pp. 129--176.%
\vspace{-1ex}
\bibitem{BK84}
{\sc J.A. Bergstra \& J.W. Klop} (1984):
\newblock {\em The algebra of recursively defined processes and the algebra of regular processes.}
\newblock In J.~Paredaens, editor: {\sl Proc. $\it 11^{th}$ ICALP, {Antwerpen}}, {\rm LNCS} 172, Springer-Verlag, pp. 82--95.
\vspace{-1ex}
\bibitem{Bo85}
{\sc G.~Boudol} (1985):
\newblock {\em Notes on algebraic calculi of processes.}
\newblock In K.~Apt, editor: {\sl Logics and Models of Concurrent Systems}, Springer-Verlag, pp. 261--303.
\newblock NATO ASI Series F13.
\vspace{-1ex}
\bibitem{BHR84}
{\sc S.D. Brookes, C.A.R. Hoare \& A.W. Roscoe} (1984):
\newblock {\em A theory of communicating sequential processes.}
\newblock {JACM} 31(3), pp. 560--599.
\vspace{-1ex}
\bibitem{GrV92}
{\sc J.F. Groote \& F.W. Vaandrager} (1992):
\newblock {\em Structured operational semantics and bisimulation as a congruence.}
\newblock {I\&C} 100(2), pp. 202--260.
\vspace{-1ex}
\bibitem{Ma77}
{\sc Yu.I. Manin} (1977):
\newblock {\em A Course in Mathematical Logic}, {\sl Graduate Texts in Mathematics} 53.
\newblock Springer-Verlag.
\vspace{-1ex}
\bibitem{Mi80}
{\sc R.~Milner} (1980):
\newblock {\em A Calculus of Communicating Systems}, {\rm LNCS} 92.
\newblock Springer-Verlag.
\vspace{-1ex}
\bibitem{Mi83}
{\sc R.~Milner} (1983):
\newblock {\em Calculi for synchrony and asynchrony.}
\newblock {TCS} 25, pp. 267--310.
\vspace{-1ex}
\bibitem{Pl81}
{\sc G.D. Plotkin} (1981):
\newblock {\em A structural approach to operational semantics.}
\newblock Report DAIMI FN-19, Computer Science Department, Aarhus University.%
\vspace{-1ex}
\bibitem{Po92}
{\sc A.~Ponse} (1992):
\newblock {\em Computable processes and bisimulation equivalence.}
\newblock Report CS-R9207, CWI, Amsterdam.
\vspace{-1ex}
\bibitem{dS84a}
{\sc R.~de Simone} (1984):
\newblock {\em {On {\sc Meije} and SCCS: infinite sum operators vs. non-guarded definitions}.}
\newblock {TCS} 30, pp. 133--138.
\vspace{-1ex}
\bibitem{dS85}
{\sc R.~de Simone} (1985):
\newblock {\em {Higher-level synchronising devices in {\sc Meije}--SCCS}.}
\newblock {TCS} 37, pp. 245--267.
\newblock For more details see \cite{dS84a} and: {\em
Calculabilit\'{e} et Expressivit\'{e} dans l'Algebra de Processus
Parall\`{e}les {\sc Meije}}, Th\`{e}se de $3^e$ cycle, Univ. Paris 7,
1984.
\vspace{-1ex}
\bibitem{Va93}
{\sc F.W. Vaandrager} (1993):
\newblock {\em Expressiveness results for process algebras.}
\newblock In J.W. de~Bakker, W.P.~de Roever \& G.~Rozenberg, editors: {\sl Proceedings REX Workshop on Semantics: Foundations and Applications, {\rm Beekbergen, The Netherlands, June 1992}}, {\rm LNCS} 666, Springer-Verlag, pp. 609--638.
\end{thebibliography}
\vspace{-1.5ex}
\end{document}