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

BRICS

Basic Research in Computer Science

A Semantic Theory for Value�Passing Processes Late Approach

Part I: A Denotational Model and Its Complete Axiomatization

Anna Ing� olfsd� ottir

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

University of Aarhus. All rights reserved.

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

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

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

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

A Semantic Theory for Value–Passing Processes Late Approach

Part I: A Denotational Model and Its Complete Axiomatization

Anna Ingólfsdóttir

BRICS^{∗}

Department of Mathematics and Computer Science Aalborg University, Denmark

Abstract A general class of languages and denotational models for value-passing calculi based on the late semantic approach is defined. A concrete instantiation of the general syntax is given. This is a modification of the standard CCS according to the late approach. A denotational model for the concrete language is given, an instantiation of the general class. An equationally based proof system is defined and shown to be sound and complete with respect to the model.

1 Introduction

In the original work of Milner, [Mil80], on CCS and Hoare, [Hoa78], on CSP, 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, \overline{c}(x).p) is interpreted as a non-deterministic choice between pure terms of the form \overline{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.

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 inputting process has to accept whatever value the output process has to offer. This may be interpreted as if the result of the reception of the value is delayed until the process has received the value. The input process reports the willingness to communicate on a channel, c, by performing an action of the form \overline{c}, and thereby evolves 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.

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

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 give it a specific name.

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, Ing94, Ing93]).

In this series of two companion papers we will try to contribute to the studies of the late semantics of communicating processes. We will concentrate on processes which allow 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 late 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).

To make our studies more complete we follow the line of [Hen88a] and [HI93] and introduce a trinity of semantic descriptions for a CCS like process language and show their equivalence. More precisely we give an operational or behavioural semantics in terms of an extended version of labelled transition systems and corresponding bisimulation based relations, axiomatic semantics by means of an equationally based proof system and denotational semantics following the Scott-Strachey approach. 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 in the sequel to this paper, [Ing95a].

One of the main purposes of this series of papers is to give an operational characterization of the denotational interpretation of a value-passing process in an algebraic cpo. Therefore we start by giving a denotational characterization of value-passing processes using the late principle. We also give an equationally based proof system which can be naturally derived from the denotational semantics and show its soundness and completeness with respect to the denotational semantics. This is the content of this paper. Its sequel, [Ing95a], is devoted to defining operational semantics, analysing operationally the denotational semantics and to define a reasonable behavioural relation between processes which characterizes the relation induced by the denotational semantics. All three models are based on the idea of bisimulation.

In this paper, Part I in the series, we will develop a semantic theory for processes with values based on the idea of (strong) bisimulation with emphasis on the late approach. The semantics will be denotational and we shall follow the Scott-Strachey approach. Our development will proceed in two steps. First we describe a general theory for denotational semantics of value-passing processes and then we apply this theory to define a concrete model for our specific language. For the general theory we introduce both a general syntax and a general class of mathematical models to model process algebras with values which support the late semantic approach. For this purpose we introduce the general notion of applicative signature (Σ, C) and that of (Σ, C)-terms where Σ is a set of operators and C a set of channel names. We also introduce the general class of applicative (Σ, C)-domains to model the semantics of the (Σ, C)-terms. These are a direct generalizations of the standard notion of signature, Σ, Σ– terms and Σ-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. 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.

As the next step in the development of the general theory we apply the following general result for algebraic cpos ([Hen88a]):

Functions which are monotonic on the partial order consisting of the compact elements of an algebraic cpo can be extended to continuous functions on the whole cpo in a unique way.

This property enables us to turn an algebraic cpo into a (Σ, C)-model by defining the operators on the compact elements and making sure that they are monotonic. We may then use the standard result quoted above and take their unique continuous extension to be their definition on the whole domain.

By defining the operators this way, i.e. first as monotonic endofunctions on the partial order of 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, then applying it to something finitely computable should 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 following example illustrates this.

Assume that ⟨D,^{⊑}⟩ is an algebraic cpo with the set of compact elements Comp(D) ≠ D. Let d_{0} ∈ D \ Comp(D) and define the constant mapping f_{d_{0}} : D ⟶ D by

∀d ∈ D.f_{d_{0}}(d) = d_{0}

It is easy to show that f_{d_{0}} is continuous but that for any d ∈ D, f_{d_{0}}(d) ∉ Comp(D).

We complete the general theory by describing a procedure to construct the mentioned (Σ, C)-structure on a predefined algebraic cpo.

Next 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 the transmission of simple values in communications. Then we define a concrete denotational model for CCS_{L}, the domain of Applicative Communication Trees (ACT), based on the general theory described above. It is an instantiation of the general class of (Σ, C)-domains, where Σ is instantiated with the operators of CCS_{L}. The definition of this 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 from the types 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 process domain 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. Also the embedding of the empty set (which corresponds to the inactive and convergent process) as the top element of the model is intuitively incorrect. 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 defined his model in terms of the Plotkin Power Domain instead of the Smyth Power Domain. 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. He then interpreted the calculus SCCS in the model and showed the full abstractness of this interpretation with respect to a bisimulation based preorder.

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 models value-passing based on the late approach using the Plotkin Power Domain with the empty set adjoined as an isolated element. Then we apply the general theory described above to define the operators over such a domain, i.e. by defining them as monotonic endofunctions on the po of compact elements and then extending them to continuous functions on the whole domain.

The definition of the denotational model supports in a natural way a system of equations and inference rules. We define such a proof system and prove its soundness and completeness with respect to the model. The ω-algebraicity of the model together with the fact that the operators preserve compactness enables us to reduce the proof of completeness and soundness to a proof of the same property for a sublanguage which denotes exactly the compact elements of the model.

2 A General Framework for Late Semantics

In [Hen88a] a semantic theory for process algebras describing concurrent languages with pure synchronization is given by means of Σ-domains. Adding values to the language calls for more complicated mathematical structures to describe the semantics. In this section we define a general class of mathematical structures to model process algebras with values which support the late semantic approach described in the introduction. For this purpose we extend the general syntax and introduce the general class of applicative signatures, (Σ, C) and that of (Σ, C)-terms where, as usual, Σ is a set of operators but C a set of channel names. We then 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 used in [HI93]. Then we introduce the notion of recursively closed subsets of a process algebra.

Next, in §2.3, we show how we may turn an algebraic cpo into a (Σ, C)- domain by defining the operators on the compact elements, making sure that they are monotonic and then extending them to the whole domain. We also study the relationship between the evaluation mappings from our generic process language into two different (Σ, C)-preorders.

2.1 (Σ, C)-Terms

In this subsection 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. We do this by introducing the notion of applicative signature as a pair, (Σ, C), where Σ is a signature and C is a set (of channel names) and that of (Σ, C)-terms.

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

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

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

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

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

We have three kinds of actions, input actions of the form c?, c ∈ C, output actions of the form c!, c ∈ C and the silent action τ. We write C? for {c?|c ∈ C} and C! for {c!|c ∈ C}. The set Act = C! ∪ C? is ranged over by a whereas Act_{τ} = C! ∪ C? ∪ {τ} is ranged over by μ. The structure of this syntax is basically the same as 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 above mentioned 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 undecided process. Typically Σ contains the standard CCS operators such as NIL, +, | , etc. Now 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 recursion construct is a binding construct for process names. A value variable, x, is free if it is not in the scope of a prefix, [x], and a process name P is free if it is not in the scope of a recursion construct, rec P. . We shall mainly be concerned with expressions which contain no free occurrences of value variables. We denote the set of all process terms, functions terms and pair terms with no free occurrences of value variables by CP roc_{(Σ,C)}, CF un_{(Σ,C)} and CP airs_{(Σ,C)} respectively. These will be referred to as processes, functions and pairs ranged over by cp, cf and cπ. We assume a notion of substitution for both data variables and process names in terms defined in the usual way. For f = [x]p and v ∈ V al we use the convention f(v) = ([x]p)(v) = p[v/x].

In the theory to follow we will make an extensive use of the fact that the value domain V al is countable. As V al is countable it may 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}. In what follows V_{n} will have this meaning.

2.2 (Σ, 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. We assume that the reader is familiar with basic domain theory and algebraic semantics. (See e.g. [Plo81, Hen88a] for details.)

Definition 2.1 Applicative Orders A pair ⟨\overline{A},^{⊑}_{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

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. An applicative cpo is said to be algebraic/ω-algebraic if A_{proc}, A_{fun} and A_{pair} are algebraic/ω-algebraic cpos.

□

Example 2.2 Consider the domain 2 = {⊥, ⊤} with the standard ordering as A_{proc}, the po of compact elements of the domain [V al ⟶ 2] as A_{fun} (i.e. A_{fun} = V al ⟶_{fin} 2 = {f ∈ V al ⟶ 2 | {v ∈ V al|f(v) = ⊤} is finite }) and A_{pair} = V al × 2. This is an example of an applicative po which is not fully applicative. For instance the function f = λv ∈ V al.⊤ is not a compact element of [V al ⟶ 2] and thus is not an element of A_{fun}.

We often write a-pro/po/cpo as a shorthand for applicative pro/po/cpo.

Definition 2.3 [(Σ, 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. ⟨A_{proc}, ⊑_{A_{proc}}, Σ\overline{A}⟩ is a Σ − pro/po/cpo in the sense of [Hen88a].

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

(b) C?\overline{A} is a set of monotonic/monotonic/continuous functions c?\overline{A} : A_{fun} ⟶ A_{proc}.

We refer to the pair (Σ_{A}, C_{A}) as a (Σ, C)-pro/po/cpo structure. 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. □

Definition 2.4 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 it maps compact elements of A_{1} into compact elements of A_{2}, i.e. if f(Comp(A_{1})) ⊆ f(Comp(A_{2})). □

Next we extend the standard notion of homomorphisms for applicative orders.

Definition 2.5 A a-pro/po/cpo homomorphism \overline{h} : ⟨\overline{A},^{⊑}\overline{A}⟩ ⟶ ⟨\overline{B},^{⊑}\overline{B}⟩ is a triple of mappings, (h_{proc}, h_{fun}, h_{pair}), where h_{proc} : A_{proc} ⟶ B_{proc}, h_{fun} : A_{fun} ⟶ B_{fun} and h_{pair} : A_{pair} ⟶ B_{pair} are monotonic/monotonic/continuous. A (Σ, C) − pro/po/cpo homomorphism \overline{h} : ⟨\overline{A},^{⊑}\overline{A}, Σ\overline{A}, C\overline{A}⟩ ⟶ ⟨\overline{B},^{⊑}\overline{B}, Σ\overline{B}, C\overline{B}⟩, is a triple, (h_{proc}, h_{fun}, h_{pair}), where h_{proc} : A_{proc} ⟶ B_{proc} is a Σ − pro/po/cpo homomorphism in the sense of [Hen88a], h_{fun} : A_{fun} ⟶ B_{fun} and h_{pair} : A_{pair} ⟶ B_{pair} are pro/po/cpo homomorphisms and satisfy:

h_{proc}(c?\overline{A}.F) = c?\overline{B}.h_{fun}(F) and h_{proc}(c!\overline{A}.Π) = c!\overline{B}.h_{pair}(Π)
h_{fun}(F) = h_{proc} ∘ F
h_{pair}(v, P) = (v, h_{proc}(P)).
□

For \overline{A} = (A_{1}, A_{2}, A_{3}) and \overline{B} = (B_{1}, B_{2}, B_{3}) we write \overline{A} ⊆ \overline{B} if A_{i} ⊆ B_{i} for i = 1, 2, 3. If \overline{f} = (f_{1}, f_{2}, f_{3}) then we write \overline{f} : \overline{A} ⟶ \overline{B} for f_{i} : A_{i} ⟶ B_{i}, i = 1, 2, 3. All the relations we use will be extended pointwise to vectors without further explanations.

Sometimes 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. This motivates the following definition of a recursively closed subset of a language. Definition 2.6 \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. c?.f ∈ S_{proc} implies f ∈ S_{fun},

3. c!.π ∈ S_{proc} implies π ∈ S_{pair},

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

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

6. (e, p) ∈ S_{proc} implies p ∈ S_{proc}. In this case we write \overline{S} ⊆_{rec} T_{(Σ,C)}(P N). □ Note that if Σ′ ⊆ Σ and C′ ⊆ C then T_{(Σ′,C′)}(P N) ⊆_{rec} T_{(Σ,C)}(P N). Definition 2.7 Let \overline{S} ⊆_{rec} T_{(Σ,C)}(P N), ⟨\overline{X}, ≺\overline{X}, Σ\overline{X}, C\overline{X}⟩ be an applicative (Σ, C) − pro and P Env\overline{X} be the set of process environments ρ : P N ⟶ X_{proc}. A function

\overline{X}[[ ]] = (X_{proc}[[ ]], X_{fun}[[ ]], X_{pair}[[ ]]) : \overline{S} ⟶ (P Env\overline{X} ⟶ ⟨\overline{X}, ≺\overline{X}, Σ\overline{X}, C\overline{X}⟩) is an evaluation function if it satisfies:

X_{proc}[[op(\underline{p})]]ρ = op\overline{X}(X_{proc}[[\underline{p}]]ρ), op ∈ Σ
X_{proc}[[c?.f]]ρ = c?\overline{X}.X_{fun}[[f]]ρ
X_{proc}[[c!.π]]ρ = c!\overline{X}.X_{pair}[[π]]ρ
X_{proc}[[ be → p_{1}, p_{2}]]ρ = \{ \begin{matrix}X_{proc}[[p_{1}]]ρ & if [[be]] = T \\ X_{proc}[[p_{2}]]ρ & if [[be]] = F \end{matrix}
X_{fun}[[[x]p]]ρ = λv.X_{proc}[[p[v/x]]]ρ
X_{pair}[[(e, p)]]ρ = ([[e]], X_{proc}[[p]]ρ)
X_{proc}[[P]]ρ = ρ(P)

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

X_{proc}[[rec P.p]]ρ = Y λd.X_{proc}[[p]]ρ[d/P]

where Y is the least fixed point operator. □

For closed terms the environments do not have any influence on the definition. For process name free terms a mapping \overline{X}[[ct]] = \overline{X}[[ct]]ρ 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 2.8 Let \overline{S} = (S_{proc}, S_{fun}, S_{pair}) ⊆_{rec} T_{(Σ,C)}(PN) and ⟨\overline{X}, ≺\overline{X}, Σ\overline{X}, C\overline{X}⟩ be an applicative (Σ, C) − pro. Then there is at most one evaluation mapping

\overline{X}[[ ]] = (X_{proc}[[ ]], X_{fun}[[ ]], X_{pair}[[ ]]) : \overline{S} ⟶ (P Env\overline{X} ⟶ \overline{X})

If ⟨\overline{X}, ≺\overline{X}, Σ\overline{X}, C\overline{X}⟩ 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{X} is not fully applicative then a function term of the form [x].p may fail to have an interpretation in \overline{X}. For instance if p is a term denoting ⊤ in the applicative po considered in Example 2.2 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 2.9 Assume that

\overline{S} = (S_{proc}, S_{fun}, S_{pair}) ⊆_{rec} (P roc_{(Σ,C)}, F un_{(Σ,C)}, P airs_{(Σ,C)}),

that ⟨\overline{X}, ≺\overline{X}, Σ\overline{X}, C\overline{X}⟩ and ⟨\overline{Y} , ≺\overline{Y} , Σ\overline{Y} , C\overline{Y} ⟩ are (Σ, C)-pros and that

\overline{ψ} : ⟨\overline{X}, ≺\overline{X}, Σ\overline{X}, C\overline{X}⟩ ⟶ ⟨\overline{Y} , ≺\overline{Y} , Σ\overline{Y} , C\overline{Y} ⟩

is a (Σ, C)-pro homomorphism. If \overline{X}[[ ]] : \overline{S} ⟶ ⟨\overline{X}, ≺\overline{X}, Σ\overline{X}, C\overline{X}⟩ and \overline{Y} [[ ]] : \overline{S} ⟶ ⟨\overline{Y} , ≺\overline{Y} , Σ\overline{Y} , C\overline{Y} ⟩ are evaluation mappings, then \overline{Y} [[ ]] = \overline{ψ} ∘ \overline{X}[[ ]].

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

2.3 Properties Derived From the Compact Elements

In this subsection we will describe how we can take advantage of the algebraicity of an applicative (Σ, C)-domain, ⟨\overline{A},^{⊑}\overline{A}, Σ\overline{A}, C\overline{A}⟩ to obtain a full description of certain properties of the domain from the knowledge of the same properties only on the partial order consisting of the compact elements of the model. In fact we do more than that: we take an applicative ω-algebraic cpo, ⟨\overline{B},^{⊑}\overline{B}⟩, and show how it may be turned into an applicative (Σ, C)-domain by defining the interpretation of the operators in Σ and C on an applicative preorder that represents the partial order of the compact elements of the model \overline{B}. (By a representation of a partial order we mean a preorder whose induced partial order obtained by factoring out the preorder is isomorphic to the original one.) If the operators are monotonic they induce in a unique way continuous operators defined on the whole of \overline{B}. The following standard theorem (see e.g. [Hen88a]) plays an important role in this connection.

Theorem 2.10 Let A and B be cpos. Assume that A is algebraic and let f : Comp(A) ⟶ B be monotonic. Then there exists a unique continuous extension of f, f̃: A ⟶ B.

The main result of this subsection is stated in the following theorem where

\overline{inc} : ⟨Comp(\overline{B}),^{⊑}_{Comp(\overline{B})}⟩ ⟶ ⟨\overline{B},^{⊑}\overline{B}⟩

is the inclusion mapping and [ ]_{∼} : \overline{X} ⟶ \overline{X}/ ∼ is the quotient mapping.

Theorem 2.11 Assume that ⟨\overline{X}, ≺\overline{X}, Σ\overline{X}, C\overline{X}⟩ is a (Σ, C) − pro with the induced partial order ⟨\overline{X}/ ∼, ⪯_{\overline{X}/∼}⟩ where ∼=≺\overline{X} ∩ ≺−1 ; \overline{X}. Further assume that ⟨\overline{B},^{⊑}\overline{B}⟩ is an applicative algebraic cpo whose po of compact elements, ⟨Comp(\overline{B}),^{⊑}_{Comp(\overline{B})}⟩, is isomorphic to ⟨\overline{X}/ ∼, ⪯_{\overline{X}/∼}⟩ under the isomorphism

ϕ : ⟨\overline{X}/ ∼, ⪯_{\overline{X}/∼}⟩ ⟶ ⟨Comp(\overline{B}),^{⊑}_{Comp(\overline{B})}⟩

Then the following holds:

1. There exists a unique (Σ, C)-structure, (Σ\overline{B}, C\overline{B}) which extends ⟨\overline{B},^{⊑}\overline{B}⟩ to a (Σ, C)-domain and extends \overline{ψ} = \overline{inc}∘\overline{ϕ}∘[ ]_{∼} to a (Σ, C)-homomorphism. The structure (Σ\overline{B}, C\overline{B}) is compact in the sense of Definition 2.4.

2. Let \overline{B}[[ ]] : T_{(C,Σ)}^{rec}(P N) ⟶ \overline{B} be an evaluation mapping. If \overline{S} ⊆_{rec} T_{(C,Σ)} and \overline{X}[[ ]] : \overline{S} ⟶ \overline{X} is an evaluation mapping then

\overline{B}[[ ]]|\overline{S} = \overline{ψ} ∘ \overline{X}[[ ]]

where \overline{B}[[ ]]|\overline{S} means the restriction of the function \overline{B}[[ ]] to \overline{S}.

Proof

1. Existence: Let \overline{B}_{1} = Comp(\overline{B}). We note that inc(c) = c for all c ∈ \overline{B}_{1}. By assumption \overline{ϕ} ∘ [ ]_{∼} : \overline{X} ⟶ \overline{B}_{1} is monotonic and surjective. In particular any element of \overline{B}_{1} may be written as \overline{ϕ}([x]_{∼}) for some x ∈ \overline{X}. Now let op ∈ Σ. We define the operator op_{\overline{B}_{1}} by

op_{\overline{B}_{1}}(c) = op_{\overline{B}_{1}}(ϕ_{proc}([x]_{∼})) = ϕ_{proc}([op\overline{X}(x)]_{∼})

for all c = \overline{ϕ}([x]_{∼}) ∈ Comp(\overline{B}). It is easy to check that op_{\overline{B}_{1}} is well defined and monotonic. Then we take op\overline{B} to be the unique continuous extension to \overline{B} given by Theorem 2.10. We define C\overline{B} in a similar way. Thus we obtain well defined and continuous operators and prefixings on ⟨\overline{B},^{⊑}\overline{B}⟩. The compactness also follows directly from the definition. It remains to prove that the structure (Σ\overline{B}, C\overline{B}) extends \overline{ψ} to a (Σ, C)-homomorphism. So take x ∈ X_{proc}. By definition of op_{\overline{B}_{1}} we get

\begin{matrix}ψ_{proc}(op\overline{X}(x)) = inc(ϕ_{proc}([op\overline{X}(x)]_{∼})) = inc(op_{\overline{B}_{1}}(ϕ_{proc}([x]_{∼}))) = \\ op_{\overline{B}_{1}}(ϕ_{proc}([x]_{∼})) = op\overline{B}(ϕ_{proc}([x]_{∼})) = op\overline{B}(ψ_{proc}(x)). \end{matrix}

Uniqueness: Assume (Σ′ ; \overline{B}, C′ ; \overline{B}) is a structure that extends \overline{ψ} as described in the theorem. We have to show that Σ′ ; \overline{B} = Σ\overline{B} and C′ ; \overline{B} = C\overline{B}. We will only show the first equality as the proof for the other one is similar and is left to the reader. So let op′ ; \overline{B} ∈ Σ′ ; \overline{B} be the operator named by op. We will show that op′ ; \overline{B} = op\overline{B}. By assumption both op\overline{B} and op′ ; \overline{B} are continuous, so by Theorem 2.10 it is sufficient to prove they coincide on the compact elements of the domain. Let c ∈ Comp(\overline{B}). It is sufficient to prove that op′ ; \overline{B}(c) = op\overline{B}(c). So, as \overline{ψ} = \overline{ϕ} ∘ [ ] : \overline{X} ⟶ Comp(\overline{B}) is onto, we have that there is an x ∈ X_{proc} such that c = ψ_{proc}(x). Thus, as (Σ′ ; \overline{B}, C′ ; \overline{B}) extends \overline{ψ} to a (Σ, C)-homomorphism, the definition of op\overline{B} gives

\begin{matrix}op′ ; \overline{B}(c) = op′ ; \overline{B}(ψ_{proc}(x)) = ψ_{proc}(op\overline{X}(x)) = \\ ϕ_{proc}([op\overline{X}(x)]_{∼}) = op\overline{B}(c). \end{matrix}

This proves the uniqueness.

2. It is easy to check that \overline{B}[[ ]]|\overline{S} is an evaluation mapping on \overline{S} and the result follows directly from Corollary 2.9.

□

3 Late CCS and Its Denotational Semantics

In this section we will give a concrete language, Late CCS, (CCS_{L}) by instantiating the applicative signature (Σ, C). Furthermore we will define a concrete (Σ, C)-domain to give a denotational semantics for this language.

3.1 The Language

The language CCS_{L} is a modification of the original CCS in the spirit of the late approach. As described in the introduction it is basically a sublanguage of the more general π-calculus in which only simple values are transmitted in communications whereas the latter allows port names to be transmitted as well as simple values. Described in our general framework CCS_{L}(P N) = (CCS_{L}^{proc}(P N), CCS_{L}^{fun}(P N), CCS_{L}^{pair}(P N)) is obtained by instantiating the signature Σ by the standard operator of CCS. So we let Σ consist of the nullary operators NIL and Ω, the families of unary operators \c, c ∈ C and [R] where

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

CCS_{L}^{fun}(P N) : f ::= [x]p CCS_{L}^{pair}(P N) : π ::= (e, p)

Figure 1: The Syntax for CCS_{L}

R is a finite permutation of the channel names (i.e. R : C ⟶ C is constant on all but finitely many channels in C) and the binary operators + and |. For the motivation of these operators we refer to the standard theory of CCS in [Mil89]. For the sake of clarity the syntax for CCS_{L}(P N) is given in Figure 1. We let CCS_{L} = (CCS_{L}^{proc}, CCS_{L}^{fun}, CCS_{L}^{pair}) denote the closed terms in CCS_{L}(P N).

3.2 A Domain Equation for Applicative Communication Trees

In this section we will construct a (Σ, C)-domain which will be used to give the denotational semantics for our language, CCS_{L}. The model we define is basically the model of [MM79] where the modifications of Abramsky’s, reported in [Abr91] and described in the introduction, are adopted. Thus we define a model for value-passing based on the late approach 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.

Completion by Ideals: ([Hen88a], §3.3,[Win85]) There is a standard way of extending a preorder with a least element to an algebraic cpo, often called completion by ideals. Let ⟨A,^{⊑}_{A}⟩ be a preorder. A set X ⊆ A is downwards closed if whenever x ∈ X and y ^{⊑}_{A} x then y ∈ X. 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 is isomorphic to 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.

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, nonempty 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}⟩. From above-mentioned results, 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 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 3.1 [Applicative Communication Trees] 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{ACT} ,^{⊑}\overline{ACT} ⟩, as follows: ⟨ACT,^{⊑}_{ACT} ⟩ 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 14),

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

• D_{τ} = D.

Then we define ACT_{proc} = ACT, ACT_{fun} = V al ⟶ ACT and ACT_{pair} = V al × ACT with the usual induced order. ^{⊑}\overline{ACT} is the applicative partial order induced by ^{⊑}_{ACT_{proc}}=^{⊑}_{ACT}. Defined in this way ⟨\overline{ACT} ,^{⊑}\overline{ACT} ⟩ is a fully applicative ω-algebraic cpo which we refer to as ACT. Also we let ^{⊑} denote ⊑\overline{ACT}. □

From the general theory in [Plo81] we get a representation of the compact elements by unfolding the recursive definition of ACT. Thus we define

COMP = ⋃_{n=0}^{∞} COMP^{n}

where

COMP^{0} = {⊥}

and

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

where (COMP^{n})_{c?} = F_{V al}(COMP^{n}), (COMP^{n})_{c!} = V al × COMP^{n} and (COMP^{n})_{τ} = COMP^{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 COMP^{n} as we are using the power domain operator P^{0} rather than P. Defining COMP this way and ordering it by ^{⊑}_{EM}^{0}, the Egli-Milner preorder over COMP extended like in (1) above, gives a representation of the compact elements of the ω-algebraic cpo ACT. This means that the kernel of the preorder is isomorphic to the partial order of compact elements of the domain ACT, ⟨Comp(ACT),^{⊑}_{Comp(ACT)}⟩. (For the sake of simplicity we assume that the kernel is equal to Comp(ACT).) This suggests an inductive definition to describe the set COMP and the preorder on COMP. Thus we define the set K and the preorder ≺ on it inductively and prove that ⟨K, ≺⟩ is equal to ⟨COMP,^{⊑}_{EM}^{0}⟩.

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

1. ∅ ∈ K

2. {⊥} ∈ K

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

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

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

6. 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_{1}∃a ∈ k_{2}. a ≤ b where ≤ is defined on the elements of the sets in K by

(a) ∀a. ⊥ ≤ a

(b) ⟨τ, k⟩ ≤ ⟨τ, k′⟩ if k ≺ k′

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

(d) ⟨c!, (v, k)⟩ ≤ ⟨c!, (v, k′)⟩ if k ≺ k′

We let ≈=≺ ∩ ≺^{−1}. □

Proposition 3.3 ⟨K, ≺⟩ = ⟨COMP,^{⊑}_{EM}^{0}⟩.

Proof First we prove that K = COMP. That K ⊆ COMP can be proved by showing that COMP 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, COMP^{n} ⊆ K. The details are left to the reader.

Then we prove that the preorder ≺ coincides with the extended Egli-Milner preorder on K. We have to prove the two following cases:

≺ ⊆^{⊑}_{EM}^{0}: It is sufficient to prove that ^{⊑}_{EM}^{0} satisfies the definition of ≺; as ≺ is the least preorder which satisfies this definition the inclusion follows. The details are straightforward and are left to the reader.

≺ ⊇^{⊑}_{EM}^{0}: To prove this case 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)

Now we proceed as follows: We will prove by induction on d(k) that

k ^{⊑}_{EM}^{0} k′ ⇒ k ≺ k′

So assume k ^{⊑}_{EM}^{0} k′.

base d(k) = 0:

k = ∅: Then k′ = ∅ and k ≺ k′.

k = {⊥}: k ≺ k′ is obvious in this case.

step d(k) = n + 1: Now k ≠ ∅ so we may assume a ∈ k. Then by definition of ^{⊑}_{EM}^{0}, a ^{⊑}_{P^{0}[COMP]} b for some b ∈ k′. We will prove that a ≤ b. We have the four different cases: a = ⊥, a = ⟨c?, f⟩, a = ⟨c!, (v, k_{1})⟩ and a = ⟨τ, k_{2}⟩. The first case is obvious. We only prove the statement for the second case as the proof for the remaining two is similar. So assume a = ⟨c?, f⟩. Then b = ⟨c?, g⟩, where f(v) ^{⊑}_{EM}^{0} g(v) for all v ∈ V al. Now the induction applies and we may conclude that f(v) ≺ g(v) for all v ∈ V al. From this we get that a ≤ b as wanted.

Next assume b ∈ k′, then again by definition of ^{⊑}_{EM}^{0} there is an a ∈ k such that a ^{⊑}_{EM}^{0} b. In the same manner as before we may conclude that a ≤ b which completes the proof of this inclusion.

□

Definition 3.4 We define ⟨\overline{K}, ≺\overline{K}⟩ by letting K_{proc} = K, K_{fun} = F_{V al}^{fin}(K) (where F_{V al}^{fin}(K) is defined as on page 14) and K_{pair} = V al × K and by defining ≺\overline{K} as the preorder induced by ≺_{proc}=≺. □

3.3 Definition of the Operators in the Model

In this subsection we will define the operators in Σ_{ACT} and prove their continuity. In the definitions we take advantage of Theorem 2.11. Thus we only have to define the operators on the applicative preorder ⟨\overline{K}, ≺\overline{K}⟩ and make sure that they are monotonic.

Definition 3.5 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 3.6 ⟨\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 3.5 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 3.3. 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})

Now 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. □

We finish this section by summarizing our results. This is done by the following theorem.

Theorem 3.7 ⟨\overline{ACT} ,^{⊑}\overline{ACT} , Σ\overline{ACT} , C\overline{ACT} ⟩, where (Σ\overline{ACT} , C\overline{ACT}) is the (unique) structure induced by ⟨\overline{K}, ≺\overline{K}, Σ\overline{K}, C\overline{K}⟩, is a fully applicative (Σ, C)-domain. The operators in (Σ\overline{ACT} , C\overline{ACT}) and C\overline{ACT} are compact.

3.4 Syntactically Compact Elements

We will now 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, CoT erms(P N) = (CoP roc(P N), CoF un(P N), CoP air(P N)).

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 in a nontrivial way. 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 3.8 Let \underline{w}_{n} = (w_{1}, …, w_{n}) and \underline{p}_{n} = (p_{1}, …, p_{n}) be vectors of values and processes respectively. We write x : \underline{w}_{n} ⟶ \underline{p}_{n} for x = w_{1} ⟶ p_{1}, (x = w_{2} ⟶ p_{2}, (… x = w_{n} ⟶ p_{n}, Ω) …). (Intuitively x : \underline{w_{n}} ⟶ \underline{p_{n}} stands for the function that maps w_{i} to p_{i} for i = 1, …, n and all the other values w ∈ V al into Ω.) Further we let \{\underline{w_{n}}\} = \{w_{i}|\underline{w_{n}} = (w_{1}, …, w_{n})\} and similarly for \{\underline{p_{n}}\}.

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

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

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

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

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

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

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

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

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

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

□

Note that CoT erms = (CoP roc, CoF un, CoP air) ⊆_{rec} (P roc, F un, P airs). We have the following:

Theorem 3.10

1. \overline{ACT} [[ ]] : CCS_{L} ⟶ \overline{ACT} and \overline{K}[[ ]] : CoT erms ⟶ \overline{K} are well-defined.

2. \overline{ACT} [[ ]] |_{CoT erms} = inc ∘ [ ]_{≈} ∘ \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 ≺ and

• inc : \overline{K}/ ≈ = Comp(\overline{ACT}) ⟶ \overline{ACT} is the inclusion mapping.

3. For any Cot ∈ CoT erms \overline{ACT} [[Cot]] ∈ Comp(\overline{ACT})

4. For all Cot_{1}, Cot_{2} ∈ CoT erms \overline{ACT} [[Cot_{1}]] ^{⊑} \overline{ACT} [[Cot_{2}]] if and only if \overline{K}[[Cot_{1}]] ≺ \overline{K}[[Cot_{2}]]

5. For any k ∈ Comp(\overline{ACT}) there is a Cot ∈ CoT erms such that \overline{ACT} [[Cot]] = k.

Proof

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

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

is well-defined. The existence of \overline{K}[[ ]] follows by a simple structural induction on CoT erms.

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

3. This part follows immediately from part 2.

4. Follows from part 2. as well.

5. We start by proving that for any k ∈ \overline{K} there is a Cot ∈ CoT erms such that \overline{K}[[Cot]] = 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 ∈ Co(\overline{ACT}). Then c = [k]_{≈} for some k ∈ \overline{K}. From what we proved above we get that \overline{K}[[Cot]] = k for some Cot ∈ CoT erms. From 1. we get

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

This completes the proof.

□

4 Algebraic Laws and Proof Systems

In this section we will introduce a proof system supported by the model \overline{ACT}. We proceed by introducing first a system, E, for finite processes which we then extend to a system, E_{rec}, which takes care of recursive processes. We prove the soundness and completeness of E_{rec} 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 are defined as sets and + as set union. The inference rules describe the structure and the preorder in 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)}

that allow us to prove inequalities over function terms and pairs. The extended system E_{rec} is then obtained by adding to E three new rules to take care of recursion. These rules are all fairly standard and will not be explained here (see e.g. [Hen88a]). The new rules introduced are

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

and

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

where p^{(n)}, the syntactically compact approximations of a process term p, are defined in Definition 4.1. 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. This enables us to take advantage of the algebraicity of the model when proving the completeness of the proof system. It is possible that the weaker version of the ω-rule with the more standard syntactically finite approximations, i.e. without restrictions on the values, would yield a complete system as well but then a more complicated proof technique would be needed. 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. Now we define the syntactically compact approximations used in the ω-rule of the proof system.

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

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

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

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

□

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

Figure 2: Equations Let X = ∑_{i} τ.X_{i} + ∑_{j} a′_{j}?.[x]X′_{j} + ∑_{k} a′′_{k}!.(v_{k}, X′′_{k}){+Ω} and Y = ∑_{l} τ.Y_{l} + ∑_{m} b′_{m}?.[y]Y′_{m} + ∑_{n} b′′_{n}!.(v_{n}, Y′′_{n}){+Ω}. Then

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

where

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

where

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

and

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

Figure 3: Interleaving Law

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

Figure 4: The Proof System E_{rec} 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 property:

Theorem 4.2 For all n and all t ∈ T erms

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

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

Proof

1. May be proved by an induction on n combined with an inner structural induction.

2. 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]. We leave it to the reader to check the details. 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 in connection with the restrictions on the values in the function and pair terms. As in the above mentioned reference we proceed by structural induction on t.

t = q ∈ P roc: We proceed by case analysis on the form q takes. Here the only nontrivial case is q = recP.p. By definition [[recP.p]]ρ = Y F where F = λa.[[p]]ρ[P ↦ a] and Y is the least fixed-point operator. Thus, to prove the result, it is sufficient to prove that l = ⨆_{n}[[q^{(n)}]]ρ is a fixed point to F. So first let ρ^{n} = ρ[P ↦ [[q^{(n)}]]ρ]. Then F ([[q^{(n)}]]ρ) = [[p]]ρ^{n} and [[p^{(k+1)}]]ρ^{k} = [[q^{(k+1)}]]ρ for all k. Now, as F is continuous, we have

F (⨆_{n}[[q^{(n)}]]ρ) = ⨆_{n} F ([[q^{(n)}]]ρ) = ⨆_{n}[[p]]ρ^{n}.

By the structural induction

[[p]]ρ^{n} = ⨆_{m}[[p^{(m)}]]ρ^{n}.

We note that for any n, m and k ≥ Max{m, n},

[[p^{(m)}]]ρ^{n} ^{⊑} [[p^{(k+1)}]]ρ^{k}.

This implies

\begin{matrix}F (⨆[[q^{(n)}]]ρ) = ⨆_{n}(⨆_{m}[[p^{(m)}]]ρ^{n}) = \\ ⨆_{k}[[p^{(k+1)}]]ρ^{k} = ⨆_{k}[[q^{(k+1)}]]ρ = ⨆_{n}[[q^{(n)}]]ρ \end{matrix}

which completes this case of the proof. t = [x]p ∈ F un: 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.

t = (v, q) ∈ P airs: May be proved in a similar way as the previous case and is left to the reader.

□

What remains of the section is devoted to the proof of 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 4.3 [Ω-normal form] A compact term, Cot ∈ CoT erms, is said to be in a Ω-normal form if the following hold:

1. If Cot = Cop ∈ CoP roc then Cop has the form

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

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

2. If Cot = (e, Cop) ∈ CoP airs then e = v ∈ V al and Cop is in a Ω-normal form.

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

□

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

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

1. δ(NIL) = δ(Ω) = 0

2. δ(Cop \ c) = δ(Cop[R]) = δ(Cop)

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

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

5. δ(pre.Cot) = 1 + δ(Cot)

6. δ((e, Cop)) = δ(Cop)

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

To prove the result we prove the following stronger result:

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

We prove the statement by induction on δ(Cot). So assume that the statement holds for all Cot′ with δ(Cot′) < n and that δ(Cot) = n. We will prove that the statement holds for Cot. We proceed by structural induction on Cot.

Cot = Cop ∈ CoP roc: We proceed by a case analysis on the form Cop takes.

Cop = NIL: Trivial. Cop = Ω: We get the result by defining n(Ω) = NIL + Ω Cop = μ.Cot, Cop_{1} + Cop_{2}: Follows from the structural induction and

a simple use of the proof system. Cop = Cop_{1} \ c: By structural induction, Cop_{1} has a Ω-normal form,

onf, such that

Cop_{1} =_{E} onf = ∑_{i} a_{i}.t_{i}{+Ω} where δ(onf) ≤ n

In particular δ(t_{i}) < n for all i. By a simple use of the proof system we get

Cop_{1} \ c =_{E} ∑_{i:a_{i}≠c} a_{i}.(t_{i} \ c){+Ω}

Furthermore δ(t_{i} \ c) = δ(t_{i}) < n. By the outer induction there are Ω-normal forms, n_{i} =_{E} t_{i} \ c, such that δ(n_{i}) ≤ δ(t_{i} \ c) < n. By substitutivity

Cop_{1} \ c =_{E} ∑_{i:a_{i}≠c} a_{i}.n_{i}{+Ω}

Obviously the right hand side of the equation is an Ω-normal form. Finally

δ( ∑_{i:a_{i}≠c} a_{i}.n_{i}{Ω}) ≤ 1 + max_{i}{δ(n_{i})} ≤ n

This completes the proof in this case.

Cop = Cop_{1}[R]: Similar.

Cop = Cop_{1}|Cop_{2}: This is the only non-trivial case. By induction Cop_{1} and Cop_{2} have Ω-normal forms, n_{1} and n_{2}, with δ(n_{i}) ≤ δ(Cop_{i}), i = 1, 2. If either n_{1} or n_{2} is NIL, the result follows from Equation (NILpar) in Figure 3. Otherwise assume

n_{1} = ∑_{i} a_{i}?.[x_{i}]r_{i} + ∑_{j} b_{j}!.(v_{j}, p_{j}) + ∑_{k} τ.q_{k}{+Ω}

and

n_{2} = ∑_{i′} a′_{i′}?.[y_{i′}]r′_{i′} + ∑_{j′} b′_{j′}!.(v′_{j′}, p′_{j′}) + ∑_{k′} τ.q′_{k′}{+Ω}.

By substitutivity and the interleaving law

Cop = Cop_{1}|Cop_{2} =_{E} n_{1}|n_{2} =_{E}
INT L_{out}(n_{1}, n_{2}) + INT L_{in}(n_{1}, n_{2})+
INT L_{τ}(n_{1}, n_{2}) + COMM(n_{1}, n_{2}){+Ω}.

It is sufficient to prove that each of the summands can be reduced to an Ω-normal form with depth no greater than that of Cop. We only prove this for the summand INT L_{in} as the proof of the statement for the remaining two is similar. We recall that

INT L_{in}(n_{1}, n_{2}) = INT L_{in}^{l}(n_{1}, n_{2}) + INT L_{in}^{r}(n_{1}, n_{2})

where

\begin{matrix}INT L_{in}^{l}(n_{1}, n_{2}) = ∑_{i} a_{i}?.[x_{i}](r_{i}|n_{2})\{+Ω\} \\ INT L_{in}^{r}(n_{1}, n_{2}) = ∑_{i′} a′_{i′}?.[y_{i′}](n_{1}|r′_{i′})\{+Ω\}. \end{matrix}

We will only prove the statement for INT L_{in}^{l}(n_{1}, n_{2}) as the proof for the other one is similar. Again it is sufficient to prove that the terms [x_{i}](r_{i}|n_{2}) may be reduced to a Ω-normal form with depth strictly less than Cop. To prove this first we recall that r_{i} has the form r_{i} = x_{i} : \underline{v_{n_{i}}}^{i} ⟶ \underline{p_{n_{i}}}^{i} where p_{j}^{i} is a Ω-normal form for j ≤ n_{i}. Therefore we get

[x_{i}](r_{i}|n_{2}) = [x_{i}]((x_{i} : \underline{v_{n_{i}}}^{i} ⟶ \underline{p_{n_{i}}}^{i})|n_{2}).

By using the rules (fun), (cond1) and (cond2) and substitutivity we obtain

[x_{i}](r_{i}|n_{2}) =_{E} [x_{i}]((x_{i} : \underline{v_{n_{i}}}^{i} ⟶ \underline{q_{n_{i}}}^{i})

where q_{j}^{i} = p_{j}^{i}|n_{2} for j ≤ n_{i}. Furthermore

δ(q_{j}^{i}) = δ(p_{j}^{i}|n_{2}) ≤ max_{j≤n_{i}}{δ(p_{j}^{i}|n_{2})} <
1 + max_{j≤n_{i}}{δ(p_{j}^{i}|n_{2})} =
1 + (1 + max_{j≤n_{i}}{δ(p_{j}^{i})} + δ(n_{2})) =
1 + (1 + δ([x_{i}]r_{i}) + δ(n_{2})) =
1 + δ(a_{i}?.[x_{i}]r_{i}) + δ(n_{2}) ≤ 1 + δ(n_{1}) + δ(n_{2}) ≤
1 + δ(Cop_{1}) + δ(Cop_{2}) = δ(Cop) = n.

Thus the outer induction applies on q_{j}^{i} and we may conclude that q_{j}^{i} =_{E} γ_{j}^{i} where γ_{j}^{i} is an Ω-normal form and such that δ(γ_{j}^{i}) ≤ δ(q_{j}^{i}). By substitutivity

INT L_{in}^{l}(n_{1}, n_{2}) =_{E} ∑_{i} a_{i}?.[x_{i}]x_{i} : \underline{v_{n}}^{i} ⟶ \underline{γ_{n}}^{i}

where the right hand side of the equality obviously is a Ω-normal form. Furthermore

δ(∑_{i} a_{i}?.[x_{i}]x_{i} : \underline{v_{n}}^{i} ⟶ \underline{γ_{n}}^{i}) =
max_{i}\{δ(a_{i}?.[x_{i}]x_{i} : \underline{v_{n}}^{i} ⟶ \underline{γ_{n}}^{i})\} =
1 + max_{i}{max_{j}{δ(γ_{j}^{i})}}) ≤
1 + max_{i}{max_{j}{δ(q_{j}^{i})}} ≤
δ(Cop).

In a similar way we may show that INT L_{in}^{r}(n_{1}, n_{2}) has a Ω-normal form with depth no greater than that of Cop and therefore that INT L_{in}(n_{1}, n_{2}) has a Ω-normal form with depth no greater than δ(Cop). We can also prove a similar statement about INT L_{out}(n_{1}, n_{2}), INT L_{τ}(n_{1}, n_{2}) and COMM(n_{1}, n_{2}) and thereby for Cop.

Cot ∈ CoP airs, CoF un: Left to the reader. □

We will end this section by stating and proving the soundness and completeness

of the proof system E_{rec} with respect to the denotational semantics.

Theorem 4.5 [Soundness and Completeness] For all closed terms ct, cu in CT erms we have

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

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 4.2 whereas the soundness of the (rec)-rule follows from the definition of the semantics of rec.p as a least fixed point. What remains to prove is the soundness of E. We do this by reducing the proof to a proof of the soundness for syntactically compact terms with respect to \overline{K}. For this purpose we need the following property.

ct ^{⊑}_{E} cu ⇒ ∃m∀n ≥ m. ct^{(n)} ^{⊑}_{E} cu^{(n)}  (2)

This may be proved by induction on the depth of the proof for ct ^{⊑}_{E} cu. 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.

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

Assume ct ^{⊑}_{E} cu. Then, by (2), ct^{(n)} ^{⊑}_{E} cu^{(n)} for all n ≥ m for some m. As ct^{(n)}, cu^{(n)} ∈ CoT erms, the soundness of E with respect to for these implies

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

or equivalently

\overline{ACT} [[ct^{(n)}]] ^{⊑} \overline{ACT} [[cu^{(n)}]] for all n ≥ m

Theorem 4.2 implies

ACT [[ct]] ^{⊑} ACT [[cu]]

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

\begin{aligned}\overline{ACT} [[ct]] ^{⊑} \overline{ACT} [[cu]] & ⇒ \\ ∀n.\overline{ACT} [[ct^{(n)}]] ^{⊑} \overline{ACT} [[cu]] & ⇒ \\ ∀n∃m.\overline{ACT} [[ct^{(n)}]] ^{⊑} \overline{ACT} [[cu^{(m)}]] & ⇒ \\ ∀n∃m.\overline{K}[[ct^{(n)}]] ≺ \overline{K}[[cu^{(m)}]]. \end{aligned}  (3)

If E is complete for CoT erms with respect to \overline{K} then

\overline{K}[[ct^{(n)}]] ≺ \overline{K}[[cu^{(m)}]] ⇒ ct^{(n)} ^{⊑}_{E} cu^{(m)}  (4)

Now cu^{(m)} ^{⊑}_{E_{rec}} cu may easily be shown so (3), (4) and the ω-rule give

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

Thus what remains to prove is the completeness of E on CoT erms with respect to \overline{K}. By Lemma 4.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}[[Cot_{1}]] ≺ \overline{K}[[Cot_{2}]]. By Lemma 4.4 Cot_{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}[[Cot_{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 Cot_{1} ^{⊑}_{E} Cot_{2} 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}}  (5)

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

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

we get, by (5), 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}  (6)

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

\begin{matrix}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} \end{matrix}

which completes the proof for this case.

n_{1} ∈ CoF un, CoP air: Follows easily from the induction.

□

5 Conclusion

In the first part of this paper we have set up a general framework for describing the syntax and the denotational semantics for value-passing calculi which support the late approach. For this purpose the standard notion of signature and Σ-algebras and Σ-orders have been extended to the so-called applicative signatures and (Σ, C)-algebras and (Σ, C)-orders. Furthermore we show how we may take advantage of the ω-algebraicity of a model to define the operators in the model.

In the second part of the paper we define the language Late-CCS 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 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.

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 solution to an recursive domain equation. It is a direct extension of the model defined by Abramsky in [Abr91] and a modification of the model 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 cpos and ω-algebraicity the solution we obtain is an ω-algebraic cpo.

The operators are constructed by isolating the compact elements. We then define the operators on the derived partial order, making sure that they are monotonic. This allows us to extend them to continuous functions defined on the whole cpo.

We have also presented an equationally based proof system and shown its soundness and completeness 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.

As already explained the construction of the domain equation and thereby the definition of the model is strongly inspired by the idea of bisimulation preorder. In the companion paper [Ing95a] it is shown that 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. In [Ing95a] a finitary version of the preorder is defined by mimicking the ω-algebraicity of the model on the syntactical level. 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.

References

[Abr87] S. Abramsky. Domain theory in logical form. In Proceedings 2^{nd} Annual Symposium on Logic in Computer Science, Ithaca, New York. IEEE Computer Society Press, 1987. Full version to appear in Annals of Pure and Applied Logic.

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

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

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

[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 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. Report 93–2008, Institute for Electronic Systems, Department of Mathematics and Computer Science, Aalborg University Centre, 1993. To appear in Theoretical Computer Science.

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

[Ing95a] A. Ingólfsdóttir. A Semantic Theory for Value-Passing Processes, Late Approach, Part II: A Behavioural Semantics and Full Abstractness To appear as Technical Report, BRICS, Aalborg University.

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

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

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

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

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

Recent Publications in the BRICS Report Series

RS-95-3 Anna Ing� olfsd� ottir. A Semantic Theory for Value�Passing Processes, Late Approach, Part I: A Denotational Model and Its Complete Axiomatization. January 1995. 37 pp.

RS-95-2 Franc�ois Laroussinie, Kim G. Larsen, and Carsten Weise. From Timed Automata to Logic - and Back. January 1995. 21 pp.

RS-95-1 Gudmund Skovbjerg Frandsen, Thore Husfeldt, Peter Bro Miltersen, Theis Rauhe, and S�ren Skyum. Dynamic Algorithms for the Dyck Languages. January 1995. 21 pp.

RS-94-48 Jens Chr. Godskesen and Kim G. Larsen. Synthesizing Distinguishing Formulae for Real Time Systems. December 1994. 21 pp.

RS-94-47 Kim G. Larsen, Bernhard Steffen, and Carsten Weise. A Constraint Oriented Proof Methodology based on Modal Transition Systems. December 1994. 13 pp.

RS-94-46 Amos Beimel, Anna G� al, and Mike Paterson. Lower Bounds for Monotone Span Programs. December 1994. 14 pp.

RS-94-45 J�rgen H. Andersen, K� are J. Kristoffersen, Kim G. Larsen, and Jesper Niedermann. Automatic Synthesis of Real Time Systems. December 1994. 17 pp.

RS-94-44 Sten Agerholm. A HOL Basis for Reasoning about Functional Programs. December 1994. PhD thesis. viii+224 pp.

RS-94-43 Luca Aceto and Alan Jeffrey. A Complete Axiomatization of Timed Bisimulation for a Class of Timed Regular Behaviours (Revised Version). December 1994. 18 pp. To appear in Theoretical Computer Science.

RS-94-42 Dany Breslauer and Leszek Ga�sieniec. Ef�cient String Matching on Coded Texts. December 1994. 20 pp.