数理解析研究所講究録902 巻 1995 年 10-25

10On Reduction-Based Process Semantics
Kohei Honda

Nobuko Yoshida

Department of Computer Science, Keio University
3-14-1 Hiyoshi, Kohoku-ku, Yokohama, 223, Japan

Abstract. A formulation of semantic theories for processes which is based on
reduction relation and equational reasoning is studied. The new construction
can induce meaningful theories for processes, both in strong and weak settings.
The resulting theories in many cases coincide with, and sometimes generalise,observation-based formulation of behavioural equivalence. The basic constructionof reduction-based theories is studied, taking a simple name passing calculus
called -calculus as an example. Results on other calculi are also briefly discussed.
$\nu$

1

Introduction

The aim of the present paper is to investigate a general formulation of process semantics
which can induce canonical congruence over agents solely based on reduction relationand equational reasoning. Our starting point is the formulation of operational semantics for processes based on reduction relation and structural rules, introduced by Berryand Boudol [3] and Milner [14]. By regarding structural rules as the embedded algebra
for processes (cf. a-equality), we can view reduction relation as representing the basic
mechanism of computation in a given formalism. Especially in the area of higher-orderprocess calculi [13, 14, 15, 8], it was found that the reduction-based formulation enjoys
much more simplicity than the transition-based one. It remains open, however, whether
we can have a general framework to derive meaningful process equivalences from the
new construction, which are as significant as well-known behavioural equivalences overagents e.g. bisimilarities $[19, 12]$ .
What we are going to show in the subsequent sections, is that a general framework
to derive significant congruences over processes from the new construction in a mathematically elegant way, does exist. While works with the aim similar to ours appeared
already $[16, 4]$ , our construction has several significant aspects not found in those preic formal apparatus is an extension of the well-studied method
cursors. Firstly, the
lazy
A-theories [2, 1, 18], using the maximality condition among ain both strict andcertain family of congruences to derive canonical equality over agents. Specifically a fundamental element of the construction is reduction-closure for equality, which generalises-equality into the stateful regime of concurrent processes. The congruence relations
over processes obtained by the method turn out to be behaviourally significant in varied
process calculi, attaining intuitively sound notions of equality over agents. Secondly, one
methodological appeal of the construction in the present paper is that we obtain those$\mathrm{b}\mathrm{a}s$$\beta$‘Appeared in Proc. of 13thin July 1994.

$\mathrm{F}\mathrm{S}\mathrm{T}/\mathrm{T}\mathrm{C}\mathrm{S}$, LNCS 761, pp.371-387, Springer-Verlag, 1993. Revised

11

canonical theories without committing ourselves to a specific notion of observation
we even do not employ convergence predicate in $[16, 4]$ , which is considered to be theobservability” in [16]. Such development is important when it is difficult to
identify a canonical notion of observation in given formalisms and programming languages (e.g. [11, 20, 13, 8]). A significant example is -calculus [8, 7, 10], an offspringfrom -calculus [13], where we have two
notions of observation which induce
quite different transition relations and bisimilarities. Semantics for this small calculus istaken as the main object of study in the present exposition, showing that a behaviourally
significant equality over agents is obtained in our reduction-based framework. Resultson other calculi are also mentioned at the end.
The structure of the paper follows. Section 2 gives a brief introduction to -calculus asfar as necessary in the present paper. Section 3 develops basic construction of reductionbased equality for -calculus. Section 4 further studies the reduction-based equational
construction for -calculus, restoring usual weak and strong bisimilarities in a purely
reduction-based framework. Section 5 mentions results on other calculi, gives comparison
with related work, and points out further issues.
Most of proofs are omitted, for which the reader would refer to [9].
–$‘(\mathrm{m}\mathrm{i}\mathrm{n}\mathrm{i}\mathrm{m}\mathrm{i}\mathrm{s}\mathrm{e}\mathrm{d}$$l\text{ノ}$

”

$\pi$

$‘\zeta \mathrm{n}\mathrm{a}\mathrm{t}\mathrm{u}\mathrm{r}\mathrm{a}\mathrm{l}$$l\text{ノ}$

$\nu$

$\nu$

-calculus2

2. 1. Terms and reduction. -calculus, an offspring from -calculus [6, 13, 14], is asmall formalism of concurrency with the notion of as ynchronous name passing as theinteraction primitive [8, 7, 10] (cf. [4]). The simple primitive, coupled with capability togenerate new names, gives -calculus enough power to construct versatile structures ofinteraction $[8, 10]$ . Below we introduce basic notions of the calculus as far as needed in
the present exposition.
Letbe a countable set of names and V be a countable set of (name) vanables,
ranged over by. and by $x,$ $y,$
, respectively.
$w,$ . range over their union,
the set of identifiers. The set of -terms, ranged over by $P,$ $Q,$ , is given by thefollowing grammar.
$\nu$

$\pi$

$\nu$

$\mathrm{N}$$a,$ $b,$ $c,$

$z,$

$.$

$u,$ $v,$

$..$

$.$

$\mathrm{T}_{\nu}$$\nu$$\ldots$

ux.P$::=arrow uv|$$P$$|P,$ $Q|a\nu

P|$ !ux.P$|$

A

Among terms, $”arrow uv$ denotes a message to a target carrying a value , while “ux.P”
denotes a receptor which receives a message at and instantiates the value in . In ux.P,
binds free occurrences of in(just like ) $x.M)$ . $P,$
is a concurrent compositionof and Q. “ais a scope restriction where the initial binds its free occurrencesin P. !ux.P is a lazy replicator which replicates its body each time it interacts, whereis a binding occurrence. “ ” is a syntactic convention to denote nothing.
Free (resp. bound) names in). Free (resp.
is denoted by(resp.
bound) variables2 in
is denoted by(resp.
). We also assume the usual
notion of (multiple) substitution, written
where and are strings of identifiers(names or variables) with the same length and all identifiers in are distinct.
etc.
range over substitutions.
denotes or-conversion. Closed and open terms are defined as
”

$u$

$v$

$P$

$u$

$x$

$x$

$P$

$\nu P$

“

$P$

$Q$

”

”

$a$

$x$

$\Lambda$

$P$

$P$

$\mathcal{F}N(P)$$\mathcal{F}\mathcal{V}(P)$$\{\tilde{v}/\tilde{u}\}$$\mathcal{B}N(P)$$B\mathcal{V}(P)$$\tilde{u}$$\tilde{v}$$\sigma’$$\tilde{u}$$\sigma,$$\equiv_{\alpha}$2

For discussions on variables for names, see [9].

12usual (with respect to name variables).
andare closed
and $ax$ .
$ax$ . $arrow cz$ are open. Then, for an open term $P,$
from variables to names, is a closing.
substitution iff
denotes $a\succ(b\nu P)$ ; “,” is the weakest in association, e.g.
Some conventions: ab$a\nu P,$ $Qdej=$(aand $c.P$ to mean we), , and associates to the left; we write
do not care the .alue to be communicated.
Reduction relation provides the basic notion of computing in the formalism. To
formulate reduction we first stipulate a set of structural rules following Milner [14] (cf.
[3] . We define
be the smallest congruence relation over -terms generated by thefollowing rules.
$arrow xb$$\mathrm{T}\mathrm{h}\mathrm{u}\mathrm{s}arrow ab$$\mathrm{b}\mathrm{u}\mathrm{t}arrow yc$$\sigma$$\mathcal{F}\mathcal{V}(P\sigma)=\emptyset$$\nu P$$\nu P$$Q$$arrow c$$\mathrm{v}$$\equiv \mathrm{t}\mathrm{o}$$)$(i) $P\equiv Q$ if(ii) $P,$ $Q\equiv Q,$ $P$(iii) $aa\nu P\equiv a$$\nu$$P\equiv_{\alpha}Q$$(P, Q),$ $R\equiv P,$ $(Q, R)$$\nu P$

ab $\nu P\equiv ba\nu P$$P$$a>\Lambda\equiv$,AA a$\equiv P$$\nu P,$if$Q\equiv a$ $\nu(P, Q)$$a\not\in \mathcal{F}N(Q)$.

‘, . . . range over a sequence of concurrent composition of terms of the forms, ux.P and !ux.P. The following simple definition of reduction relation relies on
the fact that any $P$ can. be transformed to a form
using .
Let$\partial,$$\partial$$arrow uv$$\tilde{c}\nu(\partial)$

DEFINITION 2. 1$\equiv$(Reduction relation)(i) One-step reduction, denoted $byarrow$ , is the smallest relation over terms generated
by the following rules.

COM:
REP:

$\tilde{c}\nu(\partial, arrow uv, ux.P, \partial’)arrow$$\tilde{c}\nu$($\partial,$$arrow uv,$

!ux.P,$\partial’$)$\tilde{c}\nu(\partial, P\{v/x\}, \partial’)$$\tilde{c}\nu$$arrow$($\partial,$$P\{v/x\},$!ux.P,$\partial’$

)

,

STR:

$\frac{P’\equiv P,Parrow Q,Q\equiv Q’}{Parrow Q’}$(ii) Multi step $reductionarrow is$ defined:$arrow def=arrow^{*}\cup\equiv$.

We call the pair of $”arrow uv$ , ux.P” or $”arrow uv,$ !ux.P”, a redex, and each term in one
redex is called another’s redex pair. Below we give some examples of reduction, alongwith several important expressions.
(i) Let $P\oplus Qdej=c\nu(arrow c, c.P, c.Q)$ with fresh. Then: $P\oplus Qarrow(P, c\nu c.Q)$
and $P\oplus Qarrow(Q, c\nu c.P)$ . Note $c\nu c.Q$ never reduces nor interacts.
$c$(ii) Let$F\mathcal{W}(ab)^{dej}=ay$.

$arrow by$

.

Then:

$\mathcal{F}\mathcal{W}(ab),$$arrow acarrowarrow bc$.

$\mathcal{F}\mathcal{W}(ab)$is called

a foru arder.
(iii) Let$arrow acarrow \mathcal{E}Q(ab),$ $arrow bcarrow$. Then:.
is called an equator. Note$\mathcal{E}Q(ab)^{dej}=(!\mathcal{F}\mathcal{W}(ab), !\mathcal{F}\mathcal{W}(ba))$$\mathcal{E}Q(ab),$$arrow acarrow\ldots \mathcal{E}Q(ab)$(iv) Let. Then:called an identity receptor.
$\mathcal{I}(a)def=!F\mathcal{W}(aa)$(v) Let$\Omega^{def}=\mathit{0}\nu(arrow oo, \mathcal{I}(\mathit{0}))$$\mathcal{E}Q(ab),$$\mathcal{E}Q(ab)\equiv \mathcal{E}Q(ba)$$\mathcal{I}(a),$. Then:$arrow ac$$arrow$$\mathcal{I}(a),$$arrow ac$$\Omegaarrow\Omegaarrow\Omegaarrow\ldots$$arrow$.

....

$\mathcal{I}(a)$

is

13

2. 2. Labelled transitions and bisimilarities. Let
$l=$

$l$

$l,$

‘, .. range over labels given by:$\tau|\downarrow ab|\uparrow ab|\uparrow a(b)$where “ $(b)$ ” is the only bound occurrence. We write $BN(l)$ andfor the sets ofbound and free names in . One important notion concerning labels is relevance: a label
is relevant to a pair of terms
and
if $BN(l)\cap(\mathcal{F}N(P)\cup \mathcal{F}N(Q))=\emptyset$ . Now wegive rules which induce transition relations over closed -terms each of which represents
a particular notions of observation. In the following, we assume
in IN and
OUT $f,$A, and each term as a whole is closed.
in$\mathcal{F}N(l)$

$l$

$l$

$P$

$Q$

$\nu$

$b\not\in\{\tilde{c}\}$$a,$$a\not\in\{\tilde{c}\}$$\star$IN,:$\star\star \mathrm{I}\mathrm{N}_{a}$$\mathrm{O}\mathrm{U}\mathrm{T}_{b}$$\tilde{c}\vee(\partial, ax.P, \partial’)arrow\downarrow ab$

:

COM:

$b\in\{\tilde{c}\}$$\tilde{c}\sim(\partial, \partial’)arrow\downarrow ab$$\tilde{c}\rangle(\partial, P\{b/x\}, \partial’)$$\tilde{c}\vee(\partial, arrow ab, \partial’)$$\mathrm{o}\mathrm{U}\mathrm{T}_{b}$$\mathrm{o}\mathrm{U}\mathrm{T}_{f}$$\tilde{c}\vee(\partial, arrow ab, ax.P, \partial’)arrow f\tilde{c}\vee(\partial, P\{b/x\}, \partial’)$:$\tilde{c}\vee(\partial, arrow ab, \partial’)\uparrow a(b)arrow\tilde{c}\backslash v\vee(\partial, \partial’)$:$\tilde{c}\nu(\partial, arrow ab, \partial’)arrow\uparrow ab\tilde{c}\vee(\partial, \partial’)$

STR:

,

$\frac{P’\equiv P,PQ,Q\equiv Q’\iota}{P’ Q\iota}=$

Out of six rules four without marks are common to both transition relations, while
one with is for synchronous transition, and one withis for asynchronous transition.
Intuitively
rule as sumes the synchronization is essential in observation, whileassumes just as ynchronous exchanges of messages suffices. Two different transition relations are denoted by(the synchronous case)(the asynchronous case).
Note in both cases transition coincides with one-step reduction. We also define transition which ignores actions.
(resp.
) stands, else(resp.
. Note if
is closed then $Parrow P’l$ implies $P’$ is again closed.
Then synchronous strong (resp. weak) bisimulation is any symmetric relation overclosed -terms, say , such that, if, whenever $Parrow slP’$ with relevant w.r.t.
and , there exists $Q’$ such that $Qarrow slQ’$ (resp.
) and
. The
maximum relation among such relations exists and is called synchronous strong (resp.
weak) bisimilazaty,(resp.
). By
a
’ one
gets asynchronous strong (resp. weak) bisimulation and asynchronous strong (resp. weak)bisimilarity,(resp.
). For open terms, we let $P\sim_{s}Q$ withor openwhen
for any closing substitution , and similarly for other bisimilarities.
Some properties of bisimilarities follow.
$\star$$\star\star$$\mathrm{I}\mathrm{N}_{s}$$\mathrm{I}\mathrm{N}_{a}$$arrow sl$$\mathrm{a}\mathrm{n}\mathrm{d}arrow la$$\tau$$l^{\wedge}$$\Rightarrow^{l^{\wedge}}s$$\tau$$arrowarrow a^{arrow)}l$

$P$

$P$

$P\mathcal{R}Q$$\mathcal{R}$$\nu$$\mathrm{f}\mathrm{o}\mathrm{r}arrowarrow s^{arrow}l$$\mathrm{f}\mathrm{o}\mathrm{r}arrow \mathrm{i}\mathrm{f}l=\tau$$\Rightarrow_{a}$$l$$P\Rightarrow^{l^{\wedge}}sQ$$Q$$\mathrm{c}\mathrm{h}\mathrm{a}\mathrm{n}\mathrm{g}\mathrm{i}\mathrm{n}\mathrm{g}arrow_{S}l\mathrm{i}\mathrm{n}\mathrm{t}\mathrm{o}arrow l$$P’\mathcal{R}Q’$$\mathrm{a}\mathrm{n}\mathrm{d}\Rightarrow^{l^{\wedge}}s\mathrm{i}\mathrm{n}\mathrm{t}\mathrm{o}\Rightarrow^{l^{\wedge}}a$$\approx_{s}$$\sim_{s}$$\mathrm{w}\mathrm{r}\mathrm{i}\mathrm{t}\mathrm{t}\mathrm{e}\mathrm{n}\sim_{a}$$P$$\approx_{a}$$P\sigma\sim_{s}Q\sigma$$Q$$\sigma$

PROPOSITION 2. 2
(i)
(ii)

are congruence relations3.
is a proper subset
is a proper subset$\sim_{Sf}\approx_{s_{2}}\sim_{a}and\approx_{a}$$\sim_{s}$$of\sim_{a},$$and\approx_{s}$$of\approx_{a}$We note that a differentiating pair for the strong case is e.g.
weak case, (, A). Remark that reduction of
in 2.1 shows
any effect to outside, though in fact it engages in interaction.

.

$((\mathcal{I}(a), \Omega)$$\mathcal{I}(a)$3$\mathcal{I}(a)$$\mathcal{I}(a)$,, and fordoes not give$\Omega\rangle$

As a consequence of introduction of name variables, we require a congruence over$P\{v/x\}\cong Q\{v/x\}$ for any
should satisfy:
and .
$P\underline{\simeq}_{Q}$$\Rightarrow$

$v$

$x$

$\mathrm{T}_{\nu},$$\mathrm{s}\mathrm{a}\mathrm{y}\cong$,

14

Finally an important remark is that we cannot decide which of these two paradigmsof observation is more “basic” to the calculus as far as we rely on labelled transition
relation or related notions. While this suggests an essential merit of the notion of observables, i.e. applicability to varied purposes, for canonical treatment of computational
formalisms, some universal construction is called for. Note also that the notion of convergence as employed in $[4, 16]$ cannot be the answer since we get different equivalences
convergence” (where we only take output
according to whether we take
into account) or “synchronous convergence” (where we take both input and output into
account). This is not what we can decide within the convergence-based semantic framework. These considerations motivate the construction in the subsequent sections.
($‘ \mathrm{a}\mathrm{s}\mathrm{y}\mathrm{n}\mathrm{c}\mathrm{h}\mathrm{r}\mathrm{o}\mathrm{n}\mathrm{o}\mathrm{u}\mathrm{s}$$2.3$. -theories. Equation among v-terms is the central topic in the next two sections.
$\nu$

While to directly deal with congruence relations among terms is possible, to treat equations as generated by a formal theory, is often convenient.
DEFINITION 2. 3 A -theory, or simply a theory, is a formal theory, their formulae ofthe form $P=Q$ , with at least . he following axioms and rules.
$\nu$

$t$

1. $P=Q$
when $P\equiv Q$
4. $P=Q$$Q=P$
2. $P=Q$
5. $P=Q$
3. $P=Q,$ $Q=R\Rightarrow P=R6$ . $P=Q$$\Rightarrow$$\Rightarrow$$P,$$\Rightarrow$$R,$$\Rightarrow$$R=Q,$ $R$$P=R,$ $Q$

7. $P=Q$
8. $P=Q$$c\nu P=c\nu Q9$ . $P=Q$$\Rightarrow$$\Rightarrow$$\Rightarrow$$ux.P=ux.Q$!ux.P $=!ux.Q$$P\{v/x\}=Q\{v/x\}$

Rule 9 conveys the meaning of name variables. Some notations:. range over -theories. The -theory with no additional axioms and rules.
is denoted(ii) If $P=Q$ is provable in then we write $\circ s\vdash P=Q$ , or simply $P=Q$ when theconcerned theory is obvious from the context.
is the result of adding equations as axioms to(iii) Given a set of equations.
.
is a result of adding the set of equations from twotheories as axioms to the above rules4. We extend this to an arbitrary family of-theories, writing
being an index set.
is denoted by “ . Given a family of(iv) The relation induced by a theory
theories, the maximum (resp. minimum) theories are those whose corresponding
relations are the maximum (resp. minimum) in that family. We say a v-theory. If the inclusion is strict thenifis a subtheory of another theory
the former is a proper subtheory of the latter.
(v) We say a theory is consistent if it does not equate all possible pairs of terms. A
theory is inconsistent if it is not consistent.
(i)$\Im,$$\Im’.$

$\nu$

$\nu$

$\Im_{\equiv}$$\circ s$$\mathcal{E},$$\circ s$$\mathcal{E}+\mathrm{d}\mathrm{e}\mathrm{n}\mathrm{o}\mathrm{t}\mathrm{e}\mathrm{s}\mathcal{E}+\Im_{\equiv}$$\mathcal{E}+\infty s$$”+\infty s’$$\sum\{\circ s_{i}\}_{i\in I},$

$\nu$

$I$

$\propto s$$\infty/s$$\Im$$\nu-$$|$$|\circ s|\subset|s|\infty/$

Given the above definition, we can form theories corresponding to bisimilarities presented
already, by adding equations from each bisimilarity to the minimum theory. We denotecongruence
(by
, and
. Note we have,’them by$\Im_{\sim*}$$\mathrm{o}\mathrm{f}\sim_{s})$4$\mathrm{s}_{\sim},$$\propto s_{\approx_{\epsilon}}$$\Im_{\approx_{a}}$$.,$$|\circ s_{\sim_{S}}|=\sim_{s}$$\sim_{s}\supset\equiv \mathrm{a}\mathrm{n}\mathrm{d}$and similarly for other theories.

Essentially the sum is the congruent closure of the union of congruences (or the lub in thelattice of congruences).

15

Basic Constructions

3

3. 1. Reduction closure property. The notion of states is essential in concurrency.
”
A term may change its meaning during its reduction so thatin this settingmeans that two equated terms can go to an equated state again. That is, if two terms
are ever equated and one reduces to any term, then another should be able to reduce toan equated term again. What we want here is that the notion of equation is in harmony
with the notion of reduction relation. The following formalises the idea5.
$‘(\mathrm{e}\mathrm{q}\mathrm{u}\mathrm{a}\mathrm{l}\mathrm{i}\mathrm{t}\mathrm{y}$$\mathrm{r}$DEFINITION 3. 1 A -theory is reduction-closed, if, whenever $s^{\infty}\vdash P=Q$
implies, for some $Q’$ , $Qarrow Q’$ and $\propto s\vdash P’=Q’$ .
$\propto s$

$\nu$

)

$Parrow P’$

Note if we have -equality, i.e. $Parrow P’$$P=P’$ , the closure property is satisfied
vacuously: thus the property generalises -equality into the stateful regime (the usage
insteadessential in this aspect; think ofwithAx.x). Also
note that, by Definition 3.1, is reduction-closed if and only if, whenever $\circ s\vdash P=Q$ ,$C[P]arrow P’$ implies, for some $Q’$ , $C[Q]arrow Q’$ with $s^{\infty}\vdash P’=Q’$ , where $C[]$ isan arbitrary context. This makes one orientation of the above definition explicit, i.e.
an aspect as a test on the internal consistency of an equational theory under arbitrary
contexts, considering state changes during reduction. We shall often call reduction-closed-theories simply reduction theories.
Before stating one important property of reduction theories, we need a small but
useful lemma.
$\beta$$\Rightarrow$$\beta$$\mathrm{o}\mathrm{f}arrow$$\mathrm{o}\mathrm{f}arrow \mathrm{i}\mathrm{s}$$II=_{\beta}$

$I$

$I$

$de=^{f}$$\circ s$$\nu$

LEMMA 3.2

(Chain Lemma) $Let\circ/s$ be, a sum of a family of -theories and$\circ/s\vdash P=Q.$ Then we have a chain$\Im_{j_{k}}\vdash R_{k-1}=$equations:of$j_{i}\inI,$$0\leqi\leqn$.
for some$\sum\{s_{i}\}_{i\in I}\propto$$\nu$$\propto s_{j\mathrm{o}}\vdash P=R_{0},$$R_{k},$$\ldots,$$..,$$\propto s_{j_{n}}\vdash R_{n-1}=Q$

Using the lemma we get:$\frac{\mathrm{P}\mathrm{R}\mathrm{O}\mathrm{P}\mathrm{O}\mathrm{S}\mathrm{I}\mathrm{T}\mathrm{I}\mathrm{O}\mathrm{N}3..3}{reduction- closed}$Let$\circ s_{i}$be reduction-closed for all $i\in I.$ Then$\sum\{\circ s_{i}\}_{i\in I}$

is also

Note the proposition does not imply existence of the maximum consistent reductionclosed equality, since
above can be inconsistent. In fact one unpleasant fact isthat there is no maximum element in the family of consistent reduction-closed -families(see 3.4). Moreover, though the reduction closure is intended to be theic criteria forinternal consistency of -theories, equations in some reduction theories are pathologicaleven if they are consistent. One of examples iswhere $\mathcal{G}def=g\nuarrow gg$ . Note that, since is an utterly inactive term, an agent
equatesbehaves just like in any context. Hence the fact that
andfor
any and implies that the theory absurdly identify any two behaviour solely because$\sum\{\circ s_{i}\}_{i\in I}$$\nu$$\mathrm{b}\mathrm{a}s$$\nu$$\propto s_{\mathcal{G}}de=^{f}\{(P, \mathcal{G})=(Q, \mathcal{G})|P, Q\in \mathrm{T}_{\nu}\}+$$(P, \mathcal{G})$$\mathcal{G}$

$P$

$P$

5

$s_{\mathcal{G}}\propto$$(P, \mathcal{G})$$(Q, \mathcal{G})$$Q$

The closure property has a subtle yet crucial difference from a seemingly similar notion in$[16, 15]$ by Milner and Sangiorgi. See 5.2 for discussions.

16both contain . At the same time, the theory can be easily shown to be reduction-closed,and consistency is immediate. There are infinitely many such theories.
Thus the reduction-closure property falls short of imposing satisfactory constraint
on -theories, both mathematically and intuitively. What further condition should we
impose on -theories, which should be as semantically neutral as possible and be faithful to reduction-based construction? Here we take the idea inspired by the equational
scheme of sensible A-theories, where identification of meaningless (unsolvable) terms mtemally filters off “unsound” equations, just because they would lead to inconsistency[2]. A similar equational scheme is found to be effective in the lazy A-calculus, see $[1, 18]$ .
Meaninglessness in our context, however, cannot be given by such notions as unsolvability or strong unsolvability which are specific to A-calculi, but should be given in theway applicable to concurrency formalisms in general. The notion we introduce for the
purpose is called insensitivity.
$\mathcal{G}$

$\nu$

$\nu$

3. 2. Insensitivity and sound theories. Insensitive terms are those which never interact with their enclosing contexts. The notion is intended to give a sufficient condition
for operational insignificance of a term in the weak regime. Below let AN $(P)$ be defined as: $AN(arrow ab)$ $=AN(ax.P)=AN(!ax.P)=\{a\},$ $AN(a\nu P)=AN(P)\backslash \{a\}$ ,.
AN $(P, Q)=AN(P)\cup AN(Q)$ , and AN$(\Lambda)=\emptyset$

DEFINITION 3.4 A closed term
is insensitive if for all $P’$ such that $Parrow P’$ , wehave AN $(P’)=\emptyset$ . An open term is insensitive iff it is insensitive afler any closing
substitution. The set of insensitive terms is denoted by.
$P$$/ns_{\nu}$Paraphrasing, an agent is insensitive if its subterm never participates in reduction withthe outside (i.e. never becomes a part of a redex whose pair lies outside of the agent).
It isto prove thatis closed under structural rules, multi-step reduction, andname substitution. Some examples of (non-)insensitive terms follow.
$1\mathrm{n}\mathrm{s}_{\nu}$$\mathrm{e}\mathrm{a}s\mathrm{y}$EXAMPLE 3. 5 A andare insensitive.

$\Omega$are insensitive, but $neitherarrow ab,$ $c\nu(arrow ce, cx$ . $arrow be)nor\mathcal{I}(a)$The next proposition formally tells us that insensitive terms actually “do nothing.” Let$|a\nu C_{r}[]|(C_{r}[], P)|(P, C_{r}[])$ .
the set of reduction contexts6 be given by: $C_{r}[]::=$$[]$ , .. range over the set of contexts. Then we define a genenc reduction
We let. $C_{r}[P]arrow C_{r}’[P]$ . When $C_{r}arrow$(whichof a context as: $C_{r}arrow C_{r}’$reads
generically reduces to ), the former context can reduce to the latter without
any participation of the term in a hole. Using the idea we have:$[]$$C_{r}[],$$C_{r}’$$\Leftrightarrow def$

$C_{r}$$C \int$$C_{r}’$PROPOSITION 3. 6$\forall P\in 1\mathrm{n}\mathrm{s}_{\nu}$$\forall P$(Characterization of insensitivity). $C_{r}[P]arrow R$$\Rightarrow$$R\equiv C_{r}’[P’]$A $C_{r}arrow C_{r}’$ A $Parrow P’$ A$P’\in 1\mathrm{n}\mathrm{s}_{\nu}$

The proposition says that if an insensitive term is put in a reduction context, whatever
reduction takes place in the configuration, we can collect no evidence that the term
6

We can use ordinary contexts but the reduction-contexts make the formulation simpler without losing generality.

17

in a hole has participated in the change of the configuration at all. Remark that thecharacterization is given solely in terms of reduction relation and contextual closure,thus telling us the behavioural insignificance of insensitive terms independently of any“observational commitment”.
The fundamental mechanism we are going to introduce into our equational construction is the identification of insensitive terms in reduction-closed -theories. Proposition
3.6 provides a good reason for the identification. Let us call consistent reduction theories
which equate any two insensitive terms, ’sound. Among sound -theories one finds:
$\nu$

$\nu$

PROPOSITION 3.7
In contrast,
4.3 later).

$\propto s_{\sim_{\epsilon}}$$and\propto s_{\approx_{\mathrm{O}}}$$\propto s_{\approx_{\epsilon}}$and$\Im_{\sim_{\sigma}}$are both sound.

are not sound, though they are obviously reduction-closed (cf.

3. 3. Intrinsic observables. An essential fact about sound -theories is that sound-theoare, a posteriori, automatically equipped with observables. The induced observables are behaviourally significant, and, as studied in depth in the next section, they
well reflect important aspects of operations of the calculus. The obtained observables inturn bring about a certain canonical -theory as we shall see soon.
Let a pair of terms be incompatible, written $P\neq Q$ , if for any sound , “ lf $P=Q$ .
Some such pairs become useful in deriving observability.
$\nu$

$\nu$

$7\dot{\tau}es$

$\nu$

$\Im$

LEMMA 3.8

$arrow c\neq\Lambda,$

Proof. To prove$c.\Lambda\neq\Lambda_{f}$and$(arrow c, c.\Lambda)\#$, first we show

A.

A

A for any
withsound. Take a context: $C[]dej=c\nu$ ( .
, [], A) with $c’\neq c$ . Then
$C[\Lambda]=$ A$C[arrowc]arrowc\nu(arrowc’,\Lambda)=(arrowc’,c\nu\Lambda)=arrow
c’$ .
while
Since
we
$arrowc’=$
have
A for arbitrary , as required. Next we show $arrow c\#$ A for arbitrary. Suppose
A in some sound theory. Let us be given any. Thenwe can always find some such that(sinceis always finite),and with thiswe construct a context $C[]de=^{f}c’\nu([], c’.P)$ . By assumption andthe result above, we have $arrow c’=$ A. Hence we should have $C[\Lambda]=C[arrow c’]$ . But$C[arrow c’]arrow c’\nu P=d\nu(P, \Lambda)=(P, c’\succ\Lambda)=P$ whilehence $P=\Lambda$ for an
arbitrary , contradiction.
A. To prove, take $C[]=^{f}de([], arrow c)$
and reason similarly. For, take $C[]^{def}=c\nu(c$ . $arrow e, [])$ with fresh.
$c’$$arrow c\neq\Lambda$$\circ s\vdasharrow c=$“$c$$\Rightarrow\circ s\vdasharrow c’$$=$$arrow c’$$arrow c’$$\star$$c’$$\circ s\vdasharrow c=$$c$$P\in \mathrm{T}_{\nu}$$c’$$c’\not\in \mathcal{F}N(P)$$\mathcal{F}N(P)$$c’$$C[\Lambda]=\Lambda$$P$$\mathrm{H}\mathrm{e}\mathrm{n}\mathrm{c}\mathrm{e}arrow c\neq$$(arrow c, c.\Lambda)\neq\Lambda$$c.\Lambda\#\Lambda$$\square$$e$

Other notable incompatible pairs are $(arrow a, arrow b)\oplus(arrow a, arrow c)\neq(arrow a, (arrow b\oplusarrow c))$, and$(arrow a\neqarrow b)$ if $a\neq b$ . The former example tells us how soundtheories are near to theusual (weak) bisimulation.
We now formulate a notion of “generic observable” intrinsic in sound theories, by asimple transition system.
’$\tilde{c}\nu(\partial, arrow ab, \partial’)rightarrow\uparrow a\tilde{c}\nu(\partial, \partial’)$$(a\not\in\{\tilde{c}\})$$\frac{P\equiv P’P\wedge QQ\equiv Q\uparrow a}{P\wedge Q\uparrow a},,$18

Note the transition is only concerned with the output messages, and, as such, only theirtargets, not values. Based on the transition relation, we have one of the most essential
results in the present paper.
THEOREM 3.9 (Observability)$P\wedge\uparrow aP’$

Let ’s be a sound -theory $and\circ s\vdash P=Q$ . Then$\nu$

$Qarrow\wedgearrow Q’\uparrow a$$\Rightarrow$for some$Q’$

with $\Im\vdash P’=Q’$ .

for some sound theory . We show if
with $\circ s\vdash P’=Q’$ , as far asthen there should be some $Q’$ such thatis sound. Now take a context $C[]de=^{f}$ . $arrow c, c.\Lambda, [])$ with fresh. Then easily$C[P]arrow(arrow c, c.\Lambda, P’)arrow P’$ . Since
is reduction-closed, we should have, for some
. This is$Q”$ ,$C[Q]arrow Q”$ such that $\propto s\vdash P’=Q’’$ . Now we show
$Q”$.
cannot contain a term
established by showing that$Q”$
let be such that $\{\tilde{b}\}\supset FN(P)\cup FN(Q)$ and
.
Then
is
in
But suppose
it either. But since $Q”$ contains. Since $P’=Q”$ we haveas originally(note
concurrently composed with
or .
other
anywhereoccur
cannotso$C[Q]$
can only interact with each othercontained innever interacts or,if .
than these terms during reduction). Hence. But from Lemma 3.8 this iswherewith some$Q”$
is not in $Q”$ then there should be in. But if
can not be incontradiction, hence
as required.
and a term in so that we haveteraction between .
$P\wedge\uparrow aP’$

Proof. First suppose$\circ s\vdash P=Q$$\propto s$$Qarrow\wedgearrow Q’\uparrow a$

$(a$

$\Im$

$c$

$\propto s$$Qarrow\simarrow\uparrow aQ’’$$c.\Lambda$$\tilde{b}$$c.\Lambda$$c.\Lambda$$\tilde{b}\nu P’=\tilde{b}\nu Q’’$$c\not\in\{\tilde{b}\}$$\mathrm{c}\mathrm{o}\mathrm{n}\mathrm{t}\mathrm{a}\mathrm{i}\mathrm{n}\mathrm{s}arrow c$$a$$c.\Lambda$$c.\Lambda$$arrow c$$\mathrm{a}\mathrm{n}\mathrm{d}arrow c$$c$$\tilde{b}\nu Q’’=c.\Lambda$$arrow c$$\tilde{b}\nu Q’’’=(c.\Lambda, arrow c)$$Q”’,\tilde{b}\nu Q’’arrow\tilde{b}\nu Q’’’$$c.\Lambda$$c.\Lambda$

$a$

$a$

$Qarrow\wedgearrow Q’’\uparrow a$$Q$$arrow c$$\square$In the above proof, note how equation of two terms with discrepant behaviour results in inconsistency via the reduction-closure property and identification of insensitive
terms. Thus soundness “generates sense” in equations. We also note that the result,which neglects input observable and values to carry, is basically the maximum observability we can derive from the soundness condition, see 4.1 and 4.2.

3.4. The maximal theory. The essential technical consequence of observability is. Then we say a theory “
the existence of isolation sets. Let be a proper subset ofthen $Q\in$ T. Usingis an isolation set in , if $\circ s\vdash P=Q$ andisolates , orChain Lemma we easily obtain:$\mathrm{T}_{\nu}$$\mathrm{T}$$\mathrm{T}$$P\in \mathrm{T}$$\circ s$$\mathrm{T}$a sum of a family of v-theories.
be
LEMMA 3. 10 (Isolation Lemma)
isolates for all $i\in I$ , then ’:“ also isolates .
Then$Let\circ/s$$if_{S}^{\alpha_{i}}$$\sum\{s_{i}\}_{i\in If}\propto$

$T$

$T$

for each , and
But Theorem 3.9 tells us a sound theory isol\’ates a set
isolation of some non-empty set implies that the theory is consistent. Hence we get:$\{P|Parrow\infty\}\uparrow a$

PROPOSITION 3. 11$Let\propto s_{i}$be sound for each $i\in I$ . Then

The existence of the maximum sound theory follows.

$\sum\{\propto s_{i}\}_{i\in I}$$a$is also sound.

19’$\frac{\mathrm{P}\mathrm{R}\mathrm{O}\mathrm{P}\mathrm{O}\mathrm{S}\mathrm{I}\mathrm{T}\mathrm{I}\mathrm{O}\mathrm{N}3.12}{\Im_{\nu}^{*}=\{(P=Q)|def}P\cong Q\}+.Then^{\alpha*}LetP\cong Q\Leftrightarrow defs_{\nu}isthemaximumsoundtheory\propto s\vdash P=Qforsomesoun.d$‘.

We define:

Note that, by the construction of sound theories,
is maximal among the whole familyof consistent reduction-closed theories. By, we also know there is no maximum element among the family. We also note that insensitive terms are not isolated in, e.g.
A (for the equation use), unlike unsolvable terms in
the A-theories. This is natural since all we wanted to do is to start from the smallest
semantic commitment to get the broadest meaningful equality over processes.
The following proposition suggests an interesting relationship between our frameworkand the theory in $[1, 18]$ . We use the convergence predicate in the asynchronous regime:.
.
$\circ.*\nu$$|\propto s_{\mathcal{G}}|\not\subset|s_{\nu}^{*}\propto|$$\propto s_{\nu}^{*}\vdash \mathcal{I}(a)=$$\Im_{\nu}^{*}$$P\Downarrow$$\exists a$$|s_{\nu}^{*}\propto|\supset\approx_{a}$$Parrow\wedge\uparrow a$$\Leftrightarrow def$

PROPOSITION 3. 13 (Behavioural characterization of ) We defineOrd) (the class of ordinals), by the following ordinal recursion:$\circ*s_{\nu}$$-P\simeq 0Q$

if$-P\simeq_{\kappa+1}Q$$\forall C$

if.

$C[P]\Downarrow$$\forall C$$\Leftrightarrow$$C[Q]arrow Q’$$\mathrm{A},$Then we have:.

.
$C[P]arrow P’$-For limit$C[Q]\Downarrow$$relations\simeq_{\kappa}(\kappa\in$$P\simeq_{\lambda}Q$

if$\Rightarrow$$\exists Q’$. $C[Q]arrow Q’\simeq_{\hslash}P’$ , and,$\Rightarrow$$\exists P’$. $C[P]arrow P’\simeq_{\kappa}Q’$$\forall\kappa<\mathrm{A}$$\bigcap_{\kappa\in \mathrm{O}\mathrm{r}\mathrm{d}}\simeq_{\kappa}=|s_{\nu}^{*}\propto|$. $P\simeq_{\kappa}Q(i.e$ .

$\simeq_{\lambda}=\bigcap_{\kappa<\lambda}\simeq_{\kappa})$.

.

The proposition tells us that the asynchronous convergence, together with the reductionclosure property, fully characterises the canonical theory. Note that the theory thus
characterised is obtained without presupposing any specific convergence notion, not to”sayabove. Apart from this, what we have obtained is the theory in the line ofapplicative bisimulation in [1], but closed under all possible branching of multi-step
reduction, thus incorporating the statefulness.
$”\Downarrow$

Reduction Theories and Bisimilarities

4

4. .
and equators. In the following we try to explicate the equations byin
its difference from, a theory based on bisimilarity we introduced in Section 2. As
we noted in 3.2,
are both sound, therefore are subtheories of . The fact
, andgives us a tractable way of equating terms in . Moreoveris based on asynchronous
observables, and includes “ :, in its equations (i.e.
) . So a natural question“is whether there are any pairs of terms not equated by :. but equated by . Actuallysuch pairs exist, and, interestingly, the additional equations capture one of the essential
as pects of name passing operation in the asynchronous regime. It is related with equators
in 2.1: by a chain of equators, which continuously forward messages, we can abstract
locations.
$1$$\propto s_{\nu}^{*}$$\propto s_{\nu}^{*}$$\circ s_{\approx_{a}}$$”\approx$$arrow^{\infty}\approx_{a}$$\Im_{\nu}^{*}$$\circ*s_{\nu}$$\Leftrightarrow s_{\approx_{\sigma}}$$|\propto s_{\nu}^{*}|\supset\approx\supset\approx$$a_{\wedge}s$$\propto s_{\nu}^{*}$

20

To clarify the essential point, we construct a small -theory using this special agent.
Let us writefor $P\{v/w\}\equiv Q\{v/w\}$ , i.e.
and only differ in their (free)occurrences of and . We define:
$\nu$

$P$

$P^{v\cdot w}rightarrow Q$

$w$

$v$

$\propto s_{\mathcal{E}Q}de=^{f}$$Q${ $(P,$ $\mathcal{E}Q(vw))=(Q,$We can show that
This shows that$s_{\mathcal{E}Q}^{\circ}$$\mathcal{E}Q(vw))|v,$ $w,$ $P,$ $Q$

arbitrary as far as

is reduction-closed and isolates a set
is a sound theory, thus we have:$P^{v\cdot w}rightarrow Q$$\{P|Parrow\sim\}\uparrow a$

}

$+$

.

for each .
$a$$\Im_{\nu}^{*}+\infty s_{\mathcal{E}Q}$PROPOSITION 4. 1$\circ s_{\mathcal{E}Q}$

is a subtheory

By the proposition, we know

COROLLARY 4.2$\circ*s_{\nu}$$of\propto s_{\nu}^{*}$.

allows all the equations derivable in$\Im_{\nu}^{*}\vdash(\mathcal{E}Q(vw), arrow uv)=(\mathcal{E}Q(vw), arrow uw)$$\Im_{\mathcal{E}Q}$. Specifically:.

This explains why we only had observables which are without values to carry in theobservability theorem. Since, together with
Proposition 3.7, we obtain:$\circ s_{\approx_{\sigma}}\forall(\mathcal{E}Q(vw), arrow uv)=(\mathcal{E}Q(vw), arrow uw)$

PROPOSITION 4.3$\Im_{\approx_{a}}$is a proper subtheory

As to the exact difference between

CONJECTURE 4.4$s_{\approx_{a}}^{\infty}$and$s_{\nu}^{\alpha*}$$of_{S_{\nu}}^{\mathrm{o}*}$.

, we believe the following holds.

$\Im_{\approx_{a}}+\{((\mathcal{E}Q(vw), arrow uv)=(\mathcal{E}Q(vw), arrow uw))\}$

axiomatises$\Im_{\nu}^{*}$.

The task of proving (or disproving) the statement is left as a future exercise.
4. 2. Operators and observability. In this subsection we investigate whether there is
any systematic way ofby reduction-based formulation. The method
provides an interesting correspondence between the basic operators in a given calculus,
on the one hand, and induced canonical equations, on the other hand. The basic idea is toincrease the power of agents to discern difference in behaviour by introducing additional
syntactic operators.
, we use the match operator [13]. It has the form $[u=v]$ ”, used as
To obtain“$[u=v]P$ ”, with a structural rule:$\mathrm{r}\mathrm{e}\mathrm{g}\mathrm{a}\mathrm{i}\mathrm{n}\mathrm{i}\mathrm{n}\mathrm{g}\approx_{a}\mathrm{a}\mathrm{n}\mathrm{d}\approx_{s}$“$\approx_{a}$$[u=u]P\equiv P$

Note that the operator directly compares two names, so that it might well annihilate thepower of the equators. We call the system extended with the new syntactic construct, which is a superset. The new set of terms is denoted byand the structural rule,. We use the same definitions for reduction and transition, written again asof. For thisand $-^{l}a$ . The asynchronous weak bisimilarity in this setting is written
relation we have:$\nu_{=}$$\mathrm{T}_{\nu=}$$arrow$$\mathrm{T}_{\nu}$$\approx_{a}^{=}$

21

PROPOSITION 4.5$\approx_{a}^{=}is$a congruence relation7.

For equational theories, “ $P=Q\Rightarrow$ $[u=v]P=[u=v]Q$ ” is added, and, using theincompatible pairs similar to those in Lemma 3.8, we can prove common isolation sets
for the sound theories. This guarantees the existence of the maximum element, which
we shall call
. Regarding this, an interesting observability result is known (see [9]).
$\Im_{\nu=}^{*}$PROPOSITION 4.6 Suppose
ever $Parrow$ a $P’$$\Rightarrow$. Then, with relevant $w.r.t$ .
.
for some $Q’$ with$\Im_{\nu=}^{*}\vdash P=Q’$$l$$Q\Rightarrow^{l}$a $Q’$

$l$

$P$

and

$Q$

, when-$P’\approx_{a}^{=}Q’$

The proposition tells us strict semantic difference the operator induces in the calculus,
as already suggested by Boudol [4]. In our context, the operator provides the capability
to discriminate two locations (or names), which results in inability to abstract locations.
$\mathrm{s}\mathrm{o}\mathrm{t}\mathrm{h}\mathrm{a}\mathrm{t}\mathrm{o}\mathrm{n}\mathrm{e}\mathrm{g}\mathrm{e}\mathrm{t}\mathrm{s}\approx_{a}^{=}=|\Im_{\nu=}^{*}|\mathrm{T}\mathrm{h}\mathrm{e}\mathrm{n},\mathrm{t}\mathrm{o}\mathrm{g}\mathrm{e}\mathrm{t}\mathrm{h}\mathrm{e}\mathrm{r}\mathrm{w}\mathrm{i}\mathrm{t}\mathrm{h}\mathrm{N}\mathrm{o}\mathrm{w}\mathrm{P}\mathrm{r}\mathrm{o}\mathrm{p}\mathrm{o}\mathrm{s}\mathrm{i}\mathrm{t}\mathrm{i}\mathrm{o}\mathrm{n}4.6\mathrm{t}\mathrm{e}11\mathrm{s}\mathrm{u}\mathrm{s}.\approx_{a}^{=}\supset|_{S_{\nu=}}^{\alpha*}|.\mathrm{B}\mathrm{u}\mathrm{t}\approx_{a}^{=}\subset|\Im_{\nu=}^{*}|\mathrm{i}\mathrm{s}\mathrm{e}\mathrm{a}s\mathrm{y}\mathrm{u}\mathrm{s}\mathrm{i}\mathrm{n}\mathrm{g}\mathrm{P}\mathrm{r}\mathrm{o}\mathrm{p}\mathrm{o}\mathrm{s}\mathrm{i}\mathrm{t}\mathrm{i}\mathrm{o}\mathrm{n}4.5\approx_{a}^{=}\cap(\mathrm{T}_{\nu}\mathrm{x}\mathrm{T}_{\nu})=\approx_{a},\mathrm{w}\mathrm{h}\mathrm{i}\mathrm{c}\mathrm{h}\mathrm{i}\mathrm{s}$$\mathrm{e}\mathrm{a}s\mathrm{y}$’, we obtain the following.

PROPOSITION 4.7 (restoration$i.e$ . the restriction$P,$ $Q\in T_{\nu}\}+$ ,$\mathrm{o}\mathrm{f}\approx_{a}$) Let$of\circ*s_{\nu=}to${ $P=Q|\Im_{\nu=}^{*}\vdash P=Q$ A$dej=$$\circ*s_{\nu=^{1^{T_{\nu}}}}$

the original -terms. Then$\nu$$|\Im_{\nu=^{1^{T_{\nu}}}}^{*}|=\approx_{a}$.

To, we first enrich the original -calculus with capability of output synchronisation, which makes the system essentially the -calculus in [14]. We add
to the grammar, where theis embedded as. We also replace (COM)in Definition 2.1 with(, ux.Q,)and (REP) with$\mathrm{o}\mathrm{b}\mathrm{t}\mathrm{a}\mathrm{i}\mathrm{n}\approx_{s}$$\nu$$\overline{u}v.P$$\pi$$\overline{u}v.\Lambda$$\mathrm{o}\mathrm{r}\mathrm{i}\mathrm{g}\mathrm{i}\mathrm{n}\mathrm{a}\mathrm{l}arrow uv$$\tilde{c}\nu$$\partial,$$\overline{u}v.P$$\partial’)arrow\tilde{c}\vee(\partial, P, Q\{v/x\}, \partial’)$$\tilde{c}\nu(\partial,\overline{u}v.P, !ux.Q, \partial’)arrow\tilde{c}\nu(\partial, P, Q\{v/x\}, !ux.Q,\partial’)$.

$\mathrm{T}\mathrm{h}\mathrm{e}\mathrm{n}\mathrm{w}\mathrm{e}\mathrm{e}\mathrm{a}s\mathrm{i}\mathrm{l}\mathrm{y}\mathrm{o}\mathrm{b}\mathrm{t}\mathrm{a}\mathrm{i}\mathrm{n}\mathrm{b}\mathrm{o}\mathrm{t}\mathrm{h}\mathrm{i}\mathrm{n}\mathrm{p}\mathrm{u}\mathrm{t}$and output observables. However (and interestingly) we still cannot observe values inthis framework, so that we again add the match operator, with which we finally restore, by the same technical development as we have had. Thus the lattice of enrichment of operators results in the lattice of observables, hence of canonical equalities.
The following picture depicts the situation. Below observables are listed on the left of
the name of the system and the operators added to the base calculus are on the right(“ ” stands for the extension of the fragmentary -calculus with match). A dotted line
shows (upward) inclusion in canonical equations.
$\approx_{s}$$\pi_{=}$$\mathrm{f}\mathrm{o}\mathrm{r}\approx_{a}$$\pi$Note the picture arises uniformly from a single equational scheme: a deep study on operators and their semantic significance in process calculi is called for.
7This is mainly due to our proviso for bisimilarity over open terms in 2.2, cf. [13].

22

4. 3. Strong theories. Reduction theories are essentially incepted in the “weak” semantic framework, since they do not care the number of reduction steps, less the termination. Notably we havein any sound theories. The following construction now”
tells us that we can easilystrong theories out of them. In fact to any reduction
theory a certain canonical strong theory corresponds to, and, as later to be seen, onesuch theory (derived from ) corresponds to a strong bisimilarity introduced in Section
2. The framework goes from the weak semantics to the strong semantics, which might
be contrary to the usual practice: the idea here is to first try to capture the meaningof each term in the abstract setting, then refine the induced equations by considering
exact steps a term need to reach possible semantic points. Cost is measured after sense
is made, so to speak.
$\Omega=\Lambda$($‘ \mathrm{d}\mathrm{e}\mathrm{r}\mathrm{i}\mathrm{v}\mathrm{e}$$s_{\nu}^{\infty*}$

The basic definition of strong theories follows. Remember a theory is a subtheory of
another theory if its equations are included in the latter’s.
is strong reducDEFINITION 4. 8 Given a reduction theory , we say its subtheorytion theory with a base “, if, whenever $s^{\circ/}\vdash P=Q,$ $Parrow P’$ implies, for some $Q’$ ,$Qarrow Q’$ with $\Im’\vdash P’=Q’$ .
$\Im’$$s^{\circ}$$a$

Put in other words, ’s‘’ is astrong reduction theory if and only if, whenever $\circ s’\vdash P=Q$ ,$nQ’$ with $\circ/s\vdash P’=Q’$ , for all, whereimplies, for some $Q’,$
equations are only those allowed in its base. Thus a strong theory is derived from abase theory by
reduction steps”. The following is important to get a (relatively) canonical strong theory from a base theory. The result is easy from Chain Lemma.
$Parrow^{n}P’$$Q$$n\in\omega$—$‘(\mathrm{c}\mathrm{o}\mathrm{u}\mathrm{n}\mathrm{t}\mathrm{i}\mathrm{n}\mathrm{g}$be a strong theory whose base is
PROPOSITION 4.9
Let
theoryis also a strongwithas its base.

$\Im$$\Im_{i}$$\sum\{\Im_{i}\}_{i\in I}$

for all $i\in I.$ Then$s^{\infty}$

Hence, given a reduction theory , there is always the maximum strong theory with abase . We also note that if the base is a strong theory, its maximum strong theory. For theis theitself. We call the maximum strong theory with the$Parrow
al$
$P’$
$P$
theory, we have: if
andwith relevant w.r.t. and , then
$Qarrow_{a}Q’l$
there exists $Q’$ such thatand $P’\sim_{a}Q’$ (for establishment of the property,. But
the reasoning on the number of reduction steps is crucial; see [9] . Thus
, so that, i.e.
. Therefore:
is a strong theory with a base$\triangleright s$$\Im$$\mathrm{b}\mathrm{a}s\mathrm{e}$$\mathrm{b}\mathrm{a}\mathrm{s}\mathrm{e}s_{\nu}\circ*,$$\propto s_{\nu:s}^{*}\vdash P=Q$

$Q$

$l$

$)$

$|s_{\nu}^{*}|\infty\supset\approx_{a}\supset\sim_{a}$PROPOSITION 4. 10$\circ s_{\sim_{\sigma}}$$|\Im_{\nu:s}^{*}|\subset\sim_{a}$$|\propto s_{\nu s}^{*}|\supset\sim_{a}$$\propto s_{\nu}^{*}$$|\circ s_{\nu:s}*|=\sim_{a}$$s_{\nu:s}^{\alpha*}$.

. This isis againto know that the strong theory corresponding to
It isbecause some differences in weak theories depend on the use of additional reduction
steps (e.g. equators): if these should be counted, the additional equations disappear.
, leading toHence restoration of values in messages without the match operator in
Finally
wenote thatthe coincidence of the “strong core” in two different weak theories.
.
: the reasoning parallels the case ofis easily obtained$\propto s_{\sim_{a}}$$s_{\approx_{\alpha}}^{\infty}$$\mathrm{e}\mathrm{a}s\mathrm{y}$$\Im_{\nu.s}^{*}$$\Im_{\sim}$.

$\mathrm{f}\mathrm{r}\mathrm{o}\mathrm{m}s_{\approx}\propto$.

$\propto s_{\nu:s}^{*}$

23

5

Discussion

5. 1. Results on other calculi. CCS [12] is the process calculus based on dyadic
synchronization as the basic communication primitive. The structural equivalence andreduction relation for the calculus naturally follow. One essential issue in constructing
reduction theories for CCS is that the summation is problematic in weak congruent theories in general. However we restore weak
our purely equational settingby considering the maximum sound theory where congruence is understood in termsof reduction contexts (see 3.2). Then the maximum sound theory, denoted by,coincides with
via an observability theorem (cf. [16]). Finally the sound maximum
strong theory whose base is, coincides with the strong bisimilarity in [12].
Equational theories based on reduction are extensively studied in terms of A-calculus[2]. Specifically -equality is subsumed in our reduction-closure property as noted, notto say many of our formal constructions are inspired by A-theories. A natural question is: can we get any (interesting) observables following our framework based on
reduction-closure? It seems that soundness does not directly leads to observability, regarding strongly unsolvable terms $[17, 1]$ as the insensitive terms. However if we also add
identification ofterms $[17, 18]$ , then we obtain the canonical theory after picking
up head normal forms as generic observables, which coincides with, the theory of.
Note, with this canonical theory, we have restored -equality, reinforcing our standpoint
to regard -equality as a special case of the reduction-closure property.
$\mathrm{b}\mathrm{i}\mathrm{s}\mathrm{i}\mathrm{m}\mathrm{i}\mathrm{l}\mathrm{a}\mathrm{r}\mathrm{i}\mathrm{t}\mathrm{y}\approx \mathrm{i}\mathrm{n}$$\circ*s_{ccs\backslash +}$$\approx$$\circ*s_{ccs\backslash +}$$\beta$$\mathrm{P}\mathrm{O}_{\infty}$$\mathcal{K}^{*}$$D_{\infty}$$\beta$$\beta$5. 2. Related work and open issues. There are two important precursors to ourwork. Boudol [4] studied (in)equation over essentially the same system as u-calculus
based on Morris-like contextual precongruence. Milner and Sangiorgi [16] have shownthat their construction called barbed congruence coincides with strong bisimilarity in thecase of CCS, also referring to the results in the weak case. An apparent difference is that
we do not positively stipulate a presupposed notion of convergence to derive a canonicalequality, as opposed to two precursors. In this sense, it may be safe to say that thepresent construction depends on less subjective semantic commitment. Nevertheless wenote that our approach, a posteriori, reveals the import of so-called convergence predicate
in $[16, 4]$ , see e.g. Proposition 3.13, by discovering such a notion without stipulating it
beforehand. It is yet to see to what range of formal systems insensitivity-based approachis effective, and how such effectiveness is related to semantic aspects of given calculi.
The result in 4.2 is suggestive in this aspect.
Another (and possibly more important) difference from other approaches lies in our
crucial usage of reduction-closure. While [16] uses a closure property on reduction relation, the property is used rather as a “minimized bisimulation”, together with theconvergence notion, for a usual relation. Taking the union of all such relations, one takes
the maximum congruence within it. In contrast, our formulation reg.ards the closure, just as -equality
property as the essential criteria for equality over statefulover A-terms. While to take the maximum congruence within non-congruent equivalenceis already known in the case of observation congruence in CCS [12], we would like tonote that the situation in [16] is quite different from [12]; the base relation, , in [12] isbehaviourally sound while this may not be the case in barbed bisimilarity in [16] (where
and a.b.O are equated), so that we cannot know, at least a priori, that taking the$\mathrm{p}\mathrm{r}\mathrm{o}\mathrm{c}\mathrm{e}\mathrm{s}\mathrm{s}\dot{\mathrm{e}}\mathrm{s}$$\beta$$\approx$$a.\mathrm{O}$24

congruence within it is significant or not. More study is needed regarding the issue.
One remarkable point is the similarity in a way of deriving canonical congruences
over processes between our construction and those found in A-calculi [2, 1, 18], as was
already noted. What is common in these constructions is that the canonical equality is
obtained as the maximum element of a sizable family of “meaningful” equalities. The
method is not only mathematically elegant but also provides a tractable proof method(cf. development in 4:1). Mathematical canonicity may even suggest correspondence with
important models of the concerned formalism; at least such are cases in strict and lazy
-theories, though concrete results in the concurrency setting are still missing.
Finally, noting that reduction-closed equalities roughly correspond to bisimilarities,
it is natural to ask what formulation would correspond to e.g. may and must equivalences, possibly[5]. We can use “saturated” insensitive terms i.e. the set
combined with divergence notion. To find more direct ways of deriving such theories (i.e.
first) remains as an important open question.
without deriving$\mathrm{A}$$\{P|\Im_{\nu}^{*}\vdash P=\Lambda\}$$\propto s_{\nu}^{*}$

Acknowledgements. We thank Professors Cliff Jones and Robin Milner for fruitful discussions. We also thank anonymous referees and friends for providing valuablecomments and pointing out errors. Our gratitude to Professor Mario Tokoro for his encouragement and support. The first author is partially supported by JSPS Fellowships
for Japanese Junior Scientists.

References
1. Abramsky, S., The Lazy Lambda Calculus. ed. by D. Turner, Research topics in Functional
Programming, Addison Wesley 1990.
2. Barendregt, H., The Lambda Calculus: Its Syntax and Semantics. North Holand, 1984.
3. Berry, G. and Boudol, G., The Chemical Abstract Machine. Proc. 17th. Annual Symposiumon Principles of Programming Languages, 1990.
4. Boudol, G., Asynchrony and -calculus, INRIA Report 1702, INRIA, Sophia Antipolis,
1991.
5. De Nicola, R. and Hennessy, M. Testing equivalences for processes, Theoretical Computer
Science, 34(1), 1984.
6. Engberg, U. and Nielsen, M., A Calculus of Communicating Systems with Label Passing,Research Report DAIMI PB-208, University of Aarhus, 1986.
7. Honda, K., Two bisimilarities in -calculus, submitted. Also as Keio CS report 92-002,
1992.
8. Honda, K. and Tokoro, M., An Object Calculus for Asynchronous Communication. Proc.
ECOOP’91, LNCS 512, Springer-Verlag 1991.
9. Honda, K. and Yoshida, Y., Reduction-based Process Semantics, The full version as Keio
CS technical report 94-002, February 1994. A preliminary version as Keio CS technicalreport 92-003, October 1992.
10. Honda, K. and Yoshida, Y., Combinatory Representation of Mobile Processes, Proc. 21th.
Annual Symposium on Principles of Programming Languages, 1994.
11. Jones, C.B., A -calculus Semantics for an Object-Based Design Notation, Proc. CONCUR’93, LNCS 715, Springer Verlag, 1993.
12. Milner, R., Calculus of Communicating Systems. LNCS 92, Springer-Verlag, 1980.
13. Milner, R., Parrow, J.G. and Walker, D.J., A Calculus of Mobile Processes. Part $I/II$.
ECS-LFCS-89-85/86, Edinburgh University, 1989.
$\pi$

$\nu$

$\mathrm{p}\mathrm{i}$25

14. Milner, R., Functions as Processes. Proc. of ICALP’90, LNCS 443, Springer-Verla , 1990.
15. Milner, R., Polyadic -Calculus: a tutorial. Logic and Algebra of Specification, Springer$\pi$

Verlag, 1992.
16. Milner, R. and Sangiorgi, D., Barbed Bisimulation. Proc. of ICALP’92, LNCS 623,
Springer-Verlag, 1992.
17. Longo, G., Set Theoretical Models of Lambda Calculus: Theory, Expansions and Isomorphisms, Annals of Pure and Applied Logic, 24:153-188, 1983.
18. Ohg, C-H.L., The Lazy Lambda Calcu,lus: An Investigation into the Foundation of Functional Programming, Phd thesis, Imperial College, 1988.
19. Park, D., Concurrency and Automata on Infinite Sequences. LNCS 104, Springer-Verlag,
1980.
20. Thomsen, B., A calculus of higher order communicating systems. Proc. 16th. A nnual Symposium on Principles of Programming Languages, 1989.