BRICS RS-95-22 A. Ing� olfsd� ottir: Value�Passing Processes, Late Approach, Part II

BRICS

Basic Research in Computer Science

A Semantic Theory for Value�Passing Processes Late Approach

Part II: A Behavioural Semantics and Full Abstractness

Anna Ing� olfsd� ottir

BRICS Report Series RS-95-22 ISSN 0909-0878 April 1995 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1995, BRICS, Department of Computer Science

University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent publications in the BRICS Report Series. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK - 8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@daimi.aau.dk

BRICS publications are in general accessible through WWW and anonymous FTP:

http://www.brics.aau.dk/BRICS/
ftp ftp.brics.aau.dk (cd pub/BRICS)

Semantic Theory for Value–Passing Processes Late Approach

Part II: A Behavioural Semantics and Full Abstractness

Anna Ingólfsdóttir

BRICS^{∗}

Department of Mathematics and Computer Science Aalborg University, Denmark

1 Introduction

This is the second of two companion papers on a semantic theory for communicating processes with values based on the late approach. In the first one, [Ing95], we explained the general idea of the late semantic approach. Furthermore we introduced a general syntax for value-passing process algebra based on the late approach and a general class of denotational models for these languages in the Scott-Strachey style. Then we defined a concrete language, CCS_{L}, which is an extension of the standard CCS with values according to the late approach. We also provided a denotational model for it, which is an instantiation of the general class. This model is a direct extension of the model given by Abramsky [Abr91] to model the pure calculus SCCS. Furthermore we gave an axiomatic semantics by means of a proof system based on inequations and proved its soundness and completeness with respect to the denotational semantics.

In this paper we will give a behavioural semantics to the language CCS_{L} in terms of a Plotkin style operational semantics and a bisimulation based preorder. Our main aim is to relate the behavioural view of processes we present here to the domain-theoretical one developed in the companion paper [Ing95]. In the Scott-Strachey approach an infinite process is obtained as a chain of finite and possibly partially specified processes. The completely unspecified process is given by the bottom element of the domain. An operational interpretation of this approach is to take divergence into account and give the behavioural semantics in terms of a prebisimulation or bisimulation preorder [Hen81, Wal90] rather than by the standard bisimulation equivalence [Par81, Mil83].

One of the results in the pure case presented in [Abr91] is that the denotational model given in that reference is fully abstract with respect to the “finitely observable” part of the bisimulation preorder but not with respect to the bisimulation preorder which turns out to be too fine. Intuitively this is due to the algebraicity of the model and the fact that the finite elements in the model are denotable by syntactically finite terms. The algebraicity implies that the denotational semantics of a process is completely decided by the semantics of its syntactically finite approximations, whereas the same can not be said about the bisimulation preorder. In fact we need experiments of an infinite depth to investigate bisimulation while this is not the case for the preorder induced by the model as explained above. An obvious consequence of this observation is that in general, a bisimulation preorder can not be expected to be modelled by an algebraic cpo given that the compact elements are denotable by syntactically finite elements.

∗Basic Research in Computer Science, Centre of the Danish National Research Foundation.

In [Hen81] Hennessy defined a term model for SCCS. This model is ωalgebraic and fails to be fully abstract with respect to the strong bisimulation preorder. In the same paper the author introduces the notion of “the finitary part of a relation” and “a finitary relation”. The finitary part of a relation R over processes, denoted by R^{F}, is defined by

pR^{F} q iff ∀d.dRp ⇒ dRq

where d ranges over the set of syntactically finite processes. A relation R is finitary if R^{F} = R. Intuitively this property may be interpreted as algebraicity at the behavioural level provided that syntactically finite terms are interpreted as compact elements in the denotational model; if a relation is finitary then it is completely decided by the syntactically finite elements.

In both [Hen81] and [Abr91] the full abstractness of the respective denotational semantics with respect to ⊏_{∼}^{F} is shown. In [Abr91] it is also shown that if the language is sort finite and satisfies a kind of finite branching condition, then ⊏_{∼}^{F} =⊏_{∼}_{ω}, where ⊏_{∼}_{ω} is the strong bisimulation preorder induced by experiments of finite depth, i.e. the preorder is obtained by iterated application of the functional that defines the bisimulation. Note that in general the preorder ⊏_{∼} is strictly finer than the preorder ⊏_{∼}_{ω}. However if the transition system is image finite, i.e. if the number of arcs leading from a fixed state and labelled with a fixed action is finite, then these two preorders coincide.

As mentioned above the main aim of this paper is to give a bisimulation based behavioural semantics for our language CCS_{L} from [Ing95]. To reflect the late approach the operational semantics will be given in terms of an applicative transition system, a concept that is a modification of that defined in [Abr90]. We generalize the notion of bisimulation [Par81, Mil83] to be applied to applicative transition systems and introduce a preorder motivated by Abramsky’s applicative bisimulation [Abr90]. For this purpose we first introduce the notion of strong applicative prebisimulation and the corresponding strong applicative bisimulation preorder. Following the standard practice this preorder is obtained as the largest fixed point of a suitably defined monotonic functional. We show by an example that this preorder is not finitary in the sense described above and is strictly finer than the preorder induced by the model.

Next we define the strong applicative ω-bisimulation preorder in the standard way by iterative application of the functional that induces the bisimulation preorder. This gives as a result a preorder which still is too fine to match the preorder induced by the denotational model. This will be shown by an example. Intuitively the reason for this is that we still need infinite experiments to decide the operational preorder, now because of an infinite breadth due to the possibility of an infinite number of values that have to be checked.

Then we give a suitable definition of the notion of the “finitary part” of the bisimulation preorder to meet the preorder induced by the denotational model. We recall that in [Ing95] we defined the so-called compact terms as the syntactically finite terms which only use a finite number of values in a nontrivial way. We also showed that these terms correspond exactly to the compact elements in the denotational model in the sense that an element in the model is compact if and only if it can be denoted by a compact term. This motivates a definition of the finitary part, ⊏_{∼}^{F}, of the bisimulation preorder ⊏_{∼} by

p ⊏_{∼}^{F} q iff ∀c. c ⊏_{∼} p ⇒ c ⊏_{∼} q

where c ranges over the set of syntactically compact terms. We also define yet another preorder, ⊏_{∼}_{ω}^{f}, a coarser version of ⊏_{∼}_{ω} in which we only consider a finite number of values at each level in the iterative definition of the preorder. Here it is vital that the set of values is countable and can be enumerated as V al = {v_{1}, v_{2}, ⋯}. Thus in the definition of ⊏_{∼}_{1}^{f} we only test whether the defining constraints of the preorder hold when the only possible input and output value is v_{1}, and in general in the definition of ⊏_{∼}_{n}^{f} we test the constraints for the first n values only. (Here we would like to point out that this idea originally appears in [HP80].) It turns out that ⊏_{∼}_{ω}^{f} is the finitary part of ⊏_{∼} in our new sense and that the model is fully abstract with respect to ⊏_{∼}_{ω}^{f}. We will prove both these results in this paper using techniques which are similar to those used by Hennessy in the above mentioned reference [Hen81].

The structure of the paper is as follows: In Section 2 we give a short survey of the result from the companion paper [Ing95] needed in this study. The definition of the operational semantics and the notion of applicative bisimulation are the subject of Section 3. Section 4 is devoted to the analysis of the preorder and the definition of the value-finitary preorder ⊏_{∼}_{ω}^{f}. In Section 5 we give a definition of the notion of finitary part of a relation and a finitary relation over processes. In the same section we prove that the preorder ⊏_{∼}_{ω}^{f} is finitary and that it coincides with the finitary part of the preorder ⊏_{∼}. Finally we prove the soundness and the completeness of the proof system with respect to the resulting preorder. The full abstractness of the denotational semantics for CCS_{L}, given in [Ing95], then follows from the soundness and the completeness of the proof system with respect to the denotational semantics. In Section 6 we give some concluding remarks.

2 Preliminaries

In this section we will give a brief review of the definitions, notation and proved results we need in this study from the companion paper [Ing95].

2.1 Syntax

First we extend the standard notion of a signature, Σ, and that of Σ-terms used for the pure calculus in order to model processes with value-passing based on the late approach. We do this by introducing the notion of applicative signature as a pair, (Σ, C), where Σ is a signature and C is a set (of channel names) and that of (Σ, C)-terms. For motivation for these definitions we refer to the companion paper [Ing95].

The general syntax is based on predefined expression languages for value expressions and boolean expressions. Thus we assume some predefined syntactic category of expression, Exp, ranged over by e including a countable set of values, V al, ranged over by v, and a set of value variables, V ar, ranged over by x. We also assume a predefined syntactic category, BExp, of boolean expressions, ranged over by be. BExp should at least include a test for equality between the elements of Exp. From such a predicate a test for membership of a finite set can easily be derived. Value expressions are supposed to be equipped with a notion of substitution of an expression for a value variable, denoted by e[e′/x], and an evaluation function [[ ]] : Exp × V Env ⟶ V al, where V Env is the set of value environments σ : V ar ⟶ V al. For closed expression we write [[e]] instead of [[e]]σ. Further we preassume an infinite set of process names, P N, ranged over by P, Q, etc. The set of (Σ, C)-terms is now given as the triple

T_{(Σ,C)} = (P roc_{(Σ,C)}, F un_{(Σ,C)}, P air_{(Σ,C)})

of the sets generated by Σ and C according to the following syntax:

\begin{matrix}P roc_{(Σ,C)} : & p ::= op(\underline{p}), op ∈ Σ c?.f c!.π τ.p be → p, p′ \\ F un_{(Σ,C)} : & f ::= [x]p \\ P airs_{(Σ,C)} : & π ::= (e, p) \end{matrix}

where we use the notation \underline{p} to denote a vector of terms in P roc_{(Σ,C)} of the appropriate length. If the process names in P N are added as primitives to the syntax for T_{(Σ,C)}, we write T_{(Σ,C)}(P N) for the resulting triple of (Σ, C)-terms, and T_{(Σ,C)}^{rec}(P N) if the recursive binding rec . is also allowed.

We have three kinds of actions, input actions of the form c?, c ∈ C, output actions of the form c!, c ∈ C and the silent action τ. We write C? for {c?|c ∈ C} and C! for {c!|c ∈ C}. The set Act = C! ∪ C? is ranged over by a whereas Act_{τ} = C! ∪ C? ∪ {τ} is ranged over by μ.

Prefixing by [x] binds the data variable x and the recursion construct is a binding construct for process names. A value variable, x, is free if it is not in the scope of a prefix, [x], and a process name P is free if it is not in the scope of a recursion construct, rec P. . We assume a notion of substitution for both data variables and process names in terms defined in the usual way. For f = [x]p and v ∈ V al we use the convention f(v) = ([x]p)(v) = p[v/x].

The language CCS_{L}(P N) = (CCS_{L}^{proc}(P N), CCS_{L}^{fun}(P N), CCS_{L}^{pair}(P N)) is obtained by instantiating the signature Σ by the standard operator of CCS. So we let Σ consist of the nullary operators NIL and Ω, the families of unary operators \ c, c ∈ C and [R] where R is a finite permutation of the channel

CCS_{L}^{proc}(P N) : p ::= NIL Ω p[R] p \ c p + p p|p c?.f c!.π τ.p
be → p, p P recP.p
CCS_{L}^{fun}(P N) : f ::= [x]p
CCS_{L}^{pair}(P N) : π ::= (e, p)

Figure 1: The Syntax for CCS_{L}

names and the binary operators + and |. The syntax for CCS_{L}(P N) is given in Figure 1. We let CCS_{L} = (CCS_{L}^{proc}, CCS_{L}^{fun}, CCS_{L}^{pair}) denote the closed terms in CCS_{L}(P N). These will be referred to as processes, functions and pairs ranged over by cp, cf and cπ.

2.2 Semantics

In the companion paper [Ing95] we gave two kinds of semantics to CCS_{L}: denotational semantics and an axiomatic semantics in terms of inequationally based proof system. We also showed the equivalence between them. The proof of the full abstractness of the behavioural semantics with respect to the behavioural semantics presented in this second paper does not rely on the details of the definition of the denotational model, but instead we use the properties of the proof system. Therefore we just assume the existence of the denotational model \overline{ACT} and the related evaluation mapping but give a rather detailed description of the proof system. In particular we know from [Ing95] that the compact elements of the model may be denoted in the syntax by the so-called syntactically compact terms, CoT erms(P N) = (CoP roc(P N), CoF un(P N), CoP air(P N)), which are defined below. Intuitively the syntactically compact terms are the recursion-free terms which only use a finite number of values in a nontrivial way. (Note that the number of channels used by the term is automatically finite.) We start by introducing some notation.

Notation 2.1 Let \underline{w}_{n} = (w_{1}, …, w_{n}) and \underline{p}_{n} = (p_{1}, …, p_{n}) be vectors of values and processes respectively. We write x : \underline{w}_{n} ⟶ \underline{p}_{n} for x = w_{1} ⟶ p_{1}, (x = w_{2} ⟶ p_{2}, (… x = w_{n} ⟶ p_{n}, Ω) …). (Intuitively x : \underline{w_{n}} ⟶ \underline{p_{n}} stands for the function that maps w_{i} to p_{i} for i = 1, …, n and all the other values w ∈ V al into Ω.) Further we let \{\underline{w_{n}}\} = \{w_{i}|\underline{w_{n}} = (w_{1}, …, w_{n})\} and similarly for \{\underline{p_{n}}\}.

Definition 2.2 [Syntactically Compact Terms] The set of syntactically compact terms is the triple

CoT erms(P N) = (CoP roc(P N), CoF un(P N), CoP airs(P N))

where the sets CoP roc(P N), CoF un(P N) and CoP airs(P N) are the least sets satisfying:

1. NIL, Ω ∈ CoP roc(P N) and P ∈ CoP roc(P N) for all P ∈ P N

2. \overline{p} ∈ CoP roc(P N) implies op(\overline{p}) ∈ CoP roc(P N), op = |, +, \, [R] , τ.

(+1)  X + (Y + Z) = (X + Y) + Z
(+2)  X + Y = Y + X
(+3)  X + X = X
(+4)  X + NIL = X
(res+)  (X + Y) \ c = X \ c + Y \ c
(res in)  (a?.[x]X) \ c = \{ \begin{matrix}a?.[x](X \ c) & if c ≠ a \\ NIL & otherwise \end{matrix}
(res out) (a!.(e, X)) \ c = \{ \begin{matrix}a!.(e, X \ c) & if c ≠ a \\ NIL & otherwise \end{matrix}
(res NIL)  NIL \ c = NIL
(res div)  Ω \ c = Ω
(ren+)  (X + Y)[R] = X[R] + Y [R]
(ren in)  (a?.[x]X)[R] = R(a)?.[x](X[R])
(ren out) (a!.(e, X))[R] = R(a)!.(e, X[R])
(ren NIL)  NIL[R] = NIL
(ren div)  Ω[R] = Ω
(NIL par)  NIL | X = X | NIL = X
(div)  Ω ⊑ X

Figure 2: Equations

3. π ∈ CoP air(P N), c ∈ C implies c!π ∈ CoP roc(P N)

4. f ∈ CoF un(P N) and c ∈ CR implies c?f ∈ CoP roc(P N)

5. p ∈ CoP roc(P N) and e ∈ Exp implies (e, p) ∈ CoP airs(P N)

6. \{\underline{p_{n}}\} ⊆ CoP roc(P N), \{\underline{w_{n}}\} ⊆ V al and x ∈ V ar implies [x]. x : \underline{w_{n}} ⟶ \underline{p_{n}} ∈ CoF un(P N).

We use the convention CoT erms = CoT erms(∅), CoP roc = CoP roc(∅), etc. and let them be ranged over by Cot, Cop, etc. We say that a term is compact if it belongs to CoT erms(P N). □

Note that CoT erms = (CoP roc, CoF un, CoP air) ⊆ CCS_{L} is closed under sub-terms. The proof system is based on the inequations in Figures 2–3. The inference rules, Figure 4, describe the structure of the model and its preorder and their interaction with the operators. In the interleaving law the summation notation is justified by equations (+1)-(+4) and an empty sum is understood as NIL. {+Ω} indicates that Ω is an optional summand of a term and Ω is a summand of the right hand side if it is a summand of X or Y on the left hand Let X = ∑_{i} τ.X_{i} + ∑_{j} a′_{j}?.[x]X′_{j} + ∑_{k} a′′_{k}!.(v_{k}, X′′_{k}){+Ω} and Y = ∑_{l} τ.Y_{l} + ∑_{m} b′_{m}?.[y]Y′_{m} + ∑_{n} b′′_{n}!.(v_{n}, Y′′_{n}){+Ω}. Then

X | Y = INT L(X, Y) + COMM(X, Y){+Ω}

where

INT L(X, Y) = INT L_{τ}(X, Y) + INT L_{in}(X, Y) + INT L_{out}(X, Y)

where

INT L_{τ}(X, Y) = ∑_{i} τ.(X_{i}|Y) + ∑_{l} τ.(X|Y_{l})
INT L_{in}(X, Y) = ∑_{j} a′_{j}?.[x](X′_{j}|Y) + ∑_{m} b′_{m}?.[y](X|Y′_{m})
INT L_{out}(X, Y) = ∑_{k} a′′_{k}!.(v_{k}, X′′_{k}|Y) + ∑_{n} b′′_{n}!.(v′_{n}, X|Y′′_{n})

and

COMM(X, Y) = ∑_{j,n:a′_{j}=b′′_{n}} τ.X′_{j}[v_{n}/x]|Y′′_{n} + ∑_{k,m:a′′_{k}=b′_{m}} τ.X′′_{k}|Y′_{m}[v_{k}/y]

Figure 3: Interleaving Law

(ref)  p ^{⊑} p
(trans)  \frac{p ^{⊑} q, q ^{⊑} r}{p ^{⊑} r}
(sub)  \frac{p_{i} ^{⊑} q_{i}}{op(\underline{p}) ^{⊑} op(\underline{q})} op ∈ ∑
(pre)  \frac{p ^{⊑} q}{μ.p ^{⊑} μ.q}
(rec)  \overline{recP.p = p[recP.p/P]}
(inst)  \overline{pσ ^{⊑} qσ} for every inequation p ^{⊑} q and closed instantiation σ
(ω − rule) \frac{p^{(n)} ^{⊑} q for all n}{p ^{⊑} q}
(cond1)  \frac{[[be]] = T}{be ⟶ p, q = p}
(cond2)  \frac{[[be]] = F}{be ⟶ p, q = q}
(pair)  \frac{[[e]] = [[e′]], p ^{⊑} q}{(e, p) ^{⊑} (e′, q)}
(fun)  \frac{p[v/x] ^{⊑} q[v/x] for every v ∈ V}{[x]p ^{⊑} [x]q}
(α − red) \overline{[x]p = [y]p[y/x]} if y not free in p

Figure 4: The Proof System E_{rec} side. To simplify the notation we assume that i, j etc. in the sums ∑_{i}, ∑_{j}, etc. range over finite index sets I, J, etc.

We refer to the whole system as E_{rec}, to the full system minus the ωrule as E_{rec}^{−ω} and as E if both the ω-rule and the rule (rec) are omitted. The respective preorder are denoted by ^{⊑}_{E_{rec}}, ^{⊑}_{E_{rec}^{−ω}} and ^{⊑}_{E}. The syntactically compact approximations used in the ω-rule of the proof system are defined as follows.

Definition 2.3 [Compact Approximations] The n-th compact approximation of a term is defined inductively by :

I. \begin{matrix}i) p^{(0)} = Ω \\ ii) \begin{matrix}1. P^{(n+1)} = P \\ 2. (op(\underline{p}))^{(n+1)} = op(\underline{p}^{(n+1)}) \\ 3. (μ.u)^{(n+1)} = μ.u^{(n+1)} \\ 4. (recP.p)^{(n+1)} = p^{(n+1)}[(recP.p)^{(n)}/P] \\ 5. (be ⟶ p, q)^{(n+1)} = \{ \begin{matrix}p^{(n+1)} & if [[be]] = T \\ q^{(n+1)} & if [[be]] = F \end{matrix} \end{matrix} \end{matrix}

II. ([x]p)^{(n+1)} = [x](x ∈ V_{n+1} ⟶ p^{(n+1)}, Ω)

III.((e, p))^{(n+1)} = \{ \begin{matrix}([[e]], p^{(n+1)}) & if [[e]] ∈ V_{n+1} \\ ([[e]], Ω) & otherwise \end{matrix}

□

We remind the reader that V_{n} = {v_{1}, …, v_{n}} is the set of the n first values. The syntactically compact approximations have the following fundamental properties:

Theorem 2.4 For all natural numbers n, t ∈ CCS_{L}(P C) and ct ∈ CCS_{L} and ρ : P N ⟶ \overline{ACT}

1. t^{(n)} ∈ CoT erms(P N), i.e. t^{(n)} is a syntactically compact term.

2. ct^{(n)} ^{⊑}_{E_{rec}^{−ω}} ct.

3. \overline{ACT}[[t]]ρ = ⨆_{n} \overline{ACT}[[t^{(n)}]]ρ.

The soundness and completeness of the proof system E_{rec} with respect to the denotational semantics is stated in the following theorem, whose proof may be found in [Ing95].

Theorem 2.5 [Soundness and Completeness] For all closed terms ct, cu in CCS_{L} we have

ct ^{⊑}_{E_{rec}} cu if and only if \overline{ACT}[[ct]] ^{⊑} \overline{ACT}[[cu]],

i.e. the proof system E_{rec} is sound and complete with respect to the denotational semantics.

In the theory to follow we need the following notion of Ω-normal forms and a corresponding normalization theorem.

Definition 2.6 [Ω-normal form] A compact term, nt ∈ CoT erms, is said to be in a Ω-normal form if the following hold:

1. If nt = np ∈ CoP roc then np has the form

nt = ∑_{i} μ_{i}.nt_{i}{+Ω}

where Ω is an optional summand and where nt_{i} is in an Ω-normal form. The empty sum is interpreted as NIL.

2. If nt = (e, np) ∈ CoP airs then e = v ∈ V al and np is in an Ω-normal form.

3. If nt = [x]x : \underline{v_{n}} ⟶ \underline{np_{n}} ∈ F un then np_{i} is in an Ω-normal form for i ≤ n.

□

Lemma 2.7 For all Cot ∈ CoT erms there is an Ω-normal form n(Cot) such that n(Cot) =_{E} Cot.

As a consequence of the soundness and completeness theorem above we get the following useful corollary.

Corollary 2.8 For all Cot ∈ CoT erms and cu ∈ CCS_{L}

Cot ^{⊑}_{E_{rec}} cu implies Cot ^{⊑}_{E} cu^{(n)} for some n

and therefore

Cot ^{⊑}_{E_{rec}} cu iff Cot ^{⊑}_{E_{rec}^{−ω}} cu.

Proof First we note that for Cou, Cot ∈ CoT erms

Cou ^{⊑}_{E_{rec}} Cot iff Cou ^{⊑}_{E} Cot.  (1)

Now we proceed as follows

Cot ^{⊑}_{E_{rec}} cu
implies \overline{ACT} [[Cot]] ^{⊑}\overline{ACT} \overline{ACT} [[cu]]
as E_{rec} is sound wrt. \overline{ACT}
implies ∃n. \overline{ACT} [[Cot]] ^{⊑}\overline{ACT} \overline{ACT} [[cu^{(n)}]] ^{⊑}\overline{ACT} \overline{ACT} [[cu]]
by Thm. 2.4 as \overline{ACT} [[Cot]] is compact
implies ∃n. Cot ^{⊑}_{E_{rec}} cu^{(n)} ^{⊑}_{E_{rec}} cu
as E_{rec} is complete wrt. \overline{ACT}

implies ∃n. Cot ^{⊑}_{E} cu^{(n)} ^{⊑}_{E_{rec}^{−ω}} cu

by (1) and Thm. 2.4.

□

In the proof for the full abstractness of the model with respect to our representant for the behavioural preorder we will use some standard techniques which are used to prove similar full abstractness results in the literature [Hen88, AH92, HI93]. This gives us some guidelines about properties our behavioural interpretation of the preorder induced by the model should satisfy. This is formulated in the following lemma:

Theorem 2.9 Assume that ⪯ ⊆ CCS_{L} × CCS_{L} satisfies the following conditions:

1. Finitariness: For all ct, cu ∈ CCS_{L}

ct ⪯ cu iff ∀Cot. Cot ⪯ ct ⇒ Cot ⪯ cu.

2. Partial soundness: The proof system E_{rec}^{−ω} is sound with respect to ⪯.

3. Partial completeness: For all Cot ∈ CoT erms and ct ∈ CCS_{L}

Cot ⪯ ct implies Cot ^{⊑}_{E_{rec}} ct.

Then for all ct, cu ∈ CCS_{L}

ct ⪯ cu if and only if ct ^{⊑}_{E_{rec}} cu if and only if \overline{ACT}[[ct]] ^{⊑}\overline{ACT} \overline{ACT}[[cu]].

Proof First we have:

ct ⪯ cu
iff ∀Cot. Cot ⪯ ct ⇒ Cot ⪯ cu  by 1.
iff ∀Cot. Cot ^{⊑}_{E_{rec}} ct ⇒ Cot ^{⊑}_{E_{rec}} cu by 2., 3. and Cor. 2.8.

Now we proceed as follows: Assume ct ⪯ cu and therefore that

∀Cot. Cot ^{⊑}_{E_{rec}} ct ⇒ Cot ^{⊑}_{E_{rec}} cu.  (2)

As ct^{(n)} ^{⊑}_{E_{rec}} ct and ct^{(n)} ∈ CoT erms then (2) implies that ct^{(n)} ^{⊑}_{E_{rec}} cu. As this holds for all n, the ω-rule implies that ct ^{⊑}_{E_{rec}} cu.

Next assume that ct ^{⊑}_{E_{rec}} cu. To prove that ct ⪯ cu it is sufficient to prove that (2) holds. So assume that Cot ^{⊑}_{E_{rec}^{−ω}} ct. Then, by transitivity of ^{⊑}_{E_{rec}}, Cot ^{⊑}_{E_{rec}} cu and therefore we get that ct ⪯ cu. □

3 Operational Semantics

The aim of this section is to define an operational semantics and a suitable notion of preorder to describe the behaviour of our language. The operational semantics is given in terms of an applicative transition system, a slight modification of a notion originally suggested by Abramsky [Abr90]. An applicative transition system models the idea of looking at an input term as a prefixing of a function which is ready to receive values along the prefixing channel. Furthermore it reflects the idea of looking at an output term as a prefixing of a pair of the value and the resulting process. For further motivations of this approach we refer to the companion paper [Ing95].

Definition 3.1 An applicative labelled transition system (ALTS) is a five tuple

AT = ⟨Con, V al, Act, ⟶, ↓⟩

where

• Con is a set of configurations

• V al is a set of Values

• Act = Act_{Con} ⊎ Act_{P airs} ⊎ Act_{F un} is a set of actions.

• ⟶ is a transition relation

⟶⊆ \begin{matrix}(Con × Act_{Con} × Con)∪ \\ (Con × Act_{P airs} × (V al × Con))∪ \\ (Con × Act_{F un} × (V al ⟶ Con)). \end{matrix}

• ↓⊆ Con is a convergence predicate.

We refer to States = Con ∪ (V al × Con) × (V al ⟶ Con) as the set of possible states. □

Now we will define the so-called strong applicative prebisimulation (sa-prebi-simulation) as a further abstraction on the applicative transition system. More precisely we define it as the greatest fixed point to a monotonic endofunction on the complete lattice P(Con × Con). In order to obtain this we have to extend our notion of relation over configurations. Given a binary relation over Con we extend it pointwise to V al × Con by:

For all c_{1}, c_{2} ∈ Con and v_{1}, v_{2} ∈ V al, (v_{1}, c_{1})R^{pair}(v_{2}, c_{2}) iff c_{1}Rc_{2}
and v_{1} = v_{2}.

and to V al ⟶ Con by:

For all f_{1}, f_{2} ∈ V al ⟶ Con, f_{1} R_{fun} f_{2} iff f_{1}(v)Rf_{2}(v) for all
v ∈ V al.

For any s, s′ ∈ States we write sRs′ if sRs′ or sR^{pair}s′ or sR^{fun}s′ depending on the type of s and s′.

Definition 3.2 Let AT = ⟨Con, V al, Act, ⟶, ↓⟩ be an ALT S. We define F : P(Con × Con) ⟶ P(Con × Con) by:

If R ⊆ Con × Con then c_{1}F(R)c_{2} iff for all μ ∈ Act
(i) c_{1} ⟶^{μ} s_{1} implies c_{2} ⟶^{μ} s_{2} for some s_{2} such that s_{1}Rs_{2},
(ii) c_{1} ↓ implies (c_{2} ↓ and whenever c_{2} ⟶^{μ} s_{2} then c_{1} ⟶^{μ} s_{1} for
some s_{1} such that s_{1}Rs_{2}).
where s_{1}, s_{2} ∈ States.
□

Obviously F defined this way is a monotonic endofunction over the complete lattice (P(Con × Con), ⊆). Thus the Knaster-Tarski fixed point theorem, [Tar55], applies and the greatest fixed point to F exists. We may therefore give the following definition:

Definition 3.3 (Strong Applicative Prebisimulation) Let AT = ⟨Con, V al, Act, ⟶, ↓⟩ be an applicative labelled transition system and F be defined as in Definition 3.2. Then R ⊆ P(Con × Con) is called a prebisimulation if it is a post-fixed point to F, i.e. if R ⊆ F(R). We define the strong applicative bisimulation preorder ⊏_{∼} as the greatest fixed point to F, i.e.

⊏_{∼}= ⋃{R|R ⊆ F(R)}.

We define the strong applicative bisimulation equivalence as ∼=⊏_{∼} ∩ ⊏_{∼}^{−1}.

□

Similar results as for the pure case also hold here and are simply restated in the following lemma.

Lemma 3.4

1. ⊏_{∼} is a preorder

2. ∼ is an equivalence relation.

So far we have given a definition of ⊏_{∼} on an abstract ALT S. Now we define a concrete ALT S by taking Con to be CCS_{L}^{proc}, as generated by the syntax in Figure 2.1, ⟶ to be the least transition relation closed under the rules of Figures 5-6 and the convergence predicate ↓ to be the least relation on CCS_{L}^{proc} satisfying the rules in Figure 7. As usual the divergence predicate ↑ is defined as the complement of ↓. The basic rule for input has the form

c?.[x]p ⟶^{c?} [x]p,

(input) c?.cf ⟶^{c?} cf
(output) c!.(e, cp) ⟶^{c!} (v, cp) , [[e]] = v
(tau)  τ.cp ⟶^{τ} cp
(ren)  \frac{cp ⟶^{c?} [x]p′}{cp[R] ⟶^{R(c)?} [x](p′[R])}

\frac{cp ⟶^{c!} (v, cp′)}{cp[R] ⟶^{R(c)!} (v, cp′[R])}

\frac{cp ⟶^{τ} cp′}{cp[R] ⟶^{τ} cp′[R]}

(res)  \frac{cp ⟶^{c?} [x]p′}{cp\c′ ⟶^{c?} [x](p′\c′)} , c ≠ c′
\frac{cp ⟶^{c!} (v, cp′)}{cp\c′ ⟶^{c!} (v, cp′\c′)} , c ≠ c′

\frac{cp ⟶^{τ} cp′}{cp\c′ ⟶^{τ} cp′\c′}

Figure 5: Operational semantics for CCS_{L}: Part 1

(choice) \frac{cp ⟶^{μ} ct}{cp + cq ⟶^{μ} ct}

(par)  \frac{cp ⟶^{c?} [x]p′}{cp | cq ⟶^{c?} [x](p′ | cq)}

\frac{cp ⟶^{c!} (v, cp′)}{cp | cq ⟶^{c!} (v, cp′ | cq)}

\frac{cp ⟶^{τ} cp′}{cp | cq ⟶^{τ} cp′ | cq}

(com)  \frac{cp ⟶^{c?} [x]p′, cq ⟶^{c!} (v, cq′)}{cp | cq ⟶^{τ} p′[v/x] | cq′}

(cond) \frac{cp ⟶^{μ} ct}{(be ⟶ cp, cq) ⟶^{μ} ct} , [[be]] = T

\frac{cq ⟶^{μ} ct}{(be ⟶ cp, cq) ⟶^{μ} ct} , [[be]] = F

(rec)  \frac{p[rec P.p/P] ⟶^{μ} cp′}{rec P.p ⟶^{μ} cp′}

The choice, par and com rules have symmetric counterparts.

Figure 6: Operational semantics for CCS_{L}: Part 2

\overline{NIL ↓} \frac{cp ↓, cp′ ↓}{cp + cp′ ↓} \frac{cp ↓, cp′ ↓}{cp | cp′ ↓} \frac{cp ↓}{cp\c ↓} \frac{cp ↓}{cp[R] ↓} \frac{p[Ω/P] ↓}{rec P.p ↓}

\frac{[[be]] = T, cp_{1} ↓}{be ⟶ cp_{1}, cp_{2} ↓} \frac{[[be]] = F, cp_{2} ↓}{be ⟶ cp_{1}, cp_{2} ↓}

Figure 7: The convergence predicate the one for output is

c!.(v, q) ⟶^{c!} (v, q)

and that for communication express the fact that synchronization takes the form of functions application,

\frac{p ⟶^{c?} [x]p′, q ⟶^{c!} (v, q′)}{p|q ⟶^{τ} p′[v/x]|q′}.

The rules in Figure 5-6 are consistent in the following sense:

Lemma 3.5 For all cp ∈ CCS_{L}^{proc}

1. cp ⟶^{τ} ct implies ct ∈ CCS_{L}^{proc},

2. cp ⟶^{c?} ct implies ct ∈ CCS_{L}^{fun},

3. cp ⟶^{c!} ct implies ct ∈ CCS_{L}^{pair}.

Proof An easy induction on the length of the derivation of cp ⟶^{μ} ct. □

The bisimulation preorder ⊏_{∼} defined on this ALT S satisfies:

Theorem 3.6

1. ⊏_{∼} is a pre-congruence with respect to the operators in Σ.

2. (a) For all cp_{1}, cp_{2} cp_{1} ⊏_{∼} cp_{2} implies τ.cp_{1} ⊏_{∼} τ.cp_{2}.

(b) For all c ∈ Chan and cπ_{1}, cπ_{2}, cπ_{1} ⊏_{∼} cπ_{2} implies c!.cπ_{1} ⊏_{∼} c!.cπ_{2}.

(c) For all c ∈ Chan and cf_{1}, cf_{2}, cf_{1} ⊏_{∼} cf_{2} implies c?.cf_{1} ⊏_{∼} c?.cf_{2}.

3. (a) For all p_{1}, p_{2} ∈ CCS_{L}^{proc}(∅) with F V V (p_{i}) ⊆ {x}, i = 1, 2, whenever

p_{1}[v/x] ⊏_{∼} p_{2}[v/x] for every v ∈ V al then [x]p_{1} ⊏_{∼} [x]p_{2}.

(b) For all cp_{1}, cp_{2} and v, cp_{1} ⊏_{∼} cp_{2} implies (v, cp_{1}) ⊏_{∼} (v, cp_{2}).

Proof

1. We have to prove that for any operator op ∈ Σ following holds:

\underline{cp} ⊏_{∼} \underline{cq} ⇒ op(\underline{cp}) ⊏_{∼} op(\underline{cq}).

We will only prove the statement for the case op = | , leaving the remaining cases to the interested reader to check. So assume cp_{1} ⊏_{∼} cp_{2} and cq_{1} ⊏_{∼} cq_{2}. This means that there are saprebisimulations, R_{p} and R_{q} such that (cp_{1}, cp_{2}) ∈ R_{p} and (cq_{1}, cq_{2}) ∈ R_{q}. We define

R_{p}|R_{q} = {(cp′_{1}|cq′_{1}, cp′_{2}|cq′_{2}) (cp′_{1}, cp′_{2}) ∈ R_{p}, (cq′_{1}, cq′_{2}) ∈ R_{q}}.

As (cp_{1}|cq_{1}, cp_{2}|cq_{2}) ∈ R_{p}|R_{q} it is sufficient to show that R_{p}|R_{q} is a saprebisimulation. We proceed as follows:

(a) Assume that (cp′_{1}|cq′_{1}, cp′_{2}|cq′_{2}) ∈ R_{p}|R_{q} and that cp′_{1}|cq′_{1} ⟶^{μ} cr_{1}.

We have the following cases:

i. μ = τ, cp′_{1} ⟶^{τ} cp′′_{1} and cr_{1} = cp′′_{1}|cq′_{1}. Then there is a cp′′_{2} where

cp′_{2} ⟶^{τ} cp′′_{2} and (cp′′_{1}, cp′′_{2}) ∈ R_{p}. This implies that cp′_{2}|cq′_{2} ⟶^{τ}

cp′′_{2}|cq′_{2} where (cp′′_{1}|cq′_{1}, cp′′_{2}|cq′_{2}) ∈ R_{p}|R_{q}.

ii. μ = c?, cp′_{1} ⟶^{c?} [x]p′′_{1} and cr_{1} = [x](p′′_{1}|cq′_{1}). Now there is a

[y]p′′_{2} where cp′_{2} ⟶^{c?} [y]p′′_{2} and ([x]p′′_{1}, [y]p′′_{2}) ∈ R^{fun}, i.e. for all

v ∈ V al, (p′′_{1}[v/x], p′′_{2}[v/y]) ∈ R_{p}. As cq′_{1} and cq′_{2} do not contain free value-variables this implies that for all v ∈ V al

\begin{matrix}((p′′_{1}|cq′_{1})[v/x], (p′′_{2}|cq′_{2})[v/y]) = ((p′′_{1}[v/x]|cq′_{1}), (p′′_{2}[v/y]|cq′_{2})) \\ ∈ R_{p}|R_{q}. \end{matrix}

This shows that ([x](p′′_{1}|cq′_{1}), [y](p′′_{2}|cq′_{2}) ∈ R_{p}|R_{q}^{fun}. Furthermore

cp′_{2}|cq′_{2} ⟶^{c?} [y](p′′_{2}|cq′_{2}).

iii. μ = c!, cp′_{1} ⟶^{c!} (v, cp′′_{1}) and cr_{1} = (v, cp′′_{1}|cq′_{1}). Now cp′_{2} ⟶^{c!}

(v, cp′′_{2}) for some cp′′_{2} where (cp′′_{1}, cp′′_{2}) ∈ R_{p}. Thus

(cp′′_{1}|cq′_{1}, cp′′_{2}|cq′_{2}) ∈ R_{p}|R_{q}

and therefore

((v, cp′′_{1}|cq′_{1}), (v, cp′′_{2}|cq′_{2})) ∈ R_{p}|R_{q}^{pair}.

Furthermore cp′_{2}|cq′_{2} ⟶^{c!} (v, cp′′_{2}|cq′_{2}).

iv. The symmetrical cases μ = τ, c?, c! where the transition comes from cq′_{1} instead of cp′_{1} may be treated in the same way.

v. μ = τ, cp′_{1} ⟶^{c?} [x]p′′_{1}, cq′_{1} ⟶^{c!} (v, cq′′_{1}) and cr_{1} = p′′_{1}[v/x]|cq′′_{1}.

Then cp′_{2} ⟶^{c?} [y]p′′_{2} where ([x]p′′_{1}, [y]p′′_{2}) ∈ R_{p}^{fun}, i.e for all v ∈

V al, (p′′_{1}[v/x], p′′_{2}[v/y]) ∈ R_{p}. Furthermore cq′_{2} ⟶^{c!} (v′, cq′′_{2})

where ((v, cq′′_{1}), (v′, cq′′_{2}) ∈ R_{q}^{pair}, i.e. where v = v′ and (cq′′_{1}, cq′′_{2}) ∈ R_{q}. This implies that (p′′_{1}[v/x]|cq′′_{1}, p′′_{2}[v/y]|cq′′_{2}) ∈ R_{p}|R_{q}. Fur-

thermore cp′_{2}|cq′_{2} ⟶^{τ} p′′_{2}[v/y]|cq′′_{2}.

vi. The symmetrical case where cp′_{1} ⟶^{c!} (v, cp′′_{1}) and cq′_{1} ⟶^{c?} [x]q′′_{1}

may be treated similarly.

(b) Next assume that cp′_{1}|cq′_{1} ↓. This implies that cp′_{1} ↓ and cq′_{1} ↓ and therefore that cp′_{2} ↓ and cq_{2} ↓. This in turn implies that cp′_{2}|cq′_{2} ↓.

Now assume that cp′_{1}|cq′_{1} ↓, cp′_{2}|cq′_{2} ↓ and cp′_{2}|cq′_{2} ⟶^{μ} cr_{2}. In the

same way as in (a) we may show that cp′_{1}|cq′_{1} ⟶^{μ} cr_{1} for some cr_{1} such that (cr_{1}, cr_{2}) ∈ R_{p}|R_{q}.

2. Here we will only prove the last case, i.e. that cf_{1} ⊏_{∼} cf_{2} implies c?.cf_{1} ⊏_{∼} c?.cf_{2}. The remaining cases may be proved similarly. So assume that cf_{1} = [x]p and cf_{2} = [y]q and that [x]p ⊏_{∼} [y]q. This implies that ([x]p, [y]q) ∈ R^{fun} for some sa-prebisimulation R. We define c?.R = R ∪ {(c?.f, c?.g) (f, g) ∈ R^{fun}}. Obviously (c?.[x]p, c?.[y]q) ∈ c?.R. It is also easy to see that c?.R is an sa-prebisimulation.

3. This is just a rephrasing of the definition of the extension of the relations from P roc to V al ⟶ P roc and V al × P roc.

□

4 Analysis of the Preorders

The subject of this section is to give an operational characterization of the denotational semantics given in the companion paper [Ing95]. First we show by an example, Example 4.1, that the bisimulation preorder, defined in Section 3, is too fine to coincide with the partial order in the model in the sense that the model is not fully abstract with respect to this behavioural preorder. This observation supports our intuition that bisimulation is in general too fine to be completely characterized by any semantics induced by an algebraic cpo as explained in the introduction to this paper.

Example 4.1 As we only need an example from the pure calculus we use the notation \overline{a} = c?x, a.p = c!.(v_{1}, p) and \ a = \ c. Let

a^{ω} = recY.a.Y and p = [recX.(a^{ω} + X)|\overline{a}] \ a.

Then the first unfolding of p is

p_{1} = [(a^{ω} + (recX.(a^{ω} + X)|\overline{a}))|\overline{a}] \ a,

and the n + 1-th one

p_{n+1} = [(\overbrace{a^{ω} + ((a^{ω} + ((a^{ω} + … + ((a^{ω}}^{n} +recX.(a^{ω} + X)|\overline{a}))| \underbrace{\overline{a} … |\overline{a.}))|\overline{a}}_{n}] \ a.

The reader may convince himself that the behaviour of p can be given by the derivation tree described by the infinite sum Ω + ∑_{i∈ω} τ^{i}.NIL, i.e. a tree which has an infinite number of branches which all have a finite depth. Then, because of the algebraicity of the model, \overline{ACT} [[p + recP.τ.P]] = \overline{ACT} [[p]]. On the other hand the left hand side has the transition p + recP.τ.P ⟶^{τ} recP.τ.P where recP.τ.P can perform an infinite sequence of τ-moves. This move can therefore never be matched by the right hand side p. This implies that p + recP.τ.P ⊏̸_{∼} p.

Obviously Example 4.1 rules out the possibility that the behavioural preorder ⊏_{∼} characterizes the preorder of the model. Our second suggestion for a behavioural characterization of the model is the weaker version of ⊏_{∼}, the strong applicative ω-bisimulation preorder, derived from the function F by iterated application.

Definition 4.2 [Strong Applicative ω-Prebisimulation] The kth sa-prebisimulation ⊏_{∼}_{k} is defined inductively by:

1. ⊏_{∼}_{0}= Con × Con,

2. ⊏_{∼}_{n+1}= F(⊏_{∼}_{n}).

The sa-ω-prebisimulation ⊏_{∼}_{ω} is defined as ⊏_{∼}_{ω}= ⋂_{k} ⊏_{∼}_{k} and ∼_{ω}=⊏_{∼}_{ω} ∩⊏_{∼}_{ω}^{−1}. □

For all k we have that ⊏_{∼}⊆⊏_{∼}_{k+1}⊆⊏_{∼}_{k} which implies that ⊏_{∼}⊆⊏_{∼}_{ω}.

Again this preorder is too fine to match the preorder from the model as the following example shows:

Example 4.3 Let AT = ⟨Con, Act, ⟶, ↓⟩ be an applicative transition system and the process p be given by the derivation graph described by the infinite sum ∑_{n} c?.[x]x ≤ n ⟶ NIL, Ω^{1}. Now let

q = p + c?.[x]NIL.

In any denotational semantics based on an algebraic cpo, D, it is clear that D[[p]] = D[[q]]. On the other hand q has the derivation q ⟶^{c?} [x].NIL which can never be matched by p and consequently q ⊏̸_{∼}_{ω} p.

Intuitively the reason for why ⊏_{∼}_{ω} is too fine for processes with values is that the values give rise to a new kind of infinity. We recall from [Ing95] that in the model the preorder is decided completely by the compact elements. We also recall that the compact elements both have finite “depth” and “width”, i.e. map all but finite number of values to ⊥. These considerations motivate the following definition of value-finitary strong applicative ω-prebisimulation. This definition is a slight modification of the one given in [HP80].

Definition 4.4 [Value-Finitary Strong Applicative ω-Prebisimulation]

Let AT = ⟨Con, V al, Act, ⟶, ↓⟩ be an applicative transition system, V ⊆ V al and R ⊆ Con × Con. Then we define the V -restricted extension of R, R|_{V} by

1. c_{1}R|_{V} c_{2} iff c_{1}Rc_{2}

2. (v_{1}, c_{1})R|_{V} (v_{2}, c_{2}) iff (v_{1} ∈ V or v_{2} ∈ V) implies (v_{1} = v_{2} and c_{1}Rc_{2}).

3. f_{1}R|_{V} f_{2} iff f_{1}(v)Rf_{2}(v) for all v ∈ V.

The nth value-finitary sa-bisimulation preorder ⊏_{∼}_{n}^{f} is defined by:

1. ⊏_{∼}_{0}^{f}= Con × Con,

2. ⊏_{∼}_{n+1}^{f}= (F(⊏_{∼}_{n}^{f}))|_{V_{n+1}}.

1Whether this process can be expressed in the syntax of CCS_{L} or a similar language is an open question.

The value-finitary sa-ω-bisimulation preorder, ⊏_{∼}_{ω}^{f}, is defined by ⊏_{∼}_{ω}^{f}= ⋂_{k} ⊏_{∼}_{k}^{f} with the derived equivalence ∼_{ω}^{f}=⊏_{∼}_{ω}^{f} ∩(⊏_{∼}_{ω}^{f})^{−1}. □

From this definition we get that (v_{1}, c_{2}) ⊏_{∼}_{n}^{f} (v_{2}, c_{2}) if and only if v_{1}, v_{2} ∉ V_{n} or

v_{1} = v_{2} ∈ V_{n} and c_{1} ⊏_{∼}_{n}^{f} c_{2}.

We note that R|_{V} is decreasing in V, i.e. V ⊆ W implies R|_{V} ⊇ R|_{W}. This implies that ⊏_{∼}_{n}^{f}⊆⊏_{∼}_{n+1}^{f} for all n. We also note that the only difference between this definition and Definition 4.2 is the restriction on the values in the definition of ^{⊑}_{n+1}^{f}. Obviously ⊏_{∼}_{n}⊆⊏_{∼}_{n}^{f} for all n which implies ⊏_{∼}⊆⊏_{∼}_{ω}⊆⊏_{∼}_{ω}^{f}. It is easy to prove that ⊏_{∼}_{ω}^{f} actually is a preorder and has all the properties stated in Theorem 3.6. The proof for this is straightforward and is left to the reader. Now let us have a further look at our previous example, Example 4.3.

Example 4.5 Let p and q be defined as in Example 4.3. Obviously p ⊏_{∼} q and therefore p ⊏_{∼}_{ω}^{f} q. We have also shown that q ⊏̸_{∼}_{ω} p and thereby q ⊏̸_{∼} p. On the other hand one may show that q ⊏_{∼}_{ω}^{f} p by showing that q ⊏_{∼}_{n}^{f} p for all n by induction.

We summarize these results of this section in the following lemma:

Lemma 4.6 ⊏_{∼}⊆⊏_{∼}_{ω}⊆⊏_{∼}_{ω}^{f} but ⊏_{∼}_{ω}^{f}⊈⊏_{∼}_{ω}⊈⊏_{∼}.

5 The Full Abstractness

In this last section we will prove the full abstractness of the model with respect to the behavioural preorder ⊏_{∼}_{ω}^{f}. As we explained in Section 2 the proof may be reduced to proving the following three properties: the finitariness of the preorder, the soundness of the proof system E_{rec}^{−ω} and the partial completeness for the proof system E_{rec} with respect to ⊏_{∼}_{ω}^{f}.

5.1 The Finitary Part of the Preorders

In this section we will define a suitable notion of a “finitary part” of a relation over processes and that of a “finitary relation”. The definition is based on the same idea as the one given in [Hen81]. The only difference is that we use syntactically compact terms in our definition whereas Hennessy uses recursionfree terms. We will then show that the preorder ⊏_{∼}_{ω}^{f} is the finitary part of the preorders ⊏_{∼} and ⊏_{∼}_{ω}^{f} and therefore that ⊏_{∼}_{ω}^{f} is finitary in our sense. We start by defining the finitary part of a relation over CCS_{L}.

Definition 5.1 For any relation R over CCS_{L} we define the finitary part of R, R^{F}, by

ctR^{F} cu iff for all Cot ∈ CoT erms, CotRct implies CotRcu.

R is finitary if R = R^{F}. □

Following [Hen81] next we will prove that on CoT erms × CCS_{L} the preorders, ⊏_{∼} and ⊏_{∼}_{ω}^{f}, coincide. Consequently they both have the same finitary part. To show this we need a measure on CoT erms that both measures the structural depth of the term and the number of values it uses. We give the following definitions. Definition 5.2 For syntactically finite terms, d, we define the structural depth, sd(d), by:

1. sd(NIL) = sd(Ω) = 0,

2. sd(μ.d) = 1 + sd(d),

3. sd(op(d_{1}, …, d_{n}) = 1 + ∑_{i=1}^{n} sd(d_{i}), op ∈ Σ,

4. sd([x]d) = sd(e, d) = 1 + sd(d),

5. sd(be ⟶ d_{1}, d_{2}) = 1 + sd(d_{1}) + sd(d_{2}).

□

From this definition we can easily derive that if cd ⟶^{μ} ct then sd(ct) ≤ sd(cd)−1. Also for all v ∈ V al, sd(d[v/x]) = sd(d) and therefore sd(([x]d)(v)) = 1 + sd(d).

The support of a compact term is the set of values the term uses in a nontrivial way. Formally this is defined as follows: Definition 5.3 The support of the term Cot ∈ CoT erms, Supp(Cot), is defined by structural recursion as:

1. Supp(NIL) = Supp(Ω) = ∅,

2. Supp(op(p_{1}, …, p_{n})) = ⋃_{i=1}^{n} Supp(p_{i}),

3. Supp(pre.t) = Supp(t),

4. Supp(e, p) = Supp(p) ∪ {[[e]]},

5. Supp([x] (x : \underline{w}_{n} ⟶ \underline{p}_{n})) = \{\underline{w}_{n}\} ∪ ⋃_{i=1}^{n} Supp(p_{i}). Note that Supp(Cot) is a finite set. We define the value-depth of Cot, vd(Cot) by vd(Cot) = min{n|Supp(Cot) ⊆ V_{n}}. □ Now we prove the following. Proposition 5.4 For all Cot ∈ CoT erms and ct ∈ CCS_{L},

Cot ⊏_{∼}_{ω}^{f} ct if and only if Cot ⊏_{∼} ct.

and therefore

(⊏_{∼}_{ω}^{f})^{F} =⊏_{∼}^{F} .

Proof As the “if” part is already known it is sufficient to prove the “only if”

part. We do this by proving the following stronger result.

For all Cot ∈ CoT erms and ct ∈ CCS_{L}

Cot ⊏_{∼}_{m}^{f} ct ⇒ Cot ⊏_{∼} ct

for all m where m ≥ m(Cot) = sd(Cot) + vd(Cot).

The proof of this statement proceeds by induction on m(Cot).

m(Cot) = 0: We have two cases: Cot = Ω, which is trivial, and Cot = NIL which we will have a further look at. Now, as NIL ↓, the definition of ⊏_{∼}_{m}^{f} implies that ct ↓. Furthermore as NIL −̸→^{μ} for all μ this is also true for ct. This proves that Cot = NIL ⊏_{∼} ct.

m(Cot) = k+1: Assume we have proved the result for all Cot′ with m(Cot′) ≤ k and we will prove that it is true for Cot where m(Cot) = k + 1. We assume that Cot ⊏_{∼}_{m}^{f} ct, where m ≥ m(Cot) = k + 1. As F(⊏_{∼}) =⊏_{∼} it is sufficient to show that CotF(⊏_{∼})ct. We proceed by case analysis on the structure of Cot.

Cot ∈ CoP roc:

1. Assume Cot ⟶^{μ} cu. By definition of ⊏_{∼}_{m}^{f}, ct ⟶^{μ} cu′ for some cu′ such that cu ⊏_{∼}_{m−1}^{f} cu′. Also, by definition of CoT erms, cu ∈ CoT erms. Now vd(cu) ≤ vd(Cot) and sd(cu) ≤ sd(Cot) − 1. Thus m − 1 ≥ k ≥ m(cu) and by the induction cu ⊏_{∼} cu′.

2. Now assume Cot ↓, by definition of the preorder ⊏_{∼}_{ω}^{f} also ct ↓. Furthermore assume that Cot ↓, ct ↓ and that ct ⟶^{μ} cu′. Then Cot ⟶^{μ} cu for some cu such that cu ⊏_{∼}_{m−1}^{f} cu′. In a similar way as before the induction implies cu ⊏_{∼} cu′, which completes the proof in this case.

Cot ∈ CoF un: Then ct and Cot have the form ct = [x]t′ where x ∈ V ar, t′ ∈ P roc and Cot = [y]t for some y ∈ V ar where t = y : \underline{w}_{n} ⟶ \underline{Cot′}_{n}, for some \underline{w}_{n} and \underline{Cot′}_{n}. Our assumption is that [y]t ⊏_{∼}_{m}^{f} [x]t′, i.e. that t[v/y] ⊏_{∼}_{m}^{f} t′[v/x] for all v ∈ V_{m}. We have to prove that [y]t ⊏_{∼} [x]t′. i.e. that t[v/y] ⊏_{∼} t′[v/x] for all v ∈ V al. This is obviously true for v ∉ \{\underline{w}_{n}\} as in that case t[v/y] ∼ Ω. So assume that v ∈ \{\underline{w}_{n}\}. As m ≥ vd(Cot), \{\underline{w}_{n}\} ⊆ V_{m}. Furthermore we know from the assumption that for all w_{i}, i ≤ n, t[w_{i}/y] ⊏_{∼}_{m}^{f} t′[w_{i}/x] and t[w_{i}/y] ∼ Cot′_{i}. This implies that Cot′_{i} ⊏_{∼}_{m}^{f} t′[w_{i}/x]. Now we have that m(Cot′_{i}) < m(Cot) = k + 1, i.e. m(Cot′_{i}) ≤ k. As m ≥ k + 1 > k ≥ m(Cot′_{i}) the induction applies and we may conclude that Cot′_{i} ⊏_{∼} t′[w_{i}/x]. Again, as Cot′_{i} ∼ t[w_{i}/x], this implies that t[w_{i}/y] ⊏_{∼} t′[w_{i}/y] as we wanted to prove.

Cot ∈ CoP air: Now Cot = Coπ = (v′, Cot′) and ct = cπ = (v′′, ct′′). By the definition of the preorder and the assumption on m, v′ = v′′ ∈ V_{m} and Cot′ ⊏_{∼}_{m}^{f} ct. As before m > k ≥ m(Cot′) and the result follows from the induction.

□

We will now show that the preorder ⊏_{∼}_{ω}^{f} is finitary and therefore that it is the finitary part of ⊏_{∼}. Again following closely [Hen81], we introduce the so called compact projections and show some of their properties. The remainder of this section is devoted to this. We adopt Abramsky’s definition of the sort of a term, t, Sort(t), as the set of channel names it uses. Definition 5.5 The sort of ct ∈ CCS_{L} is given by

1. Sort(cp) = {c ∈ Chan|cp ⟶^{a}, chan(a) = c} ∪ ⋃{Sort(cu)|∃μ.cp ⟶^{μ} cu}

2. Sort([x]t) = ⋃{Sort(t[v/x])|v ∈ V al}

3. Sort(e, cq) = Sort(cq).

□

Note that, because of our restriction to finite renamings, Sort(ct) is finite for all ct [Abr91, AH92]. Definition 5.6 [Compact Projections] We define the n-th projection of ct on CoT erms inductively as follows:

1. (a) cp^{[0]} = Ω

(b) cp^{[n+1]} = ∑{μ.ct^{[n]}|cp ⟶^{μ} ct} + {Ω|cp ↑}

2. (a) ([x]p)^{[0]} = [x]Ω (b) ([x]p)^{[n+1]} = [x]x:(v_{1}, ⋯, v_{n+1})→((p[v_{1}/x])^{[n+1]}, ⋯,(p[v_{n+1}/x])^{[n+1]})

3. (a) (v, cp)^{[0]} = (v_{1}, Ω),

(b) (v, cp)^{[n+1]} = \{ \begin{matrix}(v, cp^{[n+1]}) & if v ∈ V_{n+1} \\ (v_{n+2}, Ω) & otherwise \end{matrix} .

Note that the sum in 1.(b) only makes sense as we are summing over a finite set (up to commutativity, absorption and α-congruence). That this is the case may be proved by induction on n. □ The syntactically compact projections have the following properties: Lemma 5.7 For all ct and all n,

1. ct^{[n]} ∈ CoT erms,

2. ct^{[n]} ∼_{n}^{f} ct.

Proof

1. A simple induction on n, using a case analysis on the structure of ct for the inductive step.

2. First we prove ct ⊏_{∼}_{n}^{f} ct^{[n]} by induction on n.

n = 0 : Trivial. n = k + 1 : Let us assume that ct ⊏_{∼}_{k}^{f} ct^{[k]}. We have to prove that

ct ⊏_{∼}_{k+1}^{f} ct^{[k+1]}. We proceed by a case analysis on the structure of ct.

ct = cp ∈ CCS_{L}^{proc}:

(a) Assume cp ⟶^{μ} cu. By the definition of cp^{[i]}, cp^{[k+1]} ⟶^{μ} cu^{[k]}. From the induction we get that cu ⊏_{∼}_{k}^{f} cu^{[k]} and the first clause of the definition for ⊏_{∼}_{k+1}^{f} is met.

(b) First we note that cp ↓ if and only if cp^{[i]} ↓ for all i. Thus cp ↓ implies cp^{[k+1]} ↓. Furthermore assume that cp ↓, cp^{[k+1]} ↓

and that cp^{[k+1]} ⟶^{μ} cu′. Then cp ⟶^{μ} cu such that cu^{[k]} =

cu′. Again, by the induction, cu ⊏_{∼}_{k}^{f} cu′.

ct ∈ CCS_{L}^{pair}s, CCS_{L}^{fun}: Follows easily from the previous case.

It remains to prove that ct^{[n]} ⊏_{∼}_{n}^{f} ct. The proof of this fact is similar to the previous one and is left to the reader.

□

The following results investigate the relationship between a term, ct, and its syntactically compact projections in more detail. Lemma 5.8

1. ct^{[0]} ⊏_{∼}_{ω}^{f} ct^{[1]} ⊏_{∼}_{ω}^{f} ⋯ ⊏_{∼}_{ω}^{f} ct^{[n]} ⊏_{∼}_{ω}^{f} ⋯ ⊏_{∼}_{ω}^{f} ct

2. If ct^{[0]} ⊏_{∼}_{ω}^{f} ct^{[1]} ⊏_{∼}_{ω}^{f} ⋯ ⊏_{∼}_{ω}^{f} ct^{[n]} ⊏_{∼}_{ω}^{f} ⋯ ⊏_{∼}_{ω}^{f} cu then ct ⊏_{∼}_{ω}^{f} cu, i.e. ct is a

minimal upper bound ^{2} of the chain with respect to ⊏_{∼}_{ω}^{f}.

3. The term ct is a minimal upper bound for the set App(ct) = {Cot ∈

CoT erms|Cot ⊏_{∼}_{ω}^{f} ct} with respect to ⊏_{∼}_{ω}^{f}.

Proof

1. We first prove that for all n

ct^{[n]} ⊏_{∼}_{ω}^{f} ct^{[n+1]}.

In order to do that we prove a slightly stronger result:

∀m ≥ n. ct^{[n]} ⊏_{∼}_{m}^{f} ct^{[n+1]}.

2Note that a minimal upper bound of a preorder is unique up to the induced equivalence.

We prove this by induction on n. The base case, n = 0, is immediate as ct^{[0]} ⊏_{∼}_{m}^{f} ct^{[1]} for all m is trivial. So assume

ct^{[k]} ⊏_{∼}_{m}^{f} ct^{[k+1]} for m ≥ k

and we will prove that

ct^{[k+1]} ⊏_{∼}_{m+1}^{f} ct^{[k+2]} for m ≥ k.

We proceed by a case analysis on the form of ct.

ct = cp ∈ CCS_{L}^{proc}: Assume cp^{[k+1]} ⟶^{μ} ct, then cp ⟶^{μ} cu for some cu

such that cu^{[k]} = ct. Also cp^{[k+2]} ⟶^{μ} cu^{[k+1]} and by the induction , as m ≥ k, cu^{[k]} ⊏_{∼}_{m}^{f} cu^{[k+1]}. Thus the first condition of the definition of the preorder ⊏_{∼}_{m+1}^{f} is satisfied. We now note that cp ↓ if and only if cp^{[i]} ↓ for all i and the second condition of the definition can be met in a similar way to the first one.

ct = [x]p ∈ CCS_{L}^{fun}: By definition

([x]p)^{[i+1]} = [x]x:(v_{1}, ⋯, v_{i+1})→((p[v_{1}/x])^{[i+1]}, ⋯, (p[v_{i+1}/x])^{[i+1]})

We have to prove that

(([x]p)^{[k+1]})(v) ⊏_{∼}_{m+1}^{f} ([x]p^{[k+2]})(v)

for all v ∈ V al. First we note that for all v ∈ V_{k+1}

([x]p)^{[k+1]}(v) ∼ (p[v/x])^{[k+1]}

and

([x]p)^{[k+2]}(v) ∼ (p[v/x])^{[k+2]}.

Now the result follows from the previous case, the transitivity and the fact that ⊏_{∼}⊆⊏_{∼}_{m+1}^{f}. Otherwise if v ∉ V_{k+1} then ([x]p)^{[k+1]}(v) ∼ Ω and the result follows.

ct = (v, cp) ∈ CCS_{L}^{pair}: Similar.

Next we prove ct^{[n]} ⊏_{∼}_{ω}^{f} ct for all n. We know from Lemma 5.7 that ct^{[k]} ⊏_{∼}_{k}^{f} ct for all k. Furthermore for any m ≥ n

ct^{[n]} ⊏_{∼}_{ω}^{f} ct^{[m]} ⊏_{∼}_{m}^{f} ct.

Thus ct^{[n]} ⊏_{∼}_{m}^{f} ct for all m ≥ n which proves the statement.

2. To prove that ct is a minimal upper bound of the chain assume

ct^{[0]} ⊏_{∼}_{ω}^{f} ct^{[1]} ⊏_{∼}_{ω}^{f} ⋯ ct^{[n]} ⊏_{∼}_{ω}^{f} ⋯ ⊏_{∼}_{ω}^{f} cu.

As ct ∼_{n} ct^{[n]} this implies ct ⊏_{∼}_{n}^{f} cu for all n and therefore ct ⊏_{∼}_{ω}^{f} cu.

3. Follows from statement 1., as {ct^{[n]}|n = 1, ⋯} ⊆ App(ct).

The following theorem is a direct consequence of the lemma above. □

Theorem 5.9

1. ⊏_{∼}_{ω}^{f}= (⊏_{∼}_{ω}^{f})^{F}

2. The preorder ⊏_{∼}_{ω}^{f} is the finitary part of ⊏_{∼}, i.e. ⊏_{∼}^{F} =⊏_{∼}_{ω}^{f}.

Proof

1. That ⊏_{∼}_{ω}^{f}⊆ (⊏_{∼}_{ω}^{f})^{F} is obvious so we only have to prove the other inclusion. Thus assume

∀Cot ∈ CoT erms. Cot ⊏_{∼}_{ω}^{f} ct implies Cot ⊏_{∼}_{ω}^{f} cu.

This is equivalent to saying that App(ct) ⊆ App(cu) and the result follows from Lemma 5.8.

2. By Proposition 5.4, ⊏_{∼}^{F} = (⊏_{∼}_{ω}^{f})^{F} and the result follows from part 1. of this theorem.

□

5.2 The Partial Completeness and The Full Abstractness

This last subsection is devoted to the proof of the soundness of the proof system E_{rec}^{−ω} and the partial completeness of E_{rec} with respect to ⊏_{∼}_{ω}^{f}. We start by proving the soundness of the proof system E_{rec}^{−ω}, i.e the proof system that consists of the system E_{rec} where the ω-rule is omitted. This is the content of the following Lemma.

Lemma 5.10 (Partial Soundness) The proof system E_{rec}^{−ω} is sound with respect to the behavioural preorders ⊏_{∼} and ⊏_{∼}_{ω}^{f}.

Proof The soundness of E_{rec}^{−ω} with respect to ⊏_{∼} can be shown by proving

ct ^{⊑}_{E_{rec}^{−ω}} cu implies ct ⊏_{∼} cu

by induction on the depth of the proof tree for ct ^{⊑}_{E_{rec}^{−ω}} cu. The soundness of E_{rec}^{−ω} with respect to ^{⊑}_{ω}^{f} follows from this as ⊏_{∼}⊆⊏_{∼}_{ω}^{f} . The details of the proofs are omitted. □

Here we want to point out that the ω-rule is not sound with respect to the preorder ⊏_{∼} as shown by Example 4.1. Furthermore proving the soundness of the ω-rule for ⊏_{∼}_{ω}^{f} directly is notationally quite complicated.

Next we prove the mentioned partial completeness result, i.e. that for all Cot and ct,

Cot ⊏_{∼} ct ⇒ Cot ^{⊑}_{E_{rec}} ct

This proof follows very much the same pattern as the proof for a similar partial completeness result in [AH92]. First we introduce the notion of head normal forms and prove a corresponding normalization theorem.

Definition 5.11 A process term is said to be in a head normal form if it has the form ∑_{i} μ_{i}t_{i}.

□

Lemma 5.12 If cp ↓ then there is a head normal form, hnf(cp), such that cp =_{E_{rec}^{−ω}} hnf(cp).

Proof We prove the Lemma by induction on the length of the derivation of cp ↓ which we refer to as n. We proceed by a case analysis on the structure of cp.

n = 1 : We have the two cases: cp = NIL and cp = μ.t which both are trivial.

n = m + 1 : We proceed by structural induction on cp.

cp = NIL, μ.t: Already proven.

cp = Ω: Vacuous.

cp = cp_{1}+cp_{2}, cp_{1}\c, cp_{1}[R], be ⟶ cp_{1}, cp_{2}: Follows from the induction

and a simple use of the proof system. cp = cp_{1}|cp_{2}: By induction cp_{1} and cp_{2} have head normal forms h_{1} and h_{2}. If either h_{1} or h_{2} is NIL, the result follows from Equation (NILpar) in Figure 2. Otherwise assume

h_{1} = ∑_{i} μ_{i}.t_{i} and h_{2} = ∑_{i} γ_{i}.u_{i}.

By substitutivity and the interleaving law in Figure 3

\begin{matrix}cp =_{E_{rec}^{−ω}} cp_{1}|cp_{2} =_{E_{rec}^{−ω}} h_{1}|h_{2} =_{E_{rec}^{−ω}} \\ INT L(h_{1}, h_{2}) + COMM(h_{1}, h_{2}) \end{matrix}

where each of the summands is in a Head normal form. cp = recP.q: Then cp ↓ because q[recP.q/P] ↓. Thus by the induction q[recP.q/P] has a head normal form and the result follows from (rec) in Figure 4.

□

Here it is important that we only use the partial proof system E_{rec}^{−ω} in normalization procedure as the soundness of the ω-rule with respect to the preorder ⊏_{∼}_{ω}^{f} has not been proved yet.

Notation 5.13 Let p, q ∈ P roc and t, u ∈ T erms. To simplify the notation we will in what follows use the following convention (where abs stands for abstraction and app for application):

1. abs(t|u) for

(a) abs(p|q) = p|q

(b) abs([x]t|p) = [x](t|p)

(c) abs(p|[x]t) = [x](p|t)

(d) abs((v, p)|q) = (v, p|q) = abs(p|(v, q)

2. app(t|u) for

(a) app([x]t|(v, p)) = t[v/x]|p

(b) app((v, p)|[x]t) = p|t[v/x]

Using this notation we get that if cp ⟶^{μ} cp′ then cp|cq ⟶^{μ} abs(cp′|cq) and

cq|cp ⟶^{μ} abs(cq|cp′). Furthermore if cp ⟶^{c!} π and cq ⟶^{c?} f then cp|cq ⟶^{τ}

app(π|f) and cq|cp ⟶^{τ} app(f|π). We use this notation to formulate the following lemma:

Lemma 5.14 For all closed terms cp, cq and ct

1. (cp + μ.ct)|cq =_{E_{rec}} (cp + μ.ct)|cq + μ.abs(ct|cq)

2. cq|(cp + μ.ct) =_{E_{rec}} cq|(cp + μ.ct) + μ.abs(cq|ct)

3. (cp + a.ct)|(cq + \overline{a}.cu) =_{E_{rec}} (cp + a.ct)|(cq + \overline{a}.cu) + τ.app(ct|cu).

Proof We only prove the first statement as the second one follows by the commutativity of | and substitutivity and the third is similar and is left to the reader. First assume that cp and cq are syntactically compact. By Lemma 2.7 we may assume that they are in Ω-normal forms; cp = ∑_{i} μ_{i}.t_{i} + {Ω|cp ↑} and cq = ∑_{j} γ_{j}.u_{j} + {Ω|cq ↑}. The result now follows as an easy consequence of the interleaving law in Figure 3. Next assume that cp, cq and ct are any terms. It is easy to see that

(abs(ct|cu))^{(n)} = abs(ct^{(n)}|cu^{(n)})

for all n. Therefore we have that:

[(cp + μ.ct)|cq]^{(n)} =
(cp^{(n)} + μ.ct^{(n)})|cq^{(n)} =_{E_{rec}}
(cp^{(n)} + μ.ct^{(n)})|cq^{(n)} + μ.abs(ct^{(n)}|cq^{(n)}) =_{E_{rec}}
[(cp + μ.ct)|cq + μ.abs(ct|cq)]^{(n)}

for all n and the result follows from the ω-rule. □

Now we can prove the following useful property:

Proposition 5.15 For all cp, ct and μ we have that cp ⟶^{μ} ct implies cp =_{E_{rec}} cp + μ.ct.

Proof The proof is by induction on the length of the derivation of cp ⟶^{μ} ct. We proceed by a case analysis on the structure of cp. We only examine two cases, leaving the remaining ones to the reader.

cp = recP.u: Now cp ⟶^{μ} ct because u[recP.u/P] ⟶^{μ} ct. By induction

u[recP.u/P] =_{E_{rec}} u[recP.u/P] + μ.ct and by (rec) cp =_{E_{rec}} cp + μ.ct.

cp = cp_{1}|cp_{2}: We have three cases:

1. cp_{1} ⟶^{μ} ct_{1} and ct = abs(ct_{1}|cp_{2}): By induction

cp_{1} =_{E_{rec}} cp_{1} + μ.ct_{1}.

By the substitutivity and the first statement of Lemma 5.14, we have that

cp_{1}|cp_{2}  =_{E_{rec}}  (cp_{1} + μ.ct_{1})|cp_{2}
=_{E_{rec}}  (cp_{1} + μ.ct_{1})|cp_{2} + μ.abs(ct_{1}|cp_{2})
=_{E_{rec}}  cp_{1}|cp_{2} + μ.abs(ct_{1}|cp_{2})
= cp + μ.ct.

2. cp_{2} ⟶^{μ} ct_{2} and ct = abs(cp_{1}|ct_{2}): This can be proved in the same way as the previous case by using statement 2 of Lemma 5.14 instead of Lemma 5.14(1).

3. cp_{1} ⟶^{a} ct_{1}, cp_{2} ⟶^{\overline{a}} ct_{2}, μ = τ and ct = app(ct_{1}|ct_{2}): By induction

cp_{1} =_{E_{rec}} cp_{1} + a.ct_{1}

and

cp_{2} =_{E_{rec}} cp_{2} + \overline{a}.ct_{2}.

By statement 3 of Lemma 5.14 and substitutivity, we then have that

cp_{1}|cp_{2}  =_{E_{rec}}  (cp_{1} + a.ct_{1})|(cp_{2} + \overline{a}.ct_{2})
=_{E_{rec}}  (cp_{1} + a.ct_{1})|(cp_{2} + \overline{a}.ct_{2}) + τ.app(ct_{1}|ct_{2})
=_{E_{rec}}  cp_{1}|cp_{2} + τ.app(ct_{1}|ct_{2})
= cp + μ.ct.

□

In the following we will state and prove the promised partial completeness

result for the proof system E_{rec}.

Theorem 5.16 For all compact terms Cot and all closed terms ct

Cot ⊏_{∼}_{ω}^{f} ct  if and only if
Cot ^{⊑}_{E_{rec}} ct

Proof By Proposition 5.4 it is sufficient to prove the statement with ⊏_{∼}_{ω}^{f} replaced by ⊏_{∼} which we do as follows:.

Cot ⊏_{∼} ct implies Cot ^{⊑}_{E_{rec}} ct: It is sufficient to prove the result for Cot in Ω-normal form. The general result follows from the normalization result, Lemma 2.7, and the soundness of E with respect to ⊏_{∼}. We proceed by a case analysis on the form of Cot but only give the details of the case where Cot = Cotp ∈ CoP roc. In this case ct = cp ∈ CCS_{L}^{proc}.

So assume np ⊏_{∼} cp where np is an Ω-normal form and we will prove that np ^{⊑}_{E_{rec}} cp. The proof proceeds by induction on sd(np), the structural depth of np defined in Definition 5.2. So assume the theorem is true for all np′ with sd(np′) ≤ k and that sd(np) = k + 1. We proceed by a case analysis on the form of np.

np = NIL + Ω: Then np =_{E_{rec}} Ω ^{⊑}_{E_{rec}} cp. np = NIL: NIL ⊏_{∼} cp implies cp ↓. Thus cp has a head normal form

h(cp) with h(cp) =_{E_{rec}^{−ω}} cp. As NIL −̸→^{μ} then h(cp) −̸→^{μ} for all μ

which implies that h(cp) = NIL. Therefore np =_{E_{rec}} h(cp) =_{E_{rec}} cp. np = ∑_{i} μ_{i}.cp_{i}{+Ω}: We prove this case in three steps.

1. cp + np ^{⊑}_{E_{rec}} cp: Assume np ⟶^{μ} cp′ then μ = μ_{i} and cp′ = cp_{i}

for some i. As np ⊏_{∼} cp this implies that cp ⟶^{μ_{i}} cq_{i} where cp_{i} ⊏_{∼} cq_{i}. By applying induction we have that cp_{i} ^{⊑}_{E_{rec}} cq_{i} and, by substitutivity, that μ_{i}.cp_{i} ^{⊑}_{E_{rec}} μ_{i}.cq_{i}. Thus by substitutivity and Proposition 5.15

cp + μ_{i}.cp_{i} ^{⊑}_{E_{rec}} cp + μ_{i}.cq_{i} =_{E_{rec}} cp.

Repeated use of this result, substitutivity and transitivity implies cp + np ^{⊑}_{E_{rec}} cp.

2. np ^{⊑}_{E_{rec}} cp + np: If Ω is a summand of np then np ^{⊑}_{E_{rec}} np + Ω ^{⊑}_{E_{rec}} np + cp. So assume that np ↓. As np ⊏_{∼} cp this implies cp ↓ and therefore that cp has a head normal form cp =_{E_{rec}^{−ω}} h(cp) = ∑_{j} γ_{j}.cq_{j}. As the proof system E_{rec}^{−ω} is sound with respect to ⊏_{∼} then np ⊏_{∼} h(cp). Thus cp ⟶^{γ_{j}} cq_{j} implies that

γ_{j} = μ_{i_{j}} for some i_{J} and that np ⟶^{μ_{i_{j}}} cp_{i_{j}} for some cp_{i_{j}} such that cp_{i_{j}} ⊏_{∼} cq_{j}. Now by proceeding in a similar way as in the previous case we get that

np = np + ∑_{j} μ_{i_{j}}.cp_{i_{j}} ^{⊑}_{E_{rec}} np + ∑_{j} γ_{j}.cq_{j} ^{⊑}_{E_{rec}} np + cp.

3. Finally 1. and 2. imply np ^{⊑}_{E_{rec}} cp.

Cot ^{⊑}_{E_{rec}} cp implies Cot ⊏_{∼}_{ω}^{f} cp: By Corollary 2.8 we get that Cot ^{⊑}_{E_{rec}^{−ω}} cp and the result follows from the soundness of E_{rec}^{−ω} with respect to the preorder ⊑_{ω}^{f}, stated in Lemma 5.10.

□

We are now ready to prove the main result of this section, namely the full ab-

stractness of the denotational semantics with respect to the finitary behavioural semantics based on the preorder ⊏_{∼}_{ω}^{f}. This is the content of the following theorem.

Theorem 5.17 (Full Abstractness) For all closed terms, ct and cu, in CCS_{L}

ct ⊏_{∼}_{ω}^{f} cu if and only if ct ^{⊑}_{E_{rec}} cu if and only if \overline{ACT}[[ct]] ^{⊑} \overline{ACT}[[cu]].

Proof The first equivalence follows from Theorem 2.9 as the conditions of the theorem are ensure by Theorem 5.9, Lemma 5.10 and Theorem 5.16. The second one follows from the soundness and the completeness of the proof system with respect to the model stated in Theorem 2.5. □

6 Conclusion

In this last section we will give a summary of the main result of this sequel of two papers and suggest some directions for further work.

6.1 Summary of Results

In the first paper of this sequel of two paper we defined a general syntax for value passing processes which reflects the late semantic approach. We also gave a general class of denotational models to describe the semantics of languages defined by the general syntactic class. Furthermore we defined a concrete language, CCS_{L} which is a direct extension of the standard CCS by adding values to the language following the late semantic approach. We then defined a concrete denotational model which is a instantiation of the general class of models. This model is a direct extension of the one given for the pure language SCCS by Abramsky in [Abr91] and a slight modification of the model defined by Milne and Milner in [MM79]. We finish the paper by defining a proof system based on a set of inequation and proof its soundness and completeness with respect to the denotational model model.

In this second paper of the sequel the main focus is on giving a Plotkin style operational semantics [Plo81], and a suitable extension of the standard strong prebisimulation [Hen81, Wal90] to take value-passing based on the late approach into account. Thus we introduce the notion of applicative labelled transition system and the related notion of strong applicative bisimulation. One of the main purposes with this second paper is to make the semantic description of the language CCS_{L} more complete by giving an operational characterization of the preorder derived from the denotational model defined in [Ing95]. Therefore we introduce a suitable notion of a finitary part of a relation and a finitary relation over CCS_{L} processes. Then we define a value-finite version of the strong applicative ω-bisimulation preorder and show that it is finitary in our sense and is exactly the finitary part of the strong applicative bisimulation preorder. Finally we show the soundness and completeness of the proof system with respect to the value finite strong ω-bisimulation preorder. The full abstractness of the denotational semantics with respect to the value finite strong ω-bisimulation preorder follows directly from this and the soundness and the completeness of the proof system with respect to the denotational semantics.

6.2 Future Work

The results in these papers may be extended in several directions. In the following we will give some examples.

1. Giving a similar semantic description of a CCS-like language with focus on the early semantic approach.

2. Extending the theory to the notion of weak bisimulation preorder and observational congruence.

3. Extending the theory to higher order calculi.

4. Applying symbolic methods to the applicative prebisimulation.

References

[Abr90] S. Abramsky. The lazy lambda calculus. In D. Turner, editor, Research Topics in Functional Programming, pages 65–117. Addison-Wesley, 1990.

[Abr91] S. Abramsky. A domain equation for bisimulation. Information and Computation, 92:161–218, 1991.

[AH92] L. Aceto and M. Hennessy. Termination, deadlock and divergence. Journal of the ACM, 39(1):147–187, January 1992.

[Hen81] M. Hennessy. A term model for synchronous processes. Information and Computation, 51(1):58–75, 1981.

[Hen88] M. Hennessy. Algebraic Theory of Processes. MIT Press, Cambridge, Massachusetts, 1988.

[HI93] M. Hennessy and A. Ingólfsdóttir. A theory of communicating processes with value-passing. Information and Computation, 107(2):202– 236, 1993.

[HP80] M. Hennessy and G.D. Plotkin. A term model for CCS. In P. Dembiński, editor, 9^{th} Symposium on Mathematical Foundations of Computer Science, volume 88 of Lecture Notes in Computer Science, pages 261–274. Springer-Verlag, 1980.

[Ing95] A. Ingólfsdóttir. A semantic theory for value-passing processes late approach — Part I: A denotational model and its complete axiomatization. Report RS–95–3, brics, Institute for Electronic Systems, Department of Mathematics and Computer Science, Aalborg University Centre, 1995.

[Mil83] R. Milner. Calculi for synchrony and asynchrony. Theoretical Computer Science, 25:267–310, 1983.

[MM79] G. Milne and R. Milner. Concurrent processes and their syntax. Journal of the ACM, 26(2):302–321, 1979.

[Par81] D.M.R. Park. Concurrency and automata on infinite sequences. In P. Deussen, editor, 5^{th} GI Conference, volume 104 of Lecture Notes in Computer Science, pages 167–183. Springer-Verlag, 1981.

[Plo81] G.D. Plotkin. A structural approach to operational semantics. Report DAIMI FN-19, Computer Science Department, Aarhus University, 1981.

[Tar55] A. Tarski. A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics, 5, 1955.

[Wal90] D.J. Walker. Bisimulation and divergence. Information and Computation, 85(2):202–241, 1990.

Recent Publications in the BRICS Report Series

RS-95-22 Anna Ing� olfsd� ottir. A Semantic Theory for Value�Passing Processes, Late Approach, Part II: A Behavioural Semantics and Full Abstractness. April 1995. 33 pp.

RS-95-21 Jesper G. Henriksen, Ole J. L. Jensen, Michael E. J�rgensen, Nils Klarlund, Robert Paige, Theis Rauhe, and Anders B. Sandholm. MONA: Monadic Second-Order Logic in Practice. May 1995. 17 pp.

RS-95-20 Anders Kock. The Constructive Lift Monad. March 1995. 18 pp.

RS-95-19 Franc�ois Laroussinie and Kim G. Larsen. Compositional Model Checking of Real Time Systems. March 1995. 20 pp.

RS-95-18 Allan Cheng. Complexity Results for Model Checking. February 1995. 18pp.

RS-95-17 Jari Koistinen, Nils Klarlund, and Michael I. Schwartzbach. Design Architectures through Category Constraints. February 1995. 19 pp.

RS-95-16 Dany Breslauer and Ramesh Hariharan. Optimal Parallel Construction of Minimal Suf�x and Factor Automata. February 1995. 9 pp.

RS-95-15 Devdatt P. Dubhashi, Grammati E. Pantziou, Paul G. Spirakis, and Christos D. Zaroliagis. The Fourth Moment in Luby’s Distribution. February 1995. 10 pp. To appear in Theoretical Computer Science.

RS-95-14 Devdatt P. Dubhashi. Inclusion�Exclusion(3) Implies Inclusion�Exclusion(n). February 1995. 6 pp.

RS-95-13 Torben Bra� uner. The Girard Translation Extended with Recursion. 1995. Full version of paper to appear in Proceedings of CSL ’94, LNCS, 1995.

RS-95-12 Gerth St�lting Brodal. Fast Meldable Priority Queues. February 1995. 12 pp.