# On Decidability of the Bisimilarity on Higher-order Processes with
Parameterization††thanks: This work is supported by ANR 12IS02001 PACE, NSF of
China (61872142, 62072299, 61772336, 61572318, 61261130589), Shanghai Sailing
Program (21YF1417000) and the Open Project of Shanghai Key Laboratory of
Trustworthy Computing.

Xian Xu East China University of Science and Technology<EMAIL_ADDRESS>Shanghai Ocean University
Shanghai Key Laboratory of Trustworthy Computing Wenbo Zhang Shanghai Ocean
University
Shanghai Key Laboratory of Trustworthy Computing<EMAIL_ADDRESS>
###### Abstract

_Abstract_ Higher-order processes with parameterization are capable of
abstraction and application (migrated from the lambda-calculus), and thus are
computationally more expressive. For the minimal higher-order concurrency, it
is well-known that the strong bisimilarity (i.e., the strong bisimulation
equality) is decidable in absence of parameterization. By contrast, whether
the strong bisimilarity is still decidable for parameterized higher-order
processes remains unclear. In this paper, we focus on this issue. There are
basically two kinds of parameterization: one on names and the other on
processes. We show that the strong bisimilarity is indeed decidable for
higher-order processes equipped with both kinds of parameterization. Then we
demonstrate how to adapt the decision approach to build an axiom system for
the strong bisimilarity. On top of these results, we provide an algorithm for
the bisimilarity checking.

_Keywords_ : Decidability, Strong bisimilarity, Parameterization, Higher-
order, Processes

_2000 MSC_ : 68Q05, 68Q10, 68Q85

##  1 Introduction

Bisimulation is a most important concept for comparing the behaviour of
computing systems, particularly concurrent systems. An accompanying vital
question is to check whether two given systems are equal in terms of
bisimulation, hence the bisimilarity checking. Bisimilarity checking is an
important topic in concurrency theory and formal verification. Basically there
are two directions for this topic. One is to adopt an abstract manner, using
process rewrite systems [14]. An advantage of this direction is that some core
techniques can be extracted and potentially adapted to various models. The
other is to work directly on concrete models [19]. An edge of this direction
is that some well-defined operators can be harnessed thoroughly to guide the
checking. We focus on the second direction in this work.

The bisimilarity checking, including checking bisimulation equalities,
simulations, and preorders, has been attracting tremendous attention in the
past few decades [12, 24, 14, 10, 13]. In contrast to the fruitful work of
bisimilarity checking on first-order models, checking bisimulation equalities
for higher-order processes has been more challenging. Much fewer results have
been known in higher-order process models. Indeed, a major reason is that
higher-order processes communicate in the fashion of process-passing (i.e.,
program-passing), and have the innate capability of encoding recursion.
Besides, the standard bisimulation for higher-order processes, i.e., the
context bisimulation, is strikingly different from those for first-order
processes. It requires the matching of two output processes to be compared in
arbitrary contexts. To this point, simplifying the context bisimilarity has
also been a significant topic [20, 21].

To this day, the best known result of bisimilarity checking for higher-order
processes is reported in [16], to our knowledge. In that work, Lanese et al.
show that the strong bisimilarity checking of HOcore processes is decidable.
As a matter of fact, they show that all known strong bisimilarities in HOcore
are decidable. HOcore is a minimal higher-order process model that only has
the input, (asynchronous) output, and the concurrency operator (i.e., the
parallel composition). HOcore is also proven to be Turing complete, and this
result is somehow refined toward a more implementable interpretation [4], in
the manner of encoding lambda-calculus in HOcore through abstract machines.

That HOcore is Turing complete renders its process-termination problem
undecidable. This fact adds to the contrast that the strong bisimilarity is
decidable, which in turn implies the decidability of the barbed congruence.
Technically, the decidability is achieved by showing all the strong
bisimilarities to be coincident with a very special strong bisimilarity,
called IO-bisimilarity, which is decidable by its definition in the first
place. On the basis of this decidability outcome, a complete axiom system is
also established, as well as an algorithm with acceptable complexity. It is
then possible to implement the algorithm for bisimilarity checking HOcore
processes in software systems [2]. Intuitively, the essential element making
the strong bisimilarity decidable is that HOcore does not have the restriction
operator, and thus the capability of expressing recursion is weakened. It is
also shown that if restriction is recovered, i.e., if at least four static
(i.e., top concurrency level) restrictions are included in HOcore, then the
strong bisimilarity immediately becomes undecidable. The undecidability is
proven through a reduction from the PCP; similar reductions are also used in
other settings, e.g., the Ambient calculus [9]. Building upon [16, 11] further
studies the possibility of making the termination decidable, in the setting of
a fragment of HOcore where nested higher-order outputs are disabled.
Specifically, it is shown that in such a setting the termination of processes
becomes decidable (though convergence is still undecidable), due to the reason
that the Minsky machines are no longer expressible. Technically, such
decidability is achieved using the well-structured transition systems employed
in [8]. Following [11, 19] shows that termination turns back to be undecidable
if such a fragment of HOcore is enriched with a passivation operator [23],
because Turing completeness is retained with the help of passivation.

In [7], Bundgaard et al. study the decidable fragments of Homer [6], a higher
order process model with the capacity of expressing locations. They show that
two subcalculi of Homer have decidable barbed bisimilarity, in both the strong
and weak forms. Intuitively, Homer supports certain kind of pattern matching
of name sequences that model the locations of resources, and this plays a
central role in enhancing the expressiveness. For this reason, Homer can
encode first-order processes and is computationally complete, leaving little
hope for the decidability of bisimilarities. Therefore, to obtain
decidability, some constraints have to be devised. Technically, such
constraints are imposed through a finite control property. That is, some
finite reachability criterion is excerpted on the semantics of Homer
processes. Such a criterion is the key reason for the decidability of barbed
bisimilarities. The approach of [7] provides a valuable reference for
acquiring decidability sub-models from a more powerful full model.

However, there is still much space one can exploit concerning bisimilarity
checking for higher-order processes, as mentioned in [16]. HOcore is a minimal
model, with somewhat low modelling capacity. It would be interesting to quest
for a more expressive model by adding certain constructs, while still
maintaining the decidability result. Parameterization has been known to be an
effective approach of promoting the expressiveness of higher-order processes,
that is, abstraction-passing is strictly more expressive than mere process-
passing [15]. In this work, we focus on the minimal higher-order processes
with parameterization, notation $\Pi^{\mbox{\tiny mp}}$, basically HOcore
extended with parameterization. This minimal model contains solely the most
elementary parts to formalize higher-order concurrency, with extension of the
abstraction and application, two operations originating from the lambda-
calculus[3]. We will show that in such a calculus, the strong bisimilarity
remains decidable. Similar result is only conjectured in [16]. To this point,
we go beyond that conjecture in two respects. Firstly, although our general
approach resembles that of [16], the technical route has some key lemmas with
essentially different proof structures, due to the complication brought by the
parameterization. Secondly, we consider two kinds of parameterization, i.e.,
both on names and on processes themselves, rather than only one kind. Thus we
are working on a potentially more expressive model. This is evidenced by the
following two facts. (1) Parameterization, in particular process
parameterization, brings strictly more expressiveness to the higher-order
process model [15]. (2) Moreover, name parameterization is more expressive
than process parameterization [28]. Intuitively, this is true because we can
somehow encode process parameterization with name parameterization, using an
idea akin to that of encoding process-passing into name-passing. To the best
of our knowledge, there has been little work about the decidability of
bisimilarities in such a model. The decidability result of this work not only
pushes outward the boundary of higher-order processes with decidable
bisimilarity, but also digs more into the realm of bisimilarity checking more
challenging behavioural equalities, such as weak or branching bisimilarity.

Contribution Now we summarize the main contribution of this paper.

$\bullet$ We show that in the minimal higher-order process model with
parameterization, the strong bisimilarities, including the standard context
bisimilarity together with other well-known bisimulation equalities, are all
decidable. We borrow and revamp the ideas from [16], i.e., defining a
bisimilarity decidable from the very beginning and then showing that the
bisimilarities of interest coincide with it. The major novel parts are those
tackling the parameterization. Due to the presence of the parameterization, we
have a completely new design of the key bisimilarities, particularly those
defined directly over open processes (i.e., those processes carrying free
variables), as well as the normal bisimulation that needs new forms of
triggers for the two kinds of parameterizations. In turn, the congruence
proofs must take these changes into consideration. Moreover, some crucial
properties for establishing the coincidence of the bisimilarities have
entirely new proof methods, in particular, among others, the preservation of
substitution that claims the closure of variable substitutions with respect to
the strong bisimilarity (since now a variable can take an abstraction).
Indeed, the discussion of the mutual inclusion of various bisimilarities calls
for more rigorous and fine-grained investigation in the setting of
parameterization. More explanation is given in Sections 2, 3.
$\bullet$ With the decidability in place, we design an axiom system and a
checking algorithm, in roughly the same vein as those in [16], with the
following differences. (1) For the axiom system, the core part amounts to
reducing the deduction of the strong bisimilarity to the extended structural
congruence. Previously, such extension includes a distribution law. Now with
parameterization in the game, we have to further extend the structural
congruence with the laws for the application operation. (2) For the
bisimilarity-checking algorithm, the core is to transform a term (possibly
with parameterization) into certain normal form with the help of a tree
representation of the process, and then the bisimilarity checking can be
readily done almost syntactically on the normal form. In presence of
parameterization, we extend the tree to accommodate abstractions and
applications, as well as the normalization procedure. In such an extended
procedure, we execute applications as many times any possible, and operate the
tree in a bottom-up fashion so as to improve on performance. The algorithm has
linear space complexity and polynomial time complexity slightly better than
available ones. More details are given in Sections 4, 5.
An extended version of this paper with more details is available [27].

Organization The remainder of this paper is organized as follows. Section 2
gives the definitions of the process model and the strong bisimilarities.
Section 3 presents the decidability of the strong bisimilarities, with
detailed proofs. Section 4 does the axiomatization and proves its correctness.
In Section 5, we demonstrate an algorithm for the bisimilarity checking, and
analyses its complexity. Section 6 concludes this paper and points to some
future work.

##  2 Preliminary

In this section, we first define $\Pi^{\mbox{\tiny mp}}$, the minimal higher-
order process model extended with parameterization. Then we introduce the
strong bisimilarities to be discussed.

Syntax Calculus $\Pi^{\mbox{\tiny mp}}$ has the following syntax.

$\hskip
85.35826ptP,Q:=0\,\Big{|}\,X\,\Big{|}\,m(X).P\,\Big{|}\,\overline{m}(Q)\,\Big{|}\,P\,|\,Q\,\Big{|}\,\langle
X\rangle P\,\Big{|}\,P\langle Q\rangle\,\Big{|}\,\langle x\rangle
P\,\Big{|}\,P\langle n\rangle$

$\Pi^{\mbox{\tiny mp}}$ expressions (or terms, processes) are represented by
capital letters. For the sake of convenience, we divide names (ranged over by
$m,n,u,v...$) into two groups: one for name constants (ranged over by
$a,b,c,d,e...$) and the other for name variables (ranged over by $x,y,z...$).
The elements of the calculus have their standard meaning. One notices that the
output is non-blocking, i.e., asynchronous. Sometimes we write
$\overline{m}[Q]$ for output. Input $m(X).P$ and process abstraction $\langle
X\rangle P$ bind the process variable $X$, and name abstraction $\langle
x\rangle P$ binds the name variable $x$. Otherwise, a process or name variable
is free. Bound variables can be replaced subject to $\alpha$-conversion, and
the resulting term is deemed as the same. A term is closed if it does not have
free process variables. Otherwise it is open. Operations fpv($\cdot$),
bpv($\cdot$), pv($\cdot$), fnv($\cdot$), bnv($\cdot$), nv($\cdot$),
nc($\cdot$), n($\cdot$) respectively return the free process variables, bound
process variables, process variables, free name variables, bound name
variables, name variables, name constants, and names of a set of terms. A
variable or name is fresh if it does not appear in the terms under
examination. We use $\widetilde{\cdot}$ for a tuple, for example, a tuple of
terms $\widetilde{P}$ and a tuple of names $\widetilde{m}$. Process
substitution $P\\{Q/X\\}$ (respectively name substitution $P\\{m/x\\}$)
denotes the replacement of process variable $X$ (respectively name variable
$x$) with the process $Q$ (respectively name $m$). Substitutions can be
extended to tuples in the expected way, i.e., pairwise replacement.

Parameterization refers to abstraction and application, and sometimes
parameterization and abstraction are used interchangeably. Intuitively the
process abstraction $\langle X\rangle P$ (respectively name abstraction
$\langle x\rangle P$) _abstracts_ in $P$ the process variable $X$
(respectively name variable $x$), which is supposed to be instantiated by a
concrete process $Q$ (respectively name $d$) in the application $(\langle
X\rangle P)\langle Q\rangle$ (respectively $(\langle x\rangle P)\langle
d\rangle$); then in turn the application gives rise to an applied form
$P\\{P/X\\}$ (respectively $P\\{d/x\\}$). The constructs of abstract and
application stem from the counterpart in the lambda-calculus, and somehow
extend the domain of the lambda-calculus to a concurrent setting. To ensure
correct use of abstraction and application, a type system was designed by
Sangiorgi in his seminal thesis [20]. The typing rules in the type system
effect to exclude badly formed expressions, such as $(\langle x\rangle
P)\langle A\rangle$ and $\langle A\rangle P$ in which $A$ is a (non-variable)
term, $P\,|\,\langle X\rangle Q$ (dangling abstraction), and so on. That type
system is important but not essential for our work here, so we do not present
it and always assume that terms are well-formed subject to typing; interested
readers can refer to [20, 22] and reference thereof for more details. Term
$P_{1}\,|\,P_{2}\,|\,\cdots\,|\,P_{k}$ is abbreviated as
$\Pi_{i{=}1}^{k}P_{i}$. We also have some CCS-like operations defined as
follows: $a.P\stackrel{{\scriptstyle\textrm{def}}}{{=}}a(X).P$ where
$X\notin\mbox{\rm pv($P$)}$; $a\stackrel{{\scriptstyle\textrm{def}}}{{=}}a.0$;
$\overline{a}\stackrel{{\scriptstyle\textrm{def}}}{{=}}\overline{a}0$. A
context $C[\cdot]$ is an expression with some sub-expression replaced by the
hole $[\cdot]$, and $C[A]$ means substituting the hole with $A$.

Semantics We denote by $\equiv$ the standard structural congruence extended by
the rules for application, i.e., the smallest congruence meeting the following
laws among which the last two formulate the application.
$(P\,|\,Q)\,|\,R\equiv P\,|\,(Q\,|\,R),\quad P\,|\,Q\equiv Q\,|\,P,\quad
P\,|\,0\equiv P,\quad(\langle X\rangle P)\langle Q\rangle\equiv
P\\{Q/X\\},\quad(\langle x\rangle P)\langle m\rangle\equiv P\\{m/x\\}$

Calculus $\Pi^{\mbox{\tiny mp}}$ has the following operational semantics on
open terms, with symmetric rules skipped. In the third rule, we assume
$\mbox{\rm bpv($\lambda$)}\,\cap\,\mbox{\rm fpv($Q$)}=\emptyset$.

$\begin{array}[]{l}m(X).P\,{\xrightarrow{m(X)}}\,P\quad\overline{m}Q\,{\xrightarrow{\overline{m}(Q)}}\,0\quad
P\,|\,Q\,{\xrightarrow{\lambda}}\,P^{\prime}\,|\,QP\,{\xrightarrow{\lambda}}\,P^{\prime}\quad
P\,|\,Q\,{\xrightarrow{\tau}}\,P^{\prime}\,|\,Q^{\prime}\\{A/X\\}P\,{\xrightarrow{\overline{m}(A)}}\,P^{\prime}\quad
Q\,{\xrightarrow{m(X)}}\,Q^{\prime}\quad
Q\,{\xrightarrow{\lambda}}\,Q^{\prime}Q\equiv P\quad
P\,{\xrightarrow{\lambda}}\,P^{\prime}\quad P^{\prime}\equiv Q^{\prime}\\\
\end{array}$

The semantics grant a term three kinds of actions: input
$P\,{\xrightarrow{a(X)}}\,P^{\prime}$ means that $P$ can receive a term on
channel $a$ to replace the variable $X$ acting as a place-holder in $P$ (here
we have a late instantiation style); output
$P\,{\xrightarrow{\overline{a}(Q)}}\,P^{\prime}$ means that $P$ can send a
term $Q$ (which could be an abstraction) on channel $a$ in an asynchronous
fashion; interaction $P\,{\xrightarrow{\tau}}\,P^{\prime}$ means that $P$
makes a communication of some term between concurrent components. Actions are
ranged over by $\alpha,\lambda$. Operations fpv($\cdot$), bpv($\cdot$),
pv($\cdot$), fnv($\cdot$), bnv($\cdot$), nv($\cdot$), nc($\cdot$), n($\cdot$)
and also substitutions can be extended to actions in the expected way
accordingly. We sometimes write $P\,{\xrightarrow{\lambda}}\,\cdot$ to
represent the transition $P\,{\xrightarrow{\lambda}}\,P^{\prime}$ for some
$P^{\prime}$ if $P^{\prime}$ is not important. Modelling application as part
of the structural congruence follows the line of reduction in lambda-calculus,
though there are other options (see [20, 22]). Thus up-to $\equiv$, a term can
be somehow turned into an equivalent one by applying applications as many
times as possible, ending up with a term containing only those application of
the form $X\langle A\rangle$. As in [20], we ensure that applications
(substitutions) are bound to end (i.e., normalized), so as to avoid
$\Omega$-like terms such as $O\langle O\rangle$ in which
$O\stackrel{{\scriptstyle\textrm{def}}}{{=}}\langle X\rangle(X\langle
X\rangle)$. Said another way, in the sense of order, we focus on abstractions
with finite order, not $\omega$ order. See [20, 22] for more discussion about
this. We further notice that if infinite application were to be admitted
(though this is a bit strange), then essentially one would retrieve
replication, e.g.,
$!P\stackrel{{\scriptstyle\textrm{def}}}{{=}}O^{\prime}\langle
O^{\prime}\rangle$ in which
$O^{\prime}\stackrel{{\scriptstyle\textrm{def}}}{{=}}\langle
X\rangle(P\,|\,X\langle X\rangle)$. This would probably lead to a drastically
different situation, which we do not tackle in this work. Before moving on, we
give an example to illustrate the modelling capability of $\Pi^{\mbox{\tiny
mp}}$. We define two processes $P$ and $Q$ executing a simple protocol, making
good use of the parameterization.

$P\stackrel{{\scriptstyle\textrm{def}}}{{=}}\overline{a}A\,|\,b(X).(X\langle
B\rangle\,|\,O),\qquad
Q\stackrel{{\scriptstyle\textrm{def}}}{{=}}a(X).(X\langle
c\rangle\,|\,c(Y).R),\qquad A\stackrel{{\scriptstyle\textrm{def}}}{{=}}\langle
x\rangle(\overline{b}[\langle Z\rangle\overline{x}Z])$
$\begin{array}[]{lcll}P\,|\,Q&\,{\xrightarrow{\tau}}\,\equiv&b(X).(X\langle
B\rangle\,|\,O)\,|\,A\langle c\rangle\,|\,c(Y).R&\,\equiv\,b(X).(X\langle
B\rangle\,|\,O)\,|\,\overline{b}[\langle Z\rangle\overline{c}Z]\,|\,c(Y).R\\\
&\,{\xrightarrow{\tau}}\,\equiv&(\langle Z\rangle\overline{c}Z)\langle
B\rangle\,|\,O\,|\,c(Y).R&\,\equiv\,\overline{c}B\,|\,O\,|\,c(Y).R\\\
&\,{\xrightarrow{\tau}}\,\equiv&R\\{B/Y\\}\,|\,O&\end{array}$

The protocol goes as follows: (1) $P$ sends $Q$ an abstraction $A$ over
channel $a$ (which is agreed upon beforehand); (2) $Q$ instantiates the name
abstraction carried by $A$ with a name $c$ chosen by $Q$ alone (not
necessarily negotiated with $P$ before starting the protocol); (3) Part of the
code of $A$, i.e., $\langle Z\rangle\overline{c}Z$ is sent back to $P$ over
channel $b$ chosen by $P$ alone; (4) Process $B$, e.g., some computational
resource or data, is sent to $Q$ over channel $c$, so as to be used in $R$. In
the entire protocol, $P$ and $Q$ only agree on the channel name $a$, and
initially do not disclose on which channel the resource is to be transmitted.

Below we give the notion of “guarded” and some relevant properties.

######  Definition 1.

A variable $X$ is guarded in $P$ if $X$ merely occurs in the following two
situations. (1) $X$ occurs in $P$’s subexpressions of the form
$m(Y).P^{\prime}$ (in which $Y$ could be the same as $X$), or $Y\langle
P^{\prime}\rangle$ (in which $Y$ is not $X$). (2) $X$ occurs free in $P$’s
subexpressions of the form $\overline{m}P^{\prime}$. A term $P$ is guarded if
any free variable of it is guarded.

In what follows, we have the abbreviations: ${\rm
Tr}_{m}\stackrel{{\scriptstyle\textrm{def}}}{{=}}\overline{m}$, ${\rm
Tr}_{m}^{D}\stackrel{{\scriptstyle\textrm{def}}}{{=}}\langle
Z\rangle\overline{m}Z$, ${\rm
Tr}_{m}^{D,d}\stackrel{{\scriptstyle\textrm{def}}}{{=}}\langle
z\rangle\overline{m}[\langle Z\rangle(Z\langle z\rangle)]$. The proofs of the
coming two lemmas are by transition induction.

######  Lemma 2.

We have the following transition properties.
(1) If $P\,{\xrightarrow{\lambda}}\,P^{\prime}$, then
$P\\{R/X\\}\,{\xrightarrow{\lambda\\{R/X\\}}}\,P^{\prime}\\{R/X\\}$ for every
$R$ with $\mbox{\rm fpv($R$)}\cap(\mbox{\rm pv($P$)}\cup\mbox{\rm
pv($\lambda$)}\cup\\{X\\})=\emptyset$.
(2) If $P\\{R/X\\}\,{\xrightarrow{\lambda^{\prime}}}\,P_{1}$ with $X$ guarded
in $P$ and $\mbox{\rm fpv($R$)}\cap(\mbox{\rm pv($P$)}\cup\\{X\\})=\emptyset$,
then $P\,{\xrightarrow{\lambda}}\,P^{\prime}$, $P_{1}\equiv
P^{\prime}\\{R/X\\}$, and $\lambda^{\prime}$ is $\lambda\\{R/X\\}$ with
$\mbox{\rm fpv($R$)}\cap\mbox{\rm pv($\lambda$)}=\emptyset$.
(3) If $P\\{{\rm Tr}_{m}/X\\}\,{\xrightarrow{\lambda^{\prime}}}\,P_{1}$ with
$m$ fresh and not in $\lambda^{\prime}$, then
$P\,{\xrightarrow{\lambda}}\,P^{\prime}$, $P_{1}\equiv P^{\prime}\\{{\rm
Tr}_{m}/X\\}$, and $\lambda^{\prime}$ is $\lambda\\{{\rm Tr}_{m}/X\\}$.
(4) If $P\\{{\rm Tr}_{m}^{D}/X\\}\,{\xrightarrow{\lambda^{\prime}}}\,P_{1}$
with $m$ fresh and not in $\lambda^{\prime}$, then
$P\,{\xrightarrow{\lambda}}\,P^{\prime}$, $P_{1}\equiv P^{\prime}\\{{\rm
Tr}_{m}^{D}/X\\}$, and $\lambda^{\prime}$ is $\lambda\\{{\rm
Tr}_{m}^{D}/X\\}$.
(5) If $P\\{{\rm Tr}_{m}^{D,d}/X\\}\,{\xrightarrow{\lambda^{\prime}}}\,P_{1}$
with $m$ fresh and not in $\lambda^{\prime}$, then
$P\,{\xrightarrow{\lambda}}\,P^{\prime}$, $P_{1}\equiv P^{\prime}\\{{\rm
Tr}_{m}^{D,d}/X\\}$, and $\lambda^{\prime}$ is $\lambda\\{{\rm
Tr}_{m}^{D,d}/X\\}$.
(6) If $P\,{\xrightarrow{\lambda}}\,P^{\prime}$, then
$P\\{g/m\\}\,{\xrightarrow{\lambda\\{g/m\\}}}\,P^{\prime}\\{g/m\\}$.
(7) If $P\\{g/m\\}\,{\xrightarrow{\lambda^{\prime}}}\,P_{1}$ and
$\lambda^{\prime}$ is not $\tau$, then
$P\,{\xrightarrow{\lambda}}\,P^{\prime}$ in which $\lambda^{\prime}$ is
$\lambda\\{g/m\\}$, and $P_{1}\equiv P^{\prime}\\{g/m\\}$.
(8) If $P\\{g/m\\}\,{\xrightarrow{\tau}}\,P_{1}$, then there are several
possibilities: (a) $P\,{\xrightarrow{\tau}}\,P^{\prime}$ and $P_{1}\equiv
P^{\prime}\\{g/m\\}$. (b) $P\,{\xrightarrow{\overline{m}A}}\,\cdot$ and
$P\,{\xrightarrow{g(Y)}}\,\cdot$. That is,
$P\equiv\overline{m}A\,|\,g(Y).P_{2}\,|\,P_{3}$, and
$P_{1}\equiv(P_{2}\\{A/Y\\}\,|\,P_{3})\\{g/m\\}$. (c)
$P\,{\xrightarrow{\overline{g}A}}\,\cdot$ and
$P\,{\xrightarrow{m(Y)}}\,\cdot$. That is,
$P\equiv\overline{g}A\,|\,m(Y).P_{2}\,|\,P_{3}$, and
$P_{1}\equiv(P_{2}\\{A/Y\\}\,|\,P_{3})\\{g/m\\}$.

######  Lemma 3.

Assume that $P$ is a term and $X$ is a process variable. There are
$P^{\prime}$ in which $X$ is guarded and natural number $k\geqslant 0$ such
that one of the following cases is true. (1) $P\equiv
P^{\prime}\,|\,\Pi^{k}_{i{=}1}X$, and $P\\{R/X\\}\equiv
P^{\prime}\\{R/X\\}\,|\,\Pi^{k}_{i{=}1}R$ for every $R$. (2) $P\equiv
P^{\prime}\,|\,\Pi^{k}_{i{=}1}X\langle A_{i}\rangle$, and $P\\{R/X\\}\equiv
P^{\prime}\\{R/X\\}\,|\,\Pi^{k}_{i{=}1}R\langle A_{i}\\{R/X\\}\rangle$ for
every $R$. (3) $P\equiv P^{\prime}\,|\,\Pi^{k}_{i{=}1}X\langle m_{i}\rangle$,
and $P\\{R/X\\}\equiv P^{\prime}\\{R/X\\}\,|\,\Pi^{k}_{i{=}1}R\langle
m_{i}\rangle$ for every $R$.

The strong bisimilarities In the following, we first present a provably
decidable strong bisimilarity, named strong HO-IO bisimilarity. Then we go
head to define the various strong bisimilarities, including the strong context
bisimilarity and other strong bisimilarities of concern. These strong
bisimilarities turn out to be equal.

Strong HO-IO bisimilarity We define a bisimulation called strong HO-IO
bisimulation, with the corresponding equality called strong HO-IO
bisimilarity. As will be seen, the most desirable properties we want from this
bisimilarity is that it is decidable. The definition needs to take into
account the abstractions, because the terms transmitted to be compared may be
abstractions. Jumping ahead, the other strong bisimulations to be defined also
have this requirement for abstractions.

######  Definition 4 (Strong HO-IO bisimilarity).

A symmetric binary relation $\mathcal{R}$ over $\Pi^{\mbox{\tiny mp}}$ terms
is a strong HO-IO bisimulation, if whenever $P\,\mathcal{R}\,Q$ the following
properties hold.

(1) If $P$ is a non-abstraction, then so is $Q$. (2) If $P$ is a process-
abstraction $\langle Y\rangle A$, then $Q$ is a process-abstraction $\langle
Y\rangle B$, and $A\,\mathcal{R}\,B$. (3) If $P$ is a name-abstraction
$\langle y\rangle A$, then $Q$ is a name-abstraction $\langle y\rangle B$, and
$A\,\mathcal{R}\,B$. (4) If $P\,{\xrightarrow{\overline{a}A}}\,P^{\prime}$,
then $Q\,{\xrightarrow{\overline{a}B}}\,Q^{\prime}$ with $A\,\mathcal{R}\,B$
and $P^{\prime}\,\mathcal{R}\,Q^{\prime}$. (5) If
$P\,{\xrightarrow{a(X)}}\,P^{\prime}$, then
$Q\,{\xrightarrow{a(X)}}\,Q^{\prime}$ and
$P^{\prime}\,\mathcal{R}\,Q^{\prime}$. (6) If $P\equiv X\,|\,P^{\prime}$, then
$Q\equiv X\,|\,Q^{\prime}$ and $P^{\prime}\,\mathcal{R}\,Q^{\prime}$. (7) If
$P\equiv X\langle{A}\rangle\,|\,P^{\prime}$, then $Q\equiv
X\langle{B}\rangle\,|\,Q^{\prime}$, and $A\,\mathcal{R}\,B$ and
$P^{\prime}\,\mathcal{R}\,Q^{\prime}$. (8) If $P\equiv X\langle
d\rangle\,|\,P^{\prime}$, then $Q\equiv X\langle d\rangle\,|\,Q^{\prime}$ and
$P^{\prime}\,\mathcal{R}\,Q^{\prime}$. The strong HO-IO bisimilarity, notation
$\sim_{\mbox{\tiny hoio}}^{\mbox{\tiny$\circ$}}$ , is the largest strong HO-IO
bisimulation.

Strong HO bisimilarity The concept of strong HO bisimilarity is due to Thomsen
[25].

######  Definition 5 (Strong HO bisimilarity).

A symmetric binary relation $\mathcal{R}$ over closed $\Pi^{\mbox{\tiny mp}}$
terms is a strong HO bisimulation, if whenever $P\,\mathcal{R}\,Q$ the
following properties hold.

(1) If $P$ is a non-abstraction, then so is $Q$. (2) If $P$ is a process-
abstraction $\langle Y\rangle P^{\prime}$, then $Q$ is a process-abstraction
$\langle Y\rangle Q^{\prime}$, and
$P^{\prime}\\{A/Y\\}\,\mathcal{R}\,Q^{\prime}\\{A/Y\\}$ for every closed $A$.
(3) If $P$ is a name-abstraction $\langle y\rangle A$, then $Q$ is a name-
abstraction $\langle y\rangle B$, and $A\,\mathcal{R}\,B$. (4) If
$P\,{\xrightarrow{\overline{a}A}}\,P^{\prime}$, then
$Q\,{\xrightarrow{\overline{a}B}}\,Q^{\prime}$ with $A\,\mathcal{R}\,B$ and
$P^{\prime}\,\mathcal{R}\,Q^{\prime}$. (5) If
$P\,{\xrightarrow{a(X)}}\,P^{\prime}$, then
$Q\,{\xrightarrow{a(X)}}\,Q^{\prime}$ and for every closed $A$, it holds that
$P^{\prime}\\{A/X\\}\,\mathcal{R}\,Q^{\prime}\\{A/X\\}$. (6) If
$P\,{\xrightarrow{\tau}}\,P^{\prime}$, then
$Q\,{\xrightarrow{\tau}}\,Q^{\prime}$ and
$P^{\prime}\,\mathcal{R}\,Q^{\prime}$. The strong HO bisimilarity, notation
$\sim_{\mbox{\tiny ho}}$ , is the largest strong HO bisimulation.

Strong context bisimilarity We denote by $E(X)$ a process $E$ possibly with
$X$ appearing free in it, i.e., $\mbox{\rm fpv($E$)}\subseteq\\{X\\}$.
Accordingly, $E(A)$ denotes $E(X)\\{A/X\\}$. As a nearly standard version of
the bisimilarity for higher-order processes, the context bisimulation was
proposed by Sangiorgi [20].

######  Definition 6 (Strong context bisimilarity).

A symmetric binary relation $\mathcal{R}$ over closed $\Pi^{\mbox{\tiny mp}}$
terms is a strong context bisimulation, if whenever $P\,\mathcal{R}\,Q$ the
following properties hold. (1) If $P$ is a non-abstraction, then so is $Q$.
(2) If $P$ is a process-abstraction $\langle Y\rangle P^{\prime}$, then $Q$ is
a process-abstraction $\langle Y\rangle Q^{\prime}$, and
$P^{\prime}\\{A/Y\\}\,\mathcal{R}\,Q^{\prime}\\{A/Y\\}$ for every closed $A$.
(3) If $P$ is a name-abstraction $\langle y\rangle A$, then $Q$ is a name-
abstraction $\langle y\rangle B$, and $A\,\mathcal{R}\,B$. (4) If
$P\,{\xrightarrow{a(X)}}\,P^{\prime}$, then
$Q\,{\xrightarrow{a(X)}}\,Q^{\prime}$ and for every closed $A$, it holds that
$P^{\prime}\\{A/X\\}\,\mathcal{R}\,Q^{\prime}\\{A/X\\}$. (5) If
$P\,{\xrightarrow{\overline{a}A}}\,P^{\prime}$ in which $A$ is a non-
abstraction, process-abstraction , or name-abstraction, then
$Q\,{\xrightarrow{\overline{a}B}}\,Q^{\prime}$ for some $B$ that is
respectively a non-abstraction, process-abstraction , or name-abstraction, and
for every $E(X)$, it holds that
$E(A)\,|\,P^{\prime}\,\mathcal{R}\,E(B)\,|\,Q^{\prime}$. (6) If
$P\,{\xrightarrow{\tau}}\,P^{\prime}$, then
$Q\,{\xrightarrow{\tau}}\,Q^{\prime}$ and
$P^{\prime}\,\mathcal{R}\,Q^{\prime}$. The strong context bisimilarity,
notation $\sim_{\mbox{\tiny ctx}}$ , is the largest strong context
bisimulation.

We note that $\sim_{\mbox{\tiny ctx}}$ can be extended to open process terms,
similar for $\sim_{\mbox{\tiny ho}}$. That is, for open terms $P$ and $Q$ with
$\mbox{\rm fpv($P,Q$)}=\widetilde{X}$, $P\,\sim_{\mbox{\tiny ctx}}\,Q\mbox{ if
and only if }P\\{\widetilde{R}/\widetilde{X}\\}\,\sim_{\mbox{\tiny
ctx}}\,Q\\{\widetilde{R}/\widetilde{X}\\}\mbox{ for any closed
}\widetilde{R}.$

Strong normal bisimilarity Higher-order process expressions here may be
parameterized over processes themselves or names. Accordingly, abstractions
can be transmitted in communications, and thus process variables have three
types: non-abstraction, process-abstraction, and name-abstraction. We refer
the reader to [20] for the detailed formalization of types. To cater for our
need, knowing which of the three types a process variable belongs to is
sufficient for our work. For convenience, we may simply say that a process
variable is a non-abstraction, process-abstraction, or name-abstraction.

Before presenting the definition of the strong normal bisimilarity, we give
the definition of triggers: ${\rm
Tr}_{m}\stackrel{{\scriptstyle\textrm{def}}}{{=}}\overline{m}$, ${\rm
Tr}_{m}^{D}\stackrel{{\scriptstyle\textrm{def}}}{{=}}\langle
Z\rangle\overline{m}Z$, ${\rm
Tr}_{m}^{D,d}\stackrel{{\scriptstyle\textrm{def}}}{{=}}\langle
z\rangle\overline{m}[\langle Z\rangle(Z\langle z\rangle)]$. These triggers
correspond to the three types of process variables represented above, and will
be used to handle abstractions bound to instantiate these process variables.
The concept of triggers was proposed by Sangiorgi and plays a prevalent role
in the manipulation of higher-order processes; see [20][26]. We stress that
the design of the normal bisimulation in this work requires new forms of
triggers due to the presence of parameterization. The work in [16] only needs
the simplest form of triggers acting as synchronizers sending handshaking
signals, i.e., $\overline{m}$. However in contrast, in the setting of
parameterization, triggers should bear the responsibility of relocating the
parameters for an abstraction. This design is non-trivial in general, and we
harness the results in the previous work [26] to devise different forms of
triggers used by the parameterization. It is not hard to prove that the strong
normal bisimilarity is a congruence [20].

######  Definition 7 (Strong normal bisimilarity).

A symmetric binary relation $\mathcal{R}$ over closed $\Pi^{\mbox{\tiny mp}}$
terms is a strong normal bisimulation, if whenever $P\,\mathcal{R}\,Q$ the
following properties hold.

(1) If $P$ is a non-abstraction, then so is $Q$. (2) If $P$ is a process-
abstraction $\langle Y\rangle P^{\prime}$, then $Q$ is a process-abstraction
$\langle Y\rangle Q^{\prime}$, and for every closed $A$ it holds for fresh $m$
that:
(a) $P^{\prime}\\{{\rm Tr}_{m}/Y\\}\,\mathcal{R}\,Q^{\prime}\\{{\rm
Tr}_{m}/Y\\}$, if $Y$ is a non-abstraction. (b) $P^{\prime}\\{{\rm
Tr}_{m}^{D}/Y\\}\,\mathcal{R}\,Q^{\prime}\\{{\rm Tr}_{m}^{D}/Y\\}$, if $Y$ is
a process-abstraction. (c) $P^{\prime}\\{{\rm
Tr}_{m}^{D,d}/Y\\}\,\mathcal{R}\,Q^{\prime}\\{{\rm Tr}_{m}^{D,d}/Y\\}$, if $Y$
is a name-abstraction.

(3) If $P$ is a name-abstraction $\langle y\rangle A$, then $Q$ is a name-
abstraction $\langle y\rangle B$, and $A\,\mathcal{R}\,B$.

(4) If $P\,{\xrightarrow{a(X)}}\,P^{\prime}$, then
$Q\,{\xrightarrow{a(X)}}\,Q^{\prime}$ and for every closed $A$, it holds for
fresh $m$ that:
(a) $P^{\prime}\\{{\rm Tr}_{m}/X\\}\,\mathcal{R}\,Q^{\prime}\\{{\rm
Tr}_{m}/X\\}$, if $X$ is a non-abstraction. (b) $P^{\prime}\\{{\rm
Tr}_{m}^{D}/X\\}\,\mathcal{R}\,Q^{\prime}\\{{\rm Tr}_{m}^{D}/X\\}$, if $X$ is
a process-abstraction. (c) $P^{\prime}\\{{\rm
Tr}_{m}^{D,d}/X\\}\,\mathcal{R}\,Q^{\prime}\\{{\rm Tr}_{m}^{D,d}/X\\}$, if $X$
is a name-abstraction.

(5) If $P\,{\xrightarrow{\overline{a}A}}\,P^{\prime}$, there are three
possibilities: (a) If $A$ is not an abstraction, then
$Q\,{\xrightarrow{\overline{a}B}}\,Q^{\prime}$ for non-abstraction $B$, and it
holds for fresh $m$ that
$m.A\,|\,P^{\prime}\,\mathcal{R}\,m.B\,|\,Q^{\prime}$. (b) If $A$ is a
process-abstraction $\langle Y\rangle A_{1}$, then
$Q\,{\xrightarrow{\overline{a}B}}\,Q^{\prime}$ for process-abstraction $B$
that is $\langle Y\rangle B_{1}$, and it holds for fresh $m$ that
$m(Z).A\langle Z\rangle\,|\,P^{\prime}\,\mathcal{R}\,m(Z).B\langle
Z\rangle\,|\,Q^{\prime}$. (c) If $A$ is a name-abstraction $\langle y\rangle
A_{1}$, then $Q\,{\xrightarrow{\overline{a}B}}\,Q^{\prime}$ for name-
abstraction $B$ that is $\langle y\rangle B_{1}$, and it holds for fresh $m$
that $m(Z).Z\langle A\rangle\,|\,P^{\prime}\,\mathcal{R}\,m(Z).Z\langle
B\rangle\,|\,Q^{\prime}$.

(6) If $P\,{\xrightarrow{\tau}}\,P^{\prime}$, then
$Q\,{\xrightarrow{\tau}}\,Q^{\prime}$ and
$P^{\prime}\,\mathcal{R}\,Q^{\prime}$. The strong normal bisimilarity,
notation $\sim_{\mbox{\tiny nr}}$ , is the largest strong normal bisimulation.

We can also extend $\sim_{\mbox{\tiny nr}}$ to open terms. For open terms $P$
and $Q$ with $\mbox{\rm
fpv($P,Q$)}=\\{\widetilde{X_{1}},\widetilde{X_{2}},\widetilde{X_{3}}\\}$,
$P\,\sim_{\mbox{\tiny nr}}\,Q~{}~{}\mbox{ if and only if
}~{}~{}P\\{\widetilde{{\rm Tr}_{m_{1}}}/\widetilde{X_{1}}\\}\\{\widetilde{{\rm
Tr}_{m_{2}}^{D}}/\widetilde{X_{2}}\\}\\{\widetilde{{\rm
Tr}_{m_{3}}^{D,d}}/\widetilde{X_{3}}\\}\,\sim_{\mbox{\tiny
nr}}\,Q\\{\widetilde{{\rm Tr}_{m_{1}}}/\widetilde{X_{1}}\\}\\{\widetilde{{\rm
Tr}_{m_{2}}^{D}}/\widetilde{X_{2}}\\}\\{\widetilde{{\rm
Tr}_{m_{3}}^{D,d}}/\widetilde{X_{3}}\\}$, where each variable in
$\widetilde{X_{1}}$, $\widetilde{X_{2}}$ and $\widetilde{X_{3}}$ is
respectively a non-abstraction, process-abstraction and name-abstraction, and
is replaced with the corresponding trigger for that variable type. The
corresponding tuples of triggers are respectively denoted by $\widetilde{{\rm
Tr}_{m_{1}}}$, $\widetilde{{\rm Tr}_{m_{2}}^{D}}$ and $\widetilde{{\rm
Tr}_{m_{3}}^{D,d}}$, where the names of all the triggers are fresh.

Open strong normal bisimilarity The following bisimilarity is a variant of the
strong normal bisimilarity on open terms. It is basically an extension of the
same bisimilarity in [16].

######  Definition 8 (Open strong normal bisimilarity).

A symmetric binary relation $\mathcal{R}$ over $\Pi^{\mbox{\tiny mp}}$ terms
is an open strong normal bisimulation, if whenever $P\,\mathcal{R}\,Q$ the
following properties hold.

(1) If $P$ is a non-abstraction, then so is $Q$. (2) If $P$ is a process-
abstraction $\langle Y\rangle A$, then $Q$ is a process-abstraction $\langle
Y\rangle B$, and $A\,\mathcal{R}\,B$. (3) If $P$ is a name-abstraction
$\langle y\rangle A$, then $Q$ is a name-abstraction $\langle y\rangle B$, and
$A\,\mathcal{R}\,B$. (4) If $P\,{\xrightarrow{\overline{a}A}}\,P^{\prime}$ or
$P\,{\xrightarrow{\tau}}\,P^{\prime}$, then $Q$ matches $P$ in the same way as
in strong normal bisimilarity. (5) If $P\,{\xrightarrow{a(X)}}\,P^{\prime}$,
then $Q\,{\xrightarrow{a(X)}}\,Q^{\prime}$ and
$P^{\prime}\,\mathcal{R}\,Q^{\prime}$. (6) If $P\equiv X\,|\,P^{\prime}$, then
$Q\equiv X\,|\,Q^{\prime}$ and $P^{\prime}\,\mathcal{R}\,Q^{\prime}$.

(7) If $P\equiv X\langle A\rangle\,|\,P^{\prime}$, then $Q\equiv X\langle
B\rangle\,|\,Q^{\prime}$ and moreover the following is valid for fresh $m$.
(a) If $A$ is not an abstraction, then so is $B$ and
$m.A\,|\,P^{\prime}\,\mathcal{R}\,m.B\,|\,Q^{\prime}$. (b) If $A$ is a
process-abstraction, then so is $B$ and $m(Z).A\langle
Z\rangle\,|\,P^{\prime}\,\mathcal{R}\,m(Z).B\langle Z\rangle\,|\,Q^{\prime}$.
(c) If $A$ is a name-abstraction, then so is $B$ and $m(Z).Z\langle
A\rangle\,|\,P^{\prime}\,\mathcal{R}\,m(Z).Z\langle B\rangle\,|\,Q^{\prime}$.

(8) If $P\equiv X\langle d\rangle\,|\,P^{\prime}$, then $Q\equiv X\langle
d\rangle\,|\,Q^{\prime}$ and $P^{\prime}\,\mathcal{R}\,Q^{\prime}$.

The open strong normal bisimilarity, notation $\sim_{\mbox{\tiny
nr}}^{\mbox{\tiny$\circ$}}$ , is the largest open strong normal bisimulation.

##  3 Deciding the strong bisimilarity for $\Pi^{\mbox{\tiny mp}}$

In this section, we first establish the decidability of the strong HO-IO
bisimilarity. This is the cornerstone of the decidability for other
bisimilarities. Then we discuss the relationship between the strong
bisimilarities, and eventually obtain the coincidence between them. As such,
all of the strong bisimilarities are decidable.

###  3.1 The decidability and properties of $\sim_{\mbox{\tiny
hoio}}^{\mbox{\tiny$\circ$}}$

To facilitate discussion on decidability, we need a metric of the syntactical
structure of a term.

######  Definition 9 (Depth of a term).

The depth ${\rm depth}(P)$ of a term $P$ is a mapping from terms to natural
numbers defined as follows.
$\begin{array}[]{l}{\rm depth}(0)=0,~{}{\rm depth}(X)=1,~{}{\rm
depth}(m(X).P_{1})={\rm depth}(P_{1})+1,~{}{\rm
depth}(\overline{m}(P_{1}))={\rm depth}(P_{1})+1,{}\\\ {\rm
depth}(P_{1}\,|\,P_{2})={\rm depth}(P_{1})+{\rm depth}(P_{2}),~{}{\rm
depth}(\langle X\rangle P_{1})={\rm depth}(P_{1})+1,~{}{\rm depth}(X\langle
P_{1}\rangle)={\rm depth}(P_{1})+1,{}\\\ {\rm depth}(P_{1}\langle
P_{2}\rangle)={\rm depth}(P_{3}\\{P_{2}/Y\\})~{}\mbox{(where $P_{1}$ is
$\langle Y\rangle P_{3}$)},~{}{\rm depth}(\langle x\rangle P_{1})={\rm
depth}(P_{1})+1,{}\\\ {\rm depth}(X\langle n\rangle)=1,~{}{\rm
depth}(P_{1}\langle n\rangle)={\rm depth}(P_{3}\\{n/y\\})~{}\mbox{(where
$P_{1}$ is $\langle y\rangle P_{3}$)}\end{array}$

An immediate property is that both of $P\equiv Q$ and $P\sim_{\mbox{\tiny
hoio}}^{\mbox{\tiny$\circ$}}Q$ implies ${\rm depth}(P)={\rm depth}(Q)$. The
proof of this property is by induction over the depth of $P$. The details can
be found in [27].

######  Lemma 10.

If $P\equiv Q$ or $P\sim_{\mbox{\tiny hoio}}^{\mbox{\tiny$\circ$}}Q$, then
${\rm depth}(P)={\rm depth}(Q)$.

Strong HO-IO bisimulation up-to $\equiv$ Bisimulation up-to $\equiv$ is a
useful technique to establish bisimulations. Its definition is obtained by
replacing $\mathcal{R}$ with $\equiv\mathcal{R}\equiv$ in every clause of
Definition 4. The advantage of the up-to technique is that if $\mathcal{R}$ is
a strong HO-IO bisimulation up-to $\equiv$, then
$\mathcal{R}\subseteq\sim_{\mbox{\tiny hoio}}^{\mbox{\tiny$\circ$}}$. See [17,
22] for a thorough introduction and discussion.

Congruence Through standard state-diagram-chasing argument, one can prove that
$\sim_{\mbox{\tiny hoio}}^{\mbox{\tiny$\circ$}}$ is an equivalence relation.
It is also a congruence, as the follow-up lemma reveals. See [20, 16] for a
reference of proof; we also provide a proof in [27]. .

######  Lemma 11 (Congruence).

On $\Pi^{\mbox{\tiny mp}}$ terms, $\sim_{\mbox{\tiny
hoio}}^{\mbox{\tiny$\circ$}}$ is congruence. That is, suppose $P$ and $Q$ are
$\Pi^{\mbox{\tiny mp}}$ terms, then $P\,\sim_{\mbox{\tiny
hoio}}^{\mbox{\tiny$\circ$}}\,Q$ implies: (1) $a(X).P\,\sim_{\mbox{\tiny
hoio}}^{\mbox{\tiny$\circ$}}\,a(X).Q$; (2) $\overline{a}(P)\,\sim_{\mbox{\tiny
hoio}}^{\mbox{\tiny$\circ$}}\,\overline{a}(Q)$; (3)
$P\,|\,R\,\sim_{\mbox{\tiny hoio}}^{\mbox{\tiny$\circ$}}\,Q\,|\,R$; (4)
$\langle X\rangle P\,\sim_{\mbox{\tiny hoio}}^{\mbox{\tiny$\circ$}}\,\langle
X\rangle Q$; (5) $\langle x\rangle P\,\sim_{\mbox{\tiny
hoio}}^{\mbox{\tiny$\circ$}}\,\langle x\rangle Q$; (6) $Y\langle
P\rangle\,\sim_{\mbox{\tiny hoio}}^{\mbox{\tiny$\circ$}}\,Y\langle Q\rangle$.

Decidability We now establish the decidability of $\sim_{\mbox{\tiny
hoio}}^{\mbox{\tiny$\circ$}}$. As a premise, we have the following structural
property, whose proof is a simple induction over the semantic rules.

######  Lemma 12.

Suppose $P$ is a $\Pi^{\mbox{\tiny mp}}$ term. Then: (1) If
$P\,{\xrightarrow{\overline{a}(A)}}\,P^{\prime}$, then
$P\equiv\overline{a}(A)\,|\,P^{\prime}$. (2) If
$P\,{\xrightarrow{a(X)}}\,P^{\prime}$, then $P\equiv a(X).P_{1}\,|\,P_{2}$ and
$P^{\prime}\equiv P_{1}\,|\,P_{2}$.

######  Lemma 13 (Decidability).

On $\Pi^{\mbox{\tiny mp}}$ terms, $\sim_{\mbox{\tiny
hoio}}^{\mbox{\tiny$\circ$}}$ is decidable.

###### Proof of Lemma 13.

We decide whether $P\sim_{\mbox{\tiny hoio}}^{\mbox{\tiny$\circ$}}Q$ by
induction on ${\rm depth}(P)$.

Induction basis. In this case ${\rm depth}(P)$ is $0$ or $1$. The case ${\rm
depth}(P)$ is $0$, i.e., $P$ is $0$, is trivial because no action is possible
from $P$ and it has no free variables. If ${\rm depth}(P)$ is $1$, i.e., $P$
is $X$ or $X\langle d\rangle$, then no action is possible from $P$. One simply
checks that $Q$ is also $X$ or $X\langle d\rangle$ respectively.

Induction step. We perform a (finite) check of each clause of
$\sim_{\mbox{\tiny hoio}}^{\mbox{\tiny$\circ$}}$ in an inductive way.

(1) If $P$ is a non-abstraction, then check that $Q$ is also a non-
abstraction.

(2) If $P$ is a process-abstraction $\langle X\rangle A$, then check that $Q$
is also a process-abstraction $\langle X\rangle B$ (up-to
$\alpha$-conversion), and continue with checking $A\,\sim_{\mbox{\tiny
hoio}}^{\mbox{\tiny$\circ$}}\,B$ using induction hypothesis since the depth of
$A$ decreases with respect to $P$, i.e., ${\rm depth}(A)<{\rm depth}(P)$.

(3) If $P$ is a name-abstraction $\langle x\rangle A$, then check that $Q$ is
also a name-abstraction $\langle x\rangle B$ (up-to $\alpha$-conversion), and
continue with checking $A\,\sim_{\mbox{\tiny hoio}}^{\mbox{\tiny$\circ$}}\,B$
using induction hypothesis since the depth of $A$ decreases with respect to
$P$, i.e., ${\rm depth}(A)<{\rm depth}(P)$.

(4) If $P\,{\xrightarrow{a(X)}}\,P^{\prime}$, we check that
$Q\,{\xrightarrow{a(X)}}\,Q^{\prime}$ and $P^{\prime}\sim_{\mbox{\tiny
hoio}}^{\mbox{\tiny$\circ$}}Q^{\prime}$. There might be a few (but finite)
possibilities concerning $Q^{\prime}$. If all such checks fail, then we
conclude that $P$ and $Q$ are not strong HO-IO bisimilar. For each possible
check, we know by Lemma 12 that $P\equiv a(X).P_{1}\,|\,P_{2}$ and
$P^{\prime}\equiv P_{1}\,|\,P_{2}$. Since the depth of the terms decrease,
i.e., ${\rm depth}(P^{\prime})<{\rm depth}(P)$, we use induction hypothesis to
continue checking $P^{\prime}\sim_{\mbox{\tiny
hoio}}^{\mbox{\tiny$\circ$}}Q^{\prime}$.

(5) If $P\,{\xrightarrow{\overline{a}(A)}}\,P^{\prime}$, we check that
$Q\,{\xrightarrow{\overline{a}(B)}}\,Q^{\prime}$ with $A\sim_{\mbox{\tiny
hoio}}^{\mbox{\tiny$\circ$}}B$ and $P^{\prime}\sim_{\mbox{\tiny
hoio}}^{\mbox{\tiny$\circ$}}Q^{\prime}$. There might be a few (but finite)
possibilities concerning $B$ and $Q^{\prime}$. If all such checks fail, then
we conclude that $P$ and $Q$ are not strong HO-IO bisimilar. For each possible
check, we know by Lemma 12 that $P\equiv\overline{a}(A)\,|\,P^{\prime}$. Since
the depth of the terms decrease, i.e., ${\rm depth}(P^{\prime})<{\rm
depth}(P)$ and ${\rm depth}(A)<{\rm depth}(P)$, we use induction hypothesis to
continue checking $A\sim_{\mbox{\tiny hoio}}^{\mbox{\tiny$\circ$}}B$ and
$P^{\prime}\sim_{\mbox{\tiny hoio}}^{\mbox{\tiny$\circ$}}Q^{\prime}$.

(6) If $P\equiv X\,|\,P^{\prime}$, we check that $Q\equiv X\,|\,Q^{\prime}$
and $P^{\prime}\sim_{\mbox{\tiny hoio}}^{\mbox{\tiny$\circ$}}Q^{\prime}$.
There might be a few (but finite) possibilities concerning $Q^{\prime}$. If
all such checks fail, then we conclude that $P$ and $Q$ are not strong HO-IO
bisimilar. For each possible check, since the depth of the terms decrease,
i.e., ${\rm depth}(P^{\prime})<{\rm depth}(P)$, we use induction hypothesis to
continue checking $P^{\prime}\sim_{\mbox{\tiny
hoio}}^{\mbox{\tiny$\circ$}}Q^{\prime}$.

(7) If $P\equiv X\langle A\rangle\,|\,P^{\prime}$, we check that $Q\equiv
X\langle B\rangle\,|\,Q^{\prime}$ with $A\sim_{\mbox{\tiny
hoio}}^{\mbox{\tiny$\circ$}}B$ and $P^{\prime}\sim_{\mbox{\tiny
hoio}}^{\mbox{\tiny$\circ$}}Q^{\prime}$. There might be a few (but finite)
possibilities concerning $B$ and $Q^{\prime}$. If all such checks fail, then
we conclude that $P$ and $Q$ are not strong HO-IO bisimilar. For each possible
check, since the depth of the terms decrease, i.e., ${\rm
depth}(P^{\prime})<{\rm depth}(P)$ and ${\rm depth}(A)<{\rm depth}(P)$, we use
induction hypothesis to continue checking $A\sim_{\mbox{\tiny
hoio}}^{\mbox{\tiny$\circ$}}B$ and $P^{\prime}\sim_{\mbox{\tiny
hoio}}^{\mbox{\tiny$\circ$}}Q^{\prime}$.

(8) If $P\equiv X\langle d\rangle\,|\,P^{\prime}$, we check that $Q\equiv
X\langle d\rangle\,|\,Q^{\prime}$ and $P^{\prime}\sim_{\mbox{\tiny
hoio}}^{\mbox{\tiny$\circ$}}Q^{\prime}$. There might be a few (but finite)
possibilities concerning $Q^{\prime}$. If all such checks fail, then we
conclude that $P$ and $Q$ are not strong HO-IO bisimilar. For each possible
check, since the depth of the terms decrease, i.e., ${\rm
depth}(P^{\prime})<{\rm depth}(P)$, we use induction hypothesis to continue
checking $P^{\prime}\sim_{\mbox{\tiny hoio}}^{\mbox{\tiny$\circ$}}Q^{\prime}$.
∎

Bisimilarity Preservation To connect the strong HO-IO bisimilarity with the
strong context bisimilarity and other bisimilarities, we need some
preparation. In what follows, we show that the strong HO-IO bisimilarity
preserves substitutions and $\tau$ simulation, as stated in the following two
lemmas in a sequel.

######  Lemma 14 (Name-substitution-preserving).

Assume $P\sim_{\mbox{\tiny hoio}}^{\mbox{\tiny$\circ$}}Q$. Then
$P\\{g/m\\}\sim_{\mbox{\tiny hoio}}^{\mbox{\tiny$\circ$}}Q\\{g/m\\}$ for all
$g,m$.

We note that to keep well-formed, substitutions should not (and are always
assumed not to) break the legality of the terms under operation. The following
lemma states that $\sim_{\mbox{\tiny hoio}}^{\mbox{\tiny$\circ$}}$ is
invariant with respect to process substitution. As mentioned, the proof of
this lemma (i.e., the process substitution preserving property) is entirely
different from the counterpart in [16], in that we are obliged to conduct an
induction on the sizes of the terms because a term in the position of
application, say the term $A$ in $X\langle A\rangle$, may introduce extra
structures. That is, the proof of the preservation of process substitution
becomes much more involved due to the process parameterization. In the current
setting, a process variable can be instantiated by a process abstraction which
is in turn fed with a process from the context. This would give rise to
certain circular arguments, so the original proof method of [16] no longer
works. To work around this difficulty, one has to use induction based
approach. This approach somewhat reminds one of the difficulty in proving the
congruence properties for higher-order processes.

######  Lemma 15 (Process-substitution-preserving).

Let $P\sim_{\mbox{\tiny hoio}}^{\mbox{\tiny$\circ$}}Q$. Then
$P\\{R/X\\}\sim_{\mbox{\tiny hoio}}^{\mbox{\tiny$\circ$}}Q\\{R/X\\}$ for all
$R,X$.

The proofs of Lemmas 14 and 15 are referred to [27]. An observation as a
corollary from these two lemmas is that $\sim_{\mbox{\tiny
hoio}}^{\mbox{\tiny$\circ$}}$ is closed under abstraction, both name
abstraction and process-abstraction.

######  Corollary 16.

Assume $P\sim_{\mbox{\tiny hoio}}^{\mbox{\tiny$\circ$}}Q$. It holds that
$\langle X\rangle P\,\sim_{\mbox{\tiny hoio}}^{\mbox{\tiny$\circ$}}\,\langle
X\rangle Q$ and $\langle x\rangle P\,\sim_{\mbox{\tiny
hoio}}^{\mbox{\tiny$\circ$}}\,\langle x\rangle Q$.

The following lemma is important and directly attributed to the open-style
nature of $\sim_{\mbox{\tiny hoio}}^{\mbox{\tiny$\circ$}}$ .

######  Lemma 17 ($\tau$-preserving).

Assume $P\sim_{\mbox{\tiny hoio}}^{\mbox{\tiny$\circ$}}Q$. If
$P\,{\xrightarrow{\tau}}\,P^{\prime}$, then
$Q\,{\xrightarrow{\tau}}\,Q^{\prime}$ and $P^{\prime}\sim_{\mbox{\tiny
hoio}}^{\mbox{\tiny$\circ$}}Q^{\prime}$.

###### Proof of Lemma 17.

The proof is by induction on the derivation of
$P\,{\xrightarrow{\tau}}\,P^{\prime}$.

(1) $P\,{\xrightarrow{\tau}}\,P^{\prime}$ comes from the interaction of
components of $P$. That is, $P\,{\xrightarrow{\overline{a}(A)}}\,\cdot$,
$P\,{\xrightarrow{a(X)}}\,\cdot$, and $P\,{\xrightarrow{\tau}}\,P^{\prime}$.
One can assume $X$ to be fresh as it is bound. So this can be rewritten as
$P\,{\xrightarrow{\overline{a}(A)}}\,\cdot\,{\xrightarrow{a(X)}}\,P_{1}\mbox{
where }P_{1}\\{A/X\\}\equiv P^{\prime}$. Because $P\sim_{\mbox{\tiny
hoio}}^{\mbox{\tiny$\circ$}}Q$, $Q$ can simulate by
$Q\,{\xrightarrow{\overline{a}(B)}}\,\cdot\,{\xrightarrow{a(X)}}\,Q_{1}\,\sim_{\mbox{\tiny
hoio}}^{\mbox{\tiny$\circ$}}\,P_{1},\mbox{ where }~{}A\,\sim_{\mbox{\tiny
hoio}}^{\mbox{\tiny$\circ$}}\,B,\mbox{ and
}~{}Q_{1}\\{B/X\\}\stackrel{{\scriptstyle\textrm{def}}}{{=}}Q^{\prime}.$ Now
since the higher-order output is non-blocking, the two consecutive actions can
contribute to forming a $\tau$ action, i.e.,
$Q\,{\xrightarrow{\tau}}\,Q^{\prime}$, and we are left with showing
$P^{\prime}\sim_{\mbox{\tiny hoio}}^{\mbox{\tiny$\circ$}}Q^{\prime}$. From
$P_{1}\,\sim_{\mbox{\tiny hoio}}^{\mbox{\tiny$\circ$}}\,Q_{1}$, Lemma 15, we
know $P^{\prime}\equiv P_{1}\\{A/X\\}\,\sim_{\mbox{\tiny
hoio}}^{\mbox{\tiny$\circ$}}\,Q_{1}\\{A/X\\}\stackrel{{\scriptstyle\textrm{def}}}{{=}}Q^{\prime\prime}.$
By the congruence properties, we can derive due to $A\,\sim_{\mbox{\tiny
hoio}}^{\mbox{\tiny$\circ$}}\,B$ that $Q^{\prime\prime}\equiv
Q_{1}\\{A/X\\}\,\sim_{\mbox{\tiny
hoio}}^{\mbox{\tiny$\circ$}}\,Q_{1}\\{B/X\\}\equiv Q^{\prime}.$ Hence we
conclude $P^{\prime}\sim_{\mbox{\tiny hoio}}^{\mbox{\tiny$\circ$}}Q^{\prime}$.

(2) $P\,{\xrightarrow{\tau}}\,P^{\prime}$ comes from a component of $P$ alone.
That is, $P\equiv P_{1}\,|\,P_{2}$,
$P_{1}\,{\xrightarrow{\tau}}\,P_{1}^{\prime}$, and $P^{\prime}\equiv
P_{1}^{\prime}\,|\,P_{2}$. Then we conclude by induction hypothesis. ∎

###  3.2 Relating the strong bisimilarities

We represent detailed relationship between the strong bisimilarities defined
so far. Such relationship will be established step by step. Eventually, as our
ultimate goal, it will be demonstrated that all these strong bisimilarities
coincide with each other. This coincidence immediately entails that every and
each of them is decidable, and moreover paves way for further discussion on
the axiomatization and algorithm. We first establish the coincidence between
$\sim_{\mbox{\tiny ho}}$ and $\sim_{\mbox{\tiny hoio}}^{\mbox{\tiny$\circ$}}$,
and then move on to the remainder parts.

$\sim_{\mbox{\tiny ho}}$ and $\sim_{\mbox{\tiny hoio}}^{\mbox{\tiny$\circ$}}$
coincide The following lemma gives a characteristic of the strong HO
bisimilarity. Its proof is a standard bisimulation deduction, with details in
[27].

######  Lemma 18.

Suppose $\mbox{\rm fpv($P,Q$)}{=}\widetilde{X}{=}{X_{1},...,X_{n}}$. For fresh
$h$ and any closed $\widetilde{R}$, it holds that
$P\\{\widetilde{R}/\widetilde{X}\\}\,\sim_{\mbox{\tiny
ho}}\,Q\\{\widetilde{R}/\widetilde{X}\\}~{}\mbox{ if and only if
}~{}h(X_{1}).\cdots.h(X_{n}).P\,\sim_{\mbox{\tiny
ho}}\,h(X_{1}).\cdots.h(X_{n}).Q.$

As Lemma 19 states, the strong HO bisimilarity and the strong HO-IO
bisimilarity are actually coincident. With the help of Lemma 18, and Lemmas
14, 15, 17 as well, we can prove the mutual inclusion of the two strong
bisimilarities. The details are provided in [27].

######  Lemma 19.

On $\Pi^{\mbox{\tiny mp}}$ terms, $\sim_{\mbox{\tiny
ho}}\;=\;\sim_{\mbox{\tiny hoio}}^{\mbox{\tiny$\circ$}}$.

Relating $\sim_{\mbox{\tiny ho}}$ and the other strong bisimilarities We now
tackle the relationship between the strong HO bisimilarity and other strong
bisimilarities, including the strong context bisimilarity ($\sim_{\mbox{\tiny
ctx}}$), strong normal bisimilarity ($\sim_{\mbox{\tiny nr}}$), and open
strong normal bisimilarity ($\sim_{\mbox{\tiny nr}}^{\mbox{\tiny$\circ$}}$),
as well as the remaining part of the overall picture of coincidence. To do
this, we need some preparation. The following lemma will be useful. The proof
employs the usual bisimulation-establishing method. The details can be found
in [27].

######  Lemma 20.

Assume that $m$ is fresh with respect to $P_{1}$, $Q_{1}$, $P$ and $Q$, said
otherwise $m\notin\mbox{\rm fn($P_{1},Q_{1},P,Q$)}$. (1) If
$m.P_{1}\,|\,P\,\sim_{\mbox{\tiny nr}}^{\mbox{\tiny$\circ$}}\,m.Q_{1}\,|\,Q$,
then $P_{1}\,\sim_{\mbox{\tiny nr}}^{\mbox{\tiny$\circ$}}\,Q_{1}$ and
$P\,\sim_{\mbox{\tiny nr}}^{\mbox{\tiny$\circ$}}\,Q$. (2) If
$m(Z).P_{1}\langle Z\rangle\,|\,P\,\sim_{\mbox{\tiny
nr}}^{\mbox{\tiny$\circ$}}\,m(Z).Q_{1}\langle Z\rangle\,|\,Q$, then
$P_{1}\,\sim_{\mbox{\tiny nr}}^{\mbox{\tiny$\circ$}}\,Q_{1}$ and
$P\,\sim_{\mbox{\tiny nr}}^{\mbox{\tiny$\circ$}}\,Q$. (3) If $m(Z).Z\langle
P_{1}\rangle\,|\,P\,\sim_{\mbox{\tiny
nr}}^{\mbox{\tiny$\circ$}}\,m(Z).Z\langle Q_{1}\rangle\,|\,Q$, then
$P_{1}\,\sim_{\mbox{\tiny nr}}^{\mbox{\tiny$\circ$}}\,Q_{1}$ and
$P\,\sim_{\mbox{\tiny nr}}^{\mbox{\tiny$\circ$}}\,Q$.

Using a similar proof strategy as Lemma 20, one can prove similarly the result
for $\sim_{\mbox{\tiny nr}}$.

######  Corollary 21.

The result of Lemma 20 also holds if one replaces $\sim_{\mbox{\tiny
nr}}^{\mbox{\tiny$\circ$}}$ with $\sim_{\mbox{\tiny nr}}$ in the statement.

Next in Lemma 22, we present the first two implications about the strong
bisimilarities. Basically, the proof of Lemma 22 (1) utilizes the congruence
of $\sim_{\mbox{\tiny ho}}$ and the proof of Lemma 22 (2) uses the fact that
the requirements of $\sim_{\mbox{\tiny nr}}$ are actually special cases of
$\sim_{\mbox{\tiny ctx}}$. The details can be found in [27].

######  Lemma 22.

(1) $\sim_{\mbox{\tiny ho}}$ implies $\sim_{\mbox{\tiny ctx}}$ on
$\Pi^{\mbox{\tiny mp}}$ processes. (2) $\sim_{\mbox{\tiny ctx}}$ implies
$\sim_{\mbox{\tiny nr}}$ on $\Pi^{\mbox{\tiny mp}}$ processes.

We now demonstrate, in Lemma 23, the two last inclusions about the strong
bisimilarities, so as to finalize the jigsaw. The proofs of them use the usual
bisimulation construction approach, by exploiting Lemmas 2,20 and Corollary
21. The details are referred to [27].

######  Lemma 23.

(1) $\sim_{\mbox{\tiny nr}}$ implies $\sim_{\mbox{\tiny
nr}}^{\mbox{\tiny$\circ$}}$ on $\Pi^{\mbox{\tiny mp}}$ processes. (2)
$\sim_{\mbox{\tiny nr}}^{\mbox{\tiny$\circ$}}$ implies $\sim_{\mbox{\tiny
hoio}}^{\mbox{\tiny$\circ$}}$ on $\Pi^{\mbox{\tiny mp}}$ processes.

The follow-up lemma essentially fills what is left in the relationship between
the strong bisimilarities.

######  Lemma 24.

$\sim_{\mbox{\tiny ho}}$, $\sim_{\mbox{\tiny nr}}^{\mbox{\tiny$\circ$}}$, and
$\sim_{\mbox{\tiny ctx}}$ coincide on open and closed $\Pi^{\mbox{\tiny mp}}$
processes.

###### Proof of Lemma 24.

The following circular implications prove this lemma.

$\textstyle{\sim_{\mbox{\tiny
hoio}}^{\mbox{\tiny$\circ$}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$Lemma
19Lemma 23 (2)$\textstyle{\sim_{\mbox{\tiny
ho}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$Lemma 22
(1)$\textstyle{\sim_{\mbox{\tiny
ctx}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$Lemma 22
(2)$\textstyle{\sim_{\mbox{\tiny
nr}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$Lemma 23
(1)$\textstyle{\sim_{\mbox{\tiny nr}}^{\mbox{\tiny$\circ$}}}$

∎

The main theorem From Lemma 24 and Lemma 13, we now have the main result of
this section.

######  Theorem 25.

All the strong bisimilarities, that is, $\sim_{\mbox{\tiny
hoio}}^{\mbox{\tiny$\circ$}}$, $\sim_{\mbox{\tiny ho}}$, $\sim_{\mbox{\tiny
ctx}}$, $\sim_{\mbox{\tiny nr}}$, and $\sim_{\mbox{\tiny
nr}}^{\mbox{\tiny$\circ$}}$, coincide on open and closed $\Pi^{\mbox{\tiny
mp}}$ processes, and are all decidable.

##  4 Axiomatization

In this section, we make an axiom system for the strong bisimilarities based
on the decidability result. For simplicity, we denote by $\sim$ the strong
bisimilarity, since all the strong bisimilarities coincide. Basically, the
equation set of the axiom system is composed of the extended structural
congruence. Compared with the setting without parameterization [16], we have
extra equations describing the application operation. We use a similar
approach to prove the correctness of the axiom system.

The axiom system of [16] consists of the basic structural congruence laws and
an extended distribution law $DIS$:
$a(x).\left(P\,|\,\prod_{1}^{k-1}a(x).P\right)=\prod_{1}^{k}a(x).P$. Recall
that the rules for application are modeled as a part of the structural
congruence. To admit parameterization, we introduce the following two more
laws $APP1$ and $APP2$: $(\langle X\rangle P)\langle Q\rangle=P\\{Q/X\\}$,
$(\langle x\rangle P)\langle m\rangle=P\\{m/x\\}$. We will show that the basic
laws for the structural congruence, together with law $DIS$ and moreover laws
$APP1$ and $APP2$, are sufficient for a complete axiom system. More
specifically, we first prove that any term $P$ has a unique _prime_
decomposition $\prod^{k}_{i{=}1}P_{i}$, and then that any term can be
simplified to a normal form (denoted as ${\rm nf}(P)$) by the laws above. By
the soundness of the laws, we infer $P\sim{\rm nf}(P)$. Finally we prove that
for any $P$ and $Q$, $P\sim Q$ if and only if ${\rm nf}(P)\equiv{\rm nf}(Q)$.

Let $\mathcal{A}$ be the axiom system containing $DIS$, $APP1$, $APP2$ and the
commutative monoid laws for parallel composition. We will prove the
completeness of $\mathcal{A}$ in the remainder of this section. We start by
the cancellation property. The point of proving this property is to deem
$\sim$ as $\sim_{\mbox{\tiny hoio}}^{\mbox{\tiny$\circ$}}$ [16], and the most
involved cases are those concerning the abstractions. We provide the details
in [27].

######  Proposition 26 (Cancellation).

For all $P,Q$ and $R$, if $P\,|\,R\sim Q\,|\,R$ then $P\sim Q$.

The notion of prime processes is due to [18, 16]. A process $P$ is _prime_ if
$P\not\sim 0$ and $P\sim P_{1}\,|\,P_{2}$ implies $P_{1}\sim 0$ or $P_{2}\sim
0$. If $P\sim\prod_{i=1}^{n}P_{i}$ where each $P_{i}$ is prime, we call
$\prod_{i=1}^{n}P_{i}$ is a _prime decomposition_ of $P$. The following
proposition states that for any process, there is a unique prime decomposition
up to the strong bisimilarity and permutation of indices. Instantiating $\sim$
as $\sim_{\mbox{\tiny hoio}}^{\mbox{\tiny$\circ$}}$, one can prove this
proposition by induction on the size of the given process. We give the proof
in [27].

######  Proposition 27 (Unique prime decomposition).

Given a process $P$, if there are two prime decompositions
$P\sim\prod_{i=1}^{n}P_{i}$ and $P\sim\prod_{j=1}^{m}Q_{j}$, then $n=m$ and
there is a permutation
$\sigma:\\{1,2,\ldots,n\\}\rightarrow\\{1,2,\ldots,n\\}$, such that $P_{i}\sim
Q_{\sigma(i)}$ for each $i\in\\{1,2,\ldots,n\\}$.

We write $P\rightsquigarrow Q$ if there are $P^{\prime}$ and $Q^{\prime}$ such
that $P\equiv P^{\prime}$, $Q\equiv Q^{\prime}$, and $Q^{\prime}$ can be
obtained from $P^{\prime}$ by rewriting a subterm of $P^{\prime}$ by laws
$DIS$, $APP1$, $APP2$ from left to right. A process $P$ is in _normal form_ if
it cannot be simplified by using $\rightsquigarrow$. Any process $P$ has a
unique normal form up to $\equiv$, denoted as ${\rm nf}(P)$. It is not hard to
derive the following property.

######  Lemma 28.

If $P\rightsquigarrow Q$, then $P\sim Q$. For any $P$, $P\sim{\rm nf}(P)$.

Next we give a lemma crucial for the completeness proof. Its counterpart in
non-parameterization setting was first presented in [16]. The proof of Lemma
29 can be found in [27].

######  Lemma 29.

If $a(X).P{\sim}Q\,|\,Q^{\prime}$ ($Q,Q^{\prime}\nsim 0$), then
$a(X).P{\sim}\prod_{i=1}^{k}a(X).A$ ($k{>}1$) with $a(X).A$ in normal form.

Now we can prove the completeness of the axiom system $\mathcal{A}$.
Basically, the proof of the completeness uses a similar approach as that of
[16]. The main novelty here is to accommodate the parameterization in the
equation system and the corresponding parts in the induction, i.e., those
parts concerning the abstraction and application for names and processes.

######  Lemma 30 (Completeness).

For any $P,Q$, if $P\sim Q$ then ${\rm nf}(P)\equiv{\rm nf}(Q)$.

###### Proof of Lemma 30.

We first show the following two properties simultaneously: 1. If $A$ is a
prefixed process in normal form, then $A$ is prime; 2. For any  $A,B$ in
normal form, $A\sim B$ implies $A\equiv B$. We proceed by induction on ${\rm
depth}(A)$. The case ${\rm depth}(A)=0$ is immediate as the only term of this
size is $0$. Suppose the property holds for all ${\rm depth}(A)<n$ with $n\geq
1$.

(1) Assume $A$ is of the form $a(X).A^{\prime}$. Suppose $A$ is not prime,
$A\sim P_{1}\,|\,P_{2}$. By Lemma 29, $A\sim\prod_{i=1}^{k}a(X).B$ with $k>1$
and $a(X).B$ in normal form. Then $A^{\prime}\sim
B\,|\,\prod_{i=1}^{k-1}a(X).B$. By ind. hyp. for 2, we have $A^{\prime}\equiv
B\,|\,\prod_{i=1}^{k-1}a(X).B$. Then $A\equiv
a(X).(B\,|\,\prod_{i=1}^{k-1}a(X).B)$, a contradiction to that $A$ is in
normal form.

(2) Suppose $A\sim B$, we proceed by a case analysis on the structure of $A$.

$\bullet$ $A$ is $X$. We have that $B$ should be the same variable $X$.

$\bullet$ $A$ is $m(X).P$. Assume $B$ is not prime, $B\sim P_{1}\,|\,P_{2}$.
By Lemma 29, we know $A\sim\prod_{i=1}^{k}a(X).Q$ with $k>1$ and $a(X).Q$ in
normal form. But according to property 1, $A$ is prime, a contradiction. We
thus have $B$ is $m(X).Q$ with $P\sim Q$. By ind. hyp., $P\equiv Q$. We thus
have $A\equiv B$.

$\bullet$ $A$ is $\overline{m}(Q)$. We have that $B$ is
$\overline{m}(Q^{\prime})$ with $Q\sim Q^{\prime}$. By ind. hyp., $Q\equiv
Q^{\prime}$. We thus have $A\equiv B$.

$\bullet$ $A$ is $\langle X\rangle P$. We have that $B$ is $\langle X\rangle
Q$ and $P\sim Q$. By ind. hyp., $P\equiv Q$. We thus have $A\equiv B$.

$\bullet$ $A$ is $X\langle Q\rangle$. We have that $B$ is $X\langle
Q^{\prime}\rangle$ and $Q\sim Q^{\prime}$. By ind. hyp., $Q\equiv Q^{\prime}$.
We thus have $A\equiv B$.

$\bullet$ $A$ is $\langle x\rangle P$. We have that $B$ is $\langle x\rangle
Q$ and $P\sim Q$. By ind. hyp., $P\equiv Q$. We thus have $A\equiv B$.

$\bullet$ $A$ is $X\langle n\rangle$. We have that $B$ is $X\langle n\rangle$,
and then $A\equiv B$.

$\bullet$ $A$ is $\prod_{i=1}^{k}P_{i}$ with $k>1$ and $P_{i}$ is not a
parallel composition. We discuss over the possible shape of $P_{i}$.

- If there exists $j$ s.t. $P_{j}=X$, then $B\equiv X\,|\,B^{\prime}$. Thus $A\equiv B$ follows by ind. hyp. on $\prod_{1\leq i\leq k,i\neq j}P_{i}$ and $B^{\prime}$.

- If there exists $j$ s.t. $P_{j}=X\langle Q\rangle$, then $B\equiv X\langle Q^{\prime}\rangle\,|\,B^{\prime}$ with $Q\sim Q^{\prime}$ and $B^{\prime}\sim\prod_{1\leq i\leq k,i\neq j}P_{i}$. By ind. hyp., $A\equiv B$.

- If there exists $j$ s.t. $P_{j}=X\langle n\rangle$, then $B\equiv X\langle n\rangle\,|\,B^{\prime}$ with $B^{\prime}\equiv\prod_{1\leq i\leq k,i\neq j}P_{i}$. By ind. hyp., $A\equiv B$.

- If there exists $j$ s.t. $P_{j}=\overline{m}(Q)$, then $B$ must contain an output component on the same channel. We thus have $B=\overline{m}(Q^{\prime})\,|\,B^{\prime}$ with $Q^{\prime}\sim Q$ and $B^{\prime}\sim\prod_{1\leq i\leq k,i\neq j}P_{i}$. By ind. hyp., $Q^{\prime}\equiv Q$ and $B^{\prime}\equiv\prod_{1\leq i\leq k,i\neq j}P_{i}$, which implies $A\equiv B$.

- The last case is $A=\prod_{i=1}^{k}m_{i}(X_{i}).P_{i}$. According to property 1, each component $m_{i}(X_{i}).P_{i}$ is prime. Similarly, $B\equiv\prod_{i=1}^{l}n_{i}(Y_{i}).Q_{i}$ and each component $n_{i}(Y_{i}).Q_{i}$ is prime. By Proposition 27, $k=l$ and $m_{i}(X_{i}).P_{i}\sim n_{i}(Y_{i}).Q_{i}$ for $1\leq i\leq k$ (up to a permutation of indices). By ind. hyp. $P_{i}\equiv Q_{i}$ for all $i$, which finally implies $A\equiv B$.

Now for $P,Q$, assume $P\sim Q$. Let
$A\stackrel{{\scriptstyle\textrm{def}}}{{=}}{\rm nf}(P)$ and
$B\stackrel{{\scriptstyle\textrm{def}}}{{=}}{\rm nf}(Q)$. By Lemma 28, $A\sim
P\sim Q\sim B$. As $A,B$ are in normal form, have $A\equiv B$, and then ${\rm
nf}(P)\equiv{\rm nf}(Q)$, as needed. ∎

##  5 Algorithm for the bisimilarity checking

In this section, based on the results in the previous sections, we develop an
algorithm for checking the strong bisimilarity. We utilize the tree approach
proposed in [16], i.e., encoding a $\Pi^{\mbox{\tiny mp}}$ process as a tree,
normalizing this tree to be compared up-to syntax. Differently now, the tree
and the normalization takes parameterization into consideration. We define a
function db that assigns De Bruijn indices to variables[5, 16]. Here the
variables include the ones introduced by input prefixed processes, name
abstraction and process abstraction. Following [16], we introduce the
representation of a term by a tree. We write $t[m_{1},\ldots,m_{k}]$ for a
tree with label $t$ and subtrees $m_{1},\ldots,m_{k}$.

######  Definition 31 (Tree representation).

The tree representation of $P$ is defined inductively as follows.

(1) $\textsf{Tree}(0)=0[\ ]$, (2) $\textsf{Tree}(X)=\textsf{db}(X)[\ ]$, (3)
$\textsf{Tree}(a(X).P)={a}[\textsf{Tree}(P)]$,
(4) $\textsf{Tree}(\overline{a}(Q))={a}^{O}[\textsf{Tree}(Q)]$, (5)
$\textsf{Tree}(x(X).P)={\textsf{db}(x)}[\textsf{Tree}(P)]$, (6)
$\textsf{Tree}(\overline{x}(Q))={\textsf{db}(x)}^{O}[\textsf{Tree}(Q)]$,
(7)
$\textsf{Tree}(\prod_{i=1}^{n}P_{i})=\textsf{par}[\textsf{Tree}(P_{1}),\ldots,\textsf{Tree}(P_{n})]$,
(8) $\textsf{Tree}(\langle X\rangle P)=\textsf{abs}[\textsf{Tree}(P)]$, (9)
$\textsf{Tree}(\langle P\rangle
Q)=\textsf{app}[\textsf{Tree}(P),\textsf{Tree}(Q)]$, (10)
$\textsf{Tree}(\langle x\rangle P)=\textsf{abs}[\textsf{Tree}(P)]$, (11)
$\textsf{Tree}(\langle P\rangle n)=\textsf{app}[\textsf{Tree}(P),n[\ ]]$.

The algorithm deciding the strong bisimilarity depends on the following 3
normalization steps:
Normalization: (1) In the first step, the term is rewritten by the application
rules $APP1$, $APP2$ if possible. (2) The second step focuses on the
normalization of parallel composition. W.l.o.g., we can assume that the
children of parallel composition nodes are not parallel composition nodes.
After this step, every parallel composition node has at least two sorted child
nodes, and none of them is $0$. (3) The last step aims to apply $DIS$ from
left to right if possible.

Now we explain the detailed algorithms given as pseudocodes below. A tree node
$n$ has the following attributes: $n.type$ for the type of corresponding
process, the values can be $zero$, $var$, $inp$, $out$, $par$, $abs$, $app$;
$n.label$ for the label of the tree node; $n.numChildren$ for the number of
children nodes; $n.children$ for the lists of all child nodes. The algorithm
App realizes the application operation. It requires three parameters:
$n_{raw}$, $ind$, and $n_{eval}$. The tree is traversed top-down and all
variables from term $n_{raw}$ are replaced with process $n_{eval}$ if the De
Bruijn index matches $ind$. In the process of application, if there are more
than one occurrence of an abstracted variable, say $X$, to be replaced, there
will be more than one duplications of $n_{eval}$. The nests of application may
result in an exponential explosion on the number of tree nodes. However, we
can make optimization by reusing $n_{eval}$, that is, each occurrence of $X$
points to the same tree of $n_{eval}$. Then it is guaranteed that the space
cost for normalized terms is still linear, leading to acceptable time
complexity of the algorithm.

Algorithm NS1 deals with terms for application. The tree is traversed bottom-
up. Every term in the form of $\langle X\rangle P)\langle Q\rangle$ or
$\langle x\rangle P)\langle m\rangle$ are rewritten as $P\\{Q/X\\}$ or
$P\\{m/x\\}$ respectively. Terms in the form of $X\langle Q\rangle$ and
$X\langle n\rangle$ remain unchanged. Algorithm NS2 deals with parallel
composition. First all zero processes are removed. Then, if attribute
$numChildren$ is $0$, the tree is collapsed to a zero node. If attribute
$numChildren$ is $1$, the tree is collapsed to its single child. After this,
all children nodes are sorted. In algorithm NS3, the tree is traversed bottom-
up to find subtrees which can apply $DIS$ from left to right. Lines 12-25
decides if node $n$ matches the pattern with the left-hand side of $DIS$. It
harnesses the property that all children nodes have been sorted in
normalization step 2. If it fails to match the pattern, the node $n$ remains
unchanged and the function returns in line 19 or 23. Otherwise, the term is
rewritten at lines 26-27. As a consequence of Lemma 30, the following lemma
shows that, if two terms are strongly bisimilar, they can be normalized to the
same tree by the three normalization steps. By checking the equalities of the
two trees, we can decide the strong bisimilarity between $\Pi^{\mbox{\tiny
mp}}$ terms.

######  Lemma 32.

Let $P,Q$ be two terms. Let $T_{P}$, $T_{Q}$ be the tree representations of
$P,Q$ respectively. Assume that $T^{\prime}_{P}$, $T^{\prime}_{Q}$ are the
normalized trees after the normalization steps $1$-$3$. Then $P\sim Q$ if and
only if $T^{\prime}_{P}=T^{\prime}_{Q}$.

Application App($n_{raw}$,$ind$,$n_{eval}$)

1:Tree nodes $n_{raw}$, $n_{eval}$, an integer $ind$.

2:if ($n_{raw}$.type == ‘var’ or $n_{raw}$.type == ‘inp’) and $n_{raw}$.label
== ${ind}$ then

3: $n_{raw}=n_{eval}$

4:end if

5:if $n_{raw}$.type == ‘out’ and $n_{raw}$.label == ${ind}^{O}$ then

6: $n_{raw}=n_{eval}$

7: $n_{raw}$.label = ($n_{raw}$.label)O

8:end if

9:if $n_{raw}$.type == ‘inp’ or $n_{raw}$.type == ‘abs’ then

10: $ind=ind+1$

11:end if

12:for $i$ = 1 to $n$.numChildren do

13: App($n_{raw}$.children[$i$], $ind$ , $n_{eval}$)

14:end for

Normalization Step 1 NS1($n$)

1:A tree node $n$

2:for $i$ = 1 to $n$.numChildren do

3: NS1($n$.children[$i$])

4:end for

5:if $n$.type == ‘app’ then

6: if $n$.children[1].type == ‘abs’ then

7: App($n$.children[1].children[1], 1, $n$.children[2])

8: end if

9:end if

Normalization Step 2 NS2($n$)

1:A tree node $n$

2:for $i$ = 1 to $n$.numChildren do

3: NS2($n$.children[$i$])

4:end for

5:if $n$.type == ‘par’ then

6: $j$ = 1

7: for $i$ = 1 to $n$.numChildren do

8: if $n$.children[$i$].type $\neq$ ‘zero’ then

9: $n$.children[$j$] = $n$.children[$i$]

10: $j$ = $j$ \+ 1

11: end if

12: end for

13: $n$.numChildren = $j$ \- 1

14: if $n$.numChildren == 0 then

15: $n$.type = ‘zero’

16: end if

17: if $n$.numChildren == 1 then

18: $n$ = $n$.children[1]

19: end if

20:end if

21:sortChildren($n$)

Normalization Step 3 NS3($n$)

1:A tree node $n$

2:for $i$ = 1 to $n$.numChildren do

3: NS3($n$.children[$i$])

4:end for

5:if $n$.type == ‘inp’ then

6: $p$ = $n$.children[1]

7: if $p$.type == ‘par’ then

8: $smallIndex$=-1

9: $small$,$big$=null

10: $pc1$=$p$.children[1]

11: $pc2$=$p$.children[$p$.numChildren]

12: if $pc1$.type == ‘inp’ and $pc1$.label == $n$.label and $pc1$.children[1]
== $pc2$ then

13: $small$ = $pc2$, $big$ = $pc1$,

14: $smallIndex$ = $p$.numChildren

15: else if $pc2$.type==‘inp’ and $pc2$.label == $n$.label and
$pc2$.children[1]==$pc1$ then

16: $small$ = $pc1$, $big$ = $pc2$

17: $smallIndex$ = 1

18: else

19: return

20: end if

21: for $i$ = 2 to $n$.numChildren-1 do

22: if $p$.children[$i$] $\neq big$ then

23: return

24: end if

25: end for

26: $p$.children[$smallIndex$] = $big$

27: $n=n$.children[$1$]

28: end if

29:end if

We now analyze the complexity of the algorithm. Given processes $P$ and $Q$,
let $n$ be the sum of the number of nodes in the tree representations of $P$
and $Q$. The algorithm $App$ and $NS1$ traverse the tree for one time and can
be done in $O(n)$ time. The most time-consuming part of $NS2$ is sorting,
which can be done in $O(n\log(n))$ time. The algorithm $NS3$ can be performed
in $O(n)$ time. Therefore, bisimilarity checking takes in $O(n\log(n))$ time
in total. As explained above, the space complexity is $O(n)$.

##  6 Conclusion

In this paper, we have exhibited that even in presence of parameterization,
which can increase the expressiveness of higher-order processes, the strong
bisimilarity is still decidable for $\Pi^{\mbox{\tiny mp}}$. The proving
approach extends the previous one for HOcore, with several significant
distinctions due to parameterization. This decidability result comes with the
more powerful modelling capability of the process model, and is thus of both
fundamental and practical importance to some extent. Besides, an axiom system
and an algorithm are provided. They can be used as an intermediate prototype
for potential application of the higher-order process model, in particular the
bisimilarity checking. A further work is to try expanding the model to allow
more convenient modelling capability, e.g., locations, while maintaining the
decidability result. A far more challenging job is to consider the
decidability of the weak bisimilarity.

Acknowledgements We are grateful to the anonymous referees for their useful
comments on this paper.

## References

  * [1]
  * [2] G. Ambal, S. Lenglet & A. Schmitt (2021): _HO $\pi$ in Coq_.  Journal of Automated Reasoning 65, pp. 75–124, 10.1007/s10817-020-09553-0.
  * [3] H. P. Barendregt (1984): _The Lambda Calculus—Its Syntax and Semantics_.  North-Holland.
  * [4] M. Biernacka, D. Biernacki, S. Lenglet, P. Polesiuk, D. Pous & A. Schmitt (2017): _Fully Abstract Encodings of $\lambda$-Calculus in HOcore through Abstract Machines_.  In: Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2017), pp. 1–12, 10.1109/LICS.2017.8005118.
  * [5] N.G. De Bruijn (1972): _Lambda Calculus Notation with Nameless Dummies: A Tool for Automatic Formula Manipulation, with Application to the Church-Rosser Theorem_.  Indagationes Mathematicae 34, pp. 381–392, 10.1016/1385-7258(72)90034-0.
  * [6] M. Bundgaard, J. C. Godskesen & T. Hildebrandt (2004): _Bisimulation Congruences for Homer ? A Calculus of Higher Order Mobile Embedded Resources_.  Technical Report, IT University of Copenhagen.
  * [7] M. Bundgaard, J. Chr. Godskesen, B. Haagensen & H. Hüttel (2009): _Decidable Fragments of a Higher Order Calculus with Locations_.  In: Proceedings of the 15th International Workshop on Expressiveness in Concurrency (EXPRESS 2008), Electronic Notes in Theoretical Computer Science 242(1), pp. 113–138, 10.1016/j.entcs.2009.06.016.
  * [8] N. Busi, M. Gabbrielli & G. Zavattaro (2009): _On the Expressive Power of Recursion, Replication and Iteration in Process Calculi_.  Mathematical Structures in Computer Science 19, pp. 1191–1222, 10.1017/S096012950999017X.
  * [9] W. Charatonik & J.-M. Talbot (2001): _The Decidability of Model Checking Mobile Ambients_.  In: In Proceedings of the 15th International Workshop on Computer Science Logic (CSL 2001), Lecture Notes in Computer Science 2142, pp. 339–354, 10.1007/3-540-44802-0_24.
  * [10] S. Christensen, Y. Hirshfeld & F. Moller (1994): _Decidable Subsets of CCS_.  The Computer Journal 37, pp. 233–242, 10.1093/comjnl/37.4.233.
  * [11] C. Di Giusto, J. A. Pérez & G. Zavattaro (2009): _On the Expressiveness of Forwarding in Higher-Order Communication_.  In: In Proceedings of the 6th International Colloquium on Theoretical Aspects of Computing (ICTAC 2009), Lecture Notes in Computer Science 5684, pp. 155–169, 10.1007/978-3-642-03466-4_10.
  * [12] P. Jančar (1995): _Undecidability of Bisimilarity for Petri Nets and Some Related Problems_.  Theoretical Computer Science 148, pp. 281–301, 10.1016/0304-3975(95)00037-W.
  * [13] V. Koutavas & M. Hennessy (2012): _First-order Reasoning for Higher-order Concurrency_.  Computer Languages, Systems and Structures 38, pp. 242–277, 10.1016/j.cl.2012.04.003.
  * [14] A. Kučera & P. Jančar (2006): _Equivalence-checking on Infinite-state Systems: Techniques and Results_.  Theory and Practice of Logic Programming 6, pp. 227–264, 10.1017/S1471068406002651.
  * [15] I. Lanese, J. A. Pérez, D. Sangiorgi & A. Schmitt (2010): _On the Expressiveness of Polyadic and Synchronous Communication in Higher-order Process Calculi_.  In: In Proceedings of 37th International Colloquium on Automata, Languages and Programming (ICALP 2010), Lecture Notes in Computer Science 6199, pp. 442–453, 10.1007/978-3-642-14162-1_37.
  * [16] I. Lanese, J. A. Pérez, D. Sangiorgi & A. Schmitt (2011): _On the Expressiveness and Decidability of Higher-Order Process Calculi_.  Information and Computation 209(2), pp. 198–226, 10.1016/j.ic.2010.10.001.
  * [17] R. Milner (1989): _Communication and Concurrency_.  Prentice Hall.
  * [18] R. Milner & F. Moller (1993): _Unique Decomposition of Processes_.  Theoretical Computer Science 107(2), pp. 357–363, 10.1016/0304-3975(93)90176-t.
  * [19] J.A. Pérez (2010): _Higher-Order Concurrency: Expressiveness and Decidability Results_.  Phd thesis, University of Bologna, Italy.
  * [20] D. Sangiorgi (1992): _Expressing Mobility in Process Algebras: First-order and Higher-order Paradigms_.  Phd thesis, University of Edinburgh.
  * [21] D. Sangiorgi (1996): _Pi-calculus, Internal Mobility and Agent-Passing Calculi_.  Theoretical Computer Science 167(2), 10.1016/0304-3975(96)00075-8.  Extracts of parts of the material contained in this paper can be found in the Proceedings of TAPSOFT’95 and ICALP’95.
  * [22] D. Sangiorgi & D. Walker (2001): _The Pi-calculus: a Theory of Mobile Processes_.  Cambridge Universtity Press.
  * [23] A. Schmitt & J. B. Stefani (2004): _The Kell Calculus: a Family of Higher-order Distributed Process Calculi_.  In: In IST/FET International Workshop on Global Computing, Lecture Notes in Computer Science 3267, pp. 146–178, 10.1007/978-3-540-31794-4_9.
  * [24] P. Schnoebelen (2001): _Bisimulation and Other Undecidable Equivalences for Lossy Channel Systems_.  In: In Proceedings of 4th International Symposium on Theoretical Aspects of Computer Software (TACS?01), Lecture Notes in Computer Science 2215, pp. 385–399, 10.1007/3-540-45500-0_19.
  * [25] B. Thomsen (1993): _Plain CHOCS, a Second Generation Calculus for Higher-Order Processes_.  Acta Informatica 30(1), pp. 1–59, 10.1007/BF01200262.
  * [26] Xian Xu (2020): _Parameterizing Higher-order Processes on Names and Processes_.  RAIRO - Theoretical Informatics and Applications 53(3-4), pp. 153–206, 10.1051/ita/2019005.
  * [27] Xian Xu & Wenbo Zhang (2021): _On Decidability of the Bisimilarity on Higher-order Processes with Parameterization (long version)_.  Available at http://basics.sjtu.edu.cn/~xuxian/main_HO_DEC_with_appendix.pdf.
  * [28] Qiang Yin, Xian Xu & Huan Long (2017): _On Parameterization of Higher-order Processes_.  International Journal of Computer Mathematics 94(7), pp. 1451–1478, 10.1080/00207160.2016.1210793.