BRICS RS-03-15 A. Ingólfsdóttir: A Semantic Theory for Value–Passing Processes Based on the Late Approach BRICS

Basic Research in Computer Science

A Semantic Theory for Value–Passing Processes Based on the Late Approach

Anna Ingólfsdóttir

BRICS Report Series RS-03-15 ISSN 0909-0878 March 2003 Copyright \begin{matrix}c \\ ◯ \end{matrix} 2003, Anna Ingólfsdóttir.

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 BRICS Report Series publications. 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@brics.dk

BRICS publications are in general accessible through the World Wide Web and anonymous FTP through these URLs:

http://www.brics.dk
ftp://ftp.brics.dk

This document in subdirectory RS/03/15/

A Semantic Theory for Value–Passing Processes Based on the Late Approach

Anna Ingólfsdóttir

BRICS^{∗}

Department of Computer Science Aalborg University, Denmark

Abstract

A general class of languages for value-passing calculi based on the late semantic approach is defined and a concrete instantiation of the general syntax is given. This is a modification of the standard CCS according to the late approach. Three kinds of semantics are given for this language. First a Plotkin style operational semantics by means of an applicative labelled transition system is introduced. This is a modification of the standard labelled transition system that caters for value-passing according to the late approach. As an abstraction, late bisimulation preorder is given. Then a general class of denotational models for the late semantics is defined. A denotational model for the concrete language is given as an instantiation of the general class. Two equationally based proof systems are defined. The first one, which is value-finitary, i. e. only reasons about a finite number of values at each time, is shown to be sound and complete with respect to this model. The second proof system, a value-infinitary one, is shown to be sound with respect to the model, whereas the completeness is proven later. The operational and the denotational semantics are compared and it is shown that the bisimulation preorder is finer than the preorder induced by the denotational model. We also show that in general the ω-bisimulation preorder is strictly included in the model induced preorder. Finally a value-finitary version of the bisimulation preorder is defined and the full abstractness of the denotational model with respect to it is shown. It is also shown that for C CS_{L} the ω-bisimulation preorder coincides with the preorder induced by the model. From this we can conclude that if we allow for parameterized recursion in our language, we may express processes which coincide in any algebraic domain but are distinguished by the ω-bisimulation. This shows that if we extend C CS_{L} in this way we obtain a strictly more expressive language.

1 Introduction

In the original work of Milner on CCS [Mil80] and Hoare on CSP [Hoa78], processes are allowed to exchange data in communications. In these original calculi the value-passing calculus is interpreted in terms of the pure calculus in which communication is pure synchronization. A process which is ready to input a value on a channel c (e. g. a prefixing with an input action, c?x.p) is interpreted as a non-deterministic choice between pure terms of the form c_{v}.p[v/x], where v ranges over the set of possible values, which in many cases is infinite. In this approach, two processes that synchronize are both supposed to know each other’s channel and value, i.e. the data variable is instantiated by the potential input values already when the process reports the willingness or ability to communicate on the channel c.

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

In more recent work on the π-calculus [MPW92] this semantic approach is referred to as early semantics due to the early instantiation of the data variables as described above. Its counterpart, the late semantics, is also introduced in the same reference. Here the idea is that the processes only synchronize on the channel name and that the input process has to accept whatever value the output process has to offer. This may be interpreted as if the result of the instantiation of the data variable is delayed until the process has received the value. The input process reports the willingness to receive a value on a channel c by performing an action of the form c? and thereby evolving to a function which waits for the value the output counterpart in the communication provides. Symmetrically the result of reporting the willingness to output an uninterpreted value on the channel c is given by the action c!. By performing this action the process evolves to a term which basically consists of a data expression, i.e. the expression whose value the sender wants to output, and a process expression, i.e. what remains to be executed of the sender.

In a more recent version of the π-calculus, the Polyadic π-calculus presented in [Mil91], the outcomes of input and output actions are modelled by extending the syntax with the new constructions abstractions and concretions. The semantics for Thomsen’s plain CHOCS in [Tho89] is based on the late approach although the author does not use that terminology.

In the literature the late semantic approach has been investigated in different ways, both in connection with the π-calculus and higher order calculi (see e.g. [MPW91, Hen94, San93]) and also with the main focus on the simpler case where only first order values are allowed (see e.g. [HL93a, HL93b, Ing93]). In this paper we will aim at contributing to the studies of the late semantics of communicating processes. We will concentrate on processes which allow for transmission of simple values only. Of course studying value-passing processes is interesting in itself, but we also believe that it may give some insight into the nature of the semantics of value passing processes, in particular the late semantic approach, which may be useful in future studies of the semantics of the more complicated calculi of higher order or mobile processes (such as the π-calculus).

In order to make our studies more complete, rather than giving only one type of semantics, we follow the line of [Hen88a] and [HI93] and introduce a trinity of semantic descriptions for a CCS like process language and show how they relate to one another. More precisely, first we put forward an operational or behavioural semantics in terms of an extended version of labelled transition systems and corresponding bisimulation based relations. Then we give a denotational semantics following the Scott-Strachey approach, and axiomatic semantics by means of equationally based proof systems. Like many researchers in the area of process algebra we believe that the operational or the behavioural semantic model is the most natural and intuitive one, but that different kinds of semantic descriptions give important alternative views of the nature of the interpretation of process languages. For instance the interpretation of an infinite process, modelled by an algebraic cpo, is fully specified by the interpretation of its finitely computable approximations. This is not the case for many behaviourally based semantics as will be explained in more detail later.

We start the study of the late semantic approach by defining a general class of syntax for languages that support this approach. To this end we extend the standard notion of a signature Σ, a set of syntactic operators, to that of applicative signature (Σ, C) where Σ is a signature in the original sense and C is a set of channel names. Then we define a concrete language Late-CCS (CCS_{L}) by instantiating the general applicative signature (Σ, C). This language is a slight modification of the standard CCS where the syntax is basically the same as for the Polyadic π-calculus although we use a slightly different notation and only allow for the transmission of simple values in communications. Then 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. 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 modelled by the bottom element of the domain and is syntactically denoted by the constant Ω. 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].

To reflect the late approach, the operational semantics is 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]. To this end we first introduce the notion of strong applicative prebisimulation and the corresponding strong applicative bisimulation preorder. Following standard practice this preorder is obtained as the largest fixed point of a suitably defined monotonic functional.

Next we define a general framework for denotational semantics for value-passing processes using the late principle. For this purpose we introduce the general class of applicative (Σ, C)- domains to model the semantics of the (Σ, C)-terms. These are a direct generalization of Σ-domains originally introduced in [GTWW77] and used for instance in [Hen88a] to model a pure calculus. In the denotational interpretation of a language in terms of a (Σ, C)-domain, the idea of the late semantic approach is made explicit; the outcome of an input action is modelled as a function which takes a value as an argument and returns an element of the model, i.e. a process, whereas the outcome of an output action is modelled by a pair consisting of the output value and the resulting process.

After having defined our general class of models, we will modify the definition of evaluation mapping, i.e. the unique mapping from the process algebra into the domain known from the theory for pure processes. As we want to be able to reason about a subset of the process algebra, we extend the definition slightly. For this purpose we introduce the notion of recursively closed subsets of a process algebra. This extension of the definition allows us to reason about the compact elements of an algebraic cpo at the syntactic level by means of structural induction. This enables us to take advantage of the notion of algebraicity when comparing the semantics defined by the model to other kinds of semantics such as behavioural or axiomatic semantics.

Then we define a concrete denotational model for CCS_{L}, the domain of Applicative Communication Trees (ACT) as an instantiation of the general class of (Σ, C)-domains, where Σ is the signature consisting of the operators of CCS_{L}. The model ACT is obtained by defining a preorder K, which acts as a representation of the compact elements of the complete model. Then we define the operators of Σ and C as monotonic functions over this preorder. Finally we apply a general result (that, for instance, can be found in [Hen88a]) that says that a preorder with monotonic operators induces a unique structure consisting of the algebraic cpo obtained as completion by ideals of the preorder and the corresponding unique continuous extension of the operators.

By defining the operators in this way, i.e. first as monotonic endofunctions on the preorder that represents the compact elements and then extending them in a continuous way to the whole domain, we ensure that they preserve compactness. By this we mean that the result of applying an operator to a compact element is again a compact element. From an intuitive point of view this is an important property; the compact elements represent the finitely computable elements of the domain so if we expect an operator op to be finitely computable, applying it to something finitely computable should again result in something finitely computable. Note that this property is not automatically satisfied in an applicative (Σ, C)-domain, or even a Σ-domain, as a continuous function does not necessarily map a compact element into a compact element.

The definition of our model is motivated by the following models that have been studied in the literature. In 1979, Milne and Milner [MM79] gave a domain theoretical definition of the concept of communicating processes. This definition reflects the late semantic approach described above. Each process has a collection of typed ports through which it may communicate with other processes. There are two types of communications: input and output. If we abstract away from the types of the possible values then the input capability of a process p along a channel c is modelled as an element of the domain V ⟶ P labelled by the channel name c, where the domain of processes is denoted by the cpo P and the domain of values by V. An output capability of p on c, on the other hand, is modelled as an element of V × P labelled by c. A process is modelled as a set of communication capabilities or more precisely as an element of the Smyth Power Domain [Smy78] over the domain of communication capabilities. The empty set is embedded into the domain in such a way that it becomes the top element of the domain. This leads to a recursive domain equation over a suitable class of domains. The domain of processes is then defined as the initial solution to this equation.

In [Abr91] Abramsky pointed out a disadvantage of this model: The use of the Smyth Power Domain to model communicating processes rules out the possibility of any correspondence with bisimulation as it only compares the processes in one direction, i. e. if the process p is smaller than the process q in the preorder then q simulates p, given that p is convergent, but not necessarily the other way around. Also the embedding of the empty set, which corresponds to the inactive and convergent process nil as the top element of the model, is intuitively incorrect as in the bisimulation based semantics, this process is not related to anything but itself and the inactive divergent process Ω. In the same reference the author defined a model to describe the semantics of pure processes. This model is similar to the model of [MM79] and is also obtained as the initial solution to a recursive domain equation. The main difference is that Abramsky, instead of the Smyth Power Domain, defined his model in terms of the Plotkin Power Domain which is based on comparison both ways; p is smaller than q if q simulates p and, in the case when p converges, p simulates q too. He added the empty set to the model as an isolated element only comparable with itself and the bottom element of the model in the obvious way. This also corresponds to the bisimulation interpretation of the process nil. Abramsky then interpreted the calculus SCCS in the model and showed the full abstractness of this interpretation with respect to a bisimulation based preorder.

In the paper we show that the model we define is basically the one presented in [MM79] where the modifications of Abramsky’s are adopted. Thus we define a model which describes value-passing based on the late approach as a solution to a recursive domain equation using the Plotkin Power Domain but with the empty set adjoined as an isolated element. Then we give an explicit representation of the compact elements of the solution by unfolding the recursive definition and show that it coincides with the preorder K. This in turn implies that the two domains we have defined so-far in two different ways are isomorphic.

The definition of the denotational model supports in a natural way systems of equations and inference rules. We define two such proof systems and prove their soundness and completeness with respect to the model. The two system are based on the same set of equations and only differ in the way the infinite terms are dealt with. In the first one, the value-finitary one, we make an extensive use of the ω-algebraicity of the model and say that t is provably smaller than u, written t ^{⊑} u, if t^{(n)} ^{⊑} u can be proven for all n where t^{(n)} is a compact approximation of t, i. e. t^{(n)} is a syntactically finite term that that only reasons about the first n values of the value space (which we take to be countable) and is interpreted as a compact element in the model. Then the ω-algebraicity of the model, together with the fact that the operators preserve compactness, enables us to reduce the proof of completeness and soundness of this proof system to a proof of the same property for the sublanguage which denotes exactly the compact elements of the model.

The second proof system, the value-infinitary one, is maybe more standard and is obtained from the first one by replacing the compact approximations t^{(n)} by the usual syntactic approximations t^{n} which may involve reasoning about an infinite number of values and are therefore not necessarily interpreted as compact elements in the model. The soundness of this system is obvious as it is weaker than the previous one. To prove the completeness, on the other hand, turns out to be more complicated and is in the paper postponed until the operational semantics is investigated. This will be explained later in this introduction.

Our next task is to compare the behavioural and the denotational semantics. One of the results in the pure case presented in [Abr91] is that the denotational model given in that reference is not fully abstract 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 cannot be said about the bisimulation preorder. In fact we need experiments of infinite depth and width 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 cannot be expected to be modelled by an algebraic cpo given that the compact elements are denotable by syntactically finite elements.

In [Hen81] Hennessy defined a term model for SCCS. This model is ω-algebraic and, as expected, fails to be fully abstract with respect to the strong bisimulation preorder. In the same reference 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. The “finitary part” of the bisimulation preorder is in [Abr91] referred to as the “finitely observable part” of the preorder. In both [Hen81] and [Abr91] the full abstractness of the respective denotational semantics with respect to ⊏_{∼}^{F} are 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.

We show by an example that the bisimulation 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 for applicative labelled transition systems in the standard way by iterative application of the functional that induces the bisimulation preorder. This gives as a result a ⊏_{∼}_{ω} preorder which in general is still too fine to match the preorder induced by the denotational model. This we demonstrate by an example given in a language which is a slight extension of our example language as it allows parameterized recursive definitions. Intuitively the reason for this mismatch is that we still need infinite experiments to decide the operational preorder, now because of an infinite breadth as an infinite number of values might need to be observed. In other words, the preorder of the model is value-finitary whereas the preorder ⊏_{∼}_{ω} is not.

By an example, given in the language C CS_{L} extended with parameterized recursion, we show that, considered on the class of applicative labelled transition systems, the behavioural preorder ^{⊑}_{ω} and a preorder induced by any algebraic cpo cannot coincide.

Motivated by the observations above we give a suitable definition of the notion of the “finitary part”, which we refer to as the emvalue-finitary part, of the bisimulation preorder to meet the preorder induced by the denotational model. We define the so-called compact terms as the syntactically finite terms which only test and use a finite number of values. We also show 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 value-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 a similar 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 aforementioned reference [Hen81]. We also prove that the value-infinitary proof system, i. e. the one based on the syntactically finite approximations is complete with respect to the preorder ⊏_{∼}_{ω}. Finally we compare the valuefinitary and the value-infinitary semantics over our example language C CS_{L} by proving that the ω-bisimulation preorder ⊏_{∼}_{ω} coincides with the preorder from the model. Thus we have proven that all the semantic preorders we have considered so far, apart from the bisimulation preorder ⊏_{∼}, coincide over this language.

As pointed out above, the example that shows that the preorder ⊏_{∼}_{ω} in general does not coincide with the preorder induced by the denotational model, is given in the language C CS_{L} extended in such a way that recursive definitions can be parameterized over value expressions. The reasoning above shows that this extended language is strictly more expressive than the original one.

The structure of the paper is as follows: In Section 2 we define a general syntax for valuepassing languages that support the late semantic approach. The definition of the operational semantics and the notion of applicative bisimulation are the subject of Section 3. In Section 4 we define the general class of (Σ, C)-domains and our concrete denotational model. In Section 5 we give a equationally based value-finitary proof system and prove its soundness and completeness with respect to the model. We also define a value-infinitary version of the system and prove that it is sound with respect to the model. Section 6 contains two examples that distinguishes the preorder^{⊑}\overline{ACT} from ⊏_{∼} and ⊏_{∼}_{ω} respectively. These examples are followed up by the definition of the value-finitary preorder ⊏_{∼}_{ω}^{f}. In Section 7 we give a definition of the notion of the value-finitary part of a relation and a value-finitary relation over processes. In the same section we prove that the preorder ⊏_{∼}_{ω}^{f} is value-finitary and that it coincides with the value-finitary part of the preorder ⊏_{∼}. Then we prove the soundness and the completeness of the value-finitary proof system with respect to the value-finitary bisimulation preorder ⊏_{∼}_{ω}^{f} and of the value-infinitary system with respect to ⊏_{∼}_{ω}. Finally we prove that the model is fully abstract with respect to ⊏_{∼}_{ω}, i. e. that the preorder from the model coincides with ⊏_{∼}_{ω}. From this we can conclude that all five preorders mentioned above coincide. In Section 8 we give some concluding remarks.

2 Syntax

In this section we will 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. To this end we introduce 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.

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, unordered 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, with the only values T (true) and F (false). 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]]σ. Furthermore we preassume an infinite set of process names PN, ranged over by P, Q, etc, to be used in recursively defined terms. The set of (Σ, C)-terms is given as the triplet

T_{(Σ,C)} = (T_{(Σ,C)}^{proc}, T_{(Σ,C)}^{fun}, T_{(Σ,C)}^{pair})

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

\begin{matrix}T_{(Σ,C)}^{proc} : & p ::= op(\underline{p}), op ∈ Σ c?.f c!.o τ.p be → p, p′, \\ T_{(Σ,C)}^{fun} : & f ::= [x]p, \\ T_{(Σ,C)}^{pair} : & o ::= (e, p), \end{matrix}

where we use the notation \underline{p} to denote a vector of terms in T_{(Σ,C)}^{proc} of a suitable length. We let t

range over the union of these three categories and f and o over T_{(Σ,C)}^{fun} and T_{(Σ,C)}^{pair} respectively. To express recursive or infinite processes we add the process names in PN, ranged over by P, and the recursive binding recP. , to the syntax and write T_{(Σ,C)}^{rec}(P N) for the resulting triplet of (Σ, C)-terms.

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 μ. The structure of this syntax is basically the same as the one suggested by Milner in [Mil91] although the notation is slightly different. The action of inputting on channel c is given by c? whereas the action of outputting on that channel is given by c!. The function terms are of the form [x]p, where x is a data variable and p a process term. These correspond to the abstractions in the aforementioned reference. The input prefixing becomes c?.[x]p. The pair terms are of the form (e, p), where e is a data expression and p a process term. These correspond to the concretions in [Mil91]. The output prefixing becomes c!.(e, p). We also assume that we have a set of operators Σ, which is supposed to contain at least the symbol Ω to model the divergent or completely unspecified process. The processes are obtained by the input and output prefixing just described, prefixing with the silent action τ and by applying the operators in Σ. We use the notation be ⟶ p, p′ to denote the standard conditional choice usually written as “If be then p else p′ ”.

Prefixing by [x] binds the data variable x and the recP. construct is a binding construct for the process name P. 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 recP. . We shall mainly be concerned with expressions which contain no free occurrences of value variables. We denote the set of all value closed terms, process terms, functions terms and pair terms by T_{(Σ,C)}(P N), T_{(Σ,C)}^{proc}(P N), T_{(Σ,C)}^{fun}(P N) and T_{(Σ,C)}^{pair}(P N) respectively. These will be referred to as processes, functions and pairs ranged over by p, f and o. We assume a notion of substitution for both data variables and process names in terms defined in the usual way.

The language C CS_{L} = (C CS_{L}^{proc}, C CS_{L}^{fun}, C CS_{L}^{pair}) (Late-CCS), ranged over by t, p, f, o respectively, is obtained by taking Σ as {nil, Ω, +, |}∪{ R|R ∈ Ren}∪{−\c|c ∈ Chan} where Ren is the set of finite^{1} permutations of Chan (the set PN is not indicated and is implicitly assumed to be known). The process nil is the convergent, inactive process, Ω is the completely unspecified or divergent one, p+q is a nondeterministic choice between p and q, p|q is a parallel composition of p, q, p[R], p renamed by R, stands for the process p with its channels renamed by R and p\c, p restricted on c, behaves like p apart from not being allowed to communicate on channel c. The corresponding closed terms CCS_{L} = (CCS_{L}^{proc}, CCS_{L}^{fun}, CCS_{L}^{pair}) are again ranged over by t, p, o, f respectively. We let d range over syntactically finite or recursion free closed terms. Note that f = [x]p can be considered as a function by using the convention f(v) = ([x]p)(v) = p[v/x] where v ∈ V al.

In the theory to follow we will make an extensive use of the fact that the value domain V al is countable and can therefore be written as V al = {v_{1}, v_{2}, v_{3}, …, }. By defining V_{n} = {v_{1}, …, v_{n}} we get that V al = ⋃_{n} V_{n}. From now on V_{n} will have this meaning.

1This restriction is of technical reasons which are not going to be explained further here.

3 Operational Semantics

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 consisting of the value and the resulting process.

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 air} ⊎ Act_{F un} is a set of actions,

• ⟶ is a transition relation

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

• ↓⊆ Con is a convergence predicate.

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

Now we will define the so-called strong applicative prebisimulation (sa-prebisimulation) 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), ⊆ ⟩. For this purpose we extend our notion of relations over configuration so they apply to states. 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 types 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.

□ 9

Obviously F defined in 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 Section 2, where, as pointed out before, CCS_{L}^{fun} may be considered as a subset of V al ⟶ CCS_{L}^{proc}. We let ⟶ be the least transition relation closed under the rules of Figure 1 and the convergence predicate ↓ to be the least relation on CCS_{L}^{proc} satisfying the rules in Figure 2. 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, the one for output is c!.(v, q) ⟶^{c!} (v, q) and that for communication expresses the fact that synchronization takes the form of functions application:

\frac{p ⟶^{c?} f, q ⟶^{c!} (v, q′)}{p|q ⟶^{τ} f(v)|q′} .

As an example of an application of the inference rules, let us have a look at the processes given by Ω and recP.P. By inspection of the rules it is not difficult to see that neither of them can be proven to be convergent which means that they both are divergent. Furthermore we can also see that neither of them can perform any action and therefore they must be equivalent according to the late strong bisimulation semantics.

The bisimulation preorder ⊏_{∼} defined on the ALT S as described above satisfies:

Theorem 3.5

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

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

(input) c?.f ⟶^{c?} f
(output) c!.(e, p) ⟶^{c!} (v, p), [[e]] = v
(tau)  τ.p ⟶^{τ} p

(ren)  \frac{p ⟶^{c?} [x]p′}{p[R] ⟶^{R(c)?} [x](p′[R])}

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

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

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

\frac{p ⟶^{c!} (v, p′)}{p\c′ ⟶^{c!} (v, p′\c′)}, c ≠ c′

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

(choice) \frac{p ⟶^{μ} ct}{p + q ⟶^{μ} ct}

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

\frac{p ⟶^{c!} (v, p′)}{p | q ⟶^{c!} (v, p′ | q)}

\frac{p ⟶^{τ} p′}{p | q ⟶^{τ} p′ | q}

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

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

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

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

Figure 1: Operational semantics for CCS_{L}; (choice), (par) and (com) have symmetric counterparts.

\overline{nil ↓} \frac{p ↓, p′ ↓}{p + p′ ↓} \frac{p ↓, p′ ↓}{p | p′ ↓} \frac{p ↓}{p\c ↓} \frac{p ↓}{p[R] ↓} \frac{p[Ω/P] ↓}{recP.p ↓}

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

Figure 2: The convergence predicate (b) For all c ∈ Chan and o_{1}, o_{2}, o_{1} ⊏_{∼} o_{2} implies c!.o_{1} ⊏_{∼} c!.o_{2}.

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

3. (a) For all p_{1}, p_{2} ∈ C CS_{L}^{proc} with {y|y free value-variable in p_{1}, p_{2}} ⊆ {x}, whenever

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

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

Proof

1. We have to prove that for any operator op ∈ Σ, \underline{p} ⊏_{∼} \underline{q} ⇒ op(\underline{p}) ⊏_{∼} op(\underline{q}). We will only prove the statement for the case op = | , leaving the remaining cases to the interested reader to check. So assume p_{1} ⊏_{∼} p_{2} and q_{1} ⊏_{∼} q_{2}. This means that there are sa-prebisimulations R_{p} and R_{q} such that (p_{1}, p_{2}) ∈ R_{p} and (q_{1}, q_{2}) ∈ R_{q}. We define

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

As (p_{1}|q_{1}, p_{2}|q_{2}) ∈ R_{p}|R_{q} it is sufficient to show that R_{p}|R_{q} is a sa-prebisimulation. To prove this we proceed as follows:

(a) Assume that (p′_{1}|q′_{1}, p′_{2}|q′_{2}) ∈ R_{p}|R_{q} and that p′_{1}|q′_{1} ⟶^{μ} r_{1}. We only consider the following cases:

i. μ = c?, p′_{1} ⟶^{c?} [x]p′′_{1} and r_{1} = [x](p′′_{1}|q′_{1}). Now there is a [y]p′′_{2} where p′_{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 q′_{1} and q′_{2} do not contain free value-variables this implies that for all v ∈ V al

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

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

ii. μ = τ, p′_{1} ⟶^{c?} [x]p′′_{1}, q′_{1} ⟶^{c!} (v, q′′_{1}) and r_{1} = p′′_{1}[v/x]|q′′_{1}. Then p′_{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 q′_{2} ⟶^{c!} (v′, q′′_{2}) where ((v, q′′_{1}), (v′, q′′_{2}) ∈ R_{q}^{pair}, i.e. where v = v′ and (q′′_{1}, q′′_{2}) ∈ R_{q}. This implies that (p′′_{1}[v/x]|q′′_{1}, p′′_{2}[v/y]|q′′_{2}) ∈ R_{p}|R_{q}.

Furthermore p′_{2}|q′_{2} ⟶^{τ} p′′_{2}[v/y]|q′′_{2}.

(b) Next assume that p′_{1}|q′_{1} ↓. This implies that p′_{1} ↓ and q′_{1} ↓ and therefore that p′_{2} ↓ and q′_{2} ↓. This in turn implies that p′_{2}|q′_{2} ↓. Now assume that p′_{1}|q′_{1} ↓, p′_{2}|q′_{2} ↓ and p′_{2}|q′_{2} ⟶^{μ} r_{2}. In the same way as in (a) we may show that p′_{1}|q′_{1} ⟶^{μ} r_{1} for some r_{1} such that (r_{1}, r_{2}) ∈ R_{p}|R_{q}.

2. Here we will only prove the last case, i.e. that f_{1} ⊏_{∼} f_{2} implies c?.f_{1} ⊏_{∼} c?.f_{2}. So assume that f_{1} = [x]p and f_{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?.[x]p, c?.[y]q)}. 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 Con to V al ⟶ Con and V al × Con in the case when Con = C CS_{L}^{proc}.

□

4 Denotational Semantics

In the previous section we extended the standard notion of a signature Σ to that of applicative signature (Σ, C). In this section we define the general class of (Σ, C)-domains which is a direct generalization of the standard Σ-domains introduced in [GTWW77]. In fact the (Σ, C)- domains are only a slight modification of the Natural Interpretations introduced in [HP80] and applied in [HI93]. We also introduce the notion of recursively closed subsets of a process algebra.

After having presented the general models we show how we may obtain a (Σ, C)-domain by defining a preordered set that represents the compact elements, defining the operators as monotonic functions over this set and then taking the domain to be the unique extension of the kernel of the preorder and the induced monotonic functions to such a structure. We also study the relationship between the evaluation mappings from our generic process language into two arbitrary (Σ, C)-preorders. In what follows we abstract away from possible structures or properties of the value domain V al and simply view it as being partially ordered by the discrete order.

4.1 (Σ, C)-Orders and (Σ, C)-Domains

In this subsection we define the notion of applicative orders and applicative ordered (Σ, C)- algebras. We borrow the notation from [Hen88a] and use the abbreviations pro for preorder, po for partial order and cpo for complete partial order together with their domains. We assume that the reader is familiar with basic domain theory and algebraic semantics. (See e.g. [Plo81, Hen88a] for details.)

Definition 4.1 (Applicative Orders) A pair ⟨\overline{A}, <\overline{A}⟩ is an applicative pro/po/cpo if \overline{A} = (A_{proc}, A_{fun}, A_{pair}) and <\overline{A}= (<_{A_{proc}}, <_{A_{fun}}, <_{A_{pair}}) are such that:

1. ⟨A_{proc}, <_{A_{proc}}⟩ is a pro/po/cpo and

2. A_{fun} ⊆ V al ⟶ A_{proc} and A_{pair} ⊆ V al × A_{proc} are pro/po/cpos with the standard induced ordering, i.e. <_{A_{fun}} is the pointwise ordering and <_{A_{pair}} is defined by:

(v_{1}, p_{1}) <_{A_{pair}} (v_{2}, p_{2}) if v_{1} = v_{2} and p_{1} <_{A_{proc}} p_{2}.

\overline{A} is said to be fully applicative if A_{proc} = A, A_{fun} = V al ⟶ A and A_{pair} = V al × A for some A. In that case we refer to \overline{A} as A. \overline{A} is said to be finitely applicative if A_{pair} = V al × A for some A and

A_{fun} = V al ⟶_{fin} A = {f ∈ V al ⟶ A | {a|f(a) ≠ ⊥} is finite}.

In this case we refer to \overline{A} as A^{fin}. An applicative cpo is said to be algebraic/ω-algebraic if A_{proc}, A_{fun} and A_{pair} are algebraic/ω-algebraic cpos. □

Here we want to point out that the partial order of compact elements of an applicative algebraic cpo is in general not fully applicative but finitely applicative. We often write apro/po/cpo as a shorthand for applicative pro/po/cpo.

Definition 4.2 ((Σ, C)-Orders) A four tuple ⟨\overline{A}, <\overline{A}, Σ\overline{A}, C\overline{A}⟩ is an applicative (Σ, C) − pro/po/cpo if \overline{A} = (A_{proc}, A_{fun}, A_{pair}) is such that 1. ⟨\overline{A}, <\overline{A}⟩ is an a-pro/po/cpo,

2. Σ\overline{A} is a set of monotonic/monotonic/continuous functions op\overline{A} : A_{proc} ⟶ A_{proc},

3. C\overline{A} = C!\overline{A} ∪ C?\overline{A} where:

(a) C!\overline{A} is a set of monotonic/monotonic/continuous functions c!.\overline{A} : A_{pair} ⟶ A_{proc} and

(b) C?\overline{A} is a set of monotonic/monotonic/continuous functions c?\overline{A} : A_{fun} ⟶ A_{proc}. An ω-algebraic applicative (Σ, C) − cpo is called a (Σ, C)-domain. For an algebraic cpo A we use Comp(A) to denote the set of compact elements of A. Usually we use <, ≺, ⊏ etc. to denote preorders but ≤, ⪯, ^{⊑} to denote partial orders, including the complete ones. □ Definition 4.3 A function f : A_{1} ⟶ A_{2}, where ⟨A_{1}, ≤_{1}⟩ and ⟨A_{2}, ≤_{2}⟩ are algebraic cpos, is said to be compact if it maps compact elements of A_{1} into compact elements of A_{2}, i.e. if f(Comp(A_{1})) ⊆ Comp(A_{2}). □ Next we extend the standard notion of homomorphisms for applicative orders. Definition 4.4 A a-pro/po/cpo homomorphism from ⟨\overline{A}, <\overline{A}⟩ to ⟨\overline{B}, <\overline{B}⟩ is a monotonic function h : A_{proc} ⟶ B_{proc} that satisfies

1. h(op\overline{A}(\overline{a})) = op\overline{B}(h(\overline{a})),

2. h(c?\overline{A}.F) = c?\overline{B}.(h ∘ F) and

3. h(c!\overline{A}.(v, \overline{a})) = c!\overline{B}.(v, h(\overline{a})). We define h_{proc} = h, h_{fun}(F) = h∘F for all F ∈ A_{fun} and h_{pair}(v, a) = (v, h(a)) for all (v, a) ∈ A_{pair}. Sometimes we refer to the triplet \overline{h} = (h_{proc}, h_{fun}, h_{pair}) as such a homomorphism. □

At times it is useful to be able to apply structural induction on a sublanguage of the full language defined by an a-signature (Σ, C) and a set of process names P N. In particular we want to be able to give recursive definitions on certain sublanguages (e.g. the language that denotes the compact elements of the model). This motivates the following definition of a recursively closed subset of a language. Definition 4.5 \overline{S} = (S_{proc}, S_{fun}, S_{pair}) ⊆ T_{(Σ,C)}(P N) is said to be recursively closed if the following hold:

1. p = op(p_{1}, …, p_{n}) ∈ S_{proc} implies p_{i} ∈ S_{proc} for i = 1, …, n,

2. [x]p ∈ S_{proc} implies p[v/x] ∈ S_{proc} for all v ∈ V al,

3. (e, p) ∈ S_{proc} implies p ∈ S_{proc},

4. c?.f ∈ S_{proc} implies f ∈ S_{fun},

5. c!.o ∈ S_{proc} implies o ∈ S_{pair},

6. be ⟶ p_{1}, p_{2} ∈ S_{proc} implies p_{1}, p_{2} ∈ S_{proc},

7. recP.p ∈ S_{proc} implies P, p ∈ S_{proc}.

In this case we write \overline{S} ⊆_{rec} T_{(Σ,C)}(P N). □

Note that if Σ′ ⊆ Σ and C′ ⊆ C then T_{(Σ′,C′)} ⊆_{rec} T_{(Σ,C)}(P N).

Definition 4.6 Let \overline{S} ⊆_{rec} T_{(Σ,C)}(P N), where \overline{S} only contains value closed terms, ⟨\overline{A}, <\overline{A} , Σ\overline{A}, C\overline{A}⟩ be an applicative (Σ, C) − pro and P Env\overline{A} be the set of process environments ρ : P N ⟶ A_{proc}. A function

\overline{A}[[ ]] : S_{proc} ⟶ (P Env\overline{A} ⟶ A_{proc}))

is an evaluation function if for each ρ ∈ P Env\overline{A}, \overline{A}[[ ]]ρ : S_{proc} ⟶ A_{proc} is a (Σ, C)-pro homomorphism, where \overline{S} is the (Σ, C)-pro obtained by taking \overline{S} with the discrete order and the operators to be the syntactic ones from Σ and C, and if the following holds:

\begin{matrix}\overline{A}[[P]]ρ = ρ(P) and \\ \overline{A}[[ be → p_{1}, p_{2}]]ρ = \{ \begin{matrix}\overline{A}[[p_{1}]]ρ & if [[be]] = T, \\ \overline{A}[[p_{2}]]ρ & if [[be]] = F. \end{matrix} \end{matrix}

If \overline{A} is a cpo then, following standard practice, we may define

\overline{A}[[recP.p]]ρ = Y λd.\overline{A}[[p]]ρ[d/P]

where Y is the least fixed point operator. □

For closed terms the environments do not have any influence on the definition of the semantics. For terms without process names, a mapping \overline{A}[[t]] = \overline{A}[[t]]ρ may be derived from the above definition omitting the last clause of the definition and the occurrence of ρ in the others. Now we show that recursively closed subsets of T_{(Σ,C)}(P N) have at most one interpretation in an a-(Σ, C)-pro. This is the subject of the next theorem.

Theorem 4.7 Let \overline{S} = (S_{proc}, S_{fun}, S_{pair}) ⊆_{rec} T_{(Σ,C)}(P N) and ⟨\overline{A}, <\overline{A}, Σ\overline{A}, C\overline{A}⟩ be an applicative (Σ, C) − pro. Then there is at most one evaluation mapping

\overline{A}[[ ]] : S_{proc} ⟶ (P Env\overline{A} ⟶ \overline{A}).

If ⟨\overline{A}, <\overline{A}, Σ\overline{A}, C\overline{A}⟩ is fully applicative then such an evaluation mapping exists.

Proof May be proved by structural induction and is left to the reader. □ Note that if \overline{A} is not fully applicative then a function term of the form [x]p, where p only

has x as a free variable, may fail to have an interpretation in \overline{A}. For instance, if \overline{A} is the a-po of compact elements of some (Σ, C)-domain \overline{A} and p is a process term denoting a compact element of A_{proc} different from ⊥, then the function term [x]p fails to have an interpretation in A_{fun}.

The following result turns out to be useful in the next section.

Corollary 4.8 Assume that

\overline{S} = (S^{proc}, S^{fun}, S^{pair}) ⊆_{rec} (C CS_{L}^{proc}, C CS_{L}^{fun}, C CS_{L}^{pair}),

that ⟨\overline{A}, <\overline{A}, Σ\overline{A}, C\overline{A}⟩ and ⟨\overline{B}, <\overline{B}, Σ\overline{B}, C\overline{B}⟩ are (Σ, C)-pros and that

ψ : ⟨\overline{A}, <\overline{A}, Σ\overline{A}, C\overline{A}⟩ ⟶ ⟨\overline{B}, <\overline{B}, Σ\overline{B}, C\overline{B}⟩

is a (Σ, C)-pro homomorphism. If \overline{A}[[ ]] : S_{proc} ⟶ ⟨\overline{A}, <\overline{A}, Σ\overline{A}, C\overline{A}⟩ and \overline{B}[[ ]] : S_{proc} ⟶ ⟨\overline{B}, <\overline{B}, Σ\overline{B}, C\overline{B}⟩ are evaluation mappings, then \overline{B}[[ ]] = ψ ∘ \overline{A}[[ ]].

Proof It is easy to check that the mapping \overline{B}[[[ ]]] defined by \overline{B}[[[ ]]] = \overline{ψ} ∘ A[[ ]] is an evaluation mapping from \overline{S} to ⟨\overline{B}, <\overline{B}, Σ\overline{B}, C\overline{B}⟩. By Theorem 4.7 such an evaluation mapping is unique and the equality follows. □

There is a standard way of extending a preorder with a least element to an algebraic cpo, often called completion by ideals ([Hen88a, §3.3], [Win85]). If ⟨A, <_{A}⟩ is a preorder, a set X ⊆ A is downwards closed if whenever x ∈ X and y ^{⊑}_{A} x then y ∈ X and directed if whenever x, y ∈ X then, for some z ∈ X, x < z and y < z. An ideal in A is a non-empty, directed and downwards closed subset of A. Let I(A) denote the set of all ideals in A. If A has a least element then ⟨ I(A), ⊆ ⟩ is an algebraic cpo. The compact elements of I(A) are Comp(I(A)) = {↓ a|a ∈ A} where ↓ a = {x|x ^{⊑}_{A} a}. I(A) is the unique algebraic cpo (up to isomorphism) whose partial order of compact elements consists of the kernel of ⟨A,^{⊑}_{A}⟩, i.e. ⟨A/ =_{A},^{⊑}_{A/=_{A}}⟩ where =_{A} is the equivalence induced by ^{⊑}_{A}. This is referred to as the ideal completion of ⟨A,^{⊑}_{A}⟩. Note that if A/ =_{A} is countable then I(A) is ω-algebraic.

We have the following standard theorem (see e.g. [Hen88a]).

Theorem 4.9 Let ⟨M,^{⊑}_{M}⟩ be a partial order, ⟨A,^{⊑}_{A}⟩ a cpo and f : M ⟶ A be monotonic. Then there is a unique continuous extension f̃ of f to I(M).

These results generalize to the applicative orders as follows. Let ⟨\overline{A}, <\overline{A}, Σ\overline{A}, C\overline{A}⟩ be a (Σ, C)- pro. We may define a continuous (Σ, C) structure on I(\overline{A}) = (I(A_{proc}), I(A_{fun}), I(A_{pair})) as follows: Let ⟨\overline{A}/ ≈,^{⊑}_{\overline{A}/≈}⟩ denote the a-po induced by ⟨\overline{A}, <\overline{A}⟩ and [ ]_{≈} : \overline{A} ⟶ \overline{A}/ ≈ denote the quotient mapping. For op\overline{A} ∈ Σ\overline{A}, we define op_{\overline{A}/≈} on \overline{A}/ ≈ by op_{\overline{A}/≈}([x]_{≈}) = [op\overline{A}(x)]_{≈}. It is easy to see that this defines an operator in \overline{A}/ ≈ that preserves the order. Now we define op_{I(\overline{A})} to be the unique continuous extension of op_{\overline{A}/≈} as described in Theorem 4.9. This gives continuous (Σ, C) structure that turns I(\overline{A}) into a (Σ, C)-domain. We refer to this domain as the domain induced by ⟨\overline{A}, <\overline{A}, Σ\overline{A}, C\overline{A}⟩. Furthermore, by Corollary 4.8, if \overline{S} ⊆_{rec} T_{(C,Σ)} and \overline{A}[[ ]] : \overline{S} ⟶ \overline{A} is an evaluation mapping then I(\overline{A})[[ ]]|\overline{S} = [ ]_{≈} ∘ \overline{A}[[ ]] where I(\overline{A})[[ ]]|\overline{S} means the restriction of the function I(\overline{A})[[ ]] to \overline{S}. In particular this implies that for all s_{1}, s_{2} ∈ \overline{S}

I(\overline{A})[[s_{1}]] ^{⊑}_{I(\overline{A})} I(\overline{A})[[s_{2}]] iff \overline{A}[[s_{1}]] <\overline{A} \overline{A}[[s_{2}]].

4.2 Definition of the Model

This section is devoted to defining the concrete model \overline{ACT}. First we give a description of a representation of the compact elements.

Definition 4.10 We define K as the least set which satisfies:

1. ∅, {⊥} ∈ K,

2. c ∈ C, V ⊆_{fin} V al and ∀v ∈ V. k_{v} ∈ K implies {⟨c?, λv.x ∈ V ⟶ k_{v}, Ω⟩} ∈ K,

3. c ∈ C, v ∈ V al and k ∈ K implies {⟨c!, (v, k)⟩} ∈ K,

4. k ∈ K implies {⟨τ, k⟩} ∈ K,

5. k_{1}, k_{2} ∈ K implies k_{1} ∪ k_{2} ∈ K.

The preorder ≺ is defined as the least preorder on K which satisfies

1. {⊥} ≺ ∅

2. k_{1} ≺ k_{2} if ∀a ∈ k_{1}∃b ∈ k_{2}. a < b and ∀b ∈ k_{2}∃a ∈ k_{1}. a < b where < is defined on the elements of the sets in K by

(a) ∀a. ⊥ < a,

(b) ⟨τ, k⟩ < ⟨τ, k′⟩ iff k ≺ k′,

(c) ⟨c?, f⟩ < ⟨c?, g⟩ iff ∀v ∈ V al.f(v) ≺ g(v),

(d) ⟨c!, (v, k)⟩ < ⟨c!, (v, k′)⟩ iff k ≺ k′. We let ≈=≺ ∩ ≺^{−1}. □ Definition 4.11 We define ⟨\overline{K}, ≺\overline{K}⟩ to be ⟨K^{fin}, ≺_{fin}⟩, i.e. the finitely applicative preorder induced by K. □

Next we define the operators on the applicative preorder ⟨\overline{K}, ≺\overline{K}⟩ and make sure that they are monotonic. Definition 4.12 We define Σ\overline{K} as follows: Constants:

nil\overline{K} = ∅,
Ω\overline{K} = \{⊥\}.

Prefixing:

c?\overline{K}. = λf.\{⟨c?, f⟩\},
c!\overline{K}. = λ(v, k).\{⟨c!, (v, k)⟩\},
τ\overline{K}. = λk.\{⟨τ, k⟩\}.

Nondeterminism:

+\overline{K} = ∪.

Restriction:

\c\overline{K} = F_{c}

where F_{c} : K_{proc} → K_{proc} is defined by

F_{c}{⊥} = {⊥},
F_{c}∅ = ∅,
F_{c}\{⟨b?, f⟩\} = \{ \begin{matrix}\{⟨b?, F_{c} ∘ f⟩\} & if b ≠ c, \\ ∅ & otherwise, \end{matrix}
F_{c}\{⟨b!, (v, k)⟩\} = \{ \begin{matrix}\{⟨b!, (v, F_{c}k)⟩\} & if b ≠ c, \\ ∅ & otherwise, \end{matrix}
F_{c}{⟨τ, k⟩} = {⟨τ, F_{c}k⟩},
F_{c}(k_{1} ∪ k_{2}) = (F_{c}k_{1}) ∪ (F_{c}k_{2}).

Renaming:

[R]\overline{K} = G_{R}

where G_{R} : K_{proc} → K_{proc} is defined by

G_{R}{⊥} = {⊥},
G_{R}∅ = ∅,
G_{R}{⟨c?, f⟩} = {⟨R(c)?, G_{R} ∘ f⟩},
G_{R}{⟨c!, (v, k)⟩} = {⟨R(c)!, (v, G_{R}k)⟩},
G_{R}{⟨τ, k⟩} = {⟨τ, G_{R}k⟩},
G_{R}(k_{1} ∪ k_{2}) = (G_{R}k_{1}) ∪ (G_{R}k_{2}).

Parallel Composition:

|\overline{K} = F

where F = int ∪ comm ∪ div where int = int_{in} ∪ int_{out} ∪ int_{τ} and

int_{in}(x, y) = {⟨c_{x}?, λv.F (f_{x}(v), y)⟩|⟨c_{x}?, f_{x}⟩ ∈ x}
∪ {⟨c_{y}?, λv.F (x, f_{y}(v))⟩|⟨c_{y}?, f_{y}⟩ ∈ y},
int_{out}(x, y) = {⟨c_{x}!, (v, F (x′, y))⟩|⟨c_{x}!, (v, x′)⟩ ∈ x}
∪ {⟨c_{y}!, (v, F (x, y′))⟩|⟨c_{y}!, (v, y′)⟩ ∈ y},
int_{τ} = {⟨τ, F (x′, y)⟩|⟨τ, x′⟩ ∈ x}
∪ {⟨τ, F (x, y′)⟩|⟨τ, y′⟩ ∈ y},
comm(x, y) = {⟨τ, F (f(v), y′)⟩ | ∃c, v.⟨c?, f⟩ ∈ x and ⟨c!, (v, y′)⟩ ∈ y}
∪ {⟨τ, F (x′, g(v))⟩ | ∃c, v.⟨c?, g⟩ ∈ y and ⟨c!, (v, x′)⟩ ∈ x}

and

div(x, y) = \{ \begin{matrix}\{⊥\} & if ⊥ ∈ x ∪ y, \\ ∅ & otherwise. \end{matrix}
□

The reader may notice the close connection between the definition of the parallel operator and the interleaving law presented later in the paper. We have the following result:

Lemma 4.13 ⟨\overline{K}, ≺\overline{K}, Σ\overline{K}, C\overline{K}⟩ is a (Σ, C)-pro.

Proof We leave it to the reader to check that the operators defined by Definition 4.12 are well-defined. The monotonicity of the operators nil\overline{K}, Ω\overline{K}, c?\overline{K}, c!\overline{K}, τ\overline{K} and +\overline{K} is obvious. To prove the monotonicity of the remaining operators we use the depth, d( ), of the elements of K defined in the proof of Proposition 4.18. To prove the monotonicity of the restriction and the renaming operators we prove by induction on d(k) that k ≺ k′ implies F_{c}k ≺ F_{c}k′ and k ≺ k′ implies G_{R}k ≺ G_{R}k′. To prove the monotonicity of the parallel operator with respect to the induced ordering on K ×K, we extend d to K ×K by d(k_{1}, k_{2}) = d(k_{1})+d(k_{2}). Then we may prove that

(k_{1}, k_{2}) ≺ (k′_{1}, k′_{2}) implies F (k_{1}, k_{2}) ≺ F (k′_{1}, k′_{2})

by induction on d(k_{1}, k_{2}). We leave the straightforward details of the proof to the reader. □

Now we let ⟨\overline{ACT} ,^{⊑}\overline{ACT} , Σ\overline{ACT} , C\overline{ACT} ⟩ be the (unique) fully applicative (Σ, C)-domain induced by ⟨\overline{K}, ≺\overline{K}, Σ\overline{K}, C\overline{K}⟩. The operators in Σ\overline{ACT} and C\overline{ACT} are compact.

4.3 Syntactically Compact Elements

Next we will show that the compact elements of the model \overline{ACT} may be denoted in our syntax by a recursively closed subset of the whole language. For this purpose we introduce the so-called syntactically compact terms, coCCS_{L} = (coCCS_{L}^{proc}, coCCS_{L}^{fun}, coCCS_{L}^{pair}).

As usual, syntactically finite terms are those without occurrences of recursion. We define syntactically compact terms as the syntactically finite ones which only use a finite number of values. Note that, as we are dealing with recursion free terms, the number of channels used by the term is automatically finite. We start by introducing some notation.

Notation 4.14 Let \underline{w} = (w_{1}, …, w_{n}) and \underline{p} = (p_{1}, …, p_{n}) be vectors of values and processes respectively. We write x : \underline{w} ⟶ \underline{p} for

x = w_{1} ⟶ p_{1}, (x = w_{2} ⟶ p_{2}, (… x = w_{n} ⟶ p_{n}, Ω) …).

(Intuitively x : \underline{w} ⟶ \underline{p} stands for the mapping that maps w_{i} to p_{i} for i = 1, …, n and all the other values w ∈ V al into Ω.) Furthermore we let \{\underline{w}\} = \{w_{i}|\underline{w_{n}} = (w_{1}, …, w_{n}), i ≤ n\} and similarly for \{\underline{p}\}.

Definition 4.15 [Syntactically Compact Terms] The set of syntactically compact terms is the triplet coCCS_{L} = (coCCS_{L}^{proc}, coCCS_{L}^{fun}, coCCS_{L}^{pair}), where coCCS_{L}^{proc}, coCCS_{L}^{fun} and coCCS_{L}^{pair} are the least sets satisfying:

1. nil, Ω ∈ coCCS_{L}^{proc},

2. \overline{p} ∈ coCCS_{L}^{proc} implies op(\overline{p}) ∈ coCCS_{L}^{proc}, op = |, +, \, [R] , τ. ,

3. o ∈ coCCS_{L}^{pair}, c ∈ C implies c!.o ∈ coCCS_{L}^{proc},

4. f ∈ coCCS_{L}^{fun} and c ∈ C implies c?.f ∈ coCCS_{L}^{proc},

5. p ∈ coCCS_{L}^{proc} and e ∈ Exp implies (e, p) ∈ coCCS_{L}^{pair},

6. p_{1}, …, p_{n} ∈ coCCS_{L}^{proc}, v_{1}, …, v_{n} ∈ V al and x ∈ V ar implies [x]. x : (v_{1} …, v_{n}) ⟶

(p_{1} …, p_{n}) ∈ coCCS_{L}^{fun}. We let coCCS_{L}, coCCS_{L}^{proc}, coCCS_{L}^{fun} and coCCS_{L}^{pair} be ranged over by ct, cp, cf and co respectively (Note that by definition these terms are value closed.). We say that a term is compact if it belongs to coCCS_{L}. □ Note that coCCS_{L} ⊆_{rec} CCS_{L}. We have the following: Theorem 4.16

1. There are unique evaluation mappings \overline{ACT} [[ ]] : CCS_{L} ⟶ \overline{ACT} and \overline{K}[[ ]] : coCCS_{L} ⟶ \overline{K}.

2. \overline{ACT} [[ ]] |_{coCCS_{L}} = [ ]_{≈} ∘ \overline{K}[[ ]] where • f|_{A} means the restriction of the function f to the set A,

• [ ]_{≈} is the quotient mapping with respect to the preorder ≺.

3. For any ct ∈ coCCS_{L}, \overline{ACT} [[ct]] ∈ Comp(\overline{ACT}).

4. For all ct_{1}, ct_{2} ∈ coCCS_{L}, \overline{ACT} [[ct_{1}]] ^{⊑} \overline{ACT} [[ct_{2}]] if and only if \overline{K}[[ct_{1}]] ≺\overline{K} \overline{K}[[ct_{2}]].

5. For any c ∈ Comp(\overline{ACT}) there is a ct ∈ coCCS_{L} such that \overline{ACT} [[ct]] = c.

Proof

1. As \overline{ACT} is a fully applicative (Σ, C)-cpo then, by Theorem 4.7,

\overline{ACT} [[ ]] : CCS_{L} ⟶ \overline{ACT}

is well-defined and unique. The existence and uniqueness of \overline{K}[[ ]] follows by a simple structural induction on coCCS_{L}.

2. As coCCS_{L} is a recursively closed subset of CCS_{L}, we get that \overline{ACT} [[ ]]|_{coCCS_{L}} is an evaluation mapping on coCCS_{L}. By construction of ⟨\overline{ACT} ,^{⊑}\overline{ACT} , Σ\overline{ACT} , C\overline{ACT} ⟩, [ ]_{≈} : \overline{K} ⟶ \overline{ACT} is a (Σ, C)-po homomorphism. It then follows from Corollary 4.8 that \overline{ACT} [[ ]] |_{coCCS_{L}} = [ ]_{≈} ∘ \overline{K}[[ ]].

3. and 4. follow immediately from 2. and the construction of \overline{ACT}.

5. We start by proving that for any k ∈ \overline{K} there is a ct ∈ coCCS_{L} such that \overline{K}[[ct]] = k. First we prove the result for the set K which by definition equals K_{proc}. This may be proved by induction on the definition of K. Then we may easily extend the proof to K_{fun} and K_{pair}.

Next assume that c is a compact element of \overline{ACT}. Then, by the construction of the model, c = [k]_{≈} for some k ∈ \overline{K}. From what we proved above we get that \overline{K}[[ct]] = k for some ct ∈ coCCS_{L}. From 2. we get

\overline{ACT} [[ct]] = [\overline{K}[[ct]]]_{≈} = [k]_{≈} = c.

This completes the proof.

□

4.4 A Domain Equation for Applicative Communication Trees

In this section we will show an alternative but equivalent definition of the model \overline{ACT}; we will show how it may be obtained as a solution to a recursive domain equation. The section is mostly of historical interest and may safely be skipped by the reader.

The equation we put forward is basically the one of [MM79] where the modifications of Abramsky’s, reported in [Abr91] and described in the introduction, are adopted. Thus we define an algebraic cpo as a solution to a domain equation using the Plotkin Power Domain with the empty set adjoined as an isolated element. Here the main difference is that we use a different representation for the Plotkin Power Domain to the one used in [Abr91]. The representation we use is the one due to Smyth, [Smy78] and will be described below. In the definition of the domain we use the following operations on cpos:

Cartesian product × ([Plo81, §2 and §6]): Let ⟨A,^{⊑}_{A}⟩ and ⟨A′,^{⊑}_{A′}⟩ be two pos. We define the partial order ^{⊑}_{A×A′} on A × A′ by:

(a, a′) ^{⊑}_{A×A′} (b, b′) if a ^{⊑}_{A} b and a′ ^{⊑}_{A′} b′.

This construction extends to any number of pos. It preserves completeness and algebraicity. Countable products preserve ω-algebraicity. If A and A′ are algebraic cpos, the set of compact elements can be obtained from the compact elements of A and A′ by Comp(A × A′) = Comp(A) × Comp(A′).

Separated Sum ∑_{i∈I} ([Abr87, §3], [Plo81, §3 and §6],): Let I be a countable index set and {A_{i}}_{i∈I} be a family of I–indexed pos. The separated sum ⟨∑_{i∈I} A_{i},^{⊑}_{∑_{i∈I} A_{i}}⟩ is defined as follows:

∑_{i∈I} A_{i} = {⊥} ∪ (⋃{{i} × A_{i}|i ∈ I}),
x ^{⊑}_{∑_{i∈I} A_{i}} y if x =⊥ or if for some i, x = ⟨i, a⟩ , y = ⟨i, a′⟩ and a ⊑_{A_{i}} a′,

where we write ⟨i, a⟩ for the elements of the disjoint union and ⊥ for the bottom element of the separated sum. The construction preserves completeness, algebraicity and ω-algebraicity. If each A_{i} is an algebraic cpo, the set of compact elements of ⟨∑_{i∈I} A_{i},^{⊑}_{∑_{i∈I} A_{i}}⟩ is given by

Comp(∑_{i∈I} A_{i}) = {⊥} ∪ (⋃{{i} × Comp(A_{i})|i ∈ I}.

Function Space from a fixed set S, F_{S} ([Plo81, §3] ): Let S be a fixed countable set. For a po ⟨A,^{⊑}_{A}⟩ we define F_{S}(A) = S ⟶ A, the set of all functions from S to A, with the pointwise ordering ^{⊑}_{F_{S}(A)} as follows:

f ^{⊑}_{F_{S}(A)} g if ∀s ∈ S.f(s) ^{⊑}_{A} g(s).

This construction preserves completeness, algebraicity and ω-algebraicity. The compact elements of F_{S}(A) can be obtained from those of A by Comp(F_{S}(A)) = F_{S}^{fin}(Comp(A)) where F_{S}^{fin}(B) = {f ∈ S ⟶ B|{s ∈ S|f(s) ≠ ⊥} is finite}. Note that the constructions ∑_{i∈I} and F_{S}(A) may just as well be defined for non-countable sets I and S but then they do not preserve ω-algebraicity in general.

The Plotkin Power Domain ([Win85]): We give a construction of the Plotkin Power Domain [Plo76] due to Smyth [Smy78] and described in [Win85]. Let ⟨A,^{⊑}_{A}⟩ be an ω-algebraic cpo and M[A] the family of finite, non-empty sets of compact elements of A. The Egli-Milner order on M[A] is defined by:

For X, Y ∈ M[A], X ^{⊑}_{EM} Y iff \begin{matrix}∀x ∈ X∃y ∈ Y. x ^{⊑}_{A} y and \\ ∀y ∈ Y ∃x ∈ X. x ^{⊑}_{A} y. \end{matrix}

The Plotkin Power Domain of ⟨A,^{⊑}_{A}⟩, ⟨P [A],^{⊑}_{P [A]}⟩ is the ideal completion of the preorder ⟨M[A],^{⊑}_{EM}⟩. As explained before, we know that ⟨P [A],^{⊑}_{P [A]}⟩ is an ω-algebraic cpo and Comp(P [A]) = M[A]/ =_{EM} (up to isomorphism).

In the definition to follow we shall use the empty set to interpret the process nil and the least element of the domain to interpret the process Ω. As nil is an isolated element with respect to bisimulation preorder, i.e. only related to itself and Ω, we adopt Abramsky’s modification of the Plotkin Power Domain, i.e. we add the empty set to the domain in such a way that it is only related to itself and the least element of the domain in the obvious way under the extended Egli-Milner order. This may be described as follows:

Given an ω-algebraic cpo we write P^{0}[D] for the Plotkin Power Domain over D with the empty set adjoined as an isolated element in the preorder. More precisely the elements of P^{0}[D] are given by P [D] ∪ {∅} with the order:

X ^{⊑}_{P^{0}[D]} Y if X, Y ∈ P [D] and X ⊑_{P [D]} Y

or Y = {∅} and (X = {∅} or X = ⊥).

(1)

All the constructions on pos described above may be turned into covariant continuous functors in the category CPO^{E}, the category of cpos with embeddings, in a straightforward way. For the details we refer to [Plo81]. Now the standard theory in [Plo81] ensures that the following definition is meaningful.

Definition 4.17 Let C (the set of channels) and V al (the set of values) be countable sets and let Act = {c?|c ∈ C} ∪ {c!|c ∈ C} ∪ {τ} (the set of actions). We define the applicative cpo of applicative communication trees, ⟨\overline{A},^{⊑}\overline{A}⟩, as follows: ⟨A,^{⊑}_{A}⟩ is the initial solution in CPO^{E} of the recursive domain equation:

D = P^{0}[ ∑_{e∈Act} D_{e}]

where

• D_{c?} = F_{V al}(D) = V al → D (as defined on page 22),

• D_{c!} = V al × D and

• D_{τ} = D.

Then we define ⟨\overline{A},^{⊑}\overline{A}⟩ as the unique fully applicative ω-algebraic cpo induced by ⟨A,^{⊑}_{A}⟩. For the sake of simplicity we refer to this domain as A or ⟨A,^{⊑} ⟩. □

From the general theory in [Plo81] we get a representation of the compact elements by unfolding the recursive definition of A. Thus we define C OMP = ⋃_{n=0}^{∞} C OMP^{n} where C OMP^{0} = {⊥} and

C OMP^{n+1} = M[ ∑_{e∈Act}(C OMP^{n})_{e}] ∪ {∅}

where (C OMP^{n})_{c?} = F_{V al}(C OMP^{n}), (C OMP^{n})_{c!} = V al × C OMP^{n} and (C OMP^{n})_{τ} = C OMP^{n}. We recall that for an algebraic cpo A, M[A] is defined as the family of non-empty sets of compact elements of A. The empty set is added to the family C OMP^{n} as we are using the power domain operator P^{0} rather than P. Defining C OMP in this way and ordering it by ⊑_{EM}^{0}, the Egli-Milner preorder over C OMP extended like in (1) above, gives a representation of the compact elements of the ω-algebraic cpo A. This means that the kernel of the preorder is isomorphic to the partial order of compact elements of the domain A, ⟨Comp(A),^{⊑}_{Comp(A)}⟩. (For the sake of simplicity we assume that the kernel is equal to Comp(A).) Now we prove that ⟨K, ≺⟩ defined above is equal to ⟨C OMP ,^{⊑}_{EM}^{0}⟩.

Proposition 4.18 ⟨K, ≺⟩ = ⟨C OMP ,^{⊑}_{EM}^{0}⟩.

Proof First we prove that K = C OMP. That K ⊆ C OMP can be proved by showing that C OMP is closed under 1. − 6. in the definition of K and then use the fact that K is the least set with this property. To prove the opposite inclusion, it is sufficient to show that, for every n, C OMP^{n} ⊆ K.

Then we prove that the preorder ≺ coincides with the extended Egli-Milner preorder on K. To prove ≺ ⊆^{⊑}_{EM}^{0}, as before it is sufficient to prove that ^{⊑}_{EM}^{0} satisfies the definition of ≺. The details are straightforward and are left to the reader. To prove ≺ ⊇^{⊑}_{EM}^{0} we first define the depth of the elements of K as follows:

1. d(∅) = d({⊥}) = 0,

2. d({⟨μ, k⟩}) = 1 + d(k),

3. d({a_{1}, …, a_{n}}) = max{d({a_{i}})|i ≤ n}, 4. d(f) = max{d(f(v))|v ∈ V al} (recall that {f(v)|v ∈ V al} is a finite set as f yields ⊥

on all but finitely many values in V al),

5. d(e, k) = d(k).

Then we prove by induction on d(k) that k ^{⊑}_{EM}^{0} k′ ⇒ k ≺ k′. The details of the proofs are straightforward and are left to the reader. □ Proposition 4.18 has the following direct corollary.

Corollary 4.19 The algebraic cpos ACT and A are isomorphic.

5 Algebraic Laws and Proof Systems

In this section we will introduce proof systems supported by the model \overline{ACT}. We proceed by introducing first a system E to reason about finite processes that reflects the structure of K. Then we extend this system to systems which take care of recursive processes in two different ways and reason about soundness and completeness of both these extensions with respect to the model.

The proof system E is equationally based where the equations reflect naturally the properties of the operators in the model. As an example the equations

X + (Y + Z) = (X + Y) + Z
X + Y = Y + X
X + X = X

reflect the fact that the elements of K, and thus of \overline{ACT}, are defined as sets and + as set union. The inference rules describe the structure and the preorder of the model and their interaction with the operators. Because of the two level structure of our syntax, we have the equations

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

(ren in) (a?.[x]X)[R] = R(a)?.[x](X[R]),
(ren out) (a!.(e, X))[R] = R(a)!.(e, X[R])

and the rules

(fun) \frac{p[v/x] ^{⊑} q[v/x] for every v ∈ V}{[x]p ^{⊑} [x]q}

(pair) \frac{[[e_{1}]] = [[e_{2}]], p ^{⊑} q}{(e_{1}, p) ^{⊑} (e_{2}, q)}

(+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τ)  (τ.X) \ c = τ.(X \ 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 cond) (be ⟶ X, Y) \ c = be ⟶ X \ c, Y \ c
(res nil)  nil \ c = nil
(res div)  Ω \ c = Ω
(ren+)  (X + Y)[R] = X[R] + Y [R]
(renτ)  (τ.X)[R] = τ.(X[R])
(ren in)  (a?.[x]X)[R] = R(a)?.[x](X[R])
(ren out)  (a!.(e, X))[R] = R(a)!.(e, X[R])
(ren cond) (be ⟶ X, Y)[R]c = be[R] ⟶ X[R], Y [R]
(ren nil)  nil[R] = nil
(ren div)  Ω[R] = Ω
(nil par)  nil | X = X | nil = X

Figure 3: Equations

that allow us to prove inequalities over function terms and pairs. The first extension of E is obtained by adding to E two new rules to take care of recursion. The new rules introduced are

(rec) recP.p = p[recP.p/P]

and

(ω − rule) \frac{p^{(n)} ^{⊑} q for all n}{p ^{⊑} q}

where t^{(n)}, the syntactically compact approximations of a term t, are defined in Definition 5.1. We write t ^{⊑}_{E_{rec}} u if t ^{⊑} u can be proven using the rules given above and t ^{⊑}_{E_{rec}^{−ω}} u if this inequality can be proven in the same system without applying the ω-rule.

Note here that the approximations that occur in the ω-rule are syntactically compact as the number of values in the approximations is finite just as the depth of the approximation is finite. Consequently we refer to this system as the value-finitary one. This correspondence with the compact elements enables us to take advantage of the algebraicity of the model when proving the completeness of the proof system. 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 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.

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 4: Interleaving Law

\begin{matrix}(ref) & p ^{⊑} p \\ (trans) & \frac{p ^{⊑} q, q ^{⊑} r}{p ^{⊑} r} \\ (least) & Ω ⊑ p \\ (sub) & \frac{p_{i} ^{⊑} q_{i}}{op(\underline{p}) ^{⊑} op(\underline{q})} op ∈ ∑ \\ (pre) & \frac{p ^{⊑} q}{μ.p ^{⊑} μ.q} \\ (cond1) & \frac{[[be]] = T}{be ⟶ p, q = p} \\ (cond2) & \frac{[[be]] = F}{be ⟶ p, q = q} \end{matrix}

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

(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 5: The Proof System E_{rec}

Now we define the syntactically compact (or just compact for short) approximations used in the ω-rule of the proof system.

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

1. (a) p^{(0)} = Ω

(b) i. P^{(n+1)} = P, ii. (op(\underline{p}))^{(n+1)} = op(\underline{p}^{(n+1)}), iii. (μ.u)^{(n+1)} = μ.u^{(n+1)}, iv. (recP.p)^{(n+1)} = p^{(n+1)}[(recP.p)^{(n)}/P], v. (be ⟶ p, q)^{(n+1)} = be ⟶ p^{(n+1)}, q^{(n+1)},

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

3. ((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 compact approximations have the following fundamental properties:

Theorem 5.2 For all natural numbers n and all t ∈ CCS_{L}

1. t^{(n)} ∈ coCCS_{L}, i.e. t^{(n)} is a compact term.

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

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

Proof

1. and 2. may be proved by an induction on n combined with an inner structural induction.

3. In what remains of the proof we write [[ ]] instead of \overline{ACT} [[ ]]. We have to prove that ⨆[[t^{(n)}]]ρ ^{⊑} [[t]]ρ and [[t]]ρ ^{⊑} ⨆[[t^{(n)}]]ρ. To prove the first inequality it is sufficient to prove that [[t^{(n)}]]ρ ^{⊑} [[t]]ρ for all n. This may be proved in the same way as a similar property for the pure calculus given in Lemma 4.2.10 in [Hen88a]. The proof for the opposite inequality, [[t]]ρ ^{⊑} ⨆[[t^{(n)}]]ρ, again follows the same pattern as the proof for a similar property given in Theorem 4.2.11 in [Hen88a]. The main difference is when t = [x]p ∈ CCS_{L}^{fun}. For this case we may proceed as follows.

It is easy to see that

[[[x]p^{(0)}]]ρ ^{⊑} ⋯ [[[x]p^{(n)}]]ρ ^{⊑} ⋯ ^{⊑} [[[x]p]]ρ.

i.e. that [[[x]p]]ρ is an upper bound of the chain given above. We have to show that it is the least upper bound of the chain. So assume

[[[x]p^{(0)}]]ρ ^{⊑} ⋯ [[[x]p^{(n)}]]ρ ^{⊑} ⋯ ^{⊑} f.

We have to show that [[[x]p]]ρ ^{⊑} f. So assume v ∈ V al. Then v ∈ V_{N} for some N. Therefore, for all n ≥ N,

\begin{matrix}([[([x]p)^{(n)}]]ρ)(v) = ([[[x]x ∈ V_{n} ⟶ p^{(n)}, Ω]]ρ)(v) = \\ [[p^{(n)}[v/x]]]ρ ^{⊑} f(v). \end{matrix}

By the structural induction, [[p[v/x]]]ρ is the least upper bound for the chain

[[p^{(0)}[v/x]]]ρ ^{⊑} [[p^{(1)}[v/x]]]ρ ^{⊑} ⋯ ^{⊑} [[p^{(n)}[v/x]]]ρ ^{⊑} · · · .

This implies that ([[[x]p]]ρ)(v) ^{⊑} f(v). As v ∈ V al was arbitrary this implies that [[[x]p]]ρ ^{⊑} f as wanted.

□

Next we prove the soundness and completeness of the proof system E_{rec} with respect to the model. To prove the completeness we introduce a notion of Ω-normal forms for compact terms and a corresponding normalization theorem.

Definition 5.3 [Ω-normal form] A compact term ct ∈ coCCS_{L} is said to be in Ω-normal form if the following hold:

1. If ct = cp ∈ coCCS_{L}^{proc} then cp has the form

∑_{i} a_{i}.ct_{i}{+Ω}

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

2. If ct = (e, cp) ∈ coCCS_{L}^{pair} then e = v ∈ V al and cp is in Ω-normal form.

3. If ct = [x]x : (v_{1}, …, v_{n}) ⟶ (cp_{1}, … cp_{n}) ∈ F un then cp_{i} is in Ω-normal form for i ≤ n.

□

Lemma 5.4 For all ct ∈ coCCS_{L} there is an Ω-normal form n(ct) such that n(ct) =_{E} ct.

Proof First we define the depth, δ(ct) of a compact term ct by

1. δ(nil) = δ(Ω) = 0,

2. δ(cp \ c) = δ(cp[R]) = δ(cp),

3. δ(cp_{1} + cp_{2}) = max{δ(cp_{i})|i ≤ n},

4. δ(cp_{1}|cp_{2}) = 1 + δ(cp_{1}) + δ(cp_{2}),

5. δ(pre.ct) = 1 + δ(ct), 6. δ((e, cp)) = δ(cp),

7. δ([x].x : (v_{1}, ⋯, v_{n}) ⟶ (cp_{1}, ⋯, cp_{n}) = max{δ(cp_{i})|i ≤ n}.

To prove the result we prove the following stronger result:

For all ct ∈ coCCS_{L} there is a Ω-normal form n(ct) such that n(ct) =_{E} ct and δ(n(ct)) ≤ δ(ct).

To prove this we proceed by induction on δ(ct). The details are left to the reader. □ Note that the notion of Ω-normal forms and the normalization lemma extend to syntactically

finite terms in a natural way. This will be useful later in this study.

Now we will prove the soundness and completeness of the proof system E_{rec} with respect to the denotational semantics. We start with the following lemma.

Lemma 5.5 For all t, u ∈ CCS_{L}, t ^{⊑}_{E} u implies ∃m∀n ≥ m. t^{(n)} ^{⊑}_{E} u^{(n)}.

Proof This may be proved by induction on the depth of the proof for t ^{⊑}_{E} u. The only non-trivial case is the base case when the interleaving law is used. We leave it to the reader to check the details of the proof. □

Theorem 5.6 (Soundness and completeness of the value-finitary proof system) For all t, u ∈ CCS_{L} we have

t ^{⊑}_{E_{rec}} u if and only if ACT [[t]] ^{⊑} ACT [[u]]

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

Proof

Soundness: The soundness of the ω-rule is the content of Theorem 5.2 whereas the soundness of the (rec)-rule follows from the definition of the semantics of recP.p as a least fixed point. What remains to prove is the soundness of E. This, in turn, can be proven by reducing the proof to a proof of the soundness for syntactically compact terms with respect to \overline{K}.

The soundness of E over coCCS_{L} with respect to \overline{K} follows easily from the definition of K and the fact that the elements of coCCS_{L} denote exactly the elements of \overline{K}. Now we may proceed as follows:

Assume t ^{⊑}_{E} u. Then, by Lemma 5.5, for some m, t^{(n)} ^{⊑}_{E} u^{(n)} for all n ≥ m. As t^{(n)}, u^{(n)} ∈ coCCS_{L}, the soundness of E with respect to \overline{K} for this set implies

\overline{K}[[t^{(n)}]] ≺\overline{K} \overline{K}[[u^{(n)}]] for all n ≥ m

or equivalently

\overline{ACT} [[t^{(n)}]] ^{⊑} \overline{ACT} [[u^{(n)}]] for all n ≥ m.

Theorem 5.2.3 implies

ACT [[t]] ^{⊑} ACT [[u]].

Completeness: Again we reduce the proof to proving that E is complete for coCCS_{L} with respect to \overline{K}. We first note that Theorem 5.2 and the ω-algebraicity of the model imply

\overline{ACT} [[t]] ^{⊑} \overline{ACT} [[u]]  ⇒
∀n.\overline{ACT} [[t^{(n)}]] ^{⊑} \overline{ACT} [[u]]  ⇒
∀n∃m.\overline{ACT} [[t^{(n)}]] ^{⊑} \overline{ACT} [[u^{(m)}]] ⇒
∀n∃m.\overline{K}[[t^{(n)}]] ≺ \overline{K}[[u^{(m)}]].

(2)

If E is complete for coCCS_{L} with respect to \overline{K} then

\overline{K}[[t^{(n)}]] ≺ \overline{K}[[u^{(m)}]] ⇒ t^{(n)} ^{⊑}_{E} u^{(m)}.  (3)

Now u^{(m)} ^{⊑}_{E_{rec}} u by Lemma 5.2.2 so (2), (3) and the ω-rule give

\overline{ACT} [[t]] ^{⊑} \overline{ACT} [[u]] ⇒ ∀n.t^{(n)} ^{⊑}_{E_{rec}} u ⇒ t ^{⊑}_{E_{rec}} u.

Thus what remains to prove is the completeness of E over coCCS_{L} with respect to \overline{K}. By Lemma 5.4 and the soundness of E it is even enough to prove the completeness for Ω-normal forms with respect to \overline{K} because:

Assume \overline{K}[[ct_{1}]] ≺ \overline{K}[[ct_{2}]]. By Lemma 5.4 ct_{i} =_{E} n_{i}, i = 1, 2 where n_{i}, i = 1, 2 are Ω-normal forms. By the soundness of E with respect to \overline{K}, \overline{K}[[n_{i}]] = \overline{K}[[ct_{i}]], i = 1, 2 and therefore \overline{K}[[n_{1}]] ≺ \overline{K}[[n_{2}]]. If E is complete for Ω-normal forms with respect to \overline{K} we may conclude that n_{1} ^{⊑}_{E} n_{2}. That ct_{1} ^{⊑}_{E} ct_{2} now follows from the transitivity of the proof system.

To prove the completeness for the Ω-normal forms we proceed as follows:

Assume n_{1}, n_{2} are Ω-normal forms. We have to prove that

\overline{K}[[n_{1}]] ≺ \overline{K}[[n_{2}]] ⇒ n_{1} ^{⊑}_{E} n_{2}.

We proceed by structural induction on n_{1}.

n_{1} = nil + Ω: Obvious.

n_{1} = nil: ∅ = \overline{K}[[nil]] ≺ \overline{K}[[n_{2}]] implies \overline{K}[[n_{2}]] = ∅ and therefore that

n_{2} = nil.

n_{1} = ∑_{i≤n} μ_{i}.t_{i}{+Ω}, n ≥ 1: Then

\overline{K}[[n_{1}]] = \{⟨μ_{i}, \overline{K}[[t_{i}]]⟩|i ≤ n\}[∪\{⊥\}]

where ⊥ ∈ \overline{K}[[n_{1}]] if and only if Ω is a summand of n_{1}. As \overline{K}[[n_{1}]] ≺ \overline{K}[[n_{2}]]

then n_{2} ≠ nil and n_{2} ≠ Ω, i.e. n_{2} has the form

n_{2} = ∑_{j≤m} γ_{j}.u_{j}{+Ω}

and

\overline{K}[[n_{2}]] = \{⟨γ_{j}, \overline{K}[[u_{j}]]⟩|j ≤ m\}[∪\{⊥\}]

where m ≥ 1. Assume that ⟨μ_{i}, \overline{K}[[t_{i}]]⟩ ∈ \overline{K}[[n_{1}]]. Then μ_{i} = γ_{j_{i}} and \overline{K}[[t_{i}]] ≺ \overline{K}[[u_{j_{i}}]] for some j_{i} ≤ m. By induction t_{i} ^{⊑}_{E} u_{j_{i}}. As this holds for any i we get that

∑_{i≤n} μ_{i}.t_{i} ^{⊑}_{E} ∑_{i≤n} γ_{j_{i}}.u_{j_{i}}  (4)

First assume that Ω is a summand in n_{1}. As obviously

Ω ^{⊑}_{E} ∑_{j} γ_{j}.u_{j}{+Ω}

we get, by (4), substitutivity and absorption of the proof system, that

n_{1} = ∑_{i} μ_{i}.t_{i} + Ω ^{⊑}_{E} ∑_{i} γ_{j_{i}}.u_{j_{i}} + ∑_{j} γ_{j}.u_{j}{+Ω} =_{E} n_{2}

which proves the statement in this case. Next assume that Ω is not a summand in n_{1}. This implies that ⊥ ∉ \overline{K}[[n_{1}]] which in turn implies that ⊥ ∉ \overline{K}[[n_{2}]]. We may therefore conclude that Ω is not a summand of n_{2} either. In a similar way as before we get

∑_{j≤m} μ_{i_{j}}.t_{i_{j}} ^{⊑}_{E} ∑_{j≤m} γ_{j}.u_{j}  (5)

where {i_{j}|j ≤ m} ⊆ {1, … n}. Now from (4), (5), the absorption and the substitutivity of the proof system we get

n_{1} = ∑_{i≤n} μ_{i}.t_{i} =_{E} ∑_{i≤n} μ_{i}.t_{i} + ∑_{j≤m} μ_{i_{j}}.t_{i_{i}}
⊑_{E} ∑_{i≤n} γ_{j_{i}}.u_{j_{i}} + ∑_{j≤m} γ_{j}.u_{j} = ∑_{j≤m} γ_{j}.u_{j} = n_{2}

which completes the proof for this case.

n_{1} ∈ coCCS_{L}^{fun}, coCCS_{L}^{pair}: Follows easily from the induction.

□

As a consequence of the soundness and completeness theorem above together with Theorem

5.2.3 we get the following useful corollary.

Corollary 5.7 For all ct ∈ coCCS_{L} and u ∈ CCS_{L}

ct ^{⊑}_{E_{rec}} u implies ct ^{⊑}_{E} u^{(n)} for some n

and therefore

ct ^{⊑}_{E_{rec}} u iff ct ^{⊑}_{E_{rec}^{−ω}} u.

The proof system we have introduced so far is nonstandard in that the ω-rule is based on compact approximations instead of the more common syntactically finite ones. Let t^{n} denote the syntactically finite approximation derived from Definition 5.1 with 2. replaced by ([x]p)^{n+1} = [x]p^{n+1} and 3. by ((e, p))^{n+1} = ([[e]], p^{n+1}) and let ≤_{E_{rec}} denote the corresponding preorder. We refer to this system as the value-infinitary one. It is easy to see that following holds.

Lemma 5.8 For all t, u ∈ CCS_{L},

1. if t ≤_{E_{rec}} u then t ^{⊑}_{E_{rec}} u,

2. if d is syntactically finite then d ≤_{E_{rec}} t iff d ^{⊑}_{E_{rec}^{−ω}} t.

The first part of Lemma 5.8 tells us that the new system is sound with respect to the denotational model. To reason about the completeness of this system turns out to be more complicated. We will postpone the discussion to Section 6 where we show that the completeness of the system follows from results regarding the bisimulation based semantics.

6 Comparison with the Operational Semantics

The subject of this section is to compare the denotational semantics and the operational one given in the previous sections. First we show by an example, Example 6.1, that for the language C CS_{L} 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 about 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 6.1 As we only need an example from the pure calculus, we use the notation \overline{a}.t = c?.[x]t, a.t = c!.(v_{1}, t) 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, up to bisimulation, by the right hand side p. This implies that p + recP.τ.P ⊏̸_{∼} p.

Obviously Example 6.1 rules out the possibility that the behavioural preorder ⊏_{∼} characterizes the preorder of the model over C CS_{L}. 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. This is a straight forward extension of the ω-bisimulation for the pure calculus known from the literature [Mil83].

Definition 6.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 in general. This is explained by the following example.

Example 6.3 If we extend our language with parameterized recursion we can define p = P (1), where P is be given by

P (n) = c?x.[x](x ≤ n ⟶ nil, Ω) + P (n + 1),

and 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 up to ⊏_{∼}_{ω} and consequently q ⊏̸_{∼}_{ω} p.

Whether p and q can be expressed in our language C CS_{L} is not obvious at this point but later we will prove that they cannot.

Intuitively the reason for why ⊏_{∼}_{ω} is too fine to match a preorder induced by an algebraic cpo for processes with values in general is that the values give rise to a new kind of infinity. We recall 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 6.4 [Value-Finitary Strong Applicative ω-Prebisimulation] Let AT = ⟨Con, V al, Act, ⟶, ↓⟩ be an applicative labelled 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}}.

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+1}^{f}⊆⊏_{∼}_{n}^{f} for all n. We also note that the only difference between this definition and Definition 6.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.5. The proof for this is straightforward and is left to the reader. Now let us have a further look at our previous example, Example 6.3.

Example 6.5 Let p and q be defined as in Example 6.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 6.6

1. On any ALTS, ⊏_{∼}⊆⊏_{∼}_{ω}⊆⊏_{∼}_{ω}^{f}.

2. There is an ALTS on which ⊏_{∼}_{ω}^{f}⊈⊏_{∼}_{ω}⊈⊏_{∼}.

7 The Full Abstractness

We have already proven that he preorder ^{⊑}_{E_{rec}} and the preorder induced by the denotational model, which we from now on refer to as^{⊑}\overline{ACT}, coincide over CCS_{L}. In this section we will prove that ⊏_{∼}_{ω}^{f} also coincides with these preorders over this language. Furthermore we prove that the preorders ⊏_{∼}_{ω} and ≤_{E_{rec}} also coincide. Finally we show that over the language CCS_{L}, all five preordered mentioned above, coincide. Here we want to remind the reader of, that considered over a general ALT S, ⊏_{∼}_{ω} is strictly included in ⊏_{∼}_{ω}^{f}. Also it should be clear from Example 6.3 that in general ≤_{E_{rec}} cannot be expected to coincide with a preorder derived from an algebraic model (although at this point it is not clear how the syntactically finite or compact approximations should look like for languages with parameterized recursion).

To prove that ^{⊑}_{E_{rec}}=⊏_{∼}_{ω}^{f} over CCS_{L} it is sufficient to prove the soundness and the completeness of the rules that define ^{⊑}_{E_{rec}} with respect to ⊏_{∼}_{ω}^{f} over this language. Similarly, as clearly ≤_{E_{rec}}⊆^{⊑}_{E_{rec}}, to prove that ≤_{E_{rec}}=⊏_{∼}_{ω}, it is sufficient to prove that the rules that define ≤_{E_{rec}} are sound and complete with respect to ⊏_{∼}_{ω} over this language.

We start by proving the first of these three properties. In the proof we will use some standard techniques which are used to prove similar completeness results in the literature [Hen88a, AH92, HI93]. Therefore we start by defining a suitable notion of a “finitary part”, i. e. the value-finitary part, of a relation over processes and that of a value-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 syntactically finite or recursion-free terms. We will then show that the preorder ⊏_{∼}_{ω}^{f} is the value-finitary part of the preorders ⊏_{∼} and ⊏_{∼}_{ω}^{f} and therefore that ⊏_{∼}_{ω}^{f} is value-finitary in our sense. We start by defining the value-finitary part of a relation over CCS_{L}.

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

tR^{F} u iff for all ct ∈ coCCS_{L}, ctRt implies ctRu.

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

The following lemma shows how we may structure the proof of full abstractness.

Lemma 7.2 Assume that the preorder ⪯ ⊆ CCS_{L} × CCS_{L} satisfies the following conditions:

1. Value-finitariness: For all t, u ∈ CCS_{L} t ⪯ u iff ∀ct. ct ⪯ t ⇒ ct ⪯ u.

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

3. Partial completeness: For all ct ∈ coCCS_{L} and t ∈ CCS_{L} ct ⪯ t implies ct ^{⊑}_{E_{rec}^{−ω}} t.

Then for all t, u ∈ CCS_{L}

t ⪯ u if and only if t ^{⊑}_{E_{rec}} u.

Proof First we have:

t ⪯ u
iff ∀ct. ct ⪯ t ⇒ ct ⪯ u  by 1.
iff ∀ct. ct ^{⊑}_{E_{rec}^{−ω}} t ⇒ ct ^{⊑}_{E_{rec}} u by 2. and 3.

Now we proceed as follows: Assume t ⪯ u and therefore that

∀ct. ct ^{⊑}_{E_{rec}^{−ω}} t ⇒ ct ^{⊑}_{E_{rec}^{−ω}} u.  (6)

As t^{(n)} ^{⊑}_{E_{rec}^{−ω}} t and t^{(n)} ∈ coCCS_{L} then (6) implies that t^{(n)} ^{⊑}_{E_{rec}} u. As this holds for all n, the ω-rule implies that t ^{⊑}_{E_{rec}} u.

Next assume that t ^{⊑}_{E_{rec}} u. To prove that t ⪯ u it is sufficient to prove that (6) holds. So assume that ct ^{⊑}_{E_{rec}^{−ω}} t. Then, by transitivity of ^{⊑}_{E_{rec}^{−ω}}, ct ^{⊑}_{E_{rec}^{−ω}} u. □

7.1 Value-finitariness

Following [Hen81] next we will prove that on coCCS_{L} × CCS_{L} the preorders ⊏_{∼} and ⊏_{∼}_{ω}^{f} coincide. Consequently they both have the same value-finitary part. To show this we need a measure on coCCS_{L} that both measures the structural depth of the term and the number of values it uses. We give the following definitions.

Definition 7.3 For a syntactically finite term 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 d ⟶^{μ} t then sd(t) ≤ sd(d) − 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 non-trivial way. Formally this is defined as follows:

Definition 7.4 The support of the term ct ∈ coCCS_{L}, Supp(ct), is defined by structural recursion as:

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

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

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

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

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

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

and therefore (⊏_{∼}_{ω}^{f})^{F} =⊏_{∼}^{F} on CCS_{L}. Proof As the “if” part is already known it is sufficient to prove the “only if” part. To this end we prove the following stronger result.

For all ct ∈ coCCS_{L} and t ∈ CCS_{L}

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

for all m where m ≥ M(ct) = sd(ct) + vd(ct). The proof of this statement proceeds by induction on M(ct). M(ct) = 0: We have two cases: ct = Ω, which is trivial, and ct = nil which we will have a

further look at. As nil ↓, the definition of ⊏_{∼}_{m}^{f} implies that t ↓. Furthermore as nil −̸→^{μ} for all μ this is also true for t. This proves that ct = nil ⊏_{∼} t.

M(ct) = k + 1: Assume we have proved the result for all ct′ with M(ct′) ≤ k and that ct ⊏_{∼}_{m}^{f} t, where m ≥ M(ct) = k + 1. We want to prove that ct ⊏_{∼} t. As F(⊏_{∼}) =⊏_{∼}, it is sufficient to show that ctF(⊏_{∼})t. We proceed by case analysis on the structure of ct. ct ∈ CCS_{L}^{proc}:

1. Assume ct ⟶^{μ} u. By definition of ⊏_{∼}_{m}^{f}, t ⟶^{μ} u′ for some u′ such that u ⊏_{∼}_{m−1}^{f} u′. Also, by definition of coCCS_{L}, u ∈ coCCS_{L}. Now vd(u) ≤ vd(ct) and sd(u) < sd(ct). Thus m − 1 ≥ k ≥ M(u) and by the induction u ⊏_{∼} u′.

2. Now assume ct ↓, by definition of the preorder ⊏_{∼}_{ω}^{f} also t ↓. Furthermore assume that ct ↓, t ↓ and that t ⟶^{μ} u′. Then ct ⟶^{μ} u for some u such that u ⊏_{∼}_{m−1}^{f} u′. In a similar way as before, the induction implies u ⊏_{∼} u′, which completes the proof in this case. ct ∈ coCCS_{L}^{fun}: Then t and ct have the form t = [x]p′ where x ∈ V ar, p′ ∈ C CS_{L}^{proc}

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

ct ∈ coCCS_{L}^{pair}: Now ct = (v′, cp′) and t = (v′′, p′′). By the definition of the preorder and the assumption on m, v′ = v′′ ∈ V_{m} and cp′ ⊏_{∼}_{m}^{f} p. As before m > k ≥ M(cp′) 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 7.6 The sort of t ∈ CCS_{L}, Sort(t) ⊆ Chan, is given by

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

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

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

□

Note that, because of our restriction to finite renamings, Sort(t) is finite for all t [Abr91, AH92].

Definition 7.7 (Compact Projections) We define the n-th projection of t on coCCS_{L} inductively as follows:

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

(b) p^{[n+1]} = ∑{μ.t^{[n]}|p ⟶^{μ} t} + {Ω|p ↑},

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. (v, p)^{[n+1]} = \{ \begin{matrix}(v, p^{[n+1]}) & if v ∈ V_{n+1,} \\ (v, Ω) & 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 7.8 For all t ∈ CCS_{L} and all n,

1. t^{[n]} ∈ coCCS_{L},

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

Proof Follows by a simple induction on n, combined with an inner induction on the structural depth of t for the inductive step. □

The following results investigate the relationship between a term t and its syntactically compact projections in more detail. Lemma 7.9 For all t, u ∈ CCS_{L}

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

2. If t^{[0]} ⊏_{∼}_{ω}^{f} t^{[1]} ⊏_{∼}_{ω}^{f} ⋯ ⊏_{∼}_{ω}^{f} t^{[n]} ⊏_{∼}_{ω}^{f} ⋯ ⊏_{∼}_{ω}^{f} u then t ⊏_{∼}_{ω}^{f} u, i.e. t is a minimal upper bound ^{2}

of the chain with respect to ⊏_{∼}_{ω}^{f}.

3. The term t is a minimal upper bound for the set App(t) = {ct ∈ coCCS_{L}|ct ⊏_{∼}_{ω}^{f} t} with respect to ⊏_{∼}_{ω}^{f}.

Proof

1. We first prove that for all n

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

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

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

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

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

and we will prove that

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

To this end assume m ≥ k. We proceed by induction on the structural depth of t. We have the following cases. t = p ∈ CCS_{L}^{proc}: Assume p^{[k+1]} ⟶^{μ} t, then p ⟶^{μ} u for some u such that u^{[k]} = t.

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

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

t = [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]}

and the result follows from the inner induction, 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.

t = (v, p) ∈ CCS_{L}^{pair}: Similar.

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

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

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

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

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

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

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

□

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

Theorem 7.10 Over CCS_{L} following holds.

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

2. The preorder ⊏_{∼}_{ω}^{f} is the value-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

∀ct ∈ coCCS_{L}. ct ⊏_{∼}_{ω}^{f} t implies ct ⊏_{∼}_{ω}^{f} u.

This is equivalent to saying that App(t) ⊆ App(u) and the result follows from Lemma 7.9.

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

□

7.2 Partial Soundness and Completeness

This 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 follows from the following Lemma.

Lemma 7.11 (Partial Soundness) The proof system E_{rec}^{−ω} is sound with respect to ⊏_{∼} over CCS_{L}.

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

t ^{⊑}_{E_{rec}^{−ω}} u implies t ⊏_{∼} u

by induction on the depth of the proof tree for t ^{⊑}_{E_{rec}^{−ω}} u. 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 6.1. Furthermore at this point we have not proved the soundness of the ω-rules for ⊏_{∼}_{ω} or ⊏_{∼}_{ω}^{f}. Next we prove the mentioned partial completeness result, i.e. that for all ct and t,

ct ⊏_{∼} t ⇒ ct ^{⊑}_{E_{rec}} t.

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 7.12 A term in C CS_{L}^{proc} is said to be in a head normal form if it has the form ∑_{i} μ_{i}t_{i}.

□

Lemma 7.13 If p ∈ CCS_{L}^{proc} and p ↓ then there is a head normal form, hnf(p), such that p =_{E_{rec}^{−ω}} hnf(p).

Proof We prove the Lemma by induction on the length of the derivation of p ↓. We proceed by a case analysis on the structure of p. □ Here it is important to notice that we only use the partial proof system E_{rec}^{−ω} in the normal-

ization procedure as the soundness of the ω-rule with respect to the preorder ⊏_{∼}_{ω}^{f} has not been proven yet.

Notation 7.14 Let p, q ∈ C CS_{L}^{proc} and t, u ∈ CCS_{L}. 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 p ⟶^{μ} p′ then p|q ⟶^{μ} abs(p′|q) and q|p ⟶^{μ} abs(q|p′). Furthermore if p ⟶^{c!} o and q ⟶^{c?} f then p|q ⟶^{τ} app(o|f) and q|p ⟶^{τ} app(f|o). We use this notation to formulate the following lemma:

Lemma 7.15 For all p ∈ CCS_{L}^{proc}, t ∈ CCS_{L} and μ we have that p ⟶^{μ} t implies p =_{E_{rec}} p + μ.t.

Proof We prove the statement by proving that for all closed terms p, q and t following holds:

1. (p + μ.t)|q =_{E_{rec}} (p + μ.t)|q + μ.abs(t|q)

2. q|(p + μ.t) =_{E_{rec}} q|(p + μ.t) + μ.abs(q|t)

3. (p + a.t)|(q + \overline{a}.u) =_{E_{rec}} (p + a.t)|(q + \overline{a}.u) + τ.app(t|u).

The proof is basically identical to a proof for similar properties in [AH92] and is omitted. □

Theorem 7.16 (Partial Completeness) For all ct ∈ coCCS_{L} and tCCS_{L}, ct ⊏_{∼} t implies ct ^{⊑}_{E_{rec}^{−ω}} t.

Proof It is sufficient to prove the result for ct in Ω-normal form as the general result follows from the normalization result in Lemma 5.4, and the soundness of ^{⊑}_{E_{rec}^{−ω}} with respect to ⊏_{∼}. We proceed by a case analysis on the form of ct but only give the details of the case where ct = cp ∈ coCCS_{L}. In this case t = p ∈ CCS_{L}^{proc}.

To this end assume np ⊏_{∼} p where np is an Ω-normal form and we will prove that np ^{⊑}_{E_{rec}} p. The proof proceeds by induction on sd(np), the structural depth of np defined in Definition 7.3. 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}^{−ω}} p.

np = nil: nil ⊏_{∼} p implies p ↓. Thus p has a head normal form h(p) with h(p) =_{E_{rec}^{−ω}} p. As nil −̸→^{μ}, h(p) −̸→^{μ} for all μ which implies that h(p) = nil. Therefore np =_{E_{rec}^{−ω}}

h(p) =_{E_{rec}^{−ω}} p.

np = ∑_{i} μ_{i}.p_{i}{+Ω}: We prove this case in three steps.

1. p+np ^{⊑}_{E_{rec^{−ω}}} p: Assume np ⟶^{μ} p′ then μ = μ_{i} and p′ = p_{i} for some i. As np ⊏_{∼} p this implies that p ⟶^{μ_{i}} q_{i} for some q_{i} where p_{i} ⊏_{∼} q_{i}. By applying the induction hypothesis we obtain that p_{i} ^{⊑}_{E_{rec}^{−ω}} q_{i} and, by substitutivity, that μ_{i}.p_{i} ^{⊑}_{E_{rec}^{−ω}} μ_{i}.q_{i}. Thus by substitutivity and Lemma 7.15

p + μ_{i}.p_{i} ^{⊑}_{E_{rec}^{−ω}} p + μ_{i}.q_{i} =_{E_{rec^{−ω}}} p.

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

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

respect to ⊏_{∼}, np ⊏_{∼} h(p). Thus p ⟶^{γ_{j}} q_{j} implies that γ_{j} = μ_{i_{j}} for some i_{j} and that

np ⟶^{μ_{i_{j}}} p_{i_{j}} for some p_{i_{j}} such that p_{i_{j}} ⊏_{∼} q_{j}. Now by proceeding in a similar way as in the previous case we get that

np = np + ∑_{j} μ_{i_{j}}.p_{i_{j}} ^{⊑}_{E_{rec}^{−ω}} np + ∑_{j} γ_{j}.q_{j} ^{⊑}_{E_{rec}^{−ω}} np + p.

3. Finally 1. and 2. imply np ^{⊑}_{E_{rec}^{−ω}} p.

The remaining cases can be proven in a similar way. □

Theorem 7.17 (Soundness and completeness of the value-finite) For all t, u ∈ CCS_{L},

t ⊏_{∼}_{ω}^{f} u if and only if t ^{⊑}_{E_{rec}} u.

Proof This follows from Theorem 7.2 as the conditions of the theorem are ensured by Theorem 7.10, Lemma 7.11 and Theorem 7.16. □

Theorem 7.18 (Soundness and completeness for value-infinite proof system) For all t, u ∈ CCS_{L},

t ⊏_{∼}_{ω} u if and only if t ≤_{E_{rec}} u.

Proof If we replace the “compact elements” t in Theorem 7.2 by “syntactically finite elements” d and ^{⊑}_{E_{rec}} by ≤_{E_{rec}}, its statement still holds (and exactly the same proof applies). Thus it is sufficient to prove that properties 1., 2. and 3. of that theorem hold for ⊏_{∼}_{ω} with these changes.

The proof of property 1., i.e. that

(∀d.d ⊏_{∼}_{ω} p ⇒ d ⊏_{∼}_{ω} q) implies p ⊏_{∼}_{ω} q,

is a simplification of the proof of Theorem 7.10, the main difference being that we replace ⊏_{∼}_{ω}^{f} by ⊏_{∼}_{ω}, the “compact terms” by the “syntactically finite terms” and the “compact projections” in Definition 7.7 by a similar notion of “syntactically finite projections” t^{{n}} t^{[n]} obtained from the same definition with the second clause replaced by ([x]p)^{{n+1}} = [x]p^{{n+1}} and the third one by (v, p)^{{n+1}} = (v, p^{{n+1}}). Property 2. is still the content of Lemma 7.11 and 3. can be obtained in exactly the same way as the proof of Theorem 7.16 with the notion of Ω-normal forms extended to syntactically finite terms instead of only applying to compact terms. The details of the proof are left to the reader to check. □ Finally we compare the value-finitary and value-infinitary semantics.

Theorem 7.19 \overline{ACT} [[t]] ^{⊑} \overline{ACT} [[u]] iff t ⊏_{∼}_{ω} u.

Proof Clearly we only have to prove the “only if” implication”. We will give an outline of the proof but refer to [Ing94, Chap.2-3] where the details of a similar proof are given. Let (D, ≺) be the preordered set defined in the same way as (K, ≺) in Definition 4.10 but with clause 2. replaced by

2.′ c ∈ C, f ∈ V al ⟶ D implies ⟨c?, f⟩ ∈ D.

Furthermore we define D_{n} as the subset of D consisting of elements of depth at most n, ordered as before. We also define the operators exactly in the same way as on K. In the following we write [[ ]] instead of \overline{ACT} [[ ]] and ^{⊑} instead of ^{⊑}\overline{ACT}. Then the following holds (up to isomorphism in some cases):

1. The unique (Σ, C)-domain induced by (\overline{D}, ≺, Σ\overline{D}, C\overline{D}) is isomorphic to \overline{ACT}.

2. D_{0} ◁ D_{1} ◁ … is a directed ω-chain with ACT as the co-limit.

3. For each i there is projection mapping ^{i} : D ⟶ D^{i} that has the following properties:

(a) If d ∈ ACT then d^{i} ∈ D_{i} and d^{i} ^{⊑}_{ACT} d.

(b) If e ∈ D_{i} and e ^{⊑} d ∈ ACT then e ^{⊑} d^{i}.

(c) d = ⨆_{i} d^{i}.

(d) If d is a syntactically finite closed process term then [[d]] ∈ D_{i} for some i.

(e) For all i and p, [[p^{{i}}]] = [[p]]^{i}. (This property can be proven by induction on i; it is language dependent and is actually the key to the proof of the full abstractness of the model with respect to ⊏_{∼}_{ω} for the language C CS_{L}. Again we remind the reader of that in general these two semantics do not coincide as explained earlier.)

Now we proceed as follows:

[[p]] ^{⊑} [[p]] implies ∀i.[[p]]^{i} ^{⊑} [[q]]^{i} implies ∀i.[[p^{{i}}]] ^{⊑} [[q^{{i}}]].

By induction on i we may prove that

∀i.p^{{i}} ⊏_{∼}_{ω} q^{{i}} ⊏_{∼}_{ω} q

which in turn implies that p ⊏_{∼}_{ω} q. □

8 Conclusion

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

In this paper we have defined a syntax and three kinds of semantics that support the late approach for value-passing calculi. First we defined a general syntax that supports this approach by extending the standard notion of a signature to the so-called applicative signature, a pair (Σ, C) consisting of a signature Σ and a set of channels C. Then we defined the language Late-CCS (C CS_{L}) which is a modification of the standard CCS with values due to the late semantic approach. This language is basically the π-calculus where the values allowed for are restricted to be of the simple type only. The language is obtained as an instantiation of the general class of languages we defined where the signature Σ is taken to be the set of the standard operators of CCS.

Then we defined 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.

Next we have set up a general framework for describing the denotational semantics for value-passing calculi which support the late approach. For this purpose the standard notion of Σ-algebras and Σ-orders have been extended to (Σ, C)-algebras and (Σ, C)-orders.

A denotational model for Late-CCS is defined, an instantiation of the general class of models we defined. The carrier set of this model is an ω-algebraic cpo and is obtained as a ideal completion of the kernel of a suitably defined partial order. The operators are defined by first defining them as monotonic functions on the preorder, taking the induced monotonic functions on the kernel and taking their unique continuous extension to the whole cpo.

Of historical reasons the carrier of the model is also described as the solution to a recursive domain equation. It is a direct extension of a similar equation given by Abramsky in [Abr91] and a modification of the one given by Milne and Milner in [MM79]. As all the constructions we use in the definition of the equation are standard and well known to preserve completeness and ω-algebraicity the solution we obtain is an ω-algebraic cpo. By unfolding the recursive definition we get a representation of the compact elements, a preorder that turns out to coincide with our original preorder used to construct the model.

We have also presented two equationally based proof systems and compared them to the model. The first one is based on the ability of approximating infinite terms by so-called compact terms, syntactically finite terms which are interpreted as compact elements in the model, and is proven to be sound and complete with respect to the model. The algebraicity of the model and the way we define the operators makes it possible for us to reduce the proof of the soundness and completeness to a proof of the same property on a sub-language of the actual language, the so-called compact terms. This is an inductively defined language which denotes exactly the compact elements of the model.

The second proof system is based on the more standard syntactically finite approximation. The soundness of this proof system follows directly from the soundness of the stronger proof system based on the compact approximations. To prove the completeness of this system we have to prove that if p is smaller than q in the model then necessarily all the syntactic approximations of p have to be smaller than q in the model too. The proof of this property turned out to be nontrivial and was postponed until the investigation of the operational semantics.

Our next task was to compare the three different kinds of semantics we had put forward so far. First we show that for Late-C CS the original late bisimulation is too strong to meet the preorder of the model ACT. The algebraicity of the model implies that the preorder in the model is completely determined by the compact elements. Behaviourally this can be interpreted as meaning that the preorder may be obtained by some kind of finite observations. This is not the case for bisimulation as it is well known even for the pure calculus. Therefore we define a value-finitary version of the preorder ⊏_{∼}_{ω}^{f} is defined by mimicking the ω-algebraicity of the model on the syntactical level and requiring that it is completely decided by the syntactically compact elements. This preorder is shown to coincide with the preorder in the model in the sense that the model is fully abstract with respect to it by proving that the value-finitary proof system is sound and complete with respect to it.

We also show that the ω-prebisimulation ⊏_{∼}_{ω} is in general strictly finer than ⊏_{∼}_{ω}^{f} but if restricted to CCS_{L} it is fully abstract with respect to the denotational model and thus coincides with ⊏_{∼}_{ω}^{f}. To prove this we have to appeal to more general results regarding the constructions of the type of model we offer. Thus we recall that the cpo ACT may be obtained as the co-limit of an ω-chain of domains (D_{i})_{i∈ω} each of which consist of trees of finite depth but which are not necessarily value finite. Consequently each element d of ACT can be approximated by an ω-chain (d^{i})_{i∈ω} of finitely deep trees which are not necessarily compact elements. The key to the completeness proof is the observation that for any t ∈ CCS_{L} and any i, \overline{ACT} [[t^{\{i\}}]] = \overline{ACT} [[t]]^{i} where t^{\{i\}} is the ith syntactically finite projection that appears in the proof of the finitariness of ⊏_{∼}_{ω} and d^{i} is the the projection on D_{i}, the ith approximation of the cpo ACT. This is a language dependent property that cannot be expected to hold in such languages in general as Example 6.3 shows.

The example we used to distinguish ⊏_{∼}_{ω} and ⊏_{∼}_{ω}^{f} was expressed in an extension of C CS_{L} that allows for parameterized recursive definitions. Therefore we may conclude that this extension of C CS_{L} is strictly more expressive than C CS_{L}.

The main conclusion we can draw from the study performed in this paper is that operational semantics is more intuitive and in general more suitable for describing the semantics for communicating processes than denotational semantics, in particular if the communication involves exchange of data. However denotational models, based on an algebraic cpo, automatically ensure the finitariness of the semantics, a property that is reasonable to require from such a semantic description.

An obvious extension of this work would be to give a similar theory for the more useful version of C CS_{L} that allows parameterized recursion.

Acknowledgment

The author would like to thank the anonymous referees for many useful comments that led to a thorough revision of the paper.

References

[Abr87] S. Abramsky. Domain theory in logical form. Annals of Pure and Applied Logic, 51(01):1–78, 1991.

[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.

[DZ82] J. W. de Bakker and J. I. Zucker. Processes and the denotational semantics of concurrency. Information and Control, 54(1/2):70-120, July/August 1982.

[FMS96] M. Fiore, E. Moggi and D. Sangiorgi. A Fully-Abstract Model for the π-calculus.

In Proceedings of the Eleventh Annual IEEE Symposium on Logic in Computer Science, pages 43–54. IEEE Computer Society Press, 1996.

[GTWW77] J.A. Goguen, J.W. Thatcher, E.G. Wagner, and J.B. Wright. Initial algebra semantics and continuous algebras. Journal of the ACM, 24(1):68–95, 1977.

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

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

[Hen94] M. Hennessy. A fully abstract denotational model for higher-order processes. Information and Computation, 112(1):55–95, July 1994.

[Hen00] M. Hennessy. A fully abstract denotational semantics for the pi-calculus.

To appear in Theoretical Computer Science.

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

[HL93a] M. Hennessy and H. Lin. Proof systems for message-passing process algebras. In E. Best, editor, Proceedings of CONCUR 93, Hildesheim, volume 715 of Lecture Notes in Computer Science, pages 202–216. Springer-Verlag, 1993.

[HL93b] M. Hennessy and X. Liu. A modal logic for message passing processes. In C. Courcoubetis, editor, Proceedings of the Fifth International Conference Computer Aided Verification, Elounda, Greece, July 1993, volume 697 of Lecture Notes in Computer Science, pages 359–370. Springer-Verlag, 1993.

[Hoa78] C.A.R. Hoare. Communicating sequential processes. Communications of the ACM, 21(8):666–677, 1978.

[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.

[Ing93] A. Ingólfsdóttir. Late and early semantics coincide for testing. Theoretical Computer Science, 146:341–349,1995.

[Ing94] A. Ingólfsdóttir. Semantic Models for Communicating Process with Value-Passing. PhD thesis, School of Cognitive and Computing Sciences, University of Sussex, June 1994. Computer Science Report 8/94. Also available as Report R–94–2044, Department of Mathematics and Computer Science, Aalborg University.

[Mil80] R. Milner. A Calculus of Communicating Systems, volume 92 of Lecture Notes in Computer Science. Springer-Verlag, 1980.

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

[Mil89] R. Milner. Communication and Concurrency. Prentice-Hall International, Englewood Cliffs, 1989.

[Mil91] R. Milner. The polyadic π-calculus: a tutorial. Technical Report ECS–LFCS–91– 180, LFCS, Department of Computer Science, University of Edinburgh, October 1991. In Proceedings of the International Summer School on Logic and Algebra of Specification, Marktoberdorf, August 1991.

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

[MPW91] R. Milner, J. Parrow, and D. Walker. Modal logics for mobile processes. In J.C.M. Baeten and J.F. Groote, editors, Proceedings CONCUR 91, Amsterdam, volume 527 of Lecture Notes in Computer Science, pages 45–60. Springer-Verlag, 1991.

[MPW92] R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes, Part I + II. Information and Computation, 100(1):1–77, 1992.

[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.

[Plo76] G.D. Plotkin. A powerdomain construction. SIAM Journal on Computing, 5:452–487, 1976.

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

[Plo81] G.D. Plotkin. Lecture notes in domain theory, 1981. University of Edinburgh.

[San93] D. Sangiorgi. From π-calculus to higher-order π-calculus — and back. In TAP-SOFT ’93, volume 668 of Lecture Notes in Computer Science. Springer-Verlag, 1993.

[Smy78] M. Smyth. Powerdomains. Journal of Computer and System Sciences, 16(1), 1978.

[Sta96] I. Stark. A Fully Abstract Domain Model for the π-Calculus. In Proceedings of the Eleventh Annual IEEE Symposium on Logic in Computer Science, pages 36–42. IEEE Computer Society Press, 1996.

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

[Tho89] B. Thomsen. Plain CHOCS. Report DOC 89/4, Department of Computing, Imperial College, 1989.

[Win85] G. Winskel. On powerdomains and modality. Theoretical Computer Science, 36:127–137, 1985.

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

Recent BRICS Report Series Publications

RS-03-15 Anna Ingólfsdóttir. A Semantic Theory for Value–Passing Processes Based on the Late Approach. March 2003. 48 pp.

RS-03-14 Mads Sig Ager, Dariusz Biernacki, Olivier Danvy, and Jan Midtgaard. From Interpreter to Compiler and Virtual Machine: A Functional Derivation. March 2003. 36 pp.

RS-03-13 Mads Sig Ager, Dariusz Biernacki, Olivier Danvy, and Jan Midtgaard. A Functional Correspondence between Evaluators and Abstract Machines. March 2003. 28 pp.

RS-03-12 Mircea-Dan Hernest and Ulrich Kohlenbach. A Complexity Analysis of Functional Interpretations. February 2003. 70 pp.

RS-03-11 Mads Sig Ager, Olivier Danvy, and Henning Korsholm Rohde. Fast Partial Evaluation of Pattern Matching in Strings. February 2003. 14 pp. To appear in Leuschel, editor, ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation, PEPM ’03 Proceedings, 2003.

RS-03-10 Federico Crazzolara and Giuseppe Milicia. Wireless Authentication in χ-Spaces. February 2003. 20 pp.

RS-03-9 Ivan B. Damgård and Gudmund Skovbjerg Frandsen. An Extended Quadratic Frobenius Primality Test with Average and Worst Case Error Estimates. February 2003. 53 pp.

RS-03-8 Ivan B. Damgård and Gudmund Skovbjerg Frandsen. Efficient Algorithms for gcd and Cubic Residuosity in the Ring of Eisenstein Integers. February 2003. 11 pp.

RS-03-7 Claus Brabrand, Michael I. Schwartzbach, and Mads Vanggaard. The METAFRONT System: Extensible Parsing and Transformation. February 2003. 24 pp.

RS-03-6 Giuseppe Milicia and Vladimiro Sassone. Jeeg: Temporal Constraints for the Synchronization of Concurrent Objects. February 2003. 41 pp. Short version appears in Fox and Getov, editors, Joint ACM-ISCOPE Conference on Java Grande, JGI ’02 Proceedings, 2002, pages 212–221.

RS-03-5 Aske Simon Christensen, Anders Møller, and Michael I. Schwartzbach. Precise Analysis of String Expressions. February 2003. 15 pp.