数理解析研究所講究録902 巻 1995 年 26-48

26

A Fully Abstract Denotational Model for
Communicating Processes with Label-Passing
Eiichi Horita (堀田英–), Fer-Jan de Vries (フェルーヤン ドゥ フリース)
NTT Communication Science Laboratories
2-2, Hikaridai, Seika-Cho, Soraku-Gun, Kyoto 619-02, Japan-mail: horita@progn.kecl.ntt.jp, ferjan@progn.kecl.ntt.jp$\mathrm{E}$,
Abstract: This paper investigates the full abstractness problem for a CCS-like language,
with a label-passing mechanism. (Here labels are used as the names of communication channels throughwhich interactions between processes take place.) This language is essentially the same as the one
proposed by Astesiano et al.; it is an extension of full CCS of Milner and contains label-passing–
an important feature of -calculus of Milner et al.– in addition to the traditional CCS constructs:, parallel composition, nondeterministic choice, action restriction, and recursion. First, ou
an operational model , called the weak maximal linear semantics, is defined in terms of a Plotkin.
serves as a behavioral criterion for assessing semantic models forstyle transition system;
and it is
Then a denotational model $D$ is constructed on the basis of a complete partial orderin the sense that $D$ is the most abstract of thoseshown that $D$ is fffiy abstract with respect toresult means that $D$models which are less abstract than and compositional. The fullthe practical viewpoint embodied by .
is the most desirable (or optimal) semantic model$\mathrm{C}\mathrm{C}\mathrm{S}^{++}$$\pi$$inp\mathrm{u}\iota_{s}$$tp\mathrm{u}ts$$O$$\mathrm{C}\mathrm{C}\mathrm{S}++$$\mathrm{O}$$(\mathrm{c}\mathrm{p}\mathrm{o})$$O$$\mathrm{a}\mathrm{b}_{\mathrm{S}}\mathrm{t}\mathrm{r}\mathrm{a}\mathrm{C}\mathrm{t}\mathrm{n}\mathrm{e}\mathrm{s}8$$\mathrm{O}$$O$$\mathrm{h}\mathrm{o}\mathrm{m}$1Introduction

abstractness concems the relationship between two semantic models, say $D$ and , for a given
language . We say that the model $D$ is fully abstract with respect to the model if the following
in :holds for any two programs$O$$\mathrm{F}\mathrm{u}\mathrm{U}$$O$$\mathcal{L}$$\mathcal{L}$$s_{0},$ $s_{1}$$D\mathbb{I}s\mathrm{o}1=D\beta s11$iff

$O[C[s\mathrm{o}\mathrm{l}\mathrm{I}=O[C[s_{1}1\mathrm{I}$for all contexts$C[\cdot]$

(1)

of C.

an operational semantics describing the behavior of processes in terms a Plotkin-stylesystem.
transition
The full abstractness problem for programming languages was first raised by Milner [26]. In general,a fully abstract model for a given language with respect to a given operational semantics is themost abstract, and hence, the most desirable (or optimal) of those models which are less abstractiff
is less abstract than another modeland compositional. (Here we say a model
than
) The
have the same meaning under
every two programs having the same meaning undermodel $D$ can be considered the optimal model in the following sense: The operational semantics
may be considered to describe the most interesting characteristic of each process; such a model,
however, need not be compositional (see Sect. 1.2 of [27]). (This fact is also exhibited in the setting, is an essential property to fit the semanticof this paper; see Example 1.) Compositionality, inequational
logic; it is also necessary for the modular
basedonframeworkanaxiomaticmodel into
to define the meaning of a composite statement in tems
definition of program meanings (i.e., inof the meanings of its components). Thus some extra information needs to be involved to construct acompositional model; it is desirable, however, for the extra information to be minimum so as not tobring about inessential details. The fully abstract model $D$ meets these requirements (see Fig. 1 foran illustration of the optimality of $D$ ).
, withIn this paper, we investigate the full abstractness problem for a CCS-likea label-passing mechanism. (Here labels are used as the names of communication channels throughwhich interactions between processes take place.) This language is essentially the same as the one
proposed in [1]; it is an extension of full CCS [27] and contains label-passing–an important feature ofaddition to the traditional CCS constructs: inputs, outputs, parallel composition,-calculus
nondeteministic choice, action restriction, and recursion.
$\mathrm{I}\mathrm{J}_{\mathrm{P}^{\mathrm{i}\mathrm{a}\mathrm{U}}}r\mathrm{C}\mathrm{y}\mathrm{O}\mathrm{i}8$

$O$

$O$

$\mathcal{D}_{2}$$D_{1}$$D_{2}.$$D_{1}$$O$$\mathrm{t}\mathrm{u}\mathrm{m}$$\mathrm{o}A\mathrm{e}\mathrm{r}$

$-$

$l$

$\mathrm{l}\mathrm{m}\mathrm{g}\mathrm{u}\mathrm{a}\mathrm{g}\tilde{\mathrm{e}},$$\pi$$[29]-\mathrm{i}\mathrm{n}$$\mathrm{c}\mathrm{C}\mathrm{s}++$27

Figure 1: The hierarchy of semantic models
First an operational model , called the weak maximal linear semantics, is defined in terms of a
Plotkin-style transition system. The model is linear and maximal in that the meaningof eachprogram is the set of maximal sequences of actions the program may perform, and it is weak in thatthe action sequences are obtained by abstracting(finite sequences of) intemal moves.1 Froma certain practical viewpoint, can be considered to represent the most interesting characteristic ofeach (software or hardware) system;
serves as a behavioral criterion for assessing semantic models
for. Then a denotational model $D$ is constructed on the basis of a complete partial orderand it is shown that $D$ is fully abstract with respect to . The full abstractness result means thatis the most desirable (or optimal) semantic model
the practical viewpoint embodied by .
The cpounderlying $D$ is called the Smyth powerdomain of failures. This domain consists offailure-divergence sets first introduced in [7]; is not only a cpo but also a compete metric space $(cms)$
with an appropriate metric defined as in [3], and this twofold structure of is conveniently used forestablishing the full abstractness of $D$ with respect to , as described in the next subsection. The
model $D$ is a natural extension of the improved failures model of $[7, 15]$ to the language with labelpassing (see the remark at the end of Sect. 1.3); thus the construction of gives a counterexample
to Hennessy’s conjecture that the improved failures model is inadequate for modeling communicatingprocesses with value-passing when the set of passed-values is infinite (see [14, pp. 234-235]).
$\mathrm{O}$$\mathrm{O}$$\mathrm{O}[s\mathrm{I}$$s$$\mathrm{h}\mathrm{o}\mathrm{m}$$\mathrm{O}$$\mathrm{O}$$\mathrm{C}\mathrm{C}\mathrm{S}^{++}$$(\mathrm{c}\mathrm{p}\mathrm{o})$

$O$

$D$

$O$

$\mathrm{h}\mathrm{o}\mathrm{m}$$\mathrm{P}$$\mathrm{P}$$\mathrm{P}$$\mathrm{O}$

$D$

1.1

Outline of the Full Abstractness Proof

There are two frameworks for denotational semantics: the $cpo$ framework [37] and theframework [3], and each of the two has its own advantages and disadvantages (see Remark 1 below);
the full abstractness result of this paper is established by combining the respective advantages of thetwo frameworks.

$met7\dot{T}c$

Remark 1 (i) The cpo hamework provides a basis for a wide range of semantic models including
weak and strong models, but it does not provide much support for establishing equivalence
between a denotational and operational models.
(ii) The metric framework provides a powerful and uniform method (by means of Banach’s fixed-point
theorem) for establishing equivalence between a denotational and operational models (see [23]for a general account of this method, and see [3, 2, 8, 18, 20, 34] forof the method
to various languages). Furthermore, a metric model can bederived, under certain
conditions, from the transition rules by which operational models are defined (see [17, 19, 35]).
This method, however, is applicable only to strong models. 1$\mathrm{a}\mathrm{p}\mathrm{p}\mathrm{l}\mathrm{i}_{\mathrm{C}}\mathrm{a}\mathrm{t}\mathrm{i}_{0}.\mathrm{n}\mathrm{S}$$\mathrm{a}\mathrm{u}\mathrm{t}_{\mathrm{o}\mathrm{m}\mathrm{a}}\mathrm{t}\mathrm{i}\mathrm{C}\mathrm{a}\mathrm{l}\mathrm{l}\mathrm{y}$.

1On the other hand, we call a semantic model strong when the model does abstract from internal moves.

28

Strong Models$\downarrow$$\mathcal{H}$$\dot{C}_{\tau}$$|=$$\mathcal{M}_{\tau}|=$$\mathcal{H}$$D_{\tau}$

Figure 2: The scheme for establishing full abstractness results
By combining the respective advantages of the cpo and metric hameworks for denotational semantics,
we obtain the following general scheme
for establishing full abstractness results. (The scheme
is illustrated by Fig. 2, where the expression) This scheme has
denotes thatbeen applied in [18, Sect. 6] to a simple language for pure
. (By “pure processes” we mean
processes which can only communicate by simultaneously performing synchronization actions; see [14]for this terminology.) The full abstractness result reported in tthis paper is
by applying
the scheme to a more complex languagewith label-passing.
$(\mathrm{i})-(\mathrm{i}\mathrm{i}\mathrm{i})$$C_{\tau}arrow C\mathcal{H}$$\mathcal{H}\mathrm{o}C_{\mathcal{T}}=C.$$\mathrm{p}\mathrm{r}\mathrm{o}\mathrm{c}\mathrm{e}\mathrm{S}5\mathrm{e}\mathrm{S}$$\mathrm{e}\mathrm{s}\mathrm{t}\mathrm{a}\mathrm{b}\mathrm{l}\mathrm{i}8\mathrm{h}\mathrm{e}\mathrm{d}$$\mathrm{C}\mathrm{C}\mathrm{S}^{++}$(i) Given alanguage and an operational model $O$ which serves as a behavioral criterion forsemantic models for , it may be possible to define a strong operational modeland a hiding
functionand to show, by an operational analysis of program behaviors, that the model
defined byis less abstract than $O$ and complete with respect to $O$ in the sense thatthe congruence induced byis finer than the equivalence induced by . Thus it is sufficient
to construct a denotational model $D$ which is equivalent to , since the equivalence and thecongruence induced by a denotational model coincide with each other. Such a denotationalmodel $D$ may be constructed as follows.
$\mathcal{L}$$\mathrm{a}\mathrm{s}\mathrm{s}\mathrm{e}\mathrm{s}3\mathrm{i}\mathrm{n}\mathrm{g}$$L$$C_{\tau}$$C$$\mathcal{H}$$C=\mathcal{H}\mathrm{o}C_{\mathcal{T}}$$C$$\mathrm{O}$$C$(ii) The metric hamework can be conveniently used to construct a-based denotational modeland to establish the equivalence between
and , when these models are strong (see.
Remark 1$\mathrm{c}\mathrm{m}\mathrm{s}$$\mathcal{M}_{\tau}$$\mathcal{M}_{\tau}$$C_{\tau}$$(\mathrm{i}\mathrm{i}))$(iii) When the semantic domain underlying
is both a cpo and a, we can construct a strong
order-theoretic model
which is equivalent to; furthermore whenis a continuous homomorphism from the underlying algebra ofto the weak version of the algebra, we canalso construct a weak order-theoretic model $D$ such that; thus we can obtain theequivalence between and $D$ , thereby establishing the full abstractness of $D$ with respect to O.
$\mathcal{M}_{\tau}$$D_{\tau}$$\mathrm{c}\mathrm{m}\mathrm{s}$$\mathcal{H}$$\mathcal{M}_{\tau}$$D_{\tau}$$D=\mathcal{H}\circ D_{\tau}$

$C$

1.2

Comparison with Other Approaches to Full Abstractness Proofs

To establish the full abstractness of a denotational $D$ with respect to a given operational model ,we have to establish detailed connections between T) and O. However, it is in general very difficult
to establish such connections directly, because the denotational method by which $D$ is defined is very
different from the operational (or transitional) method by which $O$ is defined.
The following approach is taken to overcome this difficulty in this paper as well as in the otherpapers (such as [12, 14, 30]) treating the full abstractness problem in the context weak semantic
models for concurrent languages. First, another operational model , called an intermediate model,
is introduced, and it is shown to be equivalent to $D$ ; then close connections between andareestablished by operational analysis program behaviors, and thereby the desired connections between$D$ andare obtained.
Thus, the difficulty is reduced to the problem of establishing the equivalence between and $D$ .
Our approach to establishing the equivalence is different ffom those taken in the other papers (such as
$O$

$C$

$O$

$C$

$\mathrm{O}$

of.

$C$

29

: We establish the equivalence by constructing an strong denotationaland operationalsuch thatandand by showning that bothandare the fixedpoint of the same higher-order contraction (which has a unique fixed-point by
Banach’s fixed-point
theorem). In the other papers (such as [12, 14, 30]), on the other hand, this equivalenceis establishedby a detailed operational analysis of the intermediate model , typically byshowing that the preorderinduced by is algebraic (see [12, Sect. 4.5]). Roughly, our approach is denotational, whereas
theother approaches are operational.
We believe our approach is more easily applicable to various languages, since there
is a general
method, which is insensitive to language constructs under a certain general condition,
to construct theauxiliary models
andand to establish their equivalence (see [17, 19]), whereas the operational
analyses (of ) needed in the other approaches are ad hoc and are sensitive tolanguagetreated. Moreover, such operational analyses may involve crucial errors, which are
difficult to detectin the absence of general methods (see Remark3 for such an error found in [30]).
$1^{12,14,30}])$one$D_{\tau}$$C_{\tau}$$D=\mathcal{H}\mathrm{o}D_{\tau}$$C=\mathcal{H}\mathrm{o}C_{\mathcal{T}}$$D_{\tau}$$C_{\tau}$

$C$

$C$

$D_{\tau}$$C_{\tau}$$C$$\mathrm{c}\mathrm{o}\mathrm{n}3\mathrm{t}\mathrm{r}\mathrm{u}\mathrm{c}\mathrm{t}\mathrm{S}$1.3

Connections with Other Full Abstractness Results

A similar full abstractness result has been established by Bergstra, Klop, andOlderog for a language
without recursion or intemal moves [5]. Moreover, Rutten investigated the semantics of aconcurrent
language for pure processes in the framework of, and showed that the failures model isabstract with respect to a strong linear semantics. The full abstractness of $D$ with respect
to , expressed by (1) above, is an extension of the result of Bergstra et al. to alanguage withrecursion, internal moves, and label-passing. Also it is an extension of Rutten’s result to thecase ofweak semantics (from strong semantics) and to a language with label-passing. The result
reported inthis paper is an extension of the result of [18, Chap. 6], where a sinilar full abstractness
result has
been given for a concurrent language for pure processes. (Sinilar full abstractness results havealso
been given in [16], but there
the models are constructed in a purely operational ffamework.)
In [14], Hemessy and Ing\’ofsd\’ottir proposed a denotational model for a minor variant of ffiu CCS,
which is slightly simpler thanfull CCS features value-passing but does not featurelabel-passing. Their model is closely related to our model $D$ , but the machinery used for constructing
their model is quite different fiom that used in this paper: The semantic domain in [14] is abstractly
constructed, along the lines of [32], as a solution of a system of reflexive domain equations (which
are rather complex with a powerdomain constructor appearing in a recursive way), while we use
thesimple failures domain defined in elementary set theory. And the behavioral criterion employedin [14]is based on the concept of testing and different ffom the one employed in this paper–we use
the weaklinear semantics as the behavioral criterion.
The model $D$ is a natural extension of the improved failures model of $[7, 15]$ to the languagewith label-passing, although we use the Smyth order [36] instead of the reverse set inclusion usedin$[7, 15]$ , for the convenience in relating operational and denotational semantics.2 (Note thatin $[7, 15]$ ,the improved failure model is given in a purely denotational ffmework, with no comparisonswith$\mathrm{c}\mathrm{m}\mathrm{s}’ \mathrm{s}$$\mathrm{f}\mathrm{i}_{1}11\mathrm{y}$$O_{\mathrm{L}}[33]$$O$$\mathrm{a}\mathrm{U}$$\mathrm{C}\mathrm{C}\mathrm{S}++\mathrm{b}\mathrm{e}\mathrm{c}\mathrm{a}\mathrm{u}\mathrm{s}\mathrm{e}$operational models.)2

Language$\mathrm{C}\mathrm{C}\mathrm{S}++$In this section, we define the language a CCS-like language,, with a label-passing mechanism.
(Here labels are used as the names of communication channels through whichinteractions between
processes take place.) This language is essentially the same as the one proposed in [1]; it is an extensionof full CCS [27] and contains label-passing–an important feature of -calculus
addition to
the CCS constructs: inputs, outputs, pamllel composition with value-passing, nondeterministic choice,action restriction, and recursion.
We define the language in the framework of typed -calculus with -notation as the version of
PCL given in [11]; we take the types (of values), (of Booleans), and $P$ (of process) as ground$\mathrm{C}\mathrm{C}\mathrm{S}^{++}$$[29]-\mathrm{i}\mathrm{n}$$\pi$$\lambda$

$\mu$

$V$

$\overline{2\mathrm{T}\mathrm{h}\mathrm{e}}$original failures model[6]$\mathrm{a}\mathrm{k}\mathrm{o}$$B$use the reverse set inclusion as the ordering between failure sets.

30(the type of predicates or parameterized
types, and we restrict the composite types to$P^{(1)}=(\mathcal{V}arrow B)$ (the type of parameterized processes
Booleans with one parmeter of type ) andwith one parameter of type .
, we define several basic sets.
As a preliminary to the definition of the language(Here labels
Deflnition 1 (1) It is assumed that a common domain V of values md labels is given.
Let $(b\in)$passed.)arevalueswhichthroughchannels
as the names of communication$\mathcal{B}^{(1)}=(\mathcal{V}arrow B)$$\mathcal{V}$$\mathcal{V})^{3}$$\mathrm{C}\mathrm{C}\mathrm{S}++$

serve$\mathrm{B}=${true, false} be the domain of Booleans.

and $\mathrm{V}?=\{v?|v\in \mathrm{V}\}$ . The set $(c\in)$ Out of output actions is defined(2) We put$(c\in)$ In of input actions$=\mathrm{V}!\cross \mathrm{V}=\{(v!,v’)|v,v’\in \mathrm{V}\}$ . Likewise, we define the set
by Outof communication actions
by In $=\mathrm{V}?\cross \mathrm{V}=\{(v?,v’)|v, v’\in \mathrm{V}\}$ . From these, the set.
of actions by. We define the set
is defined by
be the set of variables of type $V,$ $(X\in)$ Varp the set of variables of type , and(3) LetVarp, and define the set $(Z\in)$. We putthe set of variables of type$\mathrm{V}!=\{v!|v\in \mathrm{V}\}$$(c\in)\mathrm{C}$$\mathrm{C}_{\tau}=\mathrm{c}\cup\{\tau\}$$(a\in)\mathrm{C}_{\tau}$$\mathrm{C}=\mathrm{O}\mathrm{u}\mathrm{t}\cup \mathrm{I}\mathrm{n}$$(\xi\in)$$\mathcal{P}$$\mathrm{V}\mathrm{a}\mathrm{r}_{\mathcal{V}}$$P^{(1)}$$\mathrm{V}\mathrm{a}\mathrm{r}_{P}^{(1})$

Var of variables by Var$\mathrm{V}\mathrm{a}\mathrm{r}_{p}^{*}=\mathrm{V}\mathrm{a}\mathrm{r}_{P^{\cup}}$.

$=\mathrm{V}\mathrm{a}\mathrm{r}v\cup \mathrm{v}_{\mathrm{a}}\mathrm{r}_{p}^{*}$of Boolean $expreS\mathit{8}ions$of values expressions and a set
that a set;
we only postulate theandforare given. Here it is not necessary to specify the syntax
semantic models
defining
inconvenience,forconcerning andconditions“ $(E0=E1)”\in \mathcal{G}$
.
For
.
, and
in later sections: (i)
“
.
)
“(
A
”,
(iii) For
Boolean expressions byparameterizedof
We define the set(4) We$(G\in)\mathcal{G}$$(E\in)\mathcal{E}$$\mathrm{a}8\mathrm{s}\mathrm{u}\mathrm{m}\mathrm{e}$$\mathcal{E}$$\mathcal{G}$$\mathcal{G}$$\mathcal{E}$$(\mathrm{i})-(\mathrm{i}\mathrm{i}\mathrm{i})$$\mathrm{f}\mathrm{o}\mathrm{U}_{0}\mathrm{W}\mathrm{i}\mathrm{n}\mathrm{g}$$\mathrm{V}\mathrm{a}\mathrm{r}_{\mathcal{V}}\subseteq \mathcal{E},$$\mathrm{B}\subseteq \mathcal{G}$$\mathrm{V}\subseteq \mathcal{E}$$G_{1}$$G_{0}$$\neg(G\mathrm{o})$$G_{0},G_{1}\in \mathcal{G},$$E_{0},E_{1}\in \mathcal{E},$$(\mathrm{i}\mathrm{i})$$”\in \mathcal{G}$$\mathcal{G}^{(1)}$$(H\in)\mathcal{G}^{(1)}=${‘‘$(\lambda x$.

$G)$ ”$|x\in \mathrm{V}\mathrm{a}\mathrm{r}_{\mathcal{V}}$A$G\in \mathcal{G}$In term of the basic sets given above, the language)
Deflnition 2 (Language

}.

$1$

defined by:$\mathrm{C}\mathrm{C}\mathrm{S}++\mathrm{i}\mathrm{s}$$\mathrm{C}\mathrm{C}\mathrm{S}^{++}$of terms of type , simultaneously with the set of terms(1) First, we define a set, by the following BNF grammar:of type$(S\in)\tilde{L}$$(T\in)\tilde{L}^{(1})$$\mathcal{P}$$P^{(1)}$$S::=0|_{0}\partial_{C}(s^{\mathrm{u}\mathrm{t}})’(E0E1,\mathrm{n}(E,H,\tau)T,E|_{X|X}^{(|}s_{0}(^{1}\mu S1).

,

$\{$

$T::=(\lambda X. s)|\xi|(\mu\xi.

\tau)$|(S_{0}+S1)|S)$,$),$
ranges over)(resp.
where $X$ (resp. ) ranges over.
, and ranges over
over
Below we give a brief description of each of the constructs:$\mathrm{V}\mathrm{a}\mathrm{r}_{P}^{(1}$$\mathrm{V}\mathrm{a}\mathrm{r}_{P}$$\xi$$\mathcal{G}^{(1)}$

$C$

$E$

$\mathcal{E},$$G$

ranges over$\mathcal{G},$$H$

ranges$\wp(\mathrm{C})$

resprests inaction in the sense of CCS.
this
through the channel(ii) The constmct out $(E_{0}, E1, S)$ . represents output the value”“
corresponding. of CCS with the label
is a natural extension of the CCS constructto .
of those
represents selective input through the channel(iii) The construct inforconstruct
LOTOS
the
of
analogue. This is an
the predicate
valuesmotivationaFor
3.5.2]).
Sect.
[38,
or
(see
[10]
value-acceptance with a selection predicate
for this combinator, see Remark2(2) below.

(i) The constant$0$$E_{0;}$$E_{1}$$\overline{c}E_{1}$

$S$

$c$

$E_{0}$$(E_{0}, (\lambda x.

$E_{0}$

G),\tau)$$(\lambda x.

$\mathrm{S}\mathrm{a}\mathrm{t}\mathrm{i}\mathrm{S}\mathrm{p}_{\mathrm{i}\mathrm{n}\mathrm{g}}$G)$, without$\overline{3\mathrm{W}\mathrm{e}}$can easily extend the language so as to include such processes as take several values as theirprocesses
only
treat
we
that
simplicity
for
only
sections;
it
is
in
later
semanticsofany nontrivial changes of the definition
cause a fundamental change in the definition of the semantics, if we include
with zero or one parameter. However, it
processes as their parameters.
takeas
processes
suchprocesses,
higher-order$\mathrm{p}\mathrm{a}\mathrm{r}\mathrm{a}\mathrm{m}\mathrm{e}\mathrm{t}\mathrm{e}\mathrm{r}8$$\mathrm{w}\mathrm{i}\mathrm{U}$31(iv) The combinator$||$

represents is parallel composition of CCS.

(v) The combinatorextemal choice (or general choice) of CSP (see Sect. 3.3 of[15] . The transition rules for this combinator is slightly different
those for the choicecombinator of CCS (see rule (iv) in Definition $9(1)$ ). For a motivation for this combinator,
see Remark 2 (1) below.
$+\mathrm{r}\mathrm{e}\mathrm{p}\mathrm{r}\mathrm{e}\mathrm{S}\mathrm{e}\mathrm{n}\mathrm{t}_{\mathrm{S}}$$)$$\mathrm{h}\mathrm{o}\mathrm{m}$(vi) The constructrepresents the restriction of those actions of which are contained in$C$ ;The transition rule for this construct is slightly different
those for the restriction”
construct “of CCS (see rule (vii) in Definition $9(1)$ ). For a motivation for thisconstruct, see Remark 2(3) below.
$S$$\partial_{C}(S)$$\mathrm{h}\mathrm{o}\mathrm{m}$$S\backslash C$(vii) The construct if $(B, s_{0}, S_{1})$ is the same as the conditional construct of CCS.
(viii) The construct
is the application of the parameterized process $T$ to the actual
parameter $E$ . We sometimes write $T(E)$ instead of.
$\mathrm{a}\mathrm{p}(\tau, E)$$\mathrm{a}\mathrm{p}(\tau, E)$(ix) The -notation $(\mu X. S)$ represents a recursively defined process whose body is
$\mu$

$S$

.

(x) Likewise, the -notation $(\mu\xi. T)$ represents a recursively defined parameterized process
whose body is $T$ .
$\mu$, when each occurrence
We will say that a variable $X\in$ Varp is guarded an expressionof $X$ occurs in a subexpression of the form out $(E, E’, S”)$ or in $(E, (\lambda x. G),T)$ . Likewise we, when each occurrence ofsay that a variable
is guarded in an expression
occurs in a subexpression of the form out ( $E,$
or in $(E, (\lambda x. G), T)$ .
$S’\in\tilde{L}$$\mathrm{i}\dot{\mathrm{n}}$$T’\in\overline{\mathcal{L}}^{(1)}$$\xi\in \mathrm{V}\mathrm{a}\mathrm{r}_{P}^{(1)}$$\xi$$E^{\prime,s’)}’$The set $(S\in)L$ of statements of the language
the following guardedness condition:
For each subexpression $(\mu X. S’)$ (resp.
(resp. ) is guarded in $S’$ (resp. in $T$ ).

$\mathrm{C}\mathrm{C}\mathrm{S}.++\mathrm{i}\mathrm{s}$de.fi ed to be the set of$S\in\tilde{L}\mathrm{s}\mathrm{a}\mathrm{t}\mathrm{i}_{\mathrm{S}}\mathrm{f}\mathrm{y}.\mathrm{i}\mathrm{n}\mathrm{g}$$\mathrm{n}_{l}$$(\mu\xi$. $T)$ ) of , the variable $X$
$S$

(2)

$\xi$

Likewise we define the setof parameterized statements of the language
satisfying the above guardedness condition (2).
the set of$(T\in)\mathcal{L}^{(1)}$$\mathrm{C}\mathrm{C}\mathrm{S}++\mathrm{t}\mathrm{o}$be$T\in\overline{L}^{(1)}$Let us put$(U\in)\mathcal{L}^{*}=\mathcal{L}\cup \mathcal{L}^{(1)}$(2) The constructs “, let$U\in \mathcal{L}^{*}$””, “ $(\mu X. \cdots)$ ”, and “have the usual binding property. For
be the set of elements of Var which have a free occurrence in .

$(\lambda x.

$\mathrm{F}\mathrm{V}(U)$.
$(\mu\xi.

\cdots)$\cdots)$$U$, let us define

and bybyand) is the set of closed(resp.
, respectively. Thenstatements (resp. the set of of closed parameterized statements). Let us use (resp. ) as a(resp.
). Let us put
variable ranging over
. For $Z\in$ Var, weinstead of
.
write
For

$\mathcal{Y}\subset\wp(\mathrm{V}\mathrm{a}\mathrm{r})$$\mathcal{L}[\mathcal{Y}]$$\mathcal{L}^{(1)}[\mathcal{Y}]$$\mathcal{L}^{(1)}[\mathcal{Y}]=\{T\in L^{(1)}|\mathrm{F}\mathrm{V}(T)\subseteq \mathcal{Y}\}.$$\mathcal{L}[\mathcal{Y}]=\{S\in \mathcal{L}|\mathrm{F}\mathrm{V}(S)\subseteq \mathcal{Y}\}$$L[\emptyset]$$\mathcal{L}^{(1)}[\emptyset 1$

$t$

$s$

$\mathcal{L}[\emptyset]$$\mathcal{L}[Z]$Further we put$\mathcal{L}^{(1)}[\emptyset]$$(u\in)\mathcal{L}^{*}[\emptyset]=\mathcal{L}\cup \mathcal{L}^{(1)}$$\mathcal{L}[\{Z\}]$$(e\in)\mathcal{E}[\emptyset]=\{E\in \mathcal{E}|\mathrm{F}\mathrm{V}(E)=\emptyset\},$$(g\in)\mathcal{G}[\emptyset]=\{G\in \mathcal{G}|\mathrm{F}\mathrm{V}(G)=\emptyset\}$, and$(h\in)\mathcal{G}^{(1)}[\mathrm{o}]=\{H\in \mathcal{G}^{(1)}|\mathrm{F}\mathrm{v}(H)=\emptyset\}.1$

Remark 2 (1) We can adopt the choice combinator of CCC instead of $”+$ ” (namely we can remove$”+$ ” and introduce another binary combinator with the same transition rules as those for thethechoice combinator of CCC) and preserve the full abstractness result, by slightly
$[4,
16]$
simplicity
only
6];
for
,
Chapter[16,
itisdefinition of the semantic domain along the lines ofcombinator of CCC.
that we adopt the combinator $”+$ ” for external choice instead of the$\mathrm{m}\mathrm{o}\mathrm{d}\mathrm{i}\mathfrak{g}\mathrm{r}\mathrm{i}\mathrm{n}\mathrm{g}$$\mathrm{c}\mathrm{h}\mathrm{o}\mathrm{i}_{\mathrm{C}}.\mathrm{e}$(2) Clearly we obtain richer expressive power by adopting the construct in $(E_{0}, (\lambda x. G),T)$ for sewithout
lective input instead of a natural extension (which would be represented by inthe selection predicate) the CCS construct “cx.S” for unselective input. Such richer expressive
power is convenient for describing communication systems (see [38, Sect. 3.5.2]). By using this$(E_{0},\tau)$

32

of the denotational model $D$ givenrich expressive power, we can establish thein Sect. 5; it is not known whether or not the full abstractness can be established if we replace
for unsethe construct in $(E_{0}, (\lambda x. G),T)$ for selective input by the simper construct inslightlybymodel
denotationalaconstructingindifficulty
lective input. (Note that there is no$D$ , for a language which has in $(E_{0},T)$ instead of in $(E_{0}, (\lambda x. G),T).)$
simplifying$\mathrm{f}\mathrm{u}\mathrm{u}_{\mathrm{a}}\mathrm{b}\mathrm{s}\mathrm{t}\mathrm{r}\mathrm{a}\mathrm{C}\mathrm{t}\mathrm{n}\mathrm{e}\mathrm{s}8$$(E_{0},\tau)$of which areof CCS represents the restriction of thoseof CCS isconstruct
restriction
the
sense
,
this
In
complementitsorcontained
establish
restriction,
we
can
type
this
By
using
construct.
ourrestrictionthanunselective
more
the full abstractness of the denotational model Z); again it is not known whether or not theby the more unselective
abstractness can be established if we replace the construct
restriction construct of CCS. (Note that there is no difficulty in constructing a denotational
instead of, for a language which has the CCS constructmodel by slightly(3) The restriction construct$\mathrm{a}\mathrm{c}\mathrm{t}\mathrm{i}\mathrm{o}\mathrm{n}8$$S\backslash C$$S$$\overline{C}\cdot$$\mathrm{e}\mathrm{i}\mathrm{t}\mathrm{h}\mathrm{e}\mathrm{r}\cdot \mathrm{i}\mathrm{n}C$$\partial_{C}(S)$$\mathrm{f}\mathrm{u}\mathrm{U}$$S\backslash C$$\mathrm{m}\mathrm{o}\mathrm{d}\mathrm{i}\mathfrak{g}\Gamma \mathrm{i}\mathrm{n}\mathrm{g}\mathcal{D}$$\partial_{C}(S).)$(4) The grammar given in Definition2 is sufficient to construct a parser of the language, except; in order to construct a parser, it is necessary to introduce some
. A possible way is to introduce two constructs
the suffix $C$ in”””“which correspond to “
and “)
} $(s)$) is the evaluation of(resp.
”, respectively, where [and “) (see the beginning of Sect. 4 for more explanation of the(resp.
the expression I.
evaluation mechanism

for the constructsyntax for$\partial_{C}(S)$$\partial_{C}(S)$$\mathrm{s}\mathrm{p}\mathrm{e}\mathrm{C}\mathrm{i}\Phi \mathrm{i}\mathrm{n}\mathrm{g}$$\partial!(E, (\lambda x.

$\partial?(E, (\lambda x.

B), S)$B), S)$$\partial_{\{(\beta E\mathrm{Q}!},v$$|\ovalbox{\tt\small REJECT}_{B1v/1}x\mathrm{f}=\mathrm{t}\mathrm{r}\mathrm{u}\mathrm{e}$$[B[v/X]\mathrm{I}$$E\mathrm{J}$$\partial_{\{(\mathfrak{l}^{E}1v)\mathrm{I}[}?,B[v/x]1=\mathrm{t}\mathrm{r}\mathrm{u}\mathrm{e}\}(s)$$\mathbb{I}B[v/x]\mathrm{I}$$E\mathrm{J}$$1$$[\cdot \mathrm{I})$as a subset of the set of terms generated by a many-sorted signature Fun
We can characterize(given in Definition3 below) together with -notation and -notation. Thus, along the usual lines ofdenotational semantics, we can define a denotational model by giving a cpo as an underling domain
and by giving interpretations of the elements of Fun as continuous functions on the cpo (see [11]); inin this way.
define the denotational model $D$ for
Sect. 5 we
Definition 3 Let Fun be the set of constants and combinators of , and for $(i,j, k,l, m)\in\omega^{5}$ , let. Namely, we define)
be the set of elements with arity,
as follows:”“,, (iii)(i) Fun$(0,0,0,0,0)=\{$ “ ” , (ii)$\mathcal{L}^{*}$$\lambda$$\mu$$\mathrm{C}\mathrm{C}\mathrm{S}^{++}$$\mathrm{w}\mathrm{i}\mathrm{U}$$\mathcal{L}$$\mathcal{V}^{i}\cdot B^{j}\cdot(B(1))^{k}\cdot p\ell\cdot(p1)m$$\mathrm{F}\mathrm{u}\mathrm{n}_{(i,j,k,\ell_{m}},$$\mathrm{K}\mathrm{n}_{(*i^{k}\ell_{m)}}.,,$

$0$

(iv)

$\mathrm{F}\mathrm{u}\mathrm{n}_{(0},0,0,1,0)=\{"\partial c" |c\in^{\mathrm{c}}\}$(vi) Fun$(0,1,0,2,0)=\{$ “(viii)

3$\mathrm{i}\mathrm{f}$$\mathrm{F}\mathrm{u}\mathrm{n}_{(i_{\dot{\theta}},k},\ell_{m)},=\emptyset$”$\mathrm{F}\mathrm{u}\mathrm{n}_{()}1,0,1,0,1=\{$$\mathrm{F}\mathrm{u}\mathrm{n}_{(2,0,0,1},0)=\{" \mathrm{o}\mathrm{u}\mathrm{t}" \}$

$\}$

$\}$

, (vii), (v)$\mathrm{F}\mathrm{u}\mathrm{n}_{(0)}0,0,0,1,=\{"||", "+" \}$$\mathrm{F}\mathrm{u}\mathrm{n}_{(1,0},0,0,1)=\{$“”$\mathrm{a}\mathrm{p}$$\}$$\mathrm{i}\mathrm{n}$

$\}$

,

,

for the other indexes $(i,j, k,l,m)$ .

$1$

Preliminary Definitions

In this section we fix basic mathematical notation and introduce several notions concerning domainsof sequences.

Definition 4 Let

$A$

and

$B$

be sets.

(1) The set of natural numbers is denoted by , and each number $n\in\omega$ is identified with the set$\{i\in\omega|0\leq i<n\}$ . The powerset of(resp. the collection of finite subsets of ) is denoted by$\wp(A)$ (resp. by).
$\omega$$A$$A$$\wp \mathrm{f}\mathrm{i}\mathrm{n}(A)$. The domain and range of a(2) The set of functions from to $B$ is denoted by $(Aarrow B)$ or by$(f)$avariable and an expressionFor,
respectively.
and ranfunction are denoted by$(\lambda
x\inA.
E(x))$
which maps $x\in A$ tofunctionthedenoteused
tois$E(x)$ , the-expression
for $(\lambda x\in A. E(x))$ .
or$E(x)$ . We sometimes write$B^{A}$

$A$

$f$

$x$

$\mathrm{d}\mathrm{o}\mathrm{m}(f)$$\lambda$$\langle E(x)\rangle_{x\in A}$$\langle E(x)|x\in A\rangle$

33(3) The empty sequence is denoted by . The sequence consisting of$a_{n-1}\in A$ is denotedby. The set of finite sequences of elements of is denoted by, and $A^{+}=$. The set of fimite or infinite sequences of elements of is denoted by. Eachsequence
is regarded as a function whose domain is a member of. Thus, thelength of is, which we refer to as. (We haveby definition.)$\epsilon$$a_{0},$ $\cdots,$$\mathrm{c}$$A$$\langle a_{0}, \cdots, a_{\hslash-1}\rangle^{4}$$A^{<\mathrm{t}d}$$A^{<\omega}\backslash \{\epsilon\}$$A$$A^{\leq\omega}$$w\in A^{\leq\omega}$$w$(4) Forand$\omega\cup\{\omega\}$$\mathrm{d}\mathrm{o}\mathrm{m}(w)$$1\mathrm{g}\mathrm{t}(w)$$w_{1}\in A^{<\omega},$ $w_{2}\in A^{\leq\omega}$$p_{2}\subseteq A^{\leq\omega}$

, let

, let

$w_{1}\cdot w_{2}$$w_{1},w_{2}\in A^{\leq\omega},$(5) We define the set$B$ (whenfinite) bydenote the concatenation of

iff$w_{1}=w_{2}\uparrow \mathrm{d}\mathrm{o}\mathrm{m}(w_{1})$$A\triangleright B=(A^{<\omega}\cdot B)\cup A^{\omega}$. And forand$or\dot{d}er\prec$$\preceq$$w_{1}\preceq w_{2}$$w_{2}$$p\subseteq A\leq\omega$$w_{2}\in p_{2}$, and$w_{1}\prec w_{2}$of finite or infimite sequences of elements of$A\triangleright B$

and$w_{1}$

A{}. For. The prefix order and the strict prefix$w_{1}\cdot w_{2}|w_{1}\in p_{1}$$p_{1}\cdot p_{2}=$$p[w]=\{\tilde{w}\in A^{\leq\omega}|w\cdot\tilde{w}\in p\}$usual: For$w=\langle w(i)\rangle|.\in 1\mathrm{g}\mathrm{t}(w)$

$A$

.

iff

$p_{1}\subseteq A^{<\omega}$, let
are defined as$w\in A^{<\omega}$$w_{1}\preceq w_{2}$A $w_{1}\neq w_{2}$ .

ending with an element of(6) Let $X$ be a topological space. The closure of a subset
is denoted by. The collection ofclosed subsets of $X$ is denoted by, and the the set of nonempty subsets of $X$ is denotedby.
$\mathrm{Y}^{\mathrm{c}1}$$\mathrm{Y}\subseteq X$$\wp_{\mathrm{c}1}(X)$$\wp_{\mathrm{n}}(X)$

Hereafter, we use the convention that
denotes the set ofproperty (or properties) indicated by the suffix . Thus, for example,ofnonempty and closed subsets of X. 1$\wp\ldots(X)$(of $X$ ) having the$\mathrm{a}\mathrm{U}\mathrm{s}\mathrm{u}\mathrm{b}3\mathrm{e}\mathrm{t}_{\mathrm{S}}$$\cdots$$\wp_{\mathrm{n}\mathrm{c}1(X)}$denotes the set$\mathrm{a}\mathrm{U}$Deflnition 5 Let$A$

and $B$ disjoint nonempty sets not$\mathrm{c}\mathrm{o}\mathrm{n}\mathrm{t}\mathrm{a}\mathrm{i}\mathrm{n}\mathrm{i}\mathrm{n}\mathrm{g}\perp$. We put$B_{\perp}=B\cup\{\perp\}$(1) A function strip:
is defined as follows: For
if, and otherwise let strip $(q)=q$ . The stream
defined as follows: For, let
if either $q_{1}=q_{2}$ or (. For each, the n-th projection function:
defined as follows: For, let, and otherwise let
And for, let $p^{[n]}=\{q^{[n]}|q\in p\}$ .
$(A\triangleright B_{\perp})arrow A^{\leq\omega}$$(\cdot)$$q\uparrow(1\mathrm{g}\mathrm{t}(q)-1)$$q\in(A\triangleright B_{\perp})$$1\mathrm{g}\mathrm{t}(q)<\omega$$q_{1},$.

, let strip $(q)=$is$order\subseteq \mathrm{o}\mathrm{n}(A\triangleright B_{\perp})$$q_{2}\in(A\triangleright B_{\perp})$$q_{1}\in A^{<\omega}\cdot\{(\perp\rangle\}$$q_{1}\subseteq q_{2}$$n\in\omega$$\mathrm{s}\mathrm{t}\mathrm{r}\mathrm{i}_{\mathrm{P}(q_{1})}\preceq \mathrm{s}\mathrm{t}\mathrm{r}\mathrm{i}_{\mathrm{P}}(q2))$$(\cdot)^{[n]}$$q^{[n]}=q\mathrm{i}\mathrm{f}\mathrm{l}\mathrm{g}\mathrm{t}(q)\leq n$$q\in(A\triangleright B_{\perp})$

and
is
.

$(A\triangleright B_{1})arrow A^{<\omega}\cdot B_{1}$$q^{[n]}=(q\beta_{n})\cdot\langle\perp\rangle$$p\in\wp(A\triangleright B_{\perp})$(2) A distance function on
is defined in terms of the projection functions as follows: For, let $d(q_{1}, q_{2})= \inf$ { $(1/2)^{n}|n\in\omega$ A $(q_{1})^{[n}]=(q_{2})^{[n}]$ }.
$d$$q_{1},$$(A\triangleright B_{\perp})$$q_{2}\in(A\triangleright B_{\perp})$

Likewise, a distance function$\tilde{d}$onis defined as follows:5 For$\wp(A\triangleright B_{\perp})$$\tilde{d}(p_{1},p_{2})=\inf\{(1/2)^{n}|n\in\omega\wedge(p_{1})^{[n]}=(p_{2})^{1n]}\}$

Deflnition 6 Let
as in Definition5.
(1) A binary
let

$A$

, the Smyth order onif(2) We will say that$p\in\wp(A\triangleright B_{\perp})$$\wp_{\mathrm{f}}(A\triangleright B\perp)=$(3) We define$\wp(A\triangleright B_{\perp})$$\forall q_{2}\in p_{2},$ $\exists q_{1}\in p_{1}[q_{1}\subseteq q_{2}]${is fiat if$p\in\wp(A\triangleright B_{\perp})|p$$\wp_{\mathrm{f}\mathrm{c}1}(A\triangleright B_{\perp})$and(4) Let{by the metric . We define$d$$\forall q,$, let$\mathrm{c}\mathrm{o}\mathrm{n}\mathrm{t}\mathrm{a}\mathrm{i}\mathrm{n}\mathrm{i}\mathrm{n}\mathrm{g}\perp$, and let, is defined as follows: For$q’\in p[q\subseteq q’\Rightarrow q=q’ ]$

$d$

and

$\tilde{d}$be defined$p_{1},p_{2}\in\wp(A\triangleright B_{\perp})$,. We putis flat}.

$\wp_{\mathrm{n}\mathrm{f}\mathrm{c}1}(A\triangleright B_{1})$$p\in\wp(A\triangleright B_{\perp})|p$$\wp_{\mathrm{c}\mathrm{o}}(A\triangleright B_{\perp})=$.

$p_{1},p_{2}\in\wp(A\triangleright B_{\perp})$$\iota$and $B$ be disjoint nonempty sets not$\mathrm{r}\mathrm{e}\mathrm{l}\mathrm{a}\mathrm{t}\mathrm{i}_{0}\mathrm{n}\subseteq_{\mathrm{s}}$$p_{1}\subseteq_{\mathrm{s}}p_{2}$.

, according to the convention in$\mathrm{D}\mathrm{e}\mathrm{f}\mathrm{i}\dot{\mathrm{m}}\mathrm{t}\mathrm{i}\mathrm{o}\mathrm{n}4(6)$.

is compact}, where the notion of compactness is induced, andas in part (3).

$\wp_{\mathrm{f}\mathrm{c}\circ}(A\triangleright B_{\perp}),$$\wp_{\mathrm{n}\mathrm{f}\mathrm{c}\mathrm{o}}(A\triangleright B_{1})$$\wp_{\mathrm{n}\mathrm{f}\mathrm{c}\circ}(A\triangleright B_{\perp})$(5) Letand $q\in X$ . We will say that is minimal in $X$ when $\neg\exists q’\in X[q’\subseteq q\wedge q’\neq q]$ .
Let ${\rm Min}(X)=$ { $q\in X|q$ is minimal in $X$ }.
$X\in\wp(A\triangleright B_{\perp})$$q$

4We do not abuse notation by writing
to refer to { , because it will be confusing when we treat sequences
consisting of sequences in later sections (cf. [15, Sect. 1.5] for similar strict notation).
5It is easily checked that coincides with the Hausdorff distance induced by (for the definition of Hausdorff distancesee [9] .
$a_{0}$$\tilde{d}$$)$$a_{0}\rangle$

$d$

34

(6) The limit of a converging sequence

Notation 1 Let $(X,$(1) For a chain$\subseteq, \perp)$$\langle_{X_{n}}\rangle_{n\in\omega}$,$(\mathrm{Y}, \subseteq’, 1’)$$\langle p_{n}\rangle_{n\in\omega}$bein $X$ , the $lub$ of$\mathrm{c}\mathrm{p}\mathrm{o}’ \mathrm{s}$in$(\wp_{\mathrm{c}1}(A\triangleright B_{\perp}),\tilde{d})$is denoted by$\lim_{n}p_{n}$. I.

$\{x_{n}\}_{n\in\omega}$

in $X$ is denoted by$\mathrm{u}x_{n}n$. Let$[Xarrow \mathrm{Y}]$denote theset of continuous functions from $X$ to $Y$ .
(2) Let (X,$\subseteq,$$\perp$) be aa chain to mean that$\mathrm{u}p_{m+n}\mathfrak{n}$$m\in\omega$$\mathrm{c}\mathrm{p}\mathrm{o},$, and $\langle x_{n}\rangle_{n\geq m}\in(\{n\in\omega|n\geq m\}arrow X)$ . We say thatis a chain, we write
is a chain; whenisto denote$\langle x_{n}\rangle_{n\geq m}$$\langle x_{n}\rangle_{n\geq m}$$\langle X_{m+n}\rangle n\in\omega$$n\geq m\square p_{n}$. IDefinition 7 For
put act

and$p\in\wp(\mathrm{C}_{\tau}\triangleright\wp(\mathrm{C})\perp)$$(p)=\{a\in \mathrm{C}_{\tau}|p[\langle a\rangle]\neq\emptyset\}$.

$w\in(\mathrm{C}_{\mathcal{T}})^{<\omega}$, let$p[w]=\{q\in(\mathrm{C}_{\mathcal{T}}\triangleright\wp(\mathrm{C})\perp)|w\cdot q\in p\}$

. We

$1$

be metric spaces and be a nonnegative real number. We wtite
Deflnition 8 Let (X, ) andto denote the set $\{f\in(Xarrow \mathrm{Y})|\forall x, x’\in x1^{d’}(f(X), f(x’))\leq\epsilon\cdot d(x, x’) ]\}$ . In particular,
to denote the set of nonexpansive mappings from $X$ to Y. 1
we write$d$$(\mathrm{Y}, d’)$$\epsilon$$(Xarrow^{\mathcal{E}}\mathrm{Y})$$(Xarrow^{1}\mathrm{Y})$4

The Operational ModelIn this section, the operational model$\mathcal{O}$is defined in terms of a transition system in the style of$O$.

$\mathrm{P}\mathrm{l}\mathrm{o}\mathrm{t}\mathrm{k}\mathrm{i}\mathrm{n}[- 31]$

To define the transition system, we assume that some evaluation mechanism) is given. For(resp. to) to(resp.
.
evaluation [ by$[e]\in \mathrm{V}$$g\in B[\emptyset]$

4.1$[g\mathrm{I}\in \mathrm{B}$$[h\mathrm{J}=(\lambda v\in \mathrm{V}.

$h\mathrm{I}$$\mathrm{n}_{\mathrm{a}\mathrm{n}}\mathrm{S}\mathrm{i}\mathrm{t}\mathrm{i}_{\mathrm{o}\mathrm{n}}$Definition 9 ($h\equiv(\lambda x.

Relations)$\mathrm{b}\mathrm{a}\mathrm{n}\mathrm{s}\mathrm{i}\mathrm{t}\mathrm{i}\mathrm{o}\mathrm{n}$(ii) in$(e_{0},e_{1}, S)s\underline{(\beta e\mathrm{o}1!,\beta e_{1}\mathrm{I})}$$(e, (\lambda_{X}.

,

.

if
$v \in \mathrm{V}\bigwedge_{S_{1}}[G[arrow s_{1}\tau/vX,]\mathrm{J}=\mathrm{t}\mathrm{r}\mathrm{u}\mathrm{e}$$(c\in \mathrm{C})$

.

(iv)

$\overline{(s_{1}+s_{2})arrow(\tau s_{1^{+}2}’s)}$’,$(a \in \mathrm{C}_{\tau})$$\frac{s_{1^{arrow s’}1}a}{(_{\mathit{8}1}||_{S_{2}})aarrow(_{\mathit{8}_{1}}||s_{2})}$

.

(vi)

,

(viii)$(a\not\in C)$$\frac{s_{1}arrow(aS)}{\mathrm{i}\mathrm{f}(g,s_{1},s2)aarrow(s)}$(x) The$\mathrm{f}\mathrm{o}\mathrm{U}\mathrm{o}\mathrm{W}\mathrm{i}\mathrm{n}\mathrm{g}$,$(v,v’\in \mathrm{v})$

.

,

if

.
$\mathbb{I}g\mathrm{J}=\mathrm{t}\mathrm{r}\mathrm{u}\mathrm{e}$.

$(e\in \mathcal{E}[\mathrm{o}])$.

The following rule is called the -rule:$\lambda$,$( \mathrm{i}\mathrm{x})’\frac{s_{2}arrow(as)}{\mathrm{i}\mathrm{f}(g,s_{1,2}S)aarrow(s)}$rule is called the pre-evaluation rule:$\frac{\mathrm{a}\mathrm{p}(u,[e\mathrm{I})arrow S’a}{\mathrm{a}\mathrm{p}(u,e)aarrow_{\mathit{8}}}$$(\mathrm{x}\mathrm{i})$$\frac{s_{1^{rightarrow}2}(v!,v)\prime s’1’ srightarrow S’2(v?,v’)}{(s_{1}||_{S_{2}})\mathcal{T}arrow(_{S’}1||s_{2})\prime}$’$(s_{2}||s1)\tauarrow(s’2||S_{1})$$(s_{2}||s_{1})aarrow(S2||S’1)$$\frac{\mathit{8}arrow s’a}{\partial_{C}(\mathit{8})aarrow\partial c(S)}$.

$(s_{2}+S_{1})\mathcal{T}arrow(S_{2}+s’1)$$(s_{2}+S_{1})\mathrm{c}arrow S_{1}$(vii)

are defined as the smallest relations satisfying the.

G),t)rightarrow \mathrm{a}(1^{e1?},v)\mathrm{p}(t,v)$$( \ddot{\mathrm{u}}\mathrm{i})\frac{s_{1}arrow s_{1}’c}{(s_{1}+s_{2})carrow S_{1}\prime}$(v)$e\in \mathcal{E}[\emptyset]$

System$\mathrm{r}\mathrm{e}\mathrm{l}\mathrm{a}\mathrm{t}\mathrm{i}\mathrm{o}\mathrm{n}\mathrm{s}\sim^{a}\subseteq(\mathcal{L}[\emptyset])^{2}(a\in \mathrm{C}_{\tau})$(i) out

mapping, we define the[G[v/x]\mathrm{J})$(1) The transition
following rules:.

$\mathbb{I}\cdot 1$

G)\in \mathcal{G}^{(1)}[\emptyset]$

if$[g\mathrm{I}=\mathrm{f}\mathrm{a}\mathrm{l}\mathrm{s}\mathrm{e}$.

35$(v\in \mathrm{V})$$\frac{S[v/x]aarrow S’}{\mathrm{a}\mathrm{p}((\lambda x.s),v)aarrow s’}$$(\mathrm{x}\mathrm{i}\mathrm{i})$.

The following rule is called the recursion rule:$\frac{S[(\mu X.s)/X]aarrow S’}{(\mu X.S)aarrow_{\mathit{8}’}}$.

(xiii) The following rule is called the paramete rized recursion rule:$(v\in \mathrm{V})$$\frac{\mathrm{a}\mathrm{p}(T[(\mu\xi.\tau)/\xi],v)aarrow s’}{\mathrm{a}\mathrm{p}((\mu\xi.T),v)aarrow S’}$

(2) For$s\in \mathcal{L}[\emptyset]$, we put act $(s)=$.

$\{a \in \mathrm{C}_{\tau}|\exists s’\in \mathcal{L}[\emptyset][Sarrow_{S’}a ]\}$

.1

The transition system is image-finite in the following sense:, the image-set
andProposition 1 For every$\{s’\in \mathcal{L}[\emptyset]|s\sim^{a}S’\}$$a\in \mathrm{C}_{\tau}$$s\in \mathcal{L}[\emptyset]$

Proof. By induction on the structure of using the guardedness condition (2).
$s$

For

$a\in \mathrm{C}_{\tau}$

1$\blacksquare$, let us define the channel of , written chan $(a)$ , by
$a$

$v!$

chan $(a)=\{$$v$?

$\tau$

if $a=(v!, v)’$ ,if $a=(v?, v)’$ ,otherwise.

(3)

Then, the transition system is bounded with

Proposition 2 For every

4.2

is finite.

$s\in \mathcal{L}[\emptyset]$, the set

The Operational Modelto channels in the following sense:$re\mathit{8}pect$$\mathrm{c}\mathrm{h}\mathrm{a}\mathrm{n}[\mathrm{a}\mathrm{c}\mathrm{t}(S)]$of channels is finite. 1$O$.
In this subsection, we define the operational model in terms of the transition relations[28]):(asinoftransitions
notionsotherthreedefinition,
weintroducethetopreliminary
As a, we write $s-^{w}s’$ to mean that
, andDeflnition 10 (1) For
such that
there exist$\langle-^{a}|a\in \mathrm{C}_{\tau}\rangle$$\mathrm{O}$$w=(a_{0}, \ldots , a_{n-1})\in(\mathrm{C}_{\mathcal{T}})^{<\omega}$$s_{0},$$w\in \mathrm{C}^{<\omega}$$s_{n}\in \mathcal{L}[\emptyset]$and(3) For$(w\backslash \tau)$$w\in(\mathrm{C}_{\tau})^{\omega}$. .. $s_{n-1}arrow a_{n-}1Sn\equiv SJ$ .

$s’\in \mathcal{L}[\emptyset]$$s,$$\exists\tilde{w}\in(\mathrm{C}_{\mathcal{T}})<\omega$where$s’\mathcal{L}[\emptyset]$$\ldots,$$s\equiv s_{0}arrow a_{0}S1rightarrow a_{1}$(2) For$s,$[, we write$Sarrow S’\overline{w}$A$s\Rightarrow^{w}s$$w=(\tilde{w}\backslash \tau)$denote the result of erasing
and$s\in \mathcal{L}[\emptyset]$$\exists\langle_{S_{n}}\rangle_{n\in\omega}\in(\mathcal{L}[\iota])\omega$, we write$sarrow w$’

to mean that],$\tau’ \mathrm{s}$

in

$w$

.

to mean that

[ $s0=s$ A $\forall n\in\omega[s_{n}arrow S_{n}w(n)+1$ ]]. 1

By using the above definition, the operational model
Deflnition 11 (The Operational Model O)(1) The flattening function${\rm Min}(\cdot)$on$\wp(\mathrm{C}_{\mathcal{T}}\triangleright\{\delta, \perp\})$$O$

is defined by:

is defined as in Definition6(6).

as follows: For:(2) First, we define an auxiliary model
conditions
threefollowing
the
of
,
one
if
, we put$\tilde{O}$$\rho\in(\mathrm{C}_{\tau}\triangleright\{\delta, \perp\})$$\rho\in\overline{O}[s\mathrm{I}$$\mathcal{L}[\emptyset]arrow\wp(\mathrm{C}_{\tau}\triangleright\{\delta, \perp\})$andis satisfied:$s\in \mathcal{L}[\emptyset]$$(\mathrm{i})-(\mathrm{i}\mathrm{i}\mathrm{i})$36Lemma 4.1 Let
Then$\varphi,$$\psi$

be knowledge propositions including only disjunction and conjunction symbols.
$[\varphi\vee\psi]\div\rho\#=[\varphi]\div\rho[\#_{\mathrm{n}}\psi]\div\rho\#$[ A ]$\div\rho^{\#\#}=[\varphi]\div\rho \mathrm{u}[\psi]\div\rho^{\#}$$\psi$$\varphi$

Each agent infers from previous message and determines its next action and its next message to send.
We provide a property which guarantees that agents reasonably infer proposition from some messages.

be a knowledge proposition andknowledge propositions. We say that agent knows from the condition set

Definition 4.1 Let $s\in Q$ and let$\Gamma\equiv\psi_{1}\wedge\cdots$

A

at

$s$

$\varphi$$i$$\Gamma$$\varphi$.

$s\delta_{1}$be a conjunctive
if and only if$\psi_{m}$$\cap[\mathrm{r}]\div\rho^{\#}\subseteq[\varphi]$

As mentioned in the previous section, the quotient relation is the greatest relation
mutative diagram:$\alpha$satisfing the com-$1^{\Gamma}1k-1/\star\backslash \searrow^{\alpha}$$QQ\overline{\rho^{l}}$Lemma 4.2 Let $s\in Q.$ Assume that
.
then

$i$

knows

$\varphi$

from$\Gamma$at$s$. For every state such that $(t, s)\in p$ , if$t$$s\models K_{i}\varphi$$t\models K_{i\varphi}$

Proof: Suppose that for every state $t\in Q$ such that$t\subseteq s\rho\#,$$t\subseteq[\varphi]\div\delta_{i}$, that is$s\rho^{\#}\subseteq[\varphi]_{k}\div\delta_{i}$As$\rho$

and$\delta_{i}$are commutative,$s$$\subseteq$$s$$\subseteq$$s$$\subseteq$

8$\subseteq$$\mathit{8}\delta_{:}$$\subseteq$$([\varphi]\div\delta_{\dot{\iota}})\div p\#$$[\varphi]\div\rho^{\mathrm{t}}\delta_{i}$$[\varphi]\div\delta_{i}\rho^{\#}$$([\varphi]\div\rho^{\#})\div\delta_{\dot{\iota}}$$[\varphi]\div\rho^{\#}$

From assumption it holds that$s\delta_{i}\cap[\varphi]\div\rho^{\#}\subseteq[\psi]$

Then we have$s\delta_{i}\subseteq[\psi]$.

$\square$Remark 4.1: If the transition relation
proposition .

$\rho$

is reflexive, then it holds that$[\varphi]\div\rho\subseteq[\varphi]$

for any knowledge$\square$$\varphi$

where is a conjunctive knowledge
Theorem 4.1 Let the transition relation be reflexive, and$(t,s)\in\rho$
.
then
, if
any
transition
proposition and is a knowledge proposition. For$[\Gamma]\subseteq[\varphi]$$\rho$$t\models K_{i}\Gamma$$\varphi$

Proof: Assume that$\Gamma$$t\subseteq[\Gamma]\div\delta_{i}$for every$t\subseteq s\rho\#$, that is,$s\rho^{\#}\subseteq[\mathrm{r}]\div\delta_{i}$.

$s\models K_{\dot{*}}\varphi$

37$\star_{p}\Rightarrow \mathrm{X}\mathrm{R}$

As

$p$

and

are commutative, we have$\delta_{i}$$s\delta_{ip^{\#}=S}p\delta\# i\subseteq[\Gamma]$

so that$s\delta_{i}\subseteq[\Gamma]\div p\#$. From assumption$=$$s\delta_{i}$therefore$s\delta_{i}\subseteq[\varphi]$, hence$s\subseteq[\varphi]\div\delta_{i}$.

$s\delta_{\dot{l}}\cap[\mathrm{r}]\div p^{\#}$$\subseteq$$s\delta_{i}\mathrm{n}[\varphi]\div\rho\#$$\subseteq$$s\delta_{\dot{l}}\cap[\varphi]$$\square$Corolary 4.1 (In the same condition of theorem.) For every transition $(t, s)\in\rho$ , ifthen.

$s\models K_{i\varphi}$$t\models K_{i}\varphi$

then$s\models K_{i}\varphi$

Proof: By theorem in the case of

Proposition 4.1 Let
knowsfrom A$\varphi\psi$$\varphi$$p$$\psi$.

.

$\Gamma\equiv\varphi$$\square$be reflexive. For every transition $(t, s)\in\rho$ , if$t\models K_{i}\varphi$

and$t\models K_{i}\psi$

then

$i$

Proof: By assumption we have$s\rho^{\#}$

As

$p$

and

$\delta_{i}$$\subseteq$$[K_{i\varphi}]\cap[K_{i}\psi]$$=$$([\varphi]\div\delta_{i})\cap([\psi]\div\delta i)$$=$$([\varphi]\mathrm{n}[\psi])\div\delta_{i}$.

commutes$s\delta_{i}$$\subseteq$$=$

from assumption. Hence we have$s\delta_{i}\Pi$($[\varphi$$([\varphi]\Pi 1^{\psi}])\div\rho^{\#}$$[\varphi\wedge\psi]\div\rho \mathrm{t}$$\subseteq$$[\varphi\vee\psi]\div\rho^{\#}$$\subseteq$$[\varphi\vee\psi]$

A $\psi]\div p$ )$\#\subseteq[\varphi\vee\psi]$.

$\square$$\not\in\doteqdot \mathrm{X}\mathrm{f}\mathrm{f}\mathrm{l}$[CM86] K. M. Chandy and J. Misra. How processes learn. Distributed Computing, 1:40-52, 1986.

[FH88]

R. Fagin and J. Y. Halpern. I’m ok if you’re : On the notion of trusting communication.
Journal of Philosophical Logic, 17:329-354, 1988.
$\mathrm{o}\mathrm{k}$[HM89] J. Y. Halpern and Y. Moses. Modelling knowledge and action in distributed systems. Distributed
Computing, 3:159-177, 1989.
[HM90] J. Y. Halpern and Y. Moses. Knowledge and common knowledge in a distributed environment.
Journal of the Association for Computing Machinery, $37(3):549-587$ , 1990.

[Hoa85]$\mathrm{C}.\mathrm{A}$.R. Hoare. Communicating Sequential Processes. Prentice Hall, 1985.

38$*_{\ovalbox{\tt\small REJECT}\yen \mathrm{X}\mathrm{R}}$[HZ89]J. Y. Halpern and L. D. Zuck. A little knowledge goes a long way: Simple knowledge-based
derivation and correctness proofs for a family for protocols. Technical Report RJ 5857, IBM
Research Division, 1989.

[Kaw90] Y. Kawahara. Pushout-complements and basic concepts of grammers in toposes. TheoreticalComputer Science, 77:267-289, 1990.
[Kaw94] Y. Kawahara. Relational formalization of knowledge dynamics. draft, 1994.
[KM92] Y. Kawahara and Y. Mizoguchi. Categorical assertion semantics in topoi.
and Technology, 4:137-150, 1992.

$AdvanCe\mathit{8}$in Soflware[LL90]

L. Lamport and N. Lynch. Distributed computing: Models and methods. In van Leeuwen J.,
editor, Handbook of theoretical computer science, pages 1157-1199. Elsevier Science Publishers
B.V., 1990.

[Mi189]R. Milner. Communication and Concurrency. Prentice Hall, 1989.

[SS85]

G. Schmidt and T. Str\"ohlein. Relation algebras: Concept of points and represetntability. Discrete Mathematics, 54:83-92, 1985.

[Tar41] A. Tarski. On the calculus of relations. THE JOURNAL OF SYMBOLIC LOGIC, 6(3), 1941.

39(1) The function (P.
one has (P.
$\lambda p\in$$\lambda p\in$(2) The function ($\overline{\mathrm{o}\mathrm{u}\mathrm{t}}(v,$$\lambda p\in$P.

is a nonexpansive and continuous unary operation on$v’,p)$ )$v’,p)$ ) $\in(\mathrm{P}arrow^{1}\mathrm{P})\cap[\mathrm{P}arrow \mathrm{P}]$$\overline{\mathrm{o}\mathrm{u}\mathrm{t}}(v,$$\overline{\mathrm{o}\mathrm{u}\mathrm{t}}(v,v’,p)$$\mathrm{P},$,$i.e.$.

) is contractive in the sense that

. I(6)$\forall p_{0},p_{1}\in \mathrm{P}[\tilde{d}(\mathrm{o}\mathrm{u}\mathrm{t}(v, vp\mathrm{o})’,, \mathrm{o}\mathrm{u}\mathrm{t}(v, v’,p1))\leq(1/2)\cdot\tilde{d}(p_{0},p1)]$

Deflnition 15 We define$\pi\in \mathrm{P}^{(1})$,$\overline{\mathrm{i}\mathrm{n}}(v, \eta, \pi)=$

where

{

$\langle c\rangle|C\in\wp(\mathrm{C})$$I=\{v’\in \mathrm{V}|\eta(v’)=\mathrm{t}\mathrm{r}\mathrm{u}\mathrm{e}\}$As for$\overline{\mathrm{o}\mathrm{u}\mathrm{t}}(v, v’,p)$Proposition 6 Let(1) The function$i.e.$ , one has(2) The function$\forall\pi_{0},$5.3.2

as follows: For$\overline{in}:\mathrm{V}\cross \mathrm{B}^{(1)}\cross \mathrm{P}arrow\wp_{\mathrm{f}\mathrm{c}1(}\mathrm{C}\mathcal{T}\triangleright\wp(\mathrm{C})_{1})$A $C\cap(\{v?\}\cross I)=\emptyset$ }and$(\lambda\pi\in \mathrm{P}^{(1)}.

$\eta\in \mathrm{B}^{(1)}$

, and

.

$\cup,\cup(\langle(v!, v’)\rangle v\in I^{\cdot}\pi(v’))$

(7)

. I

, we have the following useful property of$v\mathrm{V}$$v\in \mathrm{V},$$\eta\in(\mathrm{V}arrow \mathrm{B})$\mathrm{i}\mathrm{n}(v, \eta\sim\sim’\pi))$$\overline{\mathrm{i}\mathrm{n}}(v, \eta, h)$.

.

is a nonexpansive and continuous function from$\mathrm{P}^{(1)}$to$\mathrm{P}$,.

$(\lambda\pi\in \mathrm{P}^{(1)}.

\mathrm{i}\mathrm{n}(v, \eta, \pi))\in(\mathrm{p}(1)_{arrow^{1}}\mathrm{p})\cap[\mathrm{P}^{(1)}arrow \mathrm{P}]$$(\lambda\pi\in \mathrm{P}^{(1)}.\overline{\mathrm{i}\mathrm{n}}(v, \eta, \pi))$

is contractive in the sense that.

$\pi_{1}\in \mathrm{P}^{(1)}[\tilde{d}(\mathrm{i}^{\sim}\mathrm{n}(v, \eta, \pi 0), \mathrm{i}^{\sim}\mathrm{n}(v, \eta, \pi_{1}))\leq(1/2)\cdot d\sim \mathrm{f}(\pi 0, \pi_{1})]$

(8)

$1$

Parallel Composition

The definitions of the semantic operations corresponding to parallel composition, action restriction,and extemal choice is more involved than the definitions in Sect. 5.3.1. First we need a preliminary
definition.

Definition 16 For$p_{0},p_{1}\in \mathrm{P}$, let$\sim||_{\perp}(p0,p1)=\{\langle\perp\rangle\}\cap(p_{0}\cup p_{1})$$\sim||_{\delta}(\mathrm{P}0,p1)=\{\langle C\rangle|C\in\wp(\mathrm{C})\wedge\exists C_{0},$$C\subseteq C_{0}\cap C_{1}\wedge\overline{(\mathrm{c}\backslash C\mathrm{o})}\cap(\mathrm{C}\backslash C_{1})=\emptyset.\}$We will define a binary operation

Proposition 7 For$p0,p_{1}\in \mathrm{P}$$\sim||$

on

, and
(9)

$C_{1}\in\wp(\mathrm{C})[\langle C\mathrm{o}\rangle\in p_{0}\wedge\langle C_{1}\rangle\in p1\wedge$$\mathrm{P}$I

so that the following proposition holds:, one has$\overline{||}(_{\mathrm{P}0,p_{1}})=||\perp(\sim p0,p1)\cup\overline{|}\wedge|\delta(p0,p1)\cup\tilde{\mathrm{L}}\wedge(p_{0},p1)\cup\tilde{\perp}(p1\wedge,p0)\cup \mathrm{L}\wedge\sim\sim(p0,p1)\cup \mathrm{L}(p1,p0)\wedge$

,

(10)

where
$\tilde{\perp}(p0,p1)=$

, and

(11)

$(\langle a\rangle\cdot||(p_{0}\sim[\langle a\rangle],p_{1}))$$\cup$$a\in \mathrm{a}\mathrm{c}\mathrm{t}(p_{0})$(12)$\sim\sim\lfloor(p0,p_{1})=\cup\{\langle\tau\rangle\cdot||(p0[\langle(v!, v’)\rangle],p_{1}[\langle(v?, v)’\rangle])|$$v’\in \mathrm{V}$

$v,$

A

$(v!, v)’\in \mathrm{a}\mathrm{c}\mathrm{t}(p\mathrm{o})$A$(v?, v)’\in \mathrm{a}\mathrm{c}\mathrm{t}(p_{1})\}$.I

Informally, we may supppose that is defined by the above proposition, where thecharacterized in terms ofwith. Formally, the operation
as the unique fixed-point of a higher-order mapping
defined by:$\sim||$

isis defined$\mathrm{V}\mathrm{a}\mathrm{l}\mathrm{u}\mathrm{e}_{\sim}|\sim|(\mathrm{p}0,p1)$$||(p_{0}[w_{0}],p_{1}[w_{1}])$$w_{0},$$w_{1}\in(\mathrm{C}_{\mathcal{T}})^{<\omega}$$||$$\Phi_{||}$

Deflnition 17 We define
and$(p0,p_{1})\in \mathrm{P}^{2}$$\Phi_{||}$:$(\mathrm{P}^{2}arrow \mathrm{P})arrow(\mathrm{P}^{2}arrow\wp(\mathrm{C}_{\mathcal{T}}\triangleright\wp(\mathrm{C})_{1}))$

as follows: For$F\in(\mathrm{P}^{2}arrow \mathrm{P})$

, let
(13)

$\Phi_{||}(F)(p_{0},p1)\sim$$=||\perp(p_{0},p1)\cup||_{\delta}(p\wedge\sim 0,p1)\cup\Phi(\iota F\wedge 0)(p,p1)\cup\Phi_{1^{(F)(}p_{1},p}\wedge 0)\cup\Phi_{\lfloor}(p_{0},p1)\wedge\cup\Phi_{\lfloor}(p1,p\mathrm{o})\wedge$$\Phi_{1}(F)(p0,p_{1})=$.

$\cup$$a\in \mathrm{a}\mathrm{c}\mathrm{t}(p\mathrm{o})$, and$(\langle a\rangle\cdot F(p\mathrm{o}[\langle a\rangle],p_{1}))$, where
(14)

40

(15)

$\Phi_{\lfloor}(F)(p0,p1)=\cup\{\langle T\rangle\cdot F(p01\langle(v|, v’)\rangle],p1[\langle(v?, v’)\rangle 1)|$$v,$$v’\in \mathrm{V}$A$(v|, v’)\in \mathrm{a}\mathrm{c}\mathrm{t}(p_{0})$A$(v?, v’)\in \mathrm{a}\mathrm{c}\mathrm{t}(p1)\}$.

$1$

to itself, and preserves nonexpansiveness
The mapping
is a monotonic contractionand (order-theoretical) continuity. (see Sect. 5.3.2 of [21] for the proof of this fact). We formally define, the unique flxed-point of . By Corollary 1, we haveto be fix
. Thus is nonexpansive and (order-theoretically) contin, because the limit of nonexpansive functions is nonexpansive
uous
and the lub of continuous functions is continuous.
$\mathrm{h}\mathrm{o}\mathrm{m}(\mathrm{P}^{2}arrow \mathrm{P})$$\Phi_{||}$$\sim||$$(\Phi_{1}|)$$\mathrm{u}_{n}((\Phi_{1})^{n}|(^{\sim}\perp)),$$\sim||=\mathrm{f}\mathrm{i}\mathrm{x}(\Phi_{||})=\lim_{n}((\Phi_{||})n(\perp))=\sim$$\Phi_{||}$$\mathrm{w}\mathrm{h}\mathrm{e}\mathrm{r}\mathrm{e}\perp\sim=(\lambda\vec{p}\in \mathrm{P}^{2}.

\{\langle\perp)\})$$\sim||$$(\mathrm{i}.\mathrm{e}.,||\sim\in(\mathrm{P}^{2}-^{1}\mathrm{P})\cap[\mathrm{P}^{2}-^{1}\mathrm{P}])$

5.3.3

Action Restriction and External Choice, we define acorresponding to the
For every
is similar to that of but more simple (see Sect. 5.3.3 ofcombinator
the formal definition of[21] for the defimition).
corresponding to the combinator $‘+$ ’ can be
The binary(seedefined directly without using a higher-order mapping
Sect. 5.3.4 of [21] for the definition).
$C\in\wp(\mathrm{C})$$\mathrm{u}\mathrm{n}\mathrm{a}\mathrm{r}\mathrm{y}_{0}\mathrm{p}\mathrm{e}\mathrm{r}\mathrm{a}\mathrm{t}\mathrm{i}\mathrm{o}\mathrm{n}\tilde{\partial}_{C}\in(\mathrm{P}-^{1}P)\cap[\mathrm{P}arrow \mathcal{P}]$$\partial_{C;}$$\sim||$$\partial_{C}$$\mathrm{o}\mathrm{p}\mathrm{e}\mathrm{r}\mathrm{a}\mathrm{t}\mathrm{i}\mathrm{o}\mathrm{n}+\sim:\in(\mathrm{P}^{2}arrow^{1}\mathcal{P})\cap[\mathrm{P}^{2}arrow \mathcal{P}]$5.3.4

Conditionals and Function Application

The definitions of the semantic operations corresponding to the construct if
the construct
for function application are intuitively natural.
:
as follows: For
andDeflnition 18 (1) We define$(\cdot, \cdot, \cdot)$

for conditionals and$\mathrm{a}\mathrm{p}(\cdot, \cdot)$$\mathrm{B}\cross \mathrm{P}^{2}arrow \mathrm{P}$$\mathrm{i}\mathrm{f}(b)\sim$$p_{0}$$\mathrm{i}\mathrm{f}(b,p0,p_{1})=\sim\{$$p_{1}$(2) We define

5.4

if
if

$b=\mathrm{t}\mathrm{r}\mathrm{u}\mathrm{e}$

, let
(16)

.

as follows: For

The Denotational Model$p_{0},p_{1}\in \mathrm{P}$,$b=\mathrm{f}\mathrm{a}\mathrm{l}\mathrm{s}\mathrm{e}$$\overline{\mathrm{a}\mathrm{p}\mathrm{l}}:\mathrm{P}(1)\cross \mathrm{V}arrow \mathrm{P}$$b\in \mathrm{B}$and$\pi\in \mathrm{P}^{(1)}$$v\in \mathrm{V},$let$\overline{\mathrm{a}\mathrm{p}\mathrm{l}}(\pi,v)=\pi(v)$

.I

$D$

, we define the denotational model $D$ in terms of weak versionsofOn the basis of the cpo
the semantic operations
defined in the previous subsection. The weak operations
are defined as
the compositions of the original operations
and a hiding function . First we define .
$(\mathrm{P}, \subset_{\mathrm{s}})$$\overline{\mathrm{o}\mathrm{p}}$$\overline{\mathrm{o}\mathrm{p}}$$\overline{\mathrm{o}\mathrm{p}}$5.4.1

The Hiding Function$\mathcal{H}$$\mathcal{H}$$\overline{\mathrm{o}\mathrm{p}}$$\mathcal{H}$The hiding function is defined by:
Definition 19 (1) A function
, let
with
$\mathcal{H}$is defined as follows: For, and for
, let

$h:(\mathrm{C}_{\tau}\triangleright\wp(\mathrm{C})_{\perp})arrow(\mathrm{C}_{\tau}\triangleright\wp(\mathrm{C})_{\perp})$$(w, x)\in(\mathrm{C}_{\mathcal{T}})^{<\omega}\cross\wp(\mathrm{C})_{\perp}$$(\overline{w}\backslash \tau)\cdot\langle\perp\rangle$$h(q)=\{$$h(q)=(w\backslash \tau)$$h(q)=(w\backslash \tau)\cdot\langle x\rangle$

ifotherwise.

$\exists\overline{w}[w=\tilde{w}\cdot\langle \mathcal{T}\rangle i\in\omega 1$$q=w\cdot\langle x\rangle$$q\in(\mathrm{C}_{\mathcal{T}})^{\omega}$,ding function:
is defined as follows: For $p\in$, let $\mathcal{H}(p)={\rm Min}(h[p])$ . I
The monotonicity of immediately follows fiiom this definition:
Proposition 8 The hiding function
monotonic with respect.
Moreover, we have the following lemma:
Lemma 2 The hiding function
is a continuous function fromto itself. 1
This lemma
from the continuity of on
by applying (a localized version of)
the lifting method proposed by Meyer and de Vink (see Theorem 4.6 of [24]). See Lemma 3 of [21] forthe proof.
(2) The$\dot{\mathrm{h}}$$\mathcal{H}$$\wp(\mathrm{C}_{\mathcal{T}}\triangleright\wp(\mathrm{C})_{1})arrow\wp(\mathrm{C}_{\tau}\triangleright\wp(\mathrm{C})_{1})$$\wp(\mathrm{C}_{\tau}\triangleright\wp(\mathrm{C})_{\perp})$$\mathcal{H}$$\mathcal{H}i_{\mathit{8}}$$to\subseteq_{\mathrm{S}}$$\mathcal{H}$$\mathrm{f}\mathrm{o}\mathrm{U}\mathrm{o}\mathrm{W}\mathrm{s}$$1$$\wp \mathrm{f}\mathrm{c}\mathrm{l}(\mathrm{c}\tau\triangleright\wp(\mathrm{C})_{1})$$h$$\wp(\mathrm{C}_{\tau}\triangleright\wp(\mathrm{C})_{\perp})$

41

5.4.2

Weak Versions of Semantic Operations

Deflnition 20 For $(i,j, k,\ell,m)\in\omega^{5}$ andbe defined as: For$\mathrm{f}\mathrm{o}\mathrm{u}_{\mathrm{o}\mathrm{W}\mathrm{S}}$$varrow\in \mathrm{V}|,$), let$\overline{\mathrm{o}\mathrm{p}}:\mathrm{V}^{i}\cdot \mathrm{B}^{j}\cdot(\mathrm{B}^{(1)})^{k}\cdot \mathrm{p}^{\ell}$$\mathrm{o}\mathrm{p}\in \mathrm{F}\mathrm{u}\mathrm{n}_{(k,\ell,m}$$b\sim\in \mathrm{B}^{j},\vec{\beta}\in(\mathrm{B}^{(1)})^{k}\vec{p}\in \mathrm{P}^{\ell}$, and$\vec{\pi}\in(\mathrm{P}^{(1)})^{m}$.

$(\mathrm{P}^{(1)})^{m}arrow \mathrm{P}$

, let

.I

$\overline{\mathrm{o}\mathrm{p}}(\vec{v}\cdot b\cdot\tilde{\beta}\cdot\tilde{p}\sim\cdotarrow\tilde{\pi})=\mathcal{H}(\overline{\mathrm{o}_{\mathrm{P}}}(\vec{v}\cdot b\cdot\vec{\beta}\cdot\vec{p}\cdot\tilde{\pi}))$

5.4.3

Deflnition of the Denotational Model$D$

Having defined the semantic operations
definition of the denotational model $D$ is straightforward. In order to formulate the definition, it convenient to introduce the set Valt of valuations.
Deflnition 21 Let
Valt be the set of those elements ofwhich preserve types
in the following sense:$\overline{\mathrm{o}\mathrm{p}},$$\mathrm{t}\mathrm{b}\mathrm{e}$$\mathrm{i}_{8}$$(\zeta\in)$$(\mathrm{V}\mathrm{a}\mathrm{r}arrow(\mathrm{V}\cup \mathrm{P}^{*}))$$(Z\in \mathrm{V}\mathrm{a}\mathrm{r}v\Rightarrow\zeta(\ddot{Z})\in \mathrm{V})$A

A$(Z\in \mathrm{V}\mathrm{a}\mathrm{r}_{\mathcal{P}}\Rightarrow\zeta(Z)\in \mathrm{P})$$(Z\in \mathrm{V}\mathrm{a}\mathrm{r}_{\mathcal{P}}^{(1)}\Rightarrow\zeta(Z)\in \mathrm{P}^{(1)})$.

Elements of Valt are called valuations.
We fix a valuation
Valt in the rest of this paper for notational convenience in defining
denotational. I
We define the model $D$ as the least fixed-point model based on the domain and the semantic. That is, we define $D$ as the unique function
conditions (17) $-(22)$ listed in the next.
Definition 22 The mapping
preserves types in the sensethat$\overline{\zeta}\in$$\mathrm{m}\mathrm{o}\mathrm{d}\mathrm{e}1_{8}$$\mathrm{P}$$\mathrm{o}\mathrm{p}\mathrm{e}\mathrm{r}\mathrm{a}\mathrm{t}\mathrm{i}\mathrm{o}\mathrm{n}8\overline{\mathrm{o}_{\mathrm{P}}}$$D\in \mathcal{L}^{*}arrow([\mathrm{V}\mathrm{a}\mathrm{l}\mathrm{t}arrow \mathrm{P}]\cup[\mathrm{V}\mathrm{a}\mathrm{l}\mathrm{t}arrow \mathrm{P}^{(1)}])$$\mathrm{s}\mathrm{a}\mathrm{t}\mathrm{i}\mathrm{s}\theta \mathrm{i}\mathrm{n}\mathrm{g}$$\mathrm{d}\mathrm{e}\mathrm{f}\mathrm{i}\dot{\mathrm{m}}\mathrm{t}\mathrm{i}_{0}\mathrm{n}$$D:\mathcal{L}^{*}arrow([\mathrm{V}\mathrm{a}\mathrm{l}\mathrm{t}arrow \mathrm{P}]\cup[\mathrm{v}_{\mathrm{a}}1\mathrm{t}arrow \mathrm{P}^{(1)}])$$\forall S\in \mathcal{L}[D\mathbb{I}S\mathrm{I}\in[\mathrm{V}\mathrm{a}\mathrm{l}\mathrm{t}arrow \mathrm{P}]]$and satisfies the
(i)

A

(17)

$\forall T\in \mathcal{L}^{(1)}[D[\mathrm{m}\in[\mathrm{V}\mathrm{a}\mathrm{l}\mathrm{t}arrow \mathrm{P}^{(1)}]],$

conditions:$\mathrm{f}\mathrm{o}\mathrm{U}_{0}\mathrm{w}\mathrm{i}\mathrm{n}\mathrm{g}$(18)$\forall Z\in \mathrm{V}\mathrm{a}\mathrm{r},\forall\zeta\in \mathrm{V}\mathrm{a}\mathrm{l}\mathrm{t}[D[Z\mathrm{I}(\zeta)=\zeta(Z)].$(ii)$\forall(i,j, k,\ell,m)\in\omega^{5},\forall \mathrm{o}\mathrm{p}\in \mathrm{F}\mathrm{u}\mathrm{n}_{(i,j,k,\ell_{m}},)$

,

(19)

$\forall\vec{E}\in \mathcal{E}^{i},\forall\tilde{G}\in \mathcal{G}^{j},\forall\vec{H}\in(\mathcal{G}^{(1)})^{k},\forall\tilde{S}\in \mathcal{L}^{\ell},\forall\vec{T}\in(\mathcal{L}(1))m,\forall\zeta\in \mathrm{V}\mathrm{a}\mathrm{l}\mathrm{t}[$.

$D[\mathrm{o}\mathrm{p}(\tilde{E}\cdot\vec{c}\cdot\vec{H}\cdot\tilde{s}\cdot\vec{\tau})\mathrm{I}(\zeta)=\overline{\mathrm{o}\mathrm{p}}([\tilde{E}\mathrm{I}\cdot[\vec{G}\mathrm{I}\cdot \mathbb{I}^{\vec{H}}\mathrm{I}\cdot D\mathrm{I}^{\vec{s}\mathrm{I}}(\zeta)\cdot D\mathbb{I}\tau](())]$

(iii)
(iv)

$\lambda v\in$V.

$D[S\mathrm{J}(\zeta[v/x])$

)

$]$

.

(20)
(21)

$\forall X\in \mathrm{V}\mathrm{a}\mathrm{r}_{P},\forall S\in L[(\mu X. S)\in \mathcal{L}\Rightarrow$$\forall\zeta\in \mathrm{V}\mathrm{a}\mathrm{l}\mathrm{t}$[ (P. $D[0(\zeta[\mathrm{P}/X])$ )A $D$ [ $(\mu X$ .
$\lambda p\in$$\in[\mathrm{P}arrow \mathrm{P}]$$S)\mathrm{I}(\zeta)=\mathrm{Y}(\lambda p\in$(v)($\forall x\in \mathrm{V}\mathrm{a}\mathrm{r}_{\mathcal{V}},\forall S\in \mathcal{L},\forall\zeta\in \mathrm{V}\mathrm{a}\mathrm{l}\mathrm{t}[D[(\lambda X. S)\mathrm{I}(\zeta)=$$\forall\xi\in \mathrm{V}\mathrm{a}\mathrm{r}_{p}(1),\forall T\in \mathcal{L}(1)[(\mu\xi.

$D\mathbb{I}(\mu\xi.

For every closed statement
Proposition 9$\forall s\in \mathcal{L}[\emptyset],\forall\zeta_{0},$(22)T)\in \mathcal{L}^{(1)}\Rightarrow$$\forall\zeta\in \mathrm{V}\mathrm{a}\mathrm{l}\mathrm{t}[(\lambda\pi\in \mathrm{p}(1).

A

P. $D[0(\zeta[\mathrm{P}/X]))$ ]].

D[\mathrm{r}(\zeta[\pi/\xi]))\in[\mathrm{p}(1)arrow \mathrm{P}^{(1)}]$\tau)\mathrm{I}(\zeta)=\mathrm{Y}(\lambda\pi\in \mathrm{P}(1).

$s\in \mathcal{L}[\emptyset]$, the value$D[S\mathrm{J}(()$

D[\mathrm{r}(\zeta[\pi/\xi]))$

$]]$

.1

does not depend on .
$\zeta$$(_{1}\in \mathrm{V}\mathrm{a}\mathrm{l}\mathrm{t}[D[S1(\zeta 0)=D\mathbb{I}s\mathrm{J}(\zeta_{1})]$. I

Notation 2 In the rest of this paper, we simply writeforto denote the value; thus the notation
denote either an element ofor an element of depending on thecontext. We will write
to explicitly denote an element ofwhen it is necessary. 1
The model is compositional in the sense that for any two statements
andwith the same
meaning in $D,$ in an arbitrary context can be replaced by without changing the overall meaning.
Namely, we have the following proposition.
Proposition 10$D[s\mathrm{J}$$\mathrm{P}$$D[s\mathrm{J}$$s\in \mathcal{L}[\emptyset]$$D[s\mathrm{J}(\cdot)$$(\mathrm{v}_{\mathrm{a}}1\mathrm{t}arrow \mathrm{P})$$D$$s_{0}$$s_{0}$$\forall X\in \mathrm{v}_{\mathrm{a}}\mathrm{r}p,\forall x\in \mathcal{L}[X],\forall S0,$$s_{0}$$s_{1}$$S1\in \mathcal{L}[\emptyset][D[s\mathrm{o}\mathrm{I}=D[s_{1}\mathrm{J}\Rightarrow D[S[s_{0}/X]\mathbb{I}=D[S[s1/x]\mathrm{I}]$Proof. We can prove that the following holds for every
Valt,
From this the claim (23) immediately follows.
$\forall\zeta\in$$D\beta s\mathrm{I}(\overline{\zeta})\in$$\mathrm{P}$$(\mathrm{V}\mathrm{a}\mathrm{l}\mathrm{t}arrow \mathrm{P})$$S\in \mathcal{L}[X]$$\forall s\in L[\emptyset][D[S[S/X]\mathrm{I}=D[S\mathrm{J}(\zeta[D[s\mathrm{I}/X])].$$\blacksquare$

.

(23)

by induction on the structure of :
$S$

(24)

42

Auxiliary Denotational Models

5.5

and

$D_{\tau}$$\mathcal{M}_{\tau}$

In order to relate the denotational model $D$ and the operational model , we introduce two auxiliary
andare strong denotational models based on. The models
anddenotational models,
respectively.
and the cms
the cpo$O$$D_{\tau}$$D_{\tau}$$\mathcal{M}_{\tau}$$(\mathrm{P},\tilde{d})$$(\mathrm{P}, \subseteq_{\mathrm{S}})$The Strong Order-Theoretic Model

5.5.1$\mathcal{M}_{\tau}$$D_{\tau}$, but in terms
is defined just as on the basis of the cpo
The strong order-theoretic model
is defined as theinstead of the weak versions. That is,of the original semantic operations
satisfying conditions (17) $-(22)$ with $D$
unique function, respectively.
replaced byandhas the following property corresponding to Proposition9 for $D$ .
The model. I
Proposition 11. as well as for $D$ .
We will use the notational convention in Notation2 for$D$$D_{\tau}$$(\mathrm{P}, \subset_{\mathrm{s}})$$D_{\tau}$$\overline{\mathrm{o}\mathrm{p}}$$D_{\tau}\in \mathcal{L}^{*}arrow([\mathrm{V}\mathrm{a}\mathrm{l}\mathrm{t}arrow \mathrm{P}]\mathrm{U}[\mathrm{V}\mathrm{a}\mathrm{l}\mathrm{t}arrow \mathrm{P}^{(1})])$$D_{\tau}\overline{\mathrm{o}\mathrm{p}}$$\overline{\mathrm{o}\mathrm{p}}$$D_{\tau}$$\forall s\in \mathcal{L}[\emptyset],\forall\zeta 0,$ $\zeta_{1}\in \mathrm{V}\mathrm{a}\mathrm{l}\mathrm{t}[D_{\tau}[s](\zeta_{0})=D_{\tau}\mathbb{I}S\mathrm{J}(\zeta_{1})]$$D_{\tau}$

5.5.2

The Metric Model$\mathcal{M}_{\tau}$

and in terms of the semantic operations
on the basis of the cms
We define the metric model
is defined as the unique function. More precisely,:
satisfying conditions (25) $-(30)$ listed in the next definition.
preserves types in the:
Deflnition 23 he mapping
sense that
(25),
A
and satisfies the following conditions:$(\mathrm{P},\tilde{d})$$\mathcal{M}_{\tau}$$\mathcal{M}_{\tau}$$\overline{\mathrm{o}\mathrm{p}}(\mathrm{o}\mathrm{p}\in \mathrm{F}\mathrm{u}\mathrm{n})$$\mathcal{M}_{\tau}$$L^{*}arrow((\mathrm{V}\mathrm{a}\mathrm{l}\mathrm{t}arrow^{1}\mathrm{P})\cup(\mathrm{V}\mathrm{a}\mathrm{l}\mathrm{t}arrow 1\mathrm{p}^{(1)}))$

T.

$\mathcal{L}^{*}arrow((\mathrm{V}\mathrm{a}\mathrm{l}\mathrm{t}arrow^{1}\mathrm{P})\cup(\mathrm{V}\mathrm{a}\mathrm{l}\mathrm{t}arrow^{1}\mathrm{P}^{(1)}))$$\mathcal{M}_{\tau}$$\forall T\in \mathcal{L}^{(1)}[M[S\mathrm{J}\in(\mathrm{V}\mathrm{a}\mathrm{l}\mathrm{t}arrow(1)\mathrm{p}^{(}1))]$$\forall S\in L[M[S\mathrm{J}\in(\mathrm{V}\mathrm{a}\mathrm{l}\mathrm{t}arrow^{1}\mathrm{P})]$

(i)

(26)

$\forall Z\in \mathrm{V}\mathrm{a}\mathrm{r},\forall\zeta\in \mathrm{V}\mathrm{a}\mathrm{l}\mathrm{t}[\mathcal{M}_{\tau}[Z\mathrm{J}(\zeta)=\zeta(Z)].$(ii)$\forall(i,j, k,\ell,m)\in\omega^{5},\forall \mathrm{o}\mathrm{p}\in \mathrm{F}\mathrm{u}\mathrm{n}_{(t,m)}i_{\dot{\theta}^{k}},,$

(27)

,

$\forall\vec{E}\in \mathcal{E}^{i},\forall\tilde{G}\in \mathcal{G}^{j},\forall\tilde{H}\in(\mathcal{G}^{(1)})k,\forall\vec{S}\in c\ell,\forall\tilde{T}\in(\mathcal{L}(1))^{m},\forall\zeta\in \mathrm{V}\mathrm{a}\mathrm{l}\mathrm{t}[$$\mathcal{M}_{\tau}\beta 0_{\mathrm{P}()\mathrm{J}}\tilde{E}\cdot\tilde{c}\cdot\vec{H}\cdot\tilde{s}\cdot\vec{\tau}(\zeta)=\overline{\mathrm{o}\mathrm{p}}([\tilde{E}\mathrm{J}\cdot[\tilde{G}\mathrm{J}\cdot[\tilde{H}\mathrm{I}\cdot \mathcal{M}_{\mathcal{T}}\mathbb{I}^{\vec{s}_{\mathrm{I}(}}\zeta)\cdot \mathcal{M}_{\mathcal{T}}\mathbb{I}\tau \mathrm{I}(\zeta))]$(iii)$\forall x\in \mathrm{V}\mathrm{a}\mathrm{r}_{\mathcal{V}},\forall S\in L,\forall\zeta\in \mathrm{V}\mathrm{a}\mathrm{l}\mathrm{t}$$\mathcal{M}_{\tau}$

(iv)

[

$(\lambda x$.

$S)\mathrm{J}(\zeta)=(\lambda v\in$

V.

(28)

[
$\mathcal{M}_{\tau}\mathbb{I}S\mathrm{J}(\zeta[v/x]))$

].
(29)

$\forall X\in \mathrm{V}\mathrm{a}\mathrm{r}_{\mathcal{P}},\forall S\in \mathcal{L}[(\mu X. S)\in L\Rightarrow$$\forall\zeta\in \mathrm{V}\mathrm{a}\mathrm{l}\mathrm{t}[(\lambda p\in \mathrm{P}.

A

(v)

.

\mathcal{M}_{\tau}\mathbb{I}s\mathrm{J}(\zeta[p/X]))\in(\mathrm{p}arrow^{1/2}\mathrm{P})$($\mathcal{M}_{\tau}\mathbb{I}(\mu X. S)\mathrm{I}(\zeta)=\mathrm{f}\mathrm{i}\mathrm{x}$[$\forall\xi\in \mathrm{V}\mathrm{a}\mathrm{r}_{\mathcal{P}}^{(1)},\forall\tau\in \mathcal{L}^{(1)}$$(\mu\xi.

$\lambda p\in$$\mathcal{M}_{\tau}[\mathrm{m}(\zeta[p/X])$

)

$]]$

.
(30)

T)\in \mathcal{L}^{(1)}\Rightarrow$$\forall\zeta\in \mathrm{V}\mathrm{a}\mathrm{l}\mathrm{t}[(\lambda\pi\in \mathrm{p}(1).

\mathcal{M}_{\mathcal{T}}[\mathrm{r}(\zeta[\pi/\xi]))\in(^{\mathrm{p}(1)}arrow/2\mathrm{P}1(1))$.

.1
has the following property corresponding to Proposition9 forA$\mathcal{M}_{\mathcal{T}}\beta(\mu\xi.

T)\mathrm{I}(\zeta)=\mathrm{f}\mathrm{i}\mathrm{x}(\lambda\pi\in \mathrm{P}^{(1})$

The model
Proposition 12
forIn the rest of this aper, we simply write
will use the notational convention in Notation2 for$\mathcal{M}_{\tau}$P.

$\mathcal{M}\tau \mathbb{I}\mathrm{r}(\zeta[\pi/\xi]))$

$]]$

$D$

.

. I

$\forall s\in \mathcal{L}[\emptyset],\forall\zeta 0,\zeta_{1}\in \mathrm{V}\mathrm{a}\mathrm{l}\mathrm{t}\mathrm{l}\mathcal{M}\mathcal{T}\mathbb{I}S\mathrm{I}(\zeta 0)=\mathcal{M}\tau[S1((1)]$$\dot{\mathrm{p}}$$\mathcal{M}_{\tau}[s]$$\mathcal{M}_{\tau}$

6

to denote the value. as well as for $D$ and .

$s\in \mathcal{L}[\emptyset]$$\mathcal{M}_{\tau}\mathbb{I}S1(\overline{\zeta})\in \mathrm{P}$; We$D_{\tau}$

Fhll Abstractness of $D$ with respect to$\mathcal{O}$In this section, we investigate the relationship between the denotational model $D$ and the operationalmodel , and thereby establish the full abstractness of with respect to . For relating the twoand ; these models are defined operationallymodels $D$ and , we introduce two auxiliary models
models.
and called the intermediate$O$$\mathcal{D}$$\mathrm{O}$$\mathrm{O}$$C_{\tau}$

$C$

43

6.1

Intermediate Models$C_{\tau}$

and

$C$

In this subsection, we define two intermediate models
weak. First, we define the strong intermediate model

Deflnition 24 (Strong Operational Modeland, we putis satisfied:(i)[A$s\in \mathcal{L}[\emptyset]$$q\in(\mathrm{C}_{\mathcal{T}})^{\omega}$A$\exists c\in\wp(\mathrm{C})$$qarrow w$$C$) We define:, if either of$C_{\tau}$$q=w\cdot\langle C\rangle$$L[\emptyset]arrow\wp(\mathrm{C}_{\tau}\triangleright\wp(\mathrm{C})_{1})$th.e$q\in C_{\tau}[s]$$q\in(\mathrm{C}_{\tau}\triangleright\wp(\mathrm{C})_{1})$$\exists w\in(\mathrm{C}_{\tau})^{<}\omega,$(ii)$C_{\tau}$

and ; the former is strong and the latter isby:$C_{\tau}$$C_{\tau}$following two

as follows: Forand (ii)$\mathrm{c}.\mathrm{o}\mathrm{n}\mathrm{d}\mathrm{i}\mathrm{t}\mathrm{i}_{\mathrm{o}\mathrm{n}\mathrm{S}}(\mathrm{i})$A act $(s’)\cap(C\cup\{\tau\})=\emptyset$ ]].

$\exists s’\in \mathcal{L}[\emptyset][S\Rightarrow s^{J}w$.1

For convenience in relatingwithin Sect. 6.3, we give an altemative characterization ofas the unique fixed-point of a higher-order contraction defined by:$C_{\tau}$$\mathcal{M}_{\tau}$$C_{\tau}$$\Psi$

Deflnition 25 Let
The mapping :$\mathrm{M}--(\mathcal{L}[\emptyset]arrow \mathrm{P})$$\Psi(F)(S)=${$\langle C\rangle|C\in\wp(\mathrm{C})$$\cup\cup$

where

$s$

ranges over{. Clearly

is defined as$\mathrm{M}arrow \mathrm{M}$$\Psi$

A

is a cms with the pointwise metric induced by .
$\Psi(F)$ is the mapping defined by: For every$\mathrm{M}$$F\in \mathrm{M},$

}

(31)

$(C\cup\{\tau\})\cap \mathrm{a}\mathrm{C}\mathrm{t}(s)=\emptyset$

A $sarrow s’$ } ,$a$$\langle a\rangle\cdot F(s)’|a\in \mathrm{C}_{\tau}\wedge s’\in \mathcal{L}[\emptyset]$$\mathcal{L}[\emptyset]$. I

It is easy to check that is a contraction fromis a fixed-point of , i.e., that$\Psi$$C_{\tau}$$\overline{d}$$\mathrm{f}\mathrm{o}\mathrm{U}\mathrm{o}\mathrm{w}\mathrm{s}$$\Psi$

to M. From the definition of. Thus we have:$\mathrm{M}$$C_{\tau}$, it follows that$\forall u\in \mathcal{L}^{*}[\emptyset][\Psi(c_{\tau})(u)=C_{\tau}\mathbb{I}u\mathrm{I}]$

Proposition 13 (Alternative Characterization of,$C_{\tau}$

One has)$C_{\tau}=\mathrm{f}\mathrm{i}\mathrm{x}(\Psi)$. That is, for every$s\in$$\mathcal{L}[\emptyset]$$C_{\tau}[S1=${$\langle C\rangle|C\in\wp(\mathrm{C})$$\cup\cup$

From$C_{\tau}${}$C:\mathcal{L}[\emptyset]arrow \mathrm{P}$Completeness of

$C$

(32)

$(C\cup\{\tau\})\cap \mathrm{a}\mathrm{c}\mathrm{t}(s)=\emptyset$A

A $sarrow s’$ } . I$a$$s’\in L[\emptyset]$, the weak intermediate model

Definition 26 We define

6.2

A$\langle a\rangle\cdot C\tau[S’\mathrm{J}|a\in \mathrm{C}_{r}$$C$

is defined by applying the hiding function

as follows: Forwith respect to$s\in \mathcal{L}[\emptyset]$, let$C[s\mathrm{J}=\mathcal{H}(c_{\tau}\mathrm{I}s1)$ational model

:

.I

$O$

. In this subsection, we investigate the relationship between the intermediate model$O$$\mathcal{H}$, and thereby establish a relationship called the completeness of$C$and the operwith respect to$C$O.
First, we need a few preliminary definitions.

, let$\tilde{\mathcal{F}}(p)=p\mathrm{n}^{\mathrm{n}}\mathrm{D}\mathrm{e}\mathrm{f}\mathrm{i}\mathrm{n}\mathrm{i}\mathrm{t}\mathrm{i}\mathrm{o}27\mathrm{F}_{\mathrm{o}\mathrm{r}p\wp(}((\mathrm{c}\mathcal{T})^{<}\omega.

, and$\tilde{\mathcal{T}}_{\perp}(p)=p\cap((\mathrm{C}_{\tau})^{<\omega}\cdot\{\langle\perp\rangle\}),\overline{\mathcal{T}}_{\omega}(p)=p\cap(\mathrm{C}_{\tau}.)^{\omega}$\wp(\mathrm{c}\in)).\mathrm{I}\mathrm{c}_{\tau}\triangleright\wp(\mathrm{C})_{\perp})$

Deflnition 28 We define an abstraction function $A$ :
For
, let

$\wp(\mathrm{C}_{\tau}\triangleright\wp(\mathrm{C})\perp)arrow\wp(\mathrm{C}_{\mathcal{T}}\triangleright\{\delta, \perp\})$$A(p)=\overline{\mathcal{T}}_{\perp}(p)\cup\tilde{\mathcal{T}}_{\omega}(p)\cup\{w\cdot\langle\delta\rangle|w\cdot\langle \mathrm{C}\rangle\in p\}$$p\in\wp(\mathrm{C}_{\mathcal{T}}\triangleright\wp(\mathrm{C})\perp)$

We immediately obtain the following connection between
and $A$ :Proposition 14$\forall s\in \mathcal{L}[\mathrm{o}][O[S\mathrm{I}=A(C[s\mathrm{I})]$

Moreover, the model$C$.

$s_{0}$$\mathrm{O}$$s_{0},$ $s_{1}\in L[\emptyset]$$C[s\mathrm{o}\mathrm{J}\neq c[_{S}1\mathrm{J}\Rightarrow\exists s\in \mathcal{L}\wedge[\emptyset][\mathit{0}[s0||S\wedge \mathrm{J}\neq \mathit{0}[_{S_{1}}||_{S}^{\wedge}\mathrm{I}]$Proof. Suppose V is infinite. And let. It suffices to show that

and

$C$

as follows:, from the definitions of $O,$

$C$

,

$1$

is complete with respect toLemma 3 Let V is infinite. Then for every

$O$

.I

and

$s_{1}$

in the following sense:, one has. I(33)be programs such that

$C[s_{0}\mathrm{I}\neq C[s_{1}\mathrm{J}$. We fix$X\in \mathrm{V}\mathrm{a}\mathrm{r}_{P}$$\exists S\in \mathcal{L}[X][\mathit{0}[s[s\mathrm{o}/X]\mathrm{I}\neq O[S[S0/X]\mathrm{J}]$Since$C[s\mathrm{o}\mathrm{J}\neq C[s_{1}\mathrm{J}$.

, one of the three conditions (35)(34)$(\mathrm{i}),$(35)$(\mathrm{i}\mathrm{i})$, or (35)$(\mathrm{i}\mathrm{i}\mathrm{i})$holds:

44(i), (ii)$\tilde{\mathcal{T}}_{\perp}(c\mathbb{I}s\mathrm{o}1)\neq\tilde{\mathcal{T}}_{\perp}(c[s_{1}\mathrm{I})$$\tilde{\mathcal{T}}_{\omega}(C\mathbb{I}s\mathrm{o}\mathrm{J})\neq\tilde{\mathcal{T}}_{\omega}(C[s_{1}1)$, (iii)$\tilde{F}(C\mathrm{Q}s\mathrm{o}1)\neq\tilde{F}(C1s_{1}\mathrm{I})$holds, we immediately obtains (34) by putting
When (35) or (35)holds.
remaining case that (35)andWe can assume without loss of generality that there exist$(\mathrm{i})$$S\equiv X$$(\mathrm{i}\mathrm{i})$

.

(35)

. Let us consider the$(\mathrm{i}\mathrm{i}\mathrm{i})$$w\in \mathrm{C}^{<\omega}$(i)$w\cdot\langle C\rangle\in c\mathbb{I}^{s_{0}}1$, (ii)$C\in\wp(\mathrm{C})$such that(36)$w\cdot\langle C\rangle\not\in C[s_{1}\mathrm{I}\cdot$.
Let us put, then we haveA
If there exists $w’\preceq w$ such that, and therefore this case is reduced to the case that (35) holds. Thus it suffices to consider
the case that$w=\langle c0, \ldots,c_{k}\rangle$$w’\cdot\langle\perp\rangle\not\in\tilde{\mathcal{T}}_{1}(C[s\mathrm{o}\mathrm{I})$$w’\cdot\langle\perp\rangle\in\tilde{\mathcal{T}}(C[s_{1}\mathrm{I})$$\tilde{\mathcal{T}}_{\perp}(c\mathbb{I}s_{0}\mathrm{I})$$\neg\exists w’\preceq w[w\cdot(’\perp\rangle\in\tilde{\mathcal{T}}_{\perp(}c\beta_{S}1\mathrm{J})]$

Then, we can construct a set(i)) , (ii)$\tilde{w}\in \mathrm{C}^{<\omega}$

.

(37)

$\tilde{C}\in\wp(\mathrm{C})$and a program$\wedge s$such that(38)$\langle\delta\rangle\in 0\mathbb{I}\partial_{\overline{C}(}S1||s)\wedge \mathrm{I}$$\langle\delta\rangle\in O[\partial_{\overline{c}^{(1}\mathrm{I}}s0|s\wedge$

as follows. First, we put
and, where we define{$\mathrm{c}\mathrm{h}\mathrm{a}\mathrm{n}(c)|c\in \mathrm{C}$We fix an element$\overline{v}\in \mathrm{V}$A

A$\exists s’[\tilde{s}\Rightarrow s’\tilde{w}$arbitrarily, and let$c\in \mathrm{a}\mathrm{c}\mathrm{t}(s’)$.

$\wedge s_{0}\equiv 0$; (ii) for $i\in\{1, \ldots, k\}$ , let

where we define$f(c,\tilde{s})=\{$$f(c,\tilde{s})$

out
in

, for

and

and

$\tilde{Z}\in(\mathrm{V}\mathrm{a}\mathrm{r}^{*}p)<\omega$

Deflnition 29 For$C$. See Lemma 7 of [21] for details.

$D_{\tau},$$\mathcal{M}_{\tau}$, and$\vec{U}\in(\mathcal{L}^{*})^{<\omega}$$C_{\tau}$

and$\mathcal{M}_{\tau}$$t\in \mathcal{L}^{(1)}[\iota]$, we sayand$\vec{Z}$A$\vec{U}$agree in types if$C_{\tau}[t\mathrm{J}$is a homomorphism from

Lemma 4 For $(i,j, k,t,m)\in\omega^{5}$ and op

by$\mathcal{L}^{*}[\emptyset]$$\mathrm{l}\mathrm{g}\mathrm{t}(\vec{Z})=\mathrm{l}\mathrm{g}\mathrm{t}(\vec{U})$$(\tilde{Z}(i)\in \mathrm{V}\mathrm{a}\mathrm{r}_{P}^{(1)}\Rightarrow\vec{u}(i)\in \mathcal{L}^{(1)})$, we extend the domain of, we define$\blacksquare$$C_{\tau}$$(\tilde{Z}(i)\in \mathrm{V}\mathrm{a}\mathrm{r}_{P}\Rightarrow\tilde{u}(i)\in \mathcal{L})$In order to relate

The model, by

if $c=(v!, v’)$ ,if $c=(v?,v’)$ .

x=v’), (\lambda x.\tilde{s}))$$\partial_{\overline{C}}(s_{1}||s)\wedge$

Equivalence of[$\tilde{s}\in L[\emptyset]$. Then, we can prove (38) by an operational analysis of the behaviors of the two$\partial_{\overline{C}}(s\mathrm{o}||s\wedge)$$\forall i\in 1\mathrm{g}\mathrm{t}(\vec{Z})$and,$\wedge s_{i}\equiv \mathrm{o}\mathrm{u}\mathrm{t}(\overline{v}1,\overline{v}, 0)+f(\overline{c_{k-i}},s\wedge)i-1$$(v,v\tilde{s})’,$$(v, (\lambda x.

$s\wedge\equiv\wedge s_{k}$$c\in \mathrm{C}$and (37); seeby the following clauses:$\mathrm{f}\mathrm{o}\mathrm{U}\mathrm{o}\mathrm{w}\mathrm{s}\mathrm{h}\mathrm{o}\mathrm{m}(36)(\mathrm{i})$$\wedge..\wedge s_{0},.,S_{k}$For$\tilde{s}\in L[\emptyset]$]}.

(The nonemptiness of the right-hand set bf the above formula
Proposition22 of [21] for the proof.) We inductively define

6.3

, for

be an element of V such that$\overline{v}_{1}$$\overline{v}_{1}!\in(\mathrm{V}!\backslash ,\cup w\preceq w\dot{l}\in\cup(S(si,w)’\cup 2.\overline{S(si,w’)})$

And we put
programs$S(\tilde{s},\tilde{w})$$\tilde{C}=,\bigcup_{w\preceq w}(A(s0,w’)\cup A(\mathit{8}_{1}, w)’)\backslash C$, by$S(\tilde{s},\tilde{w})=$(i)$w’\cdot\langle\perp\rangle\in$$(\mathrm{i})$$c_{\tau}\mathbb{I}t\mathrm{I}=$to$\mathrm{p}*$($C_{\tau}$

from$\lambda v\in$V.

$\mathcal{L}[\emptyset]$to$\in \mathrm{F}\mathrm{u}\mathrm{n}_{(ik,l,m)}\dot{o},$$c_{\tau}\mathrm{I}^{0_{\mathrm{P}}}(^{\sim}e\cdot\tilde{g}\cdot\tilde{h}\cdot st)arrow\cdotarrow \mathrm{I}=\overline{\mathrm{o}\mathrm{p}}([^{arrow\cdot\tilde{h}}e\vec{g}\cdot \mathrm{I}\cdot c_{\tau}\mathrm{I}^{arrow\vee}S\cdot t\mathrm{J})]$

This lemma follows from the definition of the operations
in $[17, 19]$ . See Lemma 8 of [21] for the proof.
$C_{\tau}$

Lemma 5 For every

and$\mathcal{M}_{\tau}$$U\in \mathcal{L}^{*}$$\mathrm{F}\mathrm{V}(U)\subseteq \mathrm{V}\mathrm{a}\mathrm{r}_{P}^{*}$). I, one has.I$\overline{\mathrm{o}\mathrm{p}}$(39)

by applying the general method described

are equivalent in the following sense:

with$v)\mathrm{J}$as follows.

in the following sense:$\forall e\in(arrow \mathcal{E}[\emptyset])i,\forall\tilde{g}\in(\mathcal{G}[\emptyset])^{j},\forall\vec{h}\in(\mathcal{G}^{(1)}[\mathrm{o}])^{k},\forall s\in(\vee c[\mathfrak{a}_{])^{\ell},t^{arrow}}\forall\in(\mathcal{L}^{(1)}[\emptyset])^{m}[$The two models].

$\mathcal{L}^{*}[\emptyset]$$c_{\tau}1^{\mathrm{a}}\mathrm{p}(t,$and, one has

45[$\forall\vec{Z}\in(\mathrm{V}\mathrm{a}\mathrm{r}_{\mathcal{P}}^{*})^{<\omega},\forall\vec{u}\in(\mathcal{L}^{*}[\emptyset])^{<\omega}$$\mathrm{F}\mathrm{v}(U)\subseteq \mathrm{r}\mathrm{a}\mathrm{n}(\tilde{Z})\wedge\tilde{Z}$and$\tilde{u}$.1agree in types(40)$\Rightarrow\forall\zeta\in \mathrm{V}\mathrm{a}\mathrm{l}\mathrm{t}[c_{\mathcal{T}}[U1\tilde{u}/\vec{z}]\mathrm{I}=\mathcal{M}_{\tau}\# U1(\zeta[c_{\tau}[\vec{u}\mathrm{J}/\vec{Z}]) ]]$Proof. The claim (40) can be proved by induction on the structure ofproperties (25) $-(30)$ of. See Lemma 9 of [21] for the proof.
$\mathcal{M}_{\tau}$$U\in \mathcal{L}^{*}$, using Lemma4 and$\blacksquare$

From Lemma5, we inlmediately obtain the next corollary.
Corollary 2.I$\forall s\in \mathcal{L}[\emptyset][c_{\tau}\mathrm{I}^{s1}=\mathcal{M}_{\tau}[s]]$Although the respective underlyingofandare different, the meanin of eachprogram underis equal to its meanin under.
Lemma 6
. I
Proof. This can be proved by induction on the structure of $U\in L^{*}$ , using properties (25) $-(30)$ of
and the corresponding properties of.
$D_{\tau}$$\mathcal{M}_{\tau}$$\mathrm{s}\mathrm{t}\mathrm{r}\mathrm{u}\mathrm{c}\mathrm{t}\mathrm{u},\mathrm{r}\mathrm{e}\mathrm{s}$$\mathrm{g}$$\mathcal{M}_{\tau}$$D_{\tau}$$\mathrm{g}$$\forall U\in \mathcal{L}^{*},\forall\zeta\in \mathrm{V}\mathrm{a}\mathrm{l}\mathrm{t}[\mathcal{M}_{\mathcal{T}}\mathrm{I}U1(\zeta)=D_{\tau}[U\mathrm{I}(\zeta)]$$\mathcal{M}_{\tau}$$D_{\tau}$$\blacksquare$

bom Lemma6, we immediately obtain the following
Corollary 3$\forall s\in c[\emptyset][\mathcal{M}\tau \mathrm{I}S]=D_{\tau}[s]]$From Corollary4, Lemma6, andProposition 15

Relationship between $D$ and.

.I$\mathrm{C}_{\mathrm{o}\mathrm{r}}\mathrm{o}\mathrm{u}\mathrm{a}\mathrm{r}\mathrm{y}3$$\forall s\in \mathcal{L}[\emptyset][c[S\mathrm{I}=D[s]]$6.4$\mathrm{C}\mathrm{o}\mathrm{r}\mathrm{o}\mathrm{u}_{\mathrm{a}}\mathrm{r}\mathrm{y}$, we obtain the following proposition.

.I$D_{\tau}$

The denotational model $D$ can be represented as the composition ofand the hiding function ;this is the claim of Lemma7 below. Since the two modek $D$ andare defned independently, thisrelation does not follow immediately, and we need a few prehiminanies.
$D_{\tau}$$\mathcal{H}$$D_{\tau}$

6.4.1

Hiding as a Homomorphism

We extend the domain ofDeflnition 30 For$\mathcal{H}$to (V$\cup \mathrm{B}^{(*)}\cup \mathrm{P}^{(*)}$$z\in(\mathrm{V}\cup \mathrm{B}^{*}\cup \mathrm{P}^{(*)})$$z$$\mathcal{H}(z)=\{$$\mathcal{H}(z)$$\mathcal{H}\circ z=(\lambda v\in \mathrm{V}.

For$n\in\omega$and\mathcal{H}(z(v)))$$z\sim\in(\mathrm{V}\cup \mathrm{B}^{(*)}\cup \mathrm{P}^{(*)})^{n}$

The hiding function) as follows:

, let
if
if
if

$z\in \mathrm{V}\cup \mathrm{B}^{(*}$$z\in \mathrm{P}$,$z\in \mathrm{P}^{(1)}$, we write$\mathcal{H}(z^{arrow})$),.

to denote ($\mathcal{H}(\vec{z}(i))\rangle_{\dot{l}}\in n\cdot$Iis a homomorphism in the following sense:$(i,j,
k,\ell,m)\in\omega^{5}$
Lemma 7 For
and op), one has$\mathcal{H}$$\in \mathrm{F}\mathrm{u}\mathrm{n}_{(1\dot{o},k}.,\ell,m$$\forall\tilde{v}\in \mathrm{V}^{i},\forall barrow\in \mathrm{B}^{j},\forall\vec{\beta}\in(\mathrm{B}^{(1)})k,\forall\tilde{p}\in \mathrm{P}^{\ell},\forall\vec{\pi}\in(\mathrm{P}^{(1)})^{m}[$

(41)

.I

$\mathcal{H}(_{\overline{\mathrm{O}}}\mathrm{p}(\tilde{v}\cdot b\cdot\vec{\beta}arrow\cdot\tilde{p}\cdot\tilde{\pi}))=\overline{\mathrm{o}\mathrm{p}}(\mathcal{H}(\vec{v}\cdot b\cdot\vec{\beta}\cdot\vec{p}\cdot\vec{\pi}\sim))]$

Proof. It is easy to check that (41) holds, except for the recursively defined operations and.
For these operations, we first prove (41) for finite processes by induction on their length, and thereby
prove (41) for infinite processes (see Propositions6.16 and 6.19 of [18, Chapter6]).
$\sim||$$\tilde{\partial}_{C}$$\blacksquare$

6.4.2

Relationship between

The two models$D_{\tau}$

and $D$and $D$ are related by means of the hiding function, one hasLemma 8 For every$D_{r}$$U\in \mathcal{L}^{*}$$\mathcal{H}$

as

.
. I

$\mathrm{f}\mathrm{o}\mathrm{U}\mathrm{o}\mathrm{W}\mathrm{s}$$\forall\zeta\in \mathrm{V}\mathrm{a}\mathrm{l}\mathrm{t}[\mathcal{H}(D_{\tau}[U\mathrm{I}(\zeta))=D[U\mathrm{I}(\mathcal{H}\mathrm{Q}\zeta)]$

Proof. This lemma can be established by induction on the structure of, using the continuityof and the fact that is a homomorphism (Lemma7). See Lemma6 of [21] for details.
$U\in \mathcal{L}^{*}$$\mathcal{H}$$\mathcal{H}$$\blacksquare$

The next corollary immediately follows from Lemma8:

Corollary 4$\forall s\in \mathcal{L}[D[s\mathrm{J}=\mathcal{H}(D_{\tau}[s])]$

.I

46

Full Abstractness of

6.5

$D$

with respect to$\mathrm{O}$

By combining the result established in the previous section, we can now prove the main result of ourpaper, the full abstractness of with respect to .
, one has
Theorem 1 Let V is infinite. Then for every[ $O[S1^{s_{0}}/X]\mathrm{I}=O[s[s_{1}/X]\mathrm{J}]$. I(42)
$O$

$D$

$s_{0},$$s_{1}\in \mathcal{L}[\emptyset]$$D[s\mathrm{o}\mathrm{J}=D[s_{1}\mathrm{J}\Leftrightarrow\forall X\in \mathrm{V}\mathrm{a}\mathrm{r}_{P},\forall S\in \mathcal{L}[X]$

Proof. Let
Suppose that$s_{0},$$s_{1}\in \mathcal{L}[\emptyset]$$(\Rightarrow)$. We will prove (42).

$(*):D[s\mathrm{o}\mathrm{J}=D[s\mathrm{o}\mathrm{I}\cdot$

Let$X\in \mathrm{V}\mathrm{a}\mathrm{r}_{P}$Thus we obtain
To prove$\mathrm{t}\mathrm{h}\mathrm{e}\Rightarrow$(by$(\Leftarrow)$$(*)$$S\in \mathcal{L}[X]$. We have(by Proposition 15)(by Proposition 14)$=A(C[s[s_{1}/s]\mathrm{J})=\mathit{0}[S[s_{1}/S]\mathrm{I}\cdot$
Proposition10)
and$=A(D\mathbb{I}^{s}[\mathit{8}0/S]\mathrm{I})$$\mathcal{O}[S[S_{0}/S]\mathrm{J}=A(C[S[S\mathrm{o}/S]\mathrm{J})$$=A(D[S[\mathit{8}1/S]\mathrm{I})$and-part of (42).
-part of (42), it suffices to prove its contrapositive:$\mathrm{t}\mathrm{h}\mathrm{e}\Leftarrow$(43)$D[s\mathrm{o}1\neq D[s_{1}\mathrm{J}\Rightarrow\exists X\in \mathrm{V}\mathrm{a}\mathrm{r}_{\mathcal{P}}, \exists S\in L[X][0[S[S0/X]\mathrm{J}\neq \mathrm{O}[S[s_{1}/X]\mathrm{J}].$. Thus, by Lemma 3,
Then, by Proposition15, we have
Suppose thatwith $X$ being an
Therefore, by putting
such that
there exists-part. Thus we obtain (43), and therefore]
arbitrary variable, we haveof (42) .
$C[s_{0}\mathrm{J}\neq C[s_{1}\mathrm{J}$$D\mathbb{I}s\mathrm{o}\mathrm{I}\neq \mathcal{D}[s_{1}\mathrm{I}\cdot$$\wedge s\in L[\emptyset]$$0\mathbb{I}^{s}0||s\wedge \mathrm{I}\neq \mathcal{O}[s_{1}||S\mathrm{I}\wedge.$$\mathit{0}\mathbb{I}^{S}1S_{0}/X$$S\equiv(X||s\wedge)$$\mathrm{t}\mathrm{h}\mathrm{e}\Leftarrow$$\mathrm{J}\neq \mathrm{O}[S[s_{1}/x]\mathrm{I}$$\blacksquare$

7

Concluding Remarks

There are two directions for future research.
First, it remains for future study to investigate what we can do withthe following questions:.
.

$\mathrm{C}\mathrm{C}\mathrm{S}++$, e.g., to investigate

concurrent object-oriented model? (Example 3 of [21] suggests
Is it possible to code inthat such a coding will be possible to some extent, by giving a description of a typical client-server)
system in$\mathrm{C}\mathrm{C}\mathrm{S}++\mathrm{a}$$\mathrm{C}\mathrm{C}\mathrm{S}^{++}.$? (Note that, unlike LOTOS [22],Are any (efficient) implementations ofis a programming language in nature with all the features intended to be implementable insome sense; the former is a specification language with several features not intended to be$\mathrm{C}\mathrm{C}\mathrm{S}^{++}$$\mathrm{C}\mathrm{C}\mathrm{S}++\mathrm{p}\mathrm{o}\mathrm{s}\mathrm{s}\mathrm{i}\mathrm{b}\mathrm{l}\mathrm{e}$implemented.)

Another direction for future research is to apply the general scheme described in Sect. 1.1 in order toestablish full abstractness results for more complex languages such as the ones treated in [2, 8, 20, 34]
object(these languages include Ada-style rendezvous, real-time features, shared variables,
orientation). Particularly interesting target is -calculus [29]. In [13], Hennessy provided a kind ofterm model for a version of -calculus, which model is shown to be fully abstract with respect to acertain behavioral criterion based on testing. But the behavioral criterion in [13] is different from ours
based on the weak linear semantics, and domain-theoretic construction of good denotational models
for -calculus remains for future research.
$\mathrm{a}\mathrm{n}\mathrm{d}/\mathrm{o}\mathrm{r}$

$\pi$

$\pi$

$\pi$

A

Appendix

Remark 3 In the proof of a semantic equivalence result, Theorem13.3, of [30], the following proposition (44)is claimed to hold and is used as a crucial intermediate step of the proof (see the end of the second paragraphof [30, page 61] .
(44),
are closed$)$$\forall t\in\omega,\forall n\geq t+1,\forall R_{1},$ $R_{2[}R_{1},$ $R_{2}$$\mathrm{s}\mathrm{t}\mathrm{a}\mathrm{t}\mathrm{e}\mathrm{m}\mathrm{e}\mathrm{n}\mathrm{t}_{\mathrm{S}}\Rightarrow P^{n}(R_{1})\cong_{t}Pn(R2)]$

47

where $P$ is a mapping which maps each statement $R$ to(withbeing an arbitrary statement suchthatis such a modification of Milner’s -nested observation equivalence [27] as takes thenotion of divergence into account (see [30, Sect. 12]). (We haveiff
, where denotes
the possibility of divergence at . And
is defined from, just as Milner’s $(t+1)$ -nested observationequivalence is defined from the -nested observation equivalence.) However, (44) does not hold as is shown
below. Let, and $P$ be the syntactic mapping which maps each statement $R$ to. Then, and therefore,. Thus,we have. If (44) holds for $\ell=1,$ $n=2,$, and, then there must exist a
statementsuch that, but this is clearly impossible. 1(stop) 4$\tilde{P}[R/\xi]$$\mathrm{F}\mathrm{V}(\tilde{P})\subseteq\{\xi\}),$$\tilde{P}$$t$$\mathrm{a}\mathrm{n}\mathrm{d}\cong_{\ell}$$R_{1}\cong_{0}R_{2}$$\epsilon$$\underline{\simeq}_{\ell+1}$$(R_{1}\uparrow\Leftrightarrow R_{2}\uparrow)$$\uparrow$$\underline{\simeq}_{t}$$\ell$$\tilde{P}\equiv c\cdot(\xi\backslash c)$$\tilde{P}[R/\xi]$$P(\mathrm{d}\mathrm{i}\mathrm{v})\equiv C\cdot(\mathrm{d}\mathrm{i}\mathrm{v}\backslash c)-^{c}(\mathrm{d}\mathrm{i}\mathrm{v}\backslash c)\uparrow$$P^{2}(\mathrm{d}\mathrm{i}\mathrm{V})\equiv c\cdot(P(\mathrm{d}\mathrm{i}\mathrm{v})\backslash c)arrow c(P(\mathrm{d}\mathrm{i}\mathrm{v})\backslash c)arrow r(\mathrm{d}\mathrm{i}\mathrm{v}\backslash c)\uparrow$$P^{2}(\mathrm{d}\mathrm{i}\mathrm{V})\mathscr{L}\cdot(\mathrm{d}\mathrm{i}\mathrm{v}\backslash c)\uparrow$$R_{2}’$$P^{2}$$R_{1}\equiv \mathrm{d}\mathrm{i}\mathrm{v}$$R_{2}\equiv \mathrm{s}\mathrm{t}\mathrm{o}\mathrm{p}$$R_{2}’\uparrow$

References[1] E. Astesiano and E. Zucca (1984), Parametric channels via label expressions in CCS, in Theoretical Computer
Science, Vol. 33, pp. 45-63.

[2] J.W. de Bakker and E.P. de Vink (1993), Rendez-vous with metric semantics, New Generation Computing,Vol. 12, No. 1, pp. 53-90.
[3] J.W. de Bakker and J.I. Zucker (1982), Processes and the denotational semantics of concurrency, Infomation
and Control, Vol. 54, pp. 70-120.

[4] J.A. Bergstra, J.W. Klop, and E.-R. Olderog (1987), Failures without chaos: a new process process semantics
for fair abstraction, in Proceedings of IFIP Conference on Formal Description of Programming Concepts III,
Ebberup 1986 (M. Wirsing, ed.), North-Holland, pp. 1134-1177.

[5] J.A. Bergstra, J.W. Klop, and E.-R. Olderog (1988), Readies and failures in the algebra of communicatingprocesses, SIAM J. of Computing Vol. 17, No. \^o, pp. 1134-1177.
[6] S.D. Brookes, C.A.R. Hoare, and A.W. Roscoe (1985), A theory of communicating sequential processes,
Joumal of the Association for Computing Machinery, Vol. 31, pp. 560-599.

[7] S.D. Brookes and A.W. Roscoe (1984), An improved failures model for communicating processes, in Lecture
Notes in Computer Science, Vol. 197, pp. 281-305, Springer, Berlin.
[8] F. van Breugel (1991), Comparative semantics for a real-time programming languages with integration, In
Proceeding of $TAPSoF/CAAP’ \mathit{9}\mathit{1}$ , Lecture Notes in Computer Science, Vol. 493 (S. Abramsky and T.S.E.
Maibaum, eds.), pp. 397-411, Springer, Berlin.

[9] J. Dugundji (1966), Topology, Allyn and Bacon, Boston.
[10] M.H. Goldsmith, A.W. Roscoe, and B.G.O. Scott (1993), Denotational $Sema.nti_{Cs}$ for occam 2, Technical
Monograph PRG-108, Oxford University Computing Laboratory.
[11] C.A. Gunter (1993), Semantics of Programming Languages: Structures and Techniques, MIT Press.

[12] M. Hennessy (1988), Algebraic Theory of Processes, MIT Press.
[13] M. Hennessy (1992), A Model for the. cogs. sussex.
).
$<\mathrm{f}\mathrm{t}\mathrm{p}$$\pi$-Calculus, University of Sussex (obtained by anonymous ftp from$\mathrm{a}\mathrm{c}.\mathrm{u}\mathrm{k}>$[14] M. Hennessy and A. Ing\’ofsd\’ottir (1993), A theory of communicating processes with value passing, Information and Computation Vol107, pp. 202-236.

[15] C.A.R. Hoare (1985), Communicating Sequential Processes, Prentice Hall.
[16] E. Horita (1992), Fully abstract models for communicating processes with respect to weak linear semantics
with divergence, IEICE Transactions on Information and Systems, Vol. E75-D, No. 1, pp. 64-77.
[17] E. Horita (1992), Deriving denotational models fro nonuniform concurrency from structured operationalsemantics, IPSJ Technical Report, Vol. 92, No. 67,, pp. 1-8.
$\mathit{9}\mathit{2}-PRc_{-}\mathit{8}$[18] E. Horita (1993), Fully Abstract Models for Concurrent Languages, Ph.D. thesis, the Free University of
Amsterdam (also appeared as ECL Technical $Report_{j}$ No. 8939).
[19] E. Horita (1994), Deriving failures models for nonuniform concurrency from Structured Operational Semantics, to appear in New Generation Computing.

48[20] E. Horita, J.W. de Bakker, and J.J.M.M. Rutten (1990), $Fuu_{y}$ Abstmct Denotational Models for Nonunifom Concurrent Languages, CWI Report CS-R9027, Amsterdam. (To appear in Infomation and Computation.)[21] E. Horita and F.-J. de Vries (1994), A fully abstraci denoiational model for communicating processes unthlabel-passing, to appear as an ECL Technical Report (a preliminary version was distributed at Workshop on
Concurrency Theory and Its Application, Research Institute of Mathematical Science, Kyoto, July 25-27,
1994).
[22] ISO (1989), Information Processing Systems Open Systems Interconnection –LOTOS– A Fommmal Description Technique based on the Temporal Ordering of Observational Behaviour, Intemmational Standard ISO
–

8807.

[23] J.N. Kok and J.J.M.M. Rutten (1990), Contractions in comparing concurrency semantics, in TheoreticalComputer Science, Vol. 76, pp. 179-222.

[24] J.-J.Ch. Meyer and E.P. de Vink (1990), Application of compactness in the Smyth powerdomain of streams,
Theoretical Computer Science, Vol. 57, pp. 251-282.
[25] J.-J.Ch. Meyer and E.-R. Olderog (1990), Hiding in stream semantics of uniform concurrency, Acta Informatica, Vol. 27, pp. 381-397.

[26] R. Milner (1975), Processes: a mathematical model of computing agents, in Proceedings. of Logic Colloquium. 73 (H.E. Rose, J.C. Shepherdson, eds.), pp. 157-173, North-Holland, Amsterdam.
[27] R. Milner (1980), A Calculus of Communicating Systems, Lecture Notes in Computer Science Vol. 92,
Springer, Berlin.
[28] R. Milner (1989),$C.\mathit{0}$.

mmunication and Concurrency, Prentice Hall International.

[29] R. Milner, J. Parrow, and D. Walker (1992), A calculus of mobile processes, I and II, Information andComputation, Vol. 100, pp. 1-40 and pp. 41-77.
[30] E.-R. Olderog and C.A.R. Hoare (1986), Specification-oriented semantics for communicating processes,
Acta Informatica, Vol. 23, pp. 9-66.

[31] Plotkin, G.D. (1981), A Structural Approach to Operational Semantics, Report DAIMI FN-19, Comp. Sci.
Dept., Aarhus Univ.
[32] Plotkin, G.D. (1981), Post-Graduate Lecture Notes in Advanced Domain Theory, Department of Computer
Science, University of Edinburgh.
[33] J.J.M.M. Rutten (1989), Correctness and full abstraction of metric semantics for concurrency, in Linear
Time, Branching Time and Partial Order in Logics and Models for Concurrency ( J.W. de Bakker, W.P.
de Roever, G. Rozenberg, eds.), Lecture Notes in Computer Science Vol. 354, pp. 628-658, Springer, Berlin.

[34] J.J.M.M. Rutten (1990), Semantic correctness for a parallel object-oriented language, SIAM J. of $C_{om}-$
puting Vol. 19, No. 2, pp. 341-383.

[35] Rutten, J.J.M.M. (1990), Deriving denotational models for bisimulation from Structured Operational Semantics, in Proceedings of IFIP
Working Conference on Programming Concepts and Methods (M. Broy,
C.B. Jones, eds.).
$TC\ell$[36] M.B. Smyth (1987), Powerdomains, Joumal of Computer and System Sciences, Vol. 16, pp. 23-26.

[37] J. Stoy (1977), Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory,
MIT Press.
[38] K.J. Tumer (1993), Using Fomal Description Techniques: An Introduction to ESTELLE, LOTOS andSDL, John Wiley&Sons.