A Semantic Theory for Value–Passing Processes Late Approach

Anna Ingólfsdóttir

BRICS^{∗}

Department of Mathematics and Computer Science Aalborg University, Denmark

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 prefixing with an input action, \overline{a}(x).p, is interpreted as a non-deterministic choice between pure terms of the form \overline{a}_{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 a more recent work on the π-calculus, [MPW89], 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 outputting 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 inputting 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 outputting counterpart in the communication provides. Symmetrically the result of reporting the willingness to output an uninterpreted value on the channel c is modelled by the action c. By performing this action the process evolves to a term which basically consists of a data expression and a process expressions.

In a more recent version of the π-calculus, the Polyadic π-calculus in [Mil91], the outcome of input and output actions are modelled by extending the syntax with the new constructions abstractions and concretions. For further motivation for this approach we refer to [MPW89], [Mil91] and [Ing93].

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

The aim of this paper is to develop a denotational semantics for languages with simple values based on the late approach described above although we use a slightly different notation as we will explain in the next section.

The paper is divided into two main parts: a general theory to handle valuepassing in §2, followed by an application to a concrete definition in §3. In the first part 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. This is a direct generalization of the standard Σ–terms and Σ-domains that appear in [He88] to model the pure calculus. For this purpose we introduce the general notion of applicative signature (Σ, C) where Σ is a signature and C a set (of channel names) and that of (Σ, C)-terms. This is basically the syntax of the Polyadic π-calculus presented in [Mil91] although we only allow simple values and allow Σ to be any set of operators. We also introduce the general class of applicative (Σ, C)-domains to model the semantics of the (Σ, C)-terms.

Next we apply the general result for algebraic cpos ([He88]): functions which are monotonic on 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. In this way we may take their unique continuous extension to be their definition on the whole domain.

In §3 a concrete language and its semantics is given. The language is a modification of the original CCS according to the late approach. This is obtained as the (Σ, C)-terms where Σ is instantiated with the standard operators of CCS. Then a concrete denotational model, Applicative Communication Trees, is defined, an instantiation of the general class of (Σ, C)-domains. The carrier, an ω-algebraic cpo, is defined as a solution to a recursive domain equation, a direct generalization of Abramsky’s model for SCCS presented in [Abr92]. Then we apply the described theory to define the operators.

Finally, in 4, we define a proof system to reason about our language and proof it’s soundness and completeness with respect to the denotational semantics derived from the model. The ω-algebraicity together with the construction of the operators enables us to reduce the proof of the 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 this section we will develop a general theoretical framework for describing denotational semantics for value-passing calculi based on the late approach.

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.

We assume some predefined 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 category, BExp, of boolean expressions, ranged over by be. BExp should at least include equality between the elements of Exp. From that a membership of a finite set can easily be derived. Value expressions are supposed to be equipped with a substitution, 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 preassumes an infinite set of process variables, P N, ranged over by P, Q, etc.

The set of (Σ, C)-terms is now given as the triplet

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}) c?.f c!.π τ.p be → p, p′ \\ F un_{(Σ,C)} : & f ::= [x]p \\ P airs_{(Σ,C)} : & π ::= (e, t) \end{matrix}

If the process names in P N are added as primitives to the syntax, we write T_{(Σ,C)}(P N), 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 action of inputting on channel c is given by c? whereas the action of outputting on that channel is given by c!. The abstractions are given by terms of the form [x]p, which we call function terms, where x is a data variable and p a process term. The input prefixing becomes c?.[x]p. The concretions are of the form (e, p), called pair terms, where e is a data expression and p a process term and the output prefixing becomes c!.(e, p). We also assume that we have a set of operators, Σ, which at least is supposed to contain 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 Σ.

Prefixing by [x] binds the data variable x and the recursion construct is a binding construct for process variables. A value variable, x, is free if it is not in the scope of a prefix, [x], and a process variable 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, etc. with no free occurrences of value variables by CP roc_{(Σ,C)}, CF un_{(Σ,C)}, etc. These will be referred to as processes, functions, etc. ranged over by cp, cf, etc. For f = [x]p we use the convention f(v) = ([x]p)(v) = p[v/x]. We assume a notion of substitution for both data and process variables for terms.

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

Now we define applicative orders and applicative ordered (Σ, C)-algebras where we use the abbreviations pro for pre-order, po for partial order and cpo for complete partial order:

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

□

Definition 2.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 applicative pro/po/cpo.

2. ⟨A_{proc}, ⊑_{A_{proc}}, Σ_{A}⟩ is a Σ − pro/po/cpo

3. C_{A} = C!_{A} ∪ C?_{A} where C!\overline{A} is a set of monotonic/monotonic/continuous functions c!.\overline{A} : A_{pair} → A_{proc} and 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. □

To reduce the notational complexity we allow us to write pro/po/cpo instead of applicative pro/po/cpo. As we are only dealing with applicative orders this should not cause any confusion.

Definition 2.3 A pro/po/cpo homomorphism \overline{h} : ⟨\overline{A},^{⊑}\overline{A}⟩ ⟶ ⟨\overline{B},^{⊑}\overline{B}⟩ is a triplet 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 triplet, (h_{proc}, h_{fun}, h_{pair}), where h_{proc} : A_{proc} ⟶ B_{proc} is a Σ − pro/po/cpo homomorphism, 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))

A pro/po/cpo isomorphism and a (Σ, C)-pro/po/cpo isomorphism are defined in the obvious way. □

Notation 2.4 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. We will use a similar pointwise extension of other definitions as well without further explanations.

We say that

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

is a recursively closed subset of T_{(Σ,C)}(P N) if whenever t ∈ \overline{S} then all of its subcomponents are in \overline{S} as well. In this case we write \overline{S} ⊆_{rec} T_{(Σ,C)}(P N). Note that we may apply structural induction when proving properties of recursively closed subsets.

Definition 2.5 Let \overline{S} ⊆_{rec} T_{(Σ,C)}(P N), ⟨\overline{X}, ≺\overline{X}, Σ\overline{X}, C\overline{X}⟩ an applicative (Σ, C)− pro and P Env\overline{X} 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})

is an evaluation function if whenever t ∈ \overline{S} then \overline{X}[[t]]ρ satisfies

X_{proc}[[op(\underline{p})]]ρ = op_{X}(X_{proc}[[\underline{p}]]ρ), op ∈ Σ
X_{proc}[[c?.f]]ρ = c?._{X}X_{fun}[[f]]ρ
X_{proc}[[c!.π]]ρ = c!._{X}X_{pair}[[π]]ρ
X_{proc}[[ be → p_{1}, p_{2}]]ρ = [[be]] → (X_{proc}[[p_{1}]]ρ), (X_{proc}[[p_{2}]]ρ)
X_{fun}[[[x]p]]ρ = λv.X_{proc}[[p[v/x]]]ρ
X_{pair}[[(e, p)]]ρ = ([[e]], X_{proc}[[p]]ρ)
X_{proc}[[X]]ρ = ρ(X)

If A is a cpo then, following the standard practice, we may define

A_{proc}[[rec X.p]]ρ = Y λd.A_{proc}[[p]]ρ[d/X]

where Y is the least fixed point operator. □

For closed terms the environments do not have any influence on the definition. For terms in T_{(Σ,C)} the mapping \overline{A}[[ct]] = \overline{A}[[ct]]ρ may be derived from the definition omitting the last clause of the definition and the occurrence of ρ in the others. We have the following result.

Theorem 2.6 Let \overline{S} = (S_{proc}, S_{fun}, S_{pair}) ⊆_{rec} T_{(Σ,C)}(P N) 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.

2.3 Properties Derived From the Compact Elements

In this section we will describe how we can turn an algebraic cpo into a (Σ, C)- domain if we have a complete description of its compact elements. So let us assume that ⟨\overline{B}, ⊏_{∼}\overline{B}⟩ is an algebraic cpo. Further assume that ⟨\overline{X}, ≺\overline{X}⟩ is a preorder where the induced partial order ⟨\overline{X}/ ∼, ≺_{\overline{X}/∼}⟩, ∼=≺ ∩ ≺^{−1} is isomorphic to ⟨Co(\overline{B}),^{⊑}_{Co(\overline{B})}⟩ under \overline{ϕ} : ⟨\overline{X}/ ∼, ≺\overline{X}⟩ ⟶ ⟨Co(\overline{B}),^{⊑}_{Co(\overline{B})}⟩. By defining a monotonic (Σ, C) structure on ⟨\overline{X}, ≺\overline{X}⟩ we get automatically an induced monotonic structure on ⟨\overline{X}/ ∼, ≺_{\overline{X}/∼}⟩ and thereby on the isomorphic ⟨Co(\overline{B}),^{⊑}_{Co(\overline{B})}⟩. Now, because of the algebraicity this structure may be extended in a unique way to a continuous structure on ⟨\overline{B}, ⊏_{∼}\overline{B}⟩. This procedure may be described formally by the following Theorem. We note that the function \overline{ψ} = \overline{inc} ∘ \overline{ϕ} ∘ [ ] where \overline{inc} : ⟨Co(\overline{B}),^{⊑}_{Co(\overline{B})}⟩ ⟶ ⟨\overline{B},^{⊑}\overline{B}⟩ is the inclusion mapping and [ ] : ⟨\overline{X}, ≺\overline{X}⟩ ⟶ ⟨\overline{X}/ ∼, ⪯_{\overline{X}/∼}⟩ is the quotient mapping, is a po-homomorphism.

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

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

Then the following holds:

1. There exists a unique (Σ, C)-cpo 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}) preserves compactness.

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

\overline{B}[[t]] = \overline{ψ}(X[[t]]).

3 The Language Late-CCS and its Semantics

In this section we will give a concrete language and define a denotational model for it. We also give an equationally based proof system and show its soundness and completeness with respect to the denotational model.

3.1 A Domain Equation for Applicative Communication Trees

The language Late-CCS, 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 Late-CCS is obtained by instantiating the signature Σ by the standard operator of CCS. So we let Σ consist of the nullary operators NIL and Ω, the families of unary operators \ c, c ∈ C and [R] where R is a finite permutation of the process names, and the binary operators + and |. For the motivation of these operators we refer to the standard theory of CCS in [Mil89].

Next we construct a (Σ, C)-domain to give a denotational semantics for our language. The definition of this model is motivated by the following existing work.

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 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 [Sm78], 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 definition of the process domain which is defined as the initial solution of corresponding domain equation.

In [Abr92] 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 defines 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 defines his model in terms of the Plotkin power-domain instead of the Smyth power-domain. He adds 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 interprets the calculus SCCS in the model and shows the full abstractness of this interpretation with respect to strong ω-prebisimulation.

The model we define is basically the model of [MM79] where the modifications of Abramsky’s are adapted. 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.

Here the main difference is that we use a different representation for Plotkin power-domain to the one used in [Abr92]. The representation we use is the one due to Smyth, [Sm78] and may be described as follows:

Let ⟨A,^{⊑}⟩ be an ω-algebraic cpo and M[A] the family of finite, non-empty sets of compact elements of A. The Egli-Milner preorder on M[A], ^{⊑}_{EM(A)}, is defined by

X ^{⊑}_{EM(A)} Y if ∀x ∈ X∃y ∈ Y.x ^{⊑}_{A} y and ∀y ∈ Y ∃x ∈ Y.y ^{⊑}_{A} x

The Plotkin power-domain of ⟨A,^{⊑}⟩, ⟨P [A],^{⊑}_{P [A]}⟩ is the ideal completion of the preorder ⟨M[A],^{⊑}_{EM(A)}⟩. From the standard theory, [Plo81b], we know that ⟨P [A],^{⊑}_{P [A]}⟩ is an ω-algebraic cpo and the po of compact elements is isomorphic to the po derived from the preorder ⟨M[A],^{⊑}_{M[A]}⟩. 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)

Now we can give the following definition:

Definition 3.1 [Applicative Communication Trees] Let Chan (the set of channels) and V al (the set of values) be countable sets and Act = {c?|c ∈ Chan} ∪ {c!|c ∈ Chan} ∪ {τ} (the set of actions). We define the applicative cpo of applicative communication trees, ⟨\overline{ACT} ,^{⊑}⟩, as follows: ⟨ACT,^{⊑}⟩ is the initial solution in the category of cpos with embeddings of the recursive domain equation:

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

where D_{c?} = V al → D, 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} ,^{⊑}\overline{ACT} ⟩ is a fully applicative cpo which we refer to as ACT. □

By unfolding the recursive definition of ACT, we get a description of the compact elements from the standard theory. Thus we define

Co(ACT) = ⋃_{n=0}^{∞} Comp^{n}

where

Comp^{0} = {⊥}

and

\begin{aligned}Comp^{n+1} & = Co(P^{0}[∑_{e∈Act}(Comp^{n})_{e}]) \\ & = M[∑_{e∈Act}(Comp^{n})_{e}] ∪ \{∅\} \end{aligned}

where (Comp^{n})_{c?} = 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 Co(ACT) this way and ordering it by ^{⊑}_{EM}^{0}, the Egli-Milner preorder over Co(ACT) extended as described above, gives a representation of the compact elements of the model ACT. This suggests an inductive definition to describe the compact elements and the preorder on these. Thus we define the set K and the preorder ≺ on it inductively and prove that ⟨K, ≺⟩ is a representation of ⟨Co(ACT),^{⊑}_{EM}^{0}⟩

Definition 3.2 We define K as the least set which satisfies

1. ∅ ∈ K

2. {⊥} ∈ K

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

4. c ∈ Chan, 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/ ≈, ≺_{K/≈}⟩ = ⟨Co(ACT),^{⊑}_{EM}^{0}⟩ (where we also use ^{⊑}_{EM}^{0} for the partial order induced by ^{⊑}_{EM}^{0} on Co(ACT)).

Definition 3.4 We define ⟨\overline{K}, ≺\overline{K}⟩ by K_{proc} = K, K_{fun} = F in(V al ⟶ K) and K_{pair} = V al × K and ≺\overline{K} is the induced preorder. □

3.2 Definition of the Operators in the Model

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

Definition 3.5 We define Σ\overline{K} as follows:

Constants: \begin{aligned}NIL\overline{K} & = & ∅ \\ Ω\overline{K} & = & \{⊥\} \end{aligned}

Prefixing: \begin{aligned}c?\overline{K}. & = & λf.\{⟨c?, f⟩\} \\ c!\overline{K}. & = & λ(v, k).\{⟨c!, (v, k)⟩\} \\ τ\overline{K}. & = & λk.\{⟨τ, k⟩\} \end{aligned}

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
int = int_{in} ∪ int_{out} ∪ int_{τ}
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}

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

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

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) (Σ, C)-po structure induced by ⟨\overline{K}, ≺\overline{K}, Σ\overline{K}, C\overline{K}⟩, is a fully applicative (Σ, C)- domain.

3.3 Syntactically Compact Elements

In this last subsection we will show that the compact elements of the model \overline{ACT} may be denoted in our syntax. For this purpose we introduce the syntactically compact Terms, CoT erms = (CoP roc, CoF un, CoP air).

As usual syntactically finite terms are those without occurrences of recursion. We define compact terms as the syntactically finite ones which only use a finite number of values in a nontrivial way. Note that in this case the number of channels used by the term is automatically finite. We start by introducing some notation.

Notation 3.8 Let \underline{v}_{n} = (v_{1}, …, v_{n}) and \underline{p}_{n} = (p_{1}, …, p_{n}). We write x : \underline{v}_{n} ⟶ \underline{x}_{n} for x = v_{1} ⟶ p_{1}, (x = v_{2} ⟶ p_{2}, (… x = v_{n} ⟶ p_{n}, Ω) …). Further we let \{\underline{v_{n}}\} = \{v_{i}|\underline{v_{n}} = (v_{1}, …, v_{n})\} and similarly for \{p_{n}\}.

Definition 3.9 [Compact Terms] The set of compact terms, CoT erms, is the triplet (CoP roc, CoF un, CoP airs) where the sets CoP roc, CoF un and CoP airs are the least sets satisfying:

1. NIL, Ω ∈ CoP roc

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

3. π ∈ CoP air, c ∈ Chan implies c!.π ∈ CoP roc

4. f ∈ CoF un and c ∈ Chan implies c?.f ∈ CoP roc

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

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

We say that a term is compact if it belongs to CoT erms. We let Cot, Cop, etc. range over CoT erms, CoP roc, etc.

□

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} [[ ]] and K[[ ]] are well-defined and for all t ∈ CoT erms: \overline{ACT} [[t]]ρ = [\overline{K}[[t]]]_{≈} where [ ]_{≈} is the quotient mapping with respect to ≺.

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

3. For all k ∈ Co(\overline{ACT}) there is a Cot ∈ CoT erms such that \overline{ACT} [[Cot]] = k.

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.

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

\begin{matrix}(res fun) & ([x]X) \ c = [x](X \ c) \\ (res pair) & (e, X) \ c = (e, X \ c) \\ (ren fun) & ([x]X)[R] = [x](X[R]) \\ (ren pair) & (e, X)[R] = (e, X[R]) \end{matrix}

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

The extended system E_{rec} is then obtained by adding to E three new rules, (rec1), (rec2) and (ω − rule), to take care of recursion. These rules are all fairly standard. The compact approximations, p^{(n)}, used in the rule (ω − rule) are defined in Definition 4.1.

In the rule (res pre) we use the notation chan(pre), where chan(c?) = chan(c!) = c. 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 either a summand of X or Y. To simplify the notation we assume that i, j etc. in the sums ∑_{i}, ∑_{j}, etc. range over finite index sets I, J, etc.

We now define the compact approximations used in the ω-rule of the proof system.

(+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 pre)  (a.X) \ c = \{ \begin{matrix}a.(X \ c) & if c ≠ chan(pre) \\ NIL & otherwise \end{matrix}
(res fun)  ([x]X) \ c = [x](X \ c)
(res pair)  (e, X) \ c = (e, X \ c)
(res NIL)  NIL \ c = NIL
(res div)  Ω \ c = Ω
(ren+)  (X + Y)[R] = X[R] + Y [R]
(ren pre)  (a.X)[R] = R(a).X[R]
(ren fun)  ([x]X)[R] = [x](X[R])
(ren pair  (e, X)[R] = (e, X[R])
(ren NIL)  NIL[R] = NIL
(ren div)  Ω[R] = Ω
(NIL par)  NIL | X = X | NIL = X
(div)  Ω ⊑ X

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 1: Equations

(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}
(rec1) \frac{p ^{⊑} q}{recP.p ^{⊑} recP.q} (rec2) \overline{recP.p = p[recP.p/P]}
(ω − rule) \frac{p^{(n)} ^{⊑} q for all n}{p ^{⊑} q}
(inst)  \overline{pσ ^{⊑} qσ} for every inequation p ^{⊑} q  and instantiation σ
(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 2: The Proof System E_{rec} Definition 4.1 [Compact Approximations] The n-th compact approximation of a term is defined inductively by following:

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, u)^{(n+1)} = be ⟶ p^{(n+1)}, u^{(n+1)} \end{matrix} \end{matrix}

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

III.((v, p))^{(n+1)} = (v, p^{(n+1)})

□

The compact approximations have the following property:

Theorem 4.2 For all n and all ct ∈ CT erms

1. ct^{(n)} ∈ CoT erms

2. [[ct]]ρ = ⨆_{n}[[ct^{(n)}]]ρ

We will end this section by stating the soundness and completeness of the proof system E_{rec} with respect to the denotational semantics. For the proof we refer to the full version of the paper.

Theorem 4.3 [Soundness and Completeness] For all closed terms ct, cu in CT erms, ct ^{⊑}_{E_{rec}} cu if and only if \overline{ACT}[[ct]] ^{⊑} \overline{ACT}[[cu]], i.e. the proof system E_{rec} is sound and complete with respect to the denotational semantics.

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 -orders. Furthermore we show how we may take an 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.

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 and is a direct extension of the model defined by Abramsky in [Abr92].

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

In the last subsection we define a equationally based proof system and show its soundness and completeness with respect to 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 accompanying paper [Ing94a] 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 decided by the compact elements. Behaviourally this can be interpreted as that the preorder may be obtained by finite observations. This is not the case for bisimulation as well known even for the pure calculus. In [Ing94a] 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 this preorder.

References

[Abr92] S. Abramsky: A Domain Equation For Bisimulation, Information and Computation, Vol. 92, pp 161-218, 1992.

[EN86] Engberg, U., Nielsen, M., “A Calculus of Communicating Systems with Label-passing”, Report DAIMI PB-208, Computer Science Department, University of Aarhus, 1986.

[Gue81] Guessarian, I., “Algebraic Semantics”, Springer-Verlag Lecture Notes in Computer Science, vol.99, 1981.

[HI93a] Hennessy, M., Ingólfsdóttir, A. A Theory of Communicating Processes With Value - Passing, Information and Computation, Vol. 107, no. , pp 202-236, 1993.

[HM85] M. Hennessy , R. Milner: Algebraic Laws for Nondeterminism and Concurrency, Journal of the Association for Computing Machinery, vol. 32, No. 1, pp. 137-161, 1985.

[HP80] Hennessy, M. and Plotkin, G., “A Term Model for CCS”, Springer-Verlag Lecture Notes in Computer Science, vol.88, 1980.

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

[Hoa78] Hoare, C.A.R. “Communicating Sequential Processes”, Comm. ACM, 21(8), 666-677 1978.

[Ing93] Ingólfsdóttir, A. Late and Early Semantics Coincide for Testing, Aalborg University Technical Report, IR 93-2008, 1993. To appear in Theoretical Computer Science.

[Ing94] Ingólfsdóttir, A., Semantic Models for Communicating Processes with Value-passing, Ph.D Thesis, Technical Report 8/94, Sussex University, 1994.

[Ing94a] Ingólfsdóttir, A., Semantic Theory for Value-Passing Processes, Late Approach, Part II: Behavioural Semantics and Full Abstractness. In preparation.

[IT92] A. Ingólfsdóttir, B. Thomsen. Semantic Models for CCS with Values. Technical Report 63, Programming Methodology Group, Chalmers University of Technology, 1992. In Proceedings of the Workshop on Concurrency.

[MM79] G. Milne , R. Milner: Concurrent Processes and Their Syntax, Journal of the Association for Computing Machinery, Vol. 26, No. 2, pp. 302-321, 1979.

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

[Mil83] Milner, R. Calculi for Synchrony and Asynchrony, Theoretical Computer Science, 25, pp 267–310, 1983

[Mil89] Milner, R., Communication and Concurrency, Prentice-Hall, London 1989.

[Mil91] R. Milner, Polyadic π-Calculus. A tutorial. To appear in Proceedings of the International Summer School on Logic and Algebra of Specifications, Marktoberdorf, 1991.

[MPW89] R. Milner, J. Parrow & D. Walker, “A Calculus of Mobile Processes” Part I+II, Information and Computation, Vol. 100 no. 1, pp 1-77, 1992.

[MPW91] R. Milner, J. Parrow & D. Walker, Modal Logics for Mobile Processes Proceedings of Concur ’91 , Lecture Notes in Computer Science 327, pp. 45-60, Springer-Verlag, 1991.

[Plo76] G. Plotkin: A Powerdomain Construction, SIAM Journal on Computing, 5 (1976), pp. 452-487, 1976.

[Plo81b] Plotkin, G., “Lecture Notes in Domain Theory”, University of Edinburgh, 1981.

[Sm78] Smyth, M., Powerdomains, JCSS 16(1), 1978

[SP 82] Smyth, M. and Plotkin, G., ”The Category-Theoretic Solution of Recursive Domain Equations”, SIAM Journal on Computing, vol.11, No.4, 1982.

[Win85] Winskel, G., On Powerdomains and Modality, Theoretical Computer Science, 36, pp. 127- 137, 1985.