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