The Fork Calculus

Klaus Havelund^{1} Kim G. Larsen^{2}

1LIENS – Laboratoire d’Informatique, Ecole Normale Superieure, 45 rue d’Ulm, 75005 Paris, France. Email: havelund@dmi.ens.fr.

2Department of Mathematics and Computer Science, Institute for Electronic Sytems, Aalborg University, DK9220, Aalborg, Denmark. E–mail: kgl@iesd.auc.dk. The work of this author was supported by the Danish Natural Science Research Council project DART and partially by th ESPRIT Basic Research Action 7166, CONCUR2.

Chapter 1

Introduction

The fork-calculus FC is motivated by problems encountered while originally investigating semantic properties of the programming language CML (Concurrent ML) [Rep91, BMT92]. In particular, we address the definition and axiomatisation of suitable equivalences between CML expressions, an area not yet fully investigated in the literature.

CML is an extension of ML with CCS-like concurrency primitives. The model behind CML is that of concurrently executing expressions that communicate by handshake message passing on typed channels. The concurrent aspects of CML, however, differs from CCS in a essential way: In CCS there is a binary parallel operator |, and two processes p and q are put in parallel by p|q. In CML the binary parallel operator has been replaced by a unary fork operator, and a process p is activated to “run in parallel with the rest of the program” by fork(p).

To be more precise, the concurrency primitives of CML are provided as a set of “functions”, from which the following may be derived^{1}:

  val channel  : unit -> 'a chan
  val transmit : 'a chan * 'a -> unit
  val accept   : 'a chan -> 'a
  val fork     : (unit -> 'a) -> unit

The function channel yields a fresh channel each time it is applied. The function transmit sends a value to a channel. The function accept reads a value from a channel. Finally, the function fork starts a separate evaluation of its argument function; that is: fork(f) starts the evaluation of f().

As an example, consider an implementation in CML of a function calc:real->real having the following specification:

                                                             calc(x)=cos(x)+sin(x)

The implementation can be given as follows:

                                                fun calc(x) =
                                                      let val r1 = channel()
                                                          val r2 = channel()
                                                      in
                                                        fork(fn () => transmit(r1,cos(x)));
                                                        fork(fn () => transmit(r2,sin(x)));
                                                        (accept(r1) + accept(r2))
                                                      end;

The function evaluates the expressions cos(x) and sin(x) in parallel. First, two (local) channels r1 and r2 are allocated. Then, the two evaluations are forked; The two forked evaluations send their respective result back on the channels r1 and r2.

Our ultimate goal is to define an appropriate equivalence between CML expressions. Obviously, we have a number of expectations to properties enjoyed by such an equivalence. As an example, consider the following alternative implementation of the calc function, we name it calc':

                                                fun calc'(x) =
                                                      let val r1 = channel()
                                                          val r2 = channel()
                                                      in
                                                        fork(fn () => transmit(r2,sin(x)));
                                                        fork(fn () => transmit(r1,cos(x)));
                                                        (accept(r1) + accept(r2))
                                                      end;

The only difference from calc is that we have changed the order of the two fork expressions. A natural requirement is that calc = calc': it seems reasonable to require the two sequences of fork expressions to be equal since the order of forking should not matter. The result in both cases is two parallel evaluations of the expressions cos(x) and sin(x) and we really do not care about how this result is obtained. In general, we will not want to observe the particular forking strategy — only the collected behaviour of the result. As an even more radical example, the two implementations given here should both satisfy the original specification calc(x)=cos(x)+sin(x). That is, the equation must hold when substituting the right hand sides of the definitions for calc(x).

1There are minor differences in the choice of CML primitives, their types and names, in [Rep91] and [BMT92]. In fact, [BMT92] does not call the defined language CML; but it is stated that the semantics applies to CML. In terms of the primitive features sync, send and receive of [BMT92], which we have chosen to follow, transmit and accept may be defined as: transmit(x) = (sync(send(x));()) and accept(x) = sync(receive(x)).

Another natural and important requirement to our equivalence is that it is a congruence with respect to all CML constructs as this will allow compositional verification. In particular, equivalences between composite expressions should be inferable from equivalences of subexpressions. As an example, we want the equivalence calc = calc' to be infered from an equivalence between the two fork–sequences:

fork(fn () => transmit(r1,cos(x)));
fork(fn () => transmit(r2,sin(x)))

and

fork(fn () => transmit(r2,sin(x)));
fork(fn () => transmit(r1,cos(x)))

The issues of equivalence and compositionality in the presense of forking can best be studied in isolation from the other issues in CML, so we design a calculus, FC(Fork Calculus), that is close to CCS, but which provides a one-argument fork-operator instead of the two-argument parallel-operator found in CCS. Also, the unary prefix–operator of CCS is replaced by a dyadic operator for sequential composition.

FC is thus a projection of CML which focuses on the concurrency aspects. Other existing calculi may also be regarded as projections of CML, although this was not an objective for their design. CCS [Mil89] is another projection focusing on the concurrency aspects. CHOCS [Tho89] is a projection focusing on the higher orderness of CML in the sense that processes can be communicated over channels as “values”. The π-calculus [MPW89] is a projection that focuses on channels, their scope and communication. Finally, the λ-calculus is a projection focusing on the functional subset of CML.

We give a CCS–like, structured operational semantics of FC, in which communication and the forking of processes yield internal transitions. Based on this operational semantics we carry out our search for appropriate equivalences. However, it turns out that the congruence requirement is substantially more difficult to achieve compared with the situation in CCS. As an indication of this, consider the following suggested equivalence:

fork (a); b ≡ a; b + b; a  (1.1)

Given that fork (p); q is the FC–calculus version of the CCS parallel composition of p and q, (1.1) seems to be a direct consequence of the Expansion Law of CCS. However, placing the two expressions fork (a); b and a; b+b; a in the context ; c, we obtain two clearly inequivalent expressions:

(fork (a); b); c ≢ (a; b + b; a); c  (1.2)

As ; is associative, a will be in parallel with b; c on the left–hand side of (1.2) and may thus occur after c. Clearly, this is not possible on the right–hand side, and therefore we must reject the equivalence between the two expressions of (1.2). However, requiring ≡ to be a congruence, this means that we must also reject the equivalence in (1.1). The difference between the two terms of (1.1) can be loosely characterized as a difference in the ability of a to be in parallel with a potential future computation. Attempting to remove this difference we may suggest the following equivalence instead of (1.1):

fork (a); b ≡ a; b + b; fork (a)  (1.3)

The outline of the remainder of this paper is as follows: in chapter 2 we present the syntax and a structured operational semantics of our calculus FC. The semantics is divided into two layers. In the first layer we give semantics to individual processes, whereas the second layer deals with collections of processes running in parallel. In chapter 3 we present the obvious (strong bisimulation) equivalence between processes based on the operational semantics of chapter 2. As indicated in the discussion above, it turns out that this equivalence is not a congruence with respect to the constructs of FC, a rather remarkable fact as strong bisimulation equivalence is preserved by almost all constructs introduced so far in process algebra (see e.g. [GV89]). In chapter 4, we provide an explicit characterization of the congruence induced by the strong bisimulation equivalence. The congruence is essentially a refinement of the strong bisimulation equivalence taking into account processes’ ability to compute in parallel with potential future computations. In chapter 5, we offer a complete axiomatization of this congruence. The axiomatization consists of a number of basic equational axioms and two Expansion Laws allowing as much as possible the fork –operator to be replaced by non–deterministic choice. The completeness proof is based on a notion of normal–form. Finally, in chapter 6, we discuss future work in this area. To increase readability while maintaining credibility, we have placed some full proofs in the appendix.

Syntax and Semantics

The syntax of the calculus is as follows.

L ::= nil | A | L_{1} + L_{2} | L_{1}; L_{2} | fork (L) | N
A ::= τ | a? | a!

nil is the terminated process that can perform no actions. Amongst the actions A that a process can perform are τ, the internal action, input actions of the form a?, and output actions of the form a!, where a is a channel name. Two processes that run in parallel may synchronise on complementary actions, one being an input action and the other being an output action containing the same name. The choice between two processes is written as L_{1} + L_{2}.

Two processes can be sequentially composed by L_{1}; L_{2}. This has the traditional interpretation that L_{1} is evaluated first until it terminates (becomes nil) whereupon L_{2} continues. Note that FC here differs from CCS which instead of sequential composition has action prefixing. The other main difference from CCS is the fork expression: a process is forked with fork (L). It means that a separate evaluation of L is begun such that L is made to run in parallel with the rest of the program. The fork expression itself terminates immediately after starting the separate evaluation of L.

N is the call of a process, that has been named in a definition of the form N =^{def} L. In the present theory we disallow recursion in order to obtain a complete axiomatisation, and we only introduce process naming to be able to write some more appealing (nonrecursive) examples. Except for the complete axiomatisation, it is very easy to extend the results of this paper to allow recursion.

So what are the consequences of this seemingly minor change compared to CCS: having sequential composition and forking instead of action prefixing and parallel composition? There are pragmatic as well as semantic consequences. As we shall see, the semantic consequences are quite drastic. Concerning the pragmatic consequences, let us study an example. Consider the following informal requirement specification:

A ‘session’ at a computer terminal consists of an ‘initialisation’ followed by a ‘run’. The initialisation consists of a ‘setup’ phase followed by a ‘dialog’ phase. After the ‘setup’ phase, a report is sent to a paper printer which will ‘print’ the report.

This requirement specification can be directly presented in FC as follows (note that for convenience, we shall often leave out the ‘?’ when writing input actions; actions are written with small letters by convention):

Session =^{def} Initialise; run
Initialise =^{def} setup; fork (print); dialog

The point to note is that we can locally in Initialise express the parallel activation of the printer (print) after the setup phase. This local activation of a process is not possible in CCS, where we would have to write something like:

Session =^{def} setup.(print | dialog.run.o)

We see that it is not possible to give a name (Initialise) to the pair setup and dialog: one looses abstraction. So characteristic of the fork operator is that we can start a process locally where the need arises, and this gives a possibility of naming a sequential composition that performs parallel activation as a “side effect”.

Of course the above pragmatic difference between FC and CCS is just a matter of taste, and we shall in the following concentrate on the formal implications of having ‘fork ’ and ‘;’.

First, we define an operational semantics for the language of the calculus. That is, the approach taken is that of labeled transition systems as introduced by Plotkin [Plo81] and later applied to CCS as described in [Mil89]. This approach is also the one applied to the existing two semantics of CML: [Rep91, BMT92]. The difference between the semantics here and these two is (except for the different languages) that we let transitions be labeled with actions. Both in [Rep91] and in [BMT92] transitions are basically not labeled. Labels are important from the point of view of defining an appropriate equivalence relation.

A labeled transition system is a triple (St, Lab, →), where St is the set of states (for example processes), Lab is the set of labels (actions performed by the processes) and → ⊆ St × Lab × St is the transition relation: (st_{1}, l, st_{2}) ∈ → may be interpreted as “the state st_{1} is able to perform the action l and by doing so become the state st_{2}”. Typically we use the notation st_{1} →^{l} st_{2} for (st_{1}, l, st_{2}) ∈ →. The transition relation thus defines the dynamic change of states as they perform actions.

The semantics of CCS is normally given in terms of a single labeled transition system where St is the set of CCS processes. In contrast to the CCS semantics, the FC semantics is divided into two layers, corresponding to two labeled transition systems. In the first layer we give semantics to processes seen in isolation (St is the set of processes). In the next layer, we give semantics to collections of processes running in parallel (St is the set of such process collections). When “running” a process, for example fork (p); q we start out with a collection consisting of that process. After the forking, we have a collection containing two processes, p and q, running in parallel. We refer to a collection of processes as a program (thus St is the set of programs).

2.1 Processes

In this section we give semantics to processes seen in isolation. We shall do this by defining a labeled transition system (L, Lab, ↪) where L is the set of processes introduced in chapter 2. Concerning the definition of the labels Lab, assume an infinite set of (channel) names Chan. Then Lab (the labels on process transitions) is gradually defined as follows:

Com = {a? | a ∈ Chan} ∪ {a! | a ∈ Chan}
Act = Com ∪ {τ}
Lab = Act ∪ {ϕ(p) | p ∈ L}

The set Com, ranged over by c, is the set of input-output communications that processes can perform. The set Act, ranged over by α, β, γ, …, includes in addition the τ action, and it is the set of actions that we will be able to observe in the end, when executing programs. The set Lab, ranged over by l, includes further labels of the form ϕ(p) (p ∈ L) which arise from evaluation of processes of the form fork (p). These labels will not be observable at the program layer, since at that level they will be converted into τ actions.

We now define the transition relation ↪ ⊆ L × Lab × L. Before defining this transition relation we define the predicate Stop ⊆ L. We shall use the notation Stop(p) instead of p ∈ Stop. Now Stop is defined as the least subset of L satisfying the following:

1) Stop(nil)
2) If Stop(p_{1}) and Stop(p_{2}) then Stop(p_{1} + p_{2})
3) If Stop(p_{1}) and Stop(p_{2}) then Stop(p_{1}; p_{2})
4) If Stop(p) and N =^{def} p then Stop(N)

The operational semantics of FC processes is then as follows.

Definition 2.1 (The transition relation ↪) Let ↪ be the smallest subset of L × Lab × L closed under the following rules:

(Action)  \overline{α ↪^{α} nil}

(Choice_{1}) \frac{p_{1} ↪^{l} p′_{1}}{p_{1} + p_{2} ↪^{l} p′_{1}}

(Choice_{2}) \frac{p_{2} ↪^{l} p′_{2}}{p_{1} + p_{2} ↪^{l} p′_{2}}

(Sequence_{1}) \frac{p_{1} ↪^{l} p′_{1}}{p_{1}; p_{2} ↪^{l} p′_{1}; p_{2}}

(Sequence_{2}) \frac{p_{2} ↪^{l} p′_{2}}{p_{1}; p_{2} ↪^{l} p′_{2}} Stop(p_{1})

(Fork) \overline{fork (p) ↪^{ϕ(p)} nil}

(Constant)  \frac{P ↪^{l} P′}{A ↪^{l} P′} A =^{def} P

The rules should be fairly simple to read. The Actionrule says that a process of the form α can perform the action α and become nil. The Choice_{1}-rule says that if p_{1} can perform l and become p′_{1}, then the sum p_{1} + p_{2} can also, and symmetrically by the Choice_{2}- rule. The sequencing rules explain how sequencing proceeds with the leftmost process until it has stopped (Sequence_{1}), whereupon the rightmost process continues (Sequence_{2}). The Fork-rule shows how the higher order labels ϕ(p) are created. When we come to the program semantics their use will be explained. Finally, the Constant-rule explains how the name of a process behave as the defining body. Let us look at an example. The process (α; fork (β); γ) can evaluate as follows:

α; fork (β); γ ↪^{α} nil; fork (β); γ ↪^{ϕ(β)} nil; γ ↪^{γ} nil

Note that the forked process β just becomes part of the label, and that it is not further used. When executing programs, we will make sure that the forked process is put in parallel with the “rest of the program”. As another example, consider the process fork (α); fork (β). Its evaluation proceeds as follows:

fork (α); fork (β) ↪^{ϕ(α)} nil; fork (β) ↪^{ϕ(β)} nil

Again, at this level, nothing is put in parallel.

2.2 Programs

A program is a multiset^{1} of processes. We let L_{p} denote the set of programs (L_{p} = MS(L)).

The semantics of programs is given in terms of the labeled transition system (L_{p}, Act, ⟶), where L_{p} is defined here and Act was defined in the previous section. Thus a program can perform the actions in the set Act; recall that these were of the form a?, a! or τ. The fork actions ϕ(p) are thus not amongst program actions.

We shall now define the transition relation: ⟶ ⊆ L_{p} × Act × L_{p}. We need the auxiliary function rev :

Com → Com, which for a given communication returns the complementary communication with which it can synchronise; i.e: rev(a?) = a! and rev(a!) = a?.

The operational semantics of FC programs is then as follows.

Definition 2.2 (The transition relation ⟶) Let ⟶ be the smallest subset of L_{p} × Act × L_{p} closed under the following rules:

(Action^{g})  \frac{p ↪^{α} p′}{\{|p|\} ⟶^{α} \{|p′|\}}

(Fork^{g})  \frac{p ↪^{ϕ(q)} p′}{\{|p|\} ⟶^{τ} \{|p′, q|\}}

(Parallel_{1}^{g}) \frac{P_{1} ⟶^{α} P′_{1}}{P_{1} ∪ P_{2} ⟶^{α} P′_{1} ∪ P_{2}}

(Parallel_{2}^{g}) \frac{P_{1} ⟶^{c} P′_{1} , P_{2} ⟶^{rev(c)} P′_{2}}{P_{1} ∪ P_{2} ⟶^{τ} P′_{1} ∪ P′_{2}}

The Action^{g}-rule just says that if a process can perform an action, then a program containing that process can perform the action. Note that α range over Act, which does not contain ϕ(p) actions. The Fork^{g}-rule explains how a ϕ(…) action results in a τ action at program level: the forking process and the forked process will after the transition be in parallel. Finally, the rule Parallel_{1}^{g} explains how a “subset” of a program may perform actions on its own. Note, that we need only one such rule as ∪ is clearly commutative. The Parallel_{2}^{g}–rule shows how two distinct subsets of a program may communicate, resulting in a τ action.

Example 2.3 As an example, let us deduce how the program {|fork (α); β|} can perform the three transitions τβα (note that it is also possible for the program to perform the transitions ταβ). The first transition is deduced as follows (each deduction refers to the semantic rule used):

(Fork)  \overline{fork (α) ↪^{ϕ(α)} nil}

(Sequence_{1})  \overline{fork (α); β ↪^{ϕ(α)} nil; β}

(Fork^{g}) \overline{\{|fork (α); β|\} ⟶^{τ} \{|nil; β, α|\}}

1A multiset can contain several copies of the same element, (in contrast to normal sets), corresponding to the fact that at a certain moment there may be several processes active with exactly the same structure. Formally, the multisets of A elements can be viewed as the elements in MS(A) = A → N. That is, a multiset of A elements is a total function from A to the natural numbers.

Each A element is mapped to its number of occurrences. The union operator ∪ : (MS(A) × MS(A)) → MS(A) is defined by the equation (S_{1} ∪ S_{2})(a) = S_{1}(a) + S_{2}(a). A “finite” multiset S can be written {|p_{1}, …, p_{n}|} where the number of occurrences of a process q indicates the value S(q). As an example, {|p|}(p) = 1 and {|p|}(q) = 0 whenever p ≠ q.

The second transition is deduced as follows:

(Action)  \overline{β ↪^{β} nil}

(Sequence_{2})  \overline{nil; β ↪^{β} nil}

(Action^{g})  \overline{\{|nil; β|\} ⟶^{β} \{|nil|\}}

(Parallel_{1}^{g}) \overline{\{|nil; β, α|\} ⟶^{β} \{|nil, α|\}}

Finally, the third transition is deduced as follows:

(Action)  \overline{α ↪^{α} nil}

(Action^{g})  \overline{\{|α|\} ⟶^{α} \{|nil|\}}

(Parallel_{1}^{g})

{|nil, α|} ⟶^{α} {|nil, nil|}

The program can thus evaluate as follows:

{|fork (α); β|} ⟶^{τ} {|nil; β, α|} ⟶^{β} {|nil, α|}

⟶^{α} {|nil, nil|}

Program and Process Equivalences

The purpose of this chapter is to define a congruence relation ⌣ ⊆ L_{p} × L_{p} between FC programs. We shall first define ⌣ in terms of the concept of bisimulation. We will then show that this relation is a congruence, a rather important property.

3.1 Program Equivalence

Our notion of congruence is based on the concept of bisimulation [Mil89], which again is based on the idea that we only want to distinguish between two programs, if the distinction can be observed by an “observer” examining the two programs. We say that Q is an α-derivative of P if P ⟶^{α} Q. Then what we are looking for is a relation with the following property:

P and Q are equivalent iff, for every action α, every α-derivative of P is equivalent to some α-derivative of Q and conversely.

Note that in the following we shall regard the τ action just as observable as the other actions (a? and a!) in Act. We shall for example distinguish {|α; τ; β|} and {|α; β|}. This will yield a rather strict congruence (fewer programs are congruent). We shall later in the conclusion discuss the situation where we no longer want to observe the τ actions, thus regarding them as internal. We have chosen to make τ observable in our first attempt, since it is the classical choice: first a strong notion of equivalence is defined (where τ is observable), and then one abstracts from τ.

The formal definition of ⌣ proceeds in the standard way

[Mil89] as follows. First, we define the notion of a bisimulation.

Definition 3.1 (Bisimulation) A binary relation S ⊆ L_{p} × L_{p} is a bisimulation iff (P, Q) ∈ S implies, for all α ∈ Act, 1. Whenever P ⟶^{α} P′ for some P′ then Q ⟶^{α} Q′ for

some Q′ and (P′, Q′) ∈ S

2. Whenever Q ⟶^{α} Q′ for some Q′ then P ⟶^{α} P′ for

some P′ and (P′, Q′) ∈ S

We write P ⌣ Q where (P, Q) ∈ S for some bisimulation S.

As usual it may be shown that ⌣ is itself the largest bisimulation. In fact P ⌣ Q if and only if condition 1 and 2 of definition 3.1 holds. Moreover, ⌣ is easely shown to be an equivalence.

We shall finally state and prove the quite essential property of ⌣ that it is a congruence: ⌣ divides programs into equivalence classes since it is reflexive, symmetric and transitive, and the ∪ operator defined on programs can be applied to any representative of an equivalence class without changing what is the resulting equivalence class. The congruence property is expressed formally as follows:

Lemma 3.2 (⌣ is a congruence) For all programs P_{1}, P_{2} and Q,

Whenever P_{1} ⌣ P_{2} then P_{1} ∪ Q ⌣ P_{2} ∪ Q

Proof

We will show, that the following relation S is a bisimulation:

S =^{def} {(P_{1} ∪ Q, P_{2} ∪ Q) | P_{1} ⌣ P_{2}}

Assume that (P_{1} ∪ Q, P_{2} ∪ Q) ∈ S and let P_{1} ∪ Q ⟶^{α}. There are three cases:

Case 1 P_{1} ⟶^{α} P′_{1} and P_{1} ∪ Q ⟶^{α} P′_{1} ∪ Q. Then since

P_{1} ⌣ P_{2} we have P_{2} ⟶^{α} P′_{2} where P′_{1} ⌣ P′_{2}. So

P_{2} ∪ Q ⟶^{α} P′_{2} ∪ Q and (P′_{1} ∪ Q, P′_{2} ∪ Q) ∈ S.

{|τ; α; β|}  {|fork (α); β|}
↓ τ  ↓ τ
{|nil; α; β|}  {|nil; β, α|}
↓ α  α ↙  ↘ β
{|nil; β|}  {|nil; β, nil|}  {|nil, α|}
↓ β  ↓ β  ↓ α
{|nil|}  {|nil, nil|}  {|nil, nil|}

Figure 3.1: Different Transition Trees

Case 2 Q ⟶^{α} Q′ and P_{1} ∪ Q ⟶^{α} P_{1} ∪ Q′. Then P_{2} ∪

Q ⟶^{α} P_{2} ∪ Q′ and (P_{1} ∪ Q′, P_{2} ∪ Q′) ∈ S.

Case 3 α = τ, P 1 ⟶^{c} P 1′, Q ⟶^{rev(c)} Q′ and P 1 ∪ Q ⟶^{τ}

P 1′ ∪ Q′. Then since P_{1} ⌣ P_{2} we have P_{2} ⟶^{c}

P′_{2} where P′_{1} ⌣ P′_{2}. So P_{2} ∪ Q ⟶^{τ} P′_{2} ∪ Q′ and

(P′_{1} ∪ Q′, P′_{2} ∪ Q′) ∈ S.

A symmetric argument starting with P_{2} ∪ Q ⟶^{α} ends the proof.

3.2 Process Equivalence

In the previous section we introduced an equivalence on programs, and we showed it to be a congruence with respect to the basic operator on programs: ∪. What we are really interested in is, however, not programs, but rather processes. Processes are the terms of our language, and programs are “just” semantic objects used for giving semantics to processes. So our definite goal is to define an equivalence on processes. This equivalence must additionally be a congruence with respect to the operators on processes (+ ; fork ).

In this section we shall come up with a process equivalence ∼, which seems rather natural and correct, but which, however, turns out not to be satisfactory due to lack of the congruence property. In the chapter to follow we will define an equivalence ≡ that is also a congruence, in fact the congruence induced by ∼; but the present exercise can hopefully motivate the final solution.

We shall define an equivalence relation ∼ ⊆ L × L between FC processes. Two processes p and q are said to be equivalent if (p, q) ∈ ∼, which is written more conveniently as p ∼ q.

Well, the idea is to say that two processes are equivalent, if they are equivalent when regarded as programs. Put differently: to see whether two processes are equivalent, “run” them (as programs) and see whether they behave the same way. Formally, we thus define ∼ as follows:

Definition 3.3 (Process equivalence) The relation ∼ ⊆ L × L is defined as:

p ∼ q ⇔ {|p|} ⌣ {|q|}

Let us give a couple of examples. It is easy to verify that {|α; β|} ⌣ {|α; β + α; (β + β)|} (compare the possible transitions). We can therefore conclude that α; β ∼ α; β + α; (β + β). Likewise, we can easely verify that {|α; (β +γ)|} ⌣ / {|α; β +α; γ|}, thus α; (β +γ) ∼ / α; β +α; γ.

Common to these two relationships is that they involve only the operators + and ;. The interesting operator is, however, the fork operator, and in the following we shall see that it (in combination with ;) causes ∼ not to be a congruence (although it is an equivalence since ⌣ is an equivalence). This is rather unusual since (strong) bisimilarity is normally preserved by operators. It is this semantical “melt-down”, that originally caused the design, and investigation, of this calculus.

Consider two processes that are related by ∼:

τ; α ∼ fork (α)

To see this, consider the behaviours of the programs {|τ; α|} and {|fork (α)|}:

{|τ; α|}  ↪^{τ} {|nil; α|} ↪^{α} {|nil|}
{|fork (α)|} ↪^{τ} {|nil, α|} ↪^{α} {|nil, nil|}

Clearly these behaviours are bisimilar (as they are identical). Now, suppose that we put the two processes into the same context ; β. Will it then hold that τ; α; β ∼ fork (α); β? Unfortunately no!. This can be seen from the behaviours of the programs {|τ; α; β|} and {|fork (α); β|}, as illustrated by the transition trees for the two programs in figure 3.1.

Thus, ∼ is not a congruence, and we have to repair this. In the following, we introduce a process relation that is a congruence. It is even the largest congruence induced by (contained in) ∼.

Process Congruence

In this section we introduce a new process equivalence ≡ being strictly finer than the previously given equivalence ∼. As one of the main results of this paper we prove that ≡ is precisely the congruence induced by ∼; i.e. ≡ is preserved by all operators of F C, and is the largest such equivalence included in ∼.

The fact that ∼ is not a congruence is illustrated by the previous example demonstrating the difference between the two processes τ; α and fork (α) when put into the context ; β. The difference lies essentially in the ability of the action α to be in parallel with future computation, which is here represented by the action β.

It is this ability to be in parallel with future computation that we want to capture. Future computation is what computes after the termination of the observed process. When examining the two programs {|τ; α|} and {|fork (α)|}, we cannot detect this termination: both programs perform a τ action and then an α action, and thats it.

The process τ; α, however, terminates after the second action (α), while the process fork (α) already terminates after the first action (τ), when the forking has been performed — the forked process α can then execute after this termination.

We thus need to add some information that makes it possible to observe termination. This can be done by introducing a special event, π, that, when being performed, signals the successful termination of the observed process. For a given process p under observation, we shall examine {|p; π|} rather than just {|p|}.

As an example, in order to observe the difference in terms of future computations between the processes τ; α and fork (α), we “run” τ; α; π and fork (α); π as programs. That is, we examine {|τ; α; π|} and {|fork (α); π|}. Both programs can perform the trace ταπ, but only the program {|fork (α); π|} can perform the trace τπα, where the α action occurs after the π action. This may be illustrated by the transition trees for the two programs, which will be identical to the trees in figure 3.1 with π replacing β.

We are now able to give the following formal definition of the process equivalence ≡:

Definition 4.1 (Process equivalence ≡) The relation ≡ ⊆ L × L is defined as ^{1}:

p ≡ q ⇔ {|p; π|} ⌣ {|q; π|}

Example 4.2 In this example, we shall demonstrate, that the following equivalence holds:

fork (fork (α)) ≡ fork (τ; α)

Due to definition 4.1 we must simply argue for the program equivalence:

{|fork (fork (α)); π|} ⌣ {|fork (τ; α); π|}
To  see  that  this  equation  holds,

we exhibit the following bisimulation S containing the pair ({|fork (fork (α)); π|}, {|fork (τ; α); π|})

{|fork (fork (α)); π|} , {|fork (τ; α); π|}
{|nil; π, fork (α)|} , {|nil; π, τ; α|}
{|nil, fork (α)|} , {|nil, τ; α|}
{|nil, nil, α|} , {|nil, nil; α|}
{|nil, nil, nil|} , {|nil, nil|}
{|nil; π, nil, α|} , {|nil; π, nil; α|}
{|nil; π, nil, nil|} , {|nil; π, nil|}

It is easy to verify that S is indeed a bisimulation.

As one of the main results of this paper we will in the remainder of this section prove that ≡ is the congruence induced by ∼. First of all, it is straightforward to show that ≡ is an equivalence relation.

1This equivalence is similar to one of the equivalences defined in [PGM90]; however, no properties are stated in [PGM90].

Theorem 4.3 ≡ is reflexive, transitive and symmetric.

Also, it is easy to see that ≡ is indeed included in ∼, (a fact which we shall exploit heavily in future proofs):

Lemma 4.4 (Inclusion Lemma) For all processes p_{1}, p_{2},

Whenever p_{1} ≡ p_{2} then {|p_{1}|} ⌣ {|p_{2}|}

Now to the main result — ≡ is a congruence, i.e. ≡ is preserved by the operators of FC.

Theorem 4.5 (Congruence Property) Assume for two processes p_{1}, p_{2} that p_{1} ≡ p_{2}. Then for any process q:

fork (p_{1}) ≡ fork (p_{2})  (4.1)
p_{1} + q ≡ p_{2} + q  (4.2)
q; p_{1} ≡ q; p_{2}  (4.3)
p_{1}; q ≡ p_{2}; q  (4.4)

Proof

For each equation t_{1} ≡ t_{2} we shall prove {|t_{1}; π|} ⌣ {|t_{2}; π|}. Then the equation follows from definition 4.1. Note that our assumption is that p_{1} ≡ p_{2} and therefore that {|p_{1}; π|} ⌣ {|p_{2}; π|}.

(4.1) fork (p_{1}) ≡ fork (p_{2})

We show that {|fork (p_{1}); π|} ⌣ {|fork (p_{2}); π|} by showing that if one of the programs can perform an action, then the other program can perform the same action, and the two resulting programs are equivalent.

Assume that {|fork (p_{1}); π|} ⟶^{τ} {|nil; π, p_{1}|} (note that no other move is possible for the left hand side of the equation). We also have that {|fork (p_{2}); π|} ⟶^{τ} {|nil; π, p_{2}|}. Since p_{1} ≡ p_{2}, lemma 4.4 yields that {|p_{1}|} ⌣ {|p_{2}|}, but then {|nil; π, p_{1}|} ⌣ {|nil; π, p_{2}|} due to the congruence property of ⌣ (lemma 3.2).

The case where we start with {|fork (p_{2}); π|} is similar.

(4.2) Proof left for the reader.

(4.3) Proof left for the reader.

(4.4) p_{1}; q ≡ p_{2}; q

We will show that the following relation S is a bisimulation:

S =^{def} {({|p_{1}; q; π|} ∪ R_{1}, {|p_{2}; q; π|} ∪ R_{2}) |
{|p_{1}; π|} ∪ R_{1} ⌣ {|p_{2}; π|} ∪ R_{2}}
∪ ⌣

Before we go on to show that S is a bisimulation, we will prove (4.4) under that assumption.

Assume that p_{1} ≡ p_{2}, and therefore that {|p_{1}; π|} ⌣ {|p_{2}; π|}. By applying property (5) of lemma A.1, and using transitivity of ⌣, we get that {|p_{1}; π|} ∪ {|nil|} ⌣ {|p_{2}; π|} ∪ {|nil|}. But then the definition of S yields that ({|p_{1}; q; π|} ∪ {|nil|}, {|p_{2}; q; π|} ∪ {|nil|}) ∈ S. Now since we assume that S is a bisimulation, {|p_{1}; q; π|} ∪ {|nil|} ⌣ {|p_{2}; q; π|} ∪ {|nil|}. By applying property (5) of lemma A.1, and using transitivity of ⌣, we get that {|p_{1}; q; π|} ⌣ {|p_{2}; q; π|}

We now show that S is a bisimulation. We don’t consider the pairs in ⌣ (recall that S is defined to contain ⌣) since ⌣ is itself a bisimulation.

Let ({|p_{1}; q; π|}∪R_{1}, {|p_{2}; q; π|}∪R_{2}) ∈ S. Then we know that {|p_{1}; π|} ∪ R_{1} ⌣ {|p_{2}; π|} ∪ R_{2}.

Assume that {|p_{1}; q; π|} ∪ R_{1} ⟶^{α}. Then there are three cases.

Case 1 {|p_{1}; q; π|} ⟶^{α} Q for some Q and {|p_{1}; q; π|} ∪

R_{1} ⟶^{α} Q ∪ R_{1}

Then there are three subcases.

Case 1.1 Stop(p_{1}). Then {|p_{1}; π|} ⟶^{π} {|nil|} and

therefore {|p_{1}; π|} ∪ R_{1} ⟶^{π} {|nil|} ∪ R_{1}. But

since {|p_{1}; π|} ∪ R_{1} ⌣ {|p_{2}; π|} ∪ R_{2}, also

{|p_{2}; π|} ∪ R_{2} ⟶^{π} {|nil|} ∪ R_{2} where {|nil|} ∪

R_{1} ⌣ {|nil|} ∪ R_{2}. By applying property (5) of lemma A.1, and using transitivity of ⌣, we get

that R_{1} ⌣ R_{2}. Now, since {|p_{2}; π|} ∪ R_{2} ⟶^{π}

we know that Stop(p_{2}). In addition, since {|p_{1}; q; π|} ⟶^{α} Q and Stop(p_{1}), we have that {|q; π|} ⟶^{α} Q. So these two facts yields that

{|p_{2}; q; π|} ⟶^{α} Q, and therefore {|p_{2}; q; π|} ∪

R_{2} ⟶^{α} Q ∪ R_{2}. Now finally, since R_{1} ⌣ R_{2}, also Q ∪ R_{1} ⌣ Q ∪ R_{2} due to the congruence property of ⌣. Therefore (Q∪R_{1}, Q∪R_{2}) ∈ S since S includes ⌣.

Case 1.2 p_{1} ↪^{α} p′_{1} and {|p_{1}; q; π|} ∪ R_{1} ⟶^{α}

{|p′_{1}; q; π|} ∪ R_{1}. Then also {|p_{1}; π|} ⟶^{α} {|p′_{1}; π|}

and therefore {|p_{1}; π|} ∪ R_{1} ⟶^{α} {|p′_{1}; π|} ∪ R_{1}.

But sine {|p_{1}; π|} ∪ R_{1} ⌣ {|p_{2}; π|} ∪ R_{2} also

{|p_{2}; π|} ∪ R_{2} ⟶^{α} {|p′_{2}; π|} ∪ R_{3} where {|p′_{1}; π|} ∪

R_{1} ⌣ {|p′_{2}; π|} ∪ R_{3}. But then {|p_{2}; q; π|} ∪ R_{2} ⟶^{α} {|p′_{2}; q; π|} ∪ R_{3} and the definition of S yields that ({|p′_{1}; q; π|} ∪ R_{1}, {|p′_{2}; q; π|} ∪ R_{3}) ∈ S.

Case 1.3 p_{1} ↪^{ϕ(r)} p′_{1} and {|p_{1}; q; π|} ∪ R_{1} ⟶^{τ}

{|p′_{1}; q; π|} ∪ (R_{1} ∪ {|r|}). Then also {|p_{1}; π|} ⟶^{τ}

{|p′_{1}; π|} ∪ {|r|} and therefore {|p_{1}; π|} ∪ R_{1} ⟶^{τ}

{|p′_{1}; π|}∪(R_{1} ∪{|r|}). But since {|p_{1}; π|}∪R_{1} ⌣

{|p_{2}; π|}∪R_{2} also {|p_{2}; π|}∪R_{2} ⟶^{τ} {|p′_{2}; π|}∪R_{3}

where {|p′_{1}; π|}∪(R_{1}∪{|r|}) ⌣ {|p′_{2}; π|}∪R_{3}. But

then {|p_{2}; q; π|}∪R_{2} ⟶^{τ} {|p′_{2}; q; π|}∪R_{3} and the

definition of S yields that ({|p′_{1}; q; π|} ∪ (R_{1} ∪ {|r|}), {|p′_{2}; q; π|} ∪ R_{3}) ∈ S.

Case 2 R_{1} ⟶^{α} R′_{1} and {|p_{1}; q; π|} ∪ R_{1} ⟶^{α} {|p_{1}; q; π|} ∪

R′_{1}. Then also {|p_{1}; π|} ∪ R_{1} ⟶^{α} {|p_{1}; π|} ∪ R′_{1}. But

since {|p_{1}; π|} ∪ R_{1} ⌣ {|p_{2}; π|} ∪ R_{2} also {|p_{2}; π|} ∪

R_{2} ⟶^{α} {|p′_{2}; π|}∪R′_{2} where {|p_{1}; π|}∪R′_{1} ⌣ {|p′_{2}; π|}∪

R′_{2}. Therefore {|p_{2}; q; π|} ∪ R_{2} ⟶^{α} {|p′_{2}; q; π|} ∪ R′_{2}

and the definition of S yields that ({|p_{1}; q; π|} ∪ R′_{1}, {|p′_{2}; q; π|} ∪ R′_{2}) ∈ S.

Case 3 {|p_{1}; q; π|} ⟶^{c} {|X; π|}, R_{1} ⟶^{rev(c)} R′_{1} and

{|p_{1}; q; π|} ∪ R_{1} ⟶^{τ} {|X; π|} ∪ R′_{1}.

Case 3.1 Stop(p_{1}) and {|p_{1}; q; π|}∪R_{1} ⟶^{τ} {|q′; π|}∪

R′_{1}. Since Stop(p_{1}) we have that {|p_{1}; π|} ⟶^{π}

{|nil|} and therefore {|p_{1}; π|} ∪ R_{1} ⟶^{π} {|nil|} ∪

R_{1}. But since {|p_{1}; π|} ∪ R_{1} ⌣ {|p_{2}; π|} ∪ R_{2}

also {|p_{2}; π|}∪R_{2} ⟶^{π} {|nil|}∪R_{2} where {|nil|}∪

R_{1} ⌣ {|nil|} ∪ R_{2}. By applying property (5) of lemma A.1, and using transitivity of ⌣, we

get that R_{1} ⌣ R_{2}. Now since {|p_{2}; π|}∪R_{2} ⟶^{π}

we know that Stop(p_{2}). In addition, since {|p_{1}; q; π|} ⟶^{c} {|X; π|} and Stop(p_{1}), we have that {|q; π|} ⟶^{c} {|q′; π|}. So these two facts yields that {|p_{2}; q; π|} ⟶^{c} {|q′; π|}. Now since

R_{1} ⟶^{rev(c)} R′_{1} and R_{1} ⌣ R_{2}, we get that

R_{2} ⟶^{rev(c)} R′_{2} where R′_{1} ⌣ R′_{2}. We can thus

conclude that {|p_{2}; q; π|} ∪ R_{2} ⟶^{τ} {|q′; π|} ∪ R′_{2}.

Due to the congruence property of ⌣ we have that {|q′; π|} ∪ R′_{1} ⌣ {|q′; π|} ∪ R′_{2} and therefore ({|q′; π|} ∪ R′_{1}, {|q′; π|} ∪ R′_{2}) ∈ S since S includes ⌣.

Case 3.2 p_{1} ↪^{c} p′_{1} and {|p_{1}; q; π|} ∪ R_{1} ⟶^{τ}

{|p′_{1}; q; π|} ∪ R′_{1}. Then also {|p_{1}; π|} ∪ R_{1} ⟶^{τ}

{|p′_{1}; π|} ∪ R′_{1}. But since {|p_{1}; π|} ∪ R_{1} ⌣

{|p_{2}; π|}∪R_{2} also {|p_{2}; π|}∪R_{2} ⟶^{τ} {|p′_{2}; π|}∪R′_{2}

where {|p′_{1}; π|} ∪ R′_{1} ⌣ {|p′_{2}; π|} ∪ R′_{2}. There-

fore {|p_{2}|} ∪ R_{2} ⟶^{τ} {|p′_{2}|} ∪ R′_{2} and therefore

{|p_{2}; q; π|} ∪ R_{2} ⟶^{τ} {|p′_{2}; q; π|} ∪ R′_{2}. Finally,

the definition of S yields that ({|p′_{1}; q; π|} ∪ R′_{1}, {|p′_{2}; q; π|} ∪ R′_{2}) ∈ S A symmetric argument starting with {|p_{2}; q; π|}∪R_{2} ends the proof.

We are now finally able to state (and prove) the following main result:

Theorem 4.6 (Induced Congruence Property) ≡ is the largest congruence contained in ∼.

Proof Using the previous theorem and lemma it is clear that ≡ is a congruence included in ∼. To see that ≡ is the largest such, assume that ≃ is an arbitrary congruence included in ∼. Now assume p ≃ q. As ≃ is assumed to be a congruence it follows that p; π ≃ q; π, and — as ≃ is supposed to be included in ∼ — also p; π ∼ q; π. However, then p ≡ q according to the definitin of ≡ and it follows that ≃ is included in ≡.

Strong Axiomatisation

In this chapter we present a sound and complete axiomatization for the process congruence ≡. The completeness of the axiomatization is obtained in a classical manner through the use of normalforms — being process expressions with a very restricted use of the fork –operator. More precisely, the axiomatization consists of a collection of basic equational axioms, and two Expansion Laws. The Basic Axioms achieve completeness for normalform processes, and the Expansion Laws (together with the Basic Axioms) enable arbitrary process expressions to be transformed into normalform, thus yielding completeness for the full calculus.

In more classical process calculi, Expansion Laws allow parallel composition to be replaced by non-determinism. In our calculus, the Expansion Laws will have an analogous purpose, namely that of replacing as much as possible forking with non–deterministic choice. However — as we shall see in the next section — our calculus seems to lack expressive power for suitable Expansion Laws to exist. To overcome this problem, we shall extend the calculus with an extra operator to described below ^{1}.

5.1 Searching for an Expansion Law

Axioms involving only the operators ‘+’, ‘nil‘ and ‘;‘ can easely be verified (replacing = with ≡); for example:

p + q = q + p
nil; p = p

We will, however, also need more interesting axioms involving the fork operator. Basically, we need an expansion law, that describes how forking may be expanded into nondeterminism — similar to the expansion law of CCS that expands parallel operator into nondeterminism. For example, consider the following instance of the CCS expansion law:

a.o | b.o = a.b.o + b.a.o

Let us try to search for a similar expansion law for the FC fork operator. We will simplify the problem and just search for an expansion of a simple process, similar to what we did for the CCS term a.o | b.o above. We will thus try to expand the corresponding FC–process fork (α); β. An initial guess can be the following:

fork (α); β = α; β + β; α

However, this equation is not sound (it does not hold when replacing = with ≡), and can therefore immediately be ignored. Intuitively, the reason is that the righthand side contains no information about α’s capability to be in parallel with “the rest of the program”. In the next seemingly correct equation we try to take this into account:

fork (α); β = α; β + β; fork (α)  (5.1)

This equation is not sound either: the left hand side can perform a τ action as the first thing, while the right hand side can perform either an α action or a β action (note that since we want to axiomatise strong process congruence ≡, τ actions are observable). Trying to repair this problem we obtain:

fork (α); β = τ; (α; β + β; fork (α)) (5.2)

1This phenomena is similar to the necessity of the leftmerge operator in PL in order to obtain a finite sound and complete equational axiomatization as shown in [Mol90].

This equation is not sound either: the left hand side can only perform one τ action, while the right hand side can perform two (the explicitely mentioned and the one caused by fork ).

So it seems that we cannot in general expand forking! This leaves open the problem of how to establish equality between process expressions involving the fork - operator? The latter two attempts above suggest that we need a version of fork which is instantaneous without the initial internal transition caused by fork . Put alternatively, we lack the ability to express that something has been forked, with the initial τ action already having occurred previously. To gain this expressivity, we add a new instantaneous forking operator to our calculus. We call this operator forked , and we write forked (p) to mean ‘fork p without a τ’. One can regard this operator alternatively by reading forked (p) as ‘p has been forked’, or shorter: ‘forked p’. The latter reading suggests the following relationship between fork and forked :

fork (p) = τ; forked (p)

Let us now try to write new versions of the equations (5.1) and (5.2), that contain the forked operator in appropriate positions. These equations can be shown sound on basis of the formal definition we give of the forked operator in the following section. The equations are:

forked (α); β = α; β + β; forked (α)
fork (α); β = τ; (α; β + β; forked (α))

However, it remains to settle whether it is possible to find an operator forked satisfying the above equations. In the next section we give an affirmative answer by providing an operational semantics for this new operator.

5.2 Adding the ‘Forked’-operator

The syntax is extended with the forked (p) alternative:

L^{Φ} ::= nil | A | L^{Φ}_{1} + L^{Φ}_{2} | L^{Φ}_{1}; L^{Φ}_{2} | fork (L^{Φ})
| forked (L^{Φ}) | N

The extended calculus is called FC^{Φ}.

The set Lab of actions that a process can perform is extended accordingly:

Lab = Act ∪ {ϕ(p) | p ∈ L^{Φ}} ∪ {Φ(p) | p ∈ L^{Φ}}

The new (local) semantics of processes is obtained by adding the following rule:

(Forked)

forked (p) ↪^{Φ(p)} nil

Similarly, the new (global) semantics of programs is obtained by adding the following rule:

(Forked^{g}) \frac{p ↪^{Φ(q)} p′, \{|p′, q|\} ⟶^{α} R}{\{|p|\} ⟶^{α} R}

5.3 Basic Axioms and Inference Rules

The final axiom system AS consists of a set AX of equational axiom schemes, two expansion laws E_{1} and E_{2}, using normal forms, and a set I of inference rules. In this section we shall present the basic equational axioms AX and the the inference rules I.

Definition 5.1 (The basic axiom system AX) The basic axiom system AX consists of the following axioms:

p; nil = p  (5.3)
nil; p = p  (5.4)
(p; q); r = p; (q; r)  (5.5)
(p + q); r = p; r + q; r  (5.6)

p + (q + r) = (p + q) + r  (5.7)
p + q = q + p  (5.8)
p + nil = p  (5.9)
p + p = p  (5.10)

fork (p) = τ; forked (p) (5.11)
forked (forked (p)) = forked (p)  (5.12)
forked (p + q) = forked (p) +
forked (q)  (5.13)
forked (α; forked (p)) = forked (α; p) (5.14)
forked (nil) = nil  (5.15)

Proposition 5.2 (AX is sound) The axiom system AX is sound with respect to strong process congruence.

Proof See in Appendix A, proposition A.2.

Definition 5.3 (The inference rules I) The inference rules I are:

(Reflexive)  \overline{p = p}

(Symmetric)  \frac{p = q}{q = p}

(T ransitive)  \frac{p = q, q = r}{p = r}

(Congruence) \frac{p = p′}{Op(…, p, …) = Op(…, p′, …)}

Proposition 5.4 (I is sound) The inference rules I are sound with respect to strong process congruence.

Proof The rules must hold when replacing = with ≡. For the three first equivalence rules, this is the case as stated in theorem 4.3. Concerning the last congruence rule, proposition 4.5 states this for the operators in the original calculus FC; it, however, remains to prove soundness when Op is the new forked operator. We refer to Appendix A, proposition A.3 for this fact.

5.4 Normal Forms

Our way to completeness is classical in that it is based on normal forms. For processes in normal form, the basic axioms AX will be shown to be complete, and we shall in the next section present two Expansion Laws that will enable any process term to be transformed into a provable equivalent normal form process term.

Processes in normal form contain no applications of the fork operator, and applications of the forked operator occur last. One intuition behind this is that when observing a process we cannot observe the individual forkings; and as long as the original process has not terminated, we cannot observe which actions comes from it and which actions come from the forked processes. We can, however, in contexts observe when the process terminates and what at that time has been forked. In principle a process is brought into normal form by first replacing applications fork (p) by τ; forked (p) (applying axiom 5.11), and then by moving the applications of forked as much as possible “to the right”. Note that we must deal with the forked operator in normal forms, since we must keep track of what is potentially in parallel with future computation.

As an example, consider the process fork (α); β. First, we can replace fork (α) with τ; forked (α), thus obtaining τ; forked (α); β. Then we can consider the process forked (α); β, and bring it into the form α; β + β; forked (α). As result we obtain τ; (α; β + β; forked (α)). We see that there is no application of the fork operator, and that the application of the forked operator occurs last.

We can also put some semantic light on normal forms. Consider a process N in normal form, and consider the transition tree having {|N|}, as root. Then this tree can be pictured as in figure 5.1.

Each path through the tree can be considered as consisting of two parts: a before termination part followed by a potential in parallel with future computation part. The latter part coming from an argument to the forked operator.

Let us now formally introduce normal forms:

Definition 5.5 (Normal form) A process p is in normal form, if it is a term in N, where:

N ::= ∑_{i} α_{i}; N_{i} + ∑_{j} β_{j}; forked (B_{j})
B ::= ∑_{k} β_{k}; B_{k}

A process p is in simple normal form, if it is a term in B.

                             /\
                            /  \    <---- before future computation
                           /_\
                          /::\___\        potential in parallel with
                         /::::::::\ <---- future computation
                         ----------

Figure 5.1: Computation Tree

Note that simple normal forms contain no applications of the forked operator. That is, once we have reached the termination of a process (second alternative in the definition of N), what remains has all been forked, and to express this we only need one application of the forked operator. That is, we do not care about any “further” forking.

5.5 Expansion Laws

The two Expansion Laws to be presented in this section will enable any process term to be transformed into normal form. To motivate the two Expansion Laws consider the case of a sequential composition of two process terms N and M already in normal form. Now assume N is of the following form:

N = ∑_{i} α_{i}; N_{i} + ∑_{j} β_{j}; forked (B_{j})

Then, using the laws for distributing ; over + and laws of associativity for ;, we obtain:

⊢ N; M = ∑_{i} α_{i}; (N_{i}; M) + ∑_{j} β_{j}; (forked (B_{j}); M)

To enable this term to be transformed into a normal form we introduce the following Expansion Law:

Definition 5.6 (Expansion law E_{1})

Let:

A = ∑_{i} α_{i}; A_{i}
N = ∑_{j} β_{j}; N_{j}
L = ∑_{k} γ_{k}; forked (C_{k})
M = N + L

where M is not nil, then:

forked (A); M = A′ + B′ + C′ + D′ + E′

where:

A′ = ∑_{i} α_{i}; forked (A_{i}); M
B′ = ∑_{j} β_{j}; forked (A); N_{j}
C′ = ∑_{k} γ_{k}; forked (A); forked (C_{k})
D′ = ∑_{α_{i}=rev(β_{j})} τ; forked (A_{i}); N_{j}
E′ = ∑_{α_{i}=rev(γ_{k})} τ; forked (A_{i}); forked (C_{k})

Proposition 5.7 (E_{1} is sound) The expansion law E_{1} is sound with respect to strong process congruence.

Proof

See Appendix proposition A.4

As an example illustrating expansion law E_{1}, we shall prove that ⊢ forked (α); β = α; β + β; forked (α). As a motivation for proving this, recall that we in section 5.4 indicated how the process fork (α); β could be brought into the normal form τ; (α; β + β; forked (α)). The first step was to apply axiom (5.11), thus obtaining τ; forked (α); β. The next step was to bring forked (α); β into the form α; β+β; forked (α), a step that we can now verify is legal:

forked (α); β

=

forked (α; nil); β; nil

– axiom 5.3

=

α; forked (nil); β; nil + β; forked (α; nil); nil

– expansion law E_{1}

=

α; β + β; forked (α)

– axioms (5.3), (5.15)

To be able to inductively transform forked (A); M into normal form, we see in definition 5.6 that we need to be able to handle terms of the form forked (A); forked (B). This motivates the second Expansion Law below:

Definition 5.8 (Expansion law E_{2})

Let:

A = ∑_{i} α_{i}; A_{i}
B = ∑_{j} β_{j}; B_{j}

Then:

forked (A); forked (B) = forked (A′ + B′ + C′)

where:

A′ = ∑_{i} α_{i}; forked (A_{i}); forked (B)
B′ = ∑_{j} β_{j}; forked (A); forked (B_{j})
C′ = ∑_{α_{i}=rev(β_{j})} τ; forked (A_{i}); forked (B_{j})

Proposition 5.9 (E_{2} is sound) The expansion law E_{2} is sound with respect to strong process congruence.

Proof

See Appendix proposition A.5

As an example illustrating the application of expansion law E_{2} we prove in figure 5.2 that ⊢ forked (α); forked (β) = forked (β); forked (α).

The Basic Axioms AX, the two Expansion Laws E_{1} and E_{2} and the inference rules I constitute our proof system AS, which we shall show to be (limited) complete. We write ⊢ p = q if the equivalence of p and q can be entailed within the proof system AS.

5.6 Soundness and Limited Completeness

In this section we shall show, that the axiom system AS is sound and complete with respect to strong process congruence. That is, we shall prove that ⊢ p = q ⇔ p ≡ q. The soundness (⇒) has already been proved since the axioms AX, E_{1} and E_{2} have been proved to hold when replacing ‘=’ with ‘≡’, and so have the inference rules I.

The basic technique for showing completeness is classical; i.e. first to prove that each process term in the forked (α); forked (β) = forked (α; nil); forked (β; nil)

– axiom (5.3)

=

forked (α; forked (nil); forked (β; nil)+

β; forked (α; nil); forked (nil))

– expansion law E_{2}

=

forked (α; forked (β) + β; forked (α))

– axioms (5.15),(5.3)

=

forked (α; forked (β)) + forked (β; forked (α))

– axiom (5.13)

=

forked (α; β) + forked (β; α)

– axiom (5.14)

=

forked (α; β + β; α)

– axiom (5.13)

=

forked (β; α + α; β)

– axiom (5.8)

=

⋮ = forked (β); forked (α)

– by the same reasoning

Figure 5.2: A proof using Expansion Law.

original forked -free calculus of chapter 2 is equivalent to a term in normal form, and then to prove completeness for normal forms. The fact that the completeness result only will apply to forked -free processes makes it “limited”.

AS is Sound

Proposition 5.10 (AS is sound) For all p, q in FC^{Φ},

Whenever ⊢ p = q then p ≡ q.

Proof

Soundness of AS reduces to soundness of the basic axioms AX, soundness of the expansion laws E_{1} and E_{2} and soundness of the inference rules I. This was proved in propositions 5.2, 5.7, 5.9 and 5.4.

Existence of Normal Forms

This subsection states four lemmas and a proposition. The first two lemmas state, that in certain cases, two applications of the forked operator can be reduced to one application. The next two lemmas state the existence of normal forms for subcategories of process terms. These four lemmas lead to the final proposition stating that there exists a normal form for every process term in FC. Note that there does not exist a normal form for every process term in FC^{Φ}; as an example, the process forked (α) has no normal form.

First we need a lemma saying that nested forked applications in certain cases can be removed, only keeping the outermost application.

Lemma 5.11 (Nested forked s) For any normal form N, there exists a simple normal form A such that:

⊢ forked (N) = forked (A)

Proof

See Appendix lemma A.6.

The second lemma says that two forked applications (one after the other) in certain cases can be reduced to a single forked application.

Lemma 5.12 (Sequential forked s) For any simple normal forms A and B, there exists a simple normal form C such that:

⊢ forked (A); forked (B) = forked (C)

Proof

See Appendix lemma A.7.

Now to the two lemmas stating the existence of normal forms for subcategories of process terms.

Lemma 5.13 (Normal forms for a subcategory) For any simple normal form A and normal form M (M different from nil), there exists a normal form N such that:

⊢ forked (A); M = N

Proof

See Appendix A.8.

Lemma 5.14 (Normal forms for a subcategory) For any two normal forms M, N, there exists a normal form K such that:

⊢ M; N = K

Proof

See Appendix lemma A.9.

We can finally state the following important proposition:

Proposition 5.15 (Normal forms for FC) For any p in FC, there exists a normal form N such that:

⊢ p = N

Proof

The proof is by structural induction. Assume that any subterm has a normal form. That is, if p and q are subterms, then ⊢ p = M and ⊢ q = N where:

M = ∑_{i} α_{i}; M_{i} + ∑_{k} γ_{k}; forked (C_{k})
N = ∑_{j} β_{j}; N_{j} + ∑_{l} δ_{l}; forked (D_{l})

Then we proceed by case analysis:

\underline{Case nil}: nil is on normal form.

\underline{Case α}: α = α; nil using axiom (5.3).

\underline{Case p + q}:

p + q = M + N

– induction hypothesis

=

(∑_{i} α_{i}; M_{i} + ∑_{k} γ_{k}; forked (C_{k}))+ (∑_{j} β_{j}; N_{j} + ∑_{l} δ_{l}; forked (D_{l}))

– unfolding of M and N

=

(∑_{i} α_{i}; M_{i} + ∑_{j} β_{j}; N_{j})+

(∑_{k} γ_{k}; forked (C_{k}) + ∑_{l} δ_{l}; forked (D_{l}))

– axiom (5.8)

\underline{Case p; q}: If N is nil, the normal form is M. Otherwise use the normal form lemma 5.14:

p; q =

M; N – induction hypothesis

=

K  – lemma 5.14

\underline{Case fork (p)}: Use lemma 5.11:

fork (p) =

fork (M)  – induction hypothesis

=

τ; forked (M) – axiom (5.11)

=

τ; forked (A) – lemma 5.11 applied to forked (M)

– yielding forked (A) where A is on – simple normal form

Limited Completeness

We are now able to formally present our completeness result. First, we shall state the important completeness result for normal forms. The proof, however, requires the following lemma, stating completeness for a subcategory of processes.

Lemma 5.16 For all simple normal forms A, B in FC^{Φ},

Whenever forked (A) ≡ forked (B)
then  ⊢ forked (A) = forked (B)

Proof

Assume that forked (A) ≡ forked (B). We use induction on the sum n of the depths of A and B.

\underline{Base case n = 0}: In this case both A and B are nil, and reflexivity yields that ⊢ forked (nil) = forked (nil).

\underline{Induction step n > 0}: Assume that A and B have the forms:

A = ∑_{i} α_{i}; A_{i}
B = ∑_{j} β_{j}; B_{j}

As a step towards showing that ⊢ forked (A) = forked (B), we shall show that for each summand S_{A} of A, there is a summand S_{B} of B, such that ⊢ forked (S_{A}) = forked (S_{B}); and vice versa. By definition 4.1, {|forked (A); π|} ⌣ {|forked (B); π|}. Due to axiom (A.1), we the have that {|A, π|} ⌣ {|B, π|}. Now let {|A, π|} make a move.

{|A, π|} ⟶^{α_{i}} {|nil; A_{i}, π|} where α_{i} is different from π. Then since ⌣ is a bisimulation, {|B, π|} ⟶^{α_{i}} {|nil; B_{j}, π|} where {|nil; A_{i}, π|} ⌣ {|nil; B_{j}, π|}. But then again due to axiom (A.1) we have that {|forked (nil; A_{i}); π|} ⌣ {|forked (nil; B_{j}); π|} which means that forked (nil; A_{i}) ≡ forked (nil; B_{j}). From the latter we can deduce that forked (A_{i}) ≡ forked (B_{j}) since equation (5.4) is known to be sound. Since forked (A_{i}) ≡ forked (B_{j}), the induction hypothesis yields that ⊢ forked (A_{i}) = forked (B_{j}) and therefore that ⊢ α_{i}; forked (A_{i}) = α_{i}; forked (B_{j}) due to the congruence property. Congruence again gives that ⊢ forked (α_{i}; forked (A_{i})) = forked (α_{i}; forked (B_{j})) and then axiom (5.14) yields ⊢ forked (α_{i}; A_{i}) = forked (α_{i}; B_{j}). So for every summand α_{i}; A_{i} of A, there is a summand α_{i}; B_{j} of B such that ⊢ forked (α_{i}; A_{i}) = forked (α_{i}; B_{j}):

A = … + α_{i}; A_{i} + …
B = … + α_{i}; B_{j} + …

Similarly for every summand of B. We can now deduce that ⊢ forked (A) = forked (A + B) and ⊢ forked (A + B) = forked (B) and therefore by transitivity that ⊢ forked (A) = forked (B). The technique for showing for example that ⊢ forked (A) = forked (A + B) is to apply the following transformation for each summand β_{j}; B_{j} of B. We know that there exists a summand α_{i}; A_{i} of A such that ⊢ forked (α_{i}; A_{i}) = forked (β_{j}; B_{j}). Then we can perform the following deduction:

forked (A)

=

forked (A + α_{i}; A_{i})

– axioms (5.7),(5.8) and (5.10)

=

forked (A) + forked (α_{i}; A_{i})

– axiom (5.13)

=

forked (A) + forked (β_{j}; B_{j})

– since ⊢ forked (α_{i}; A_{i}) = forked (β_{j}; B_{j})

– and then congruence property

=

forked (A + β_{j}; B_{j})

– axiom (5.13)

We can now state a completeness result for the normal forms of FC^{Φ}.

Proposition 5.17 (Normal form completeness) For all normal forms M, N in FC^{Φ},

Whenever M ≡ N then ⊢ M = N

Proof

Assume that M ≡ N. We use induction on the maximum depth n of M and N.

\underline{Base case n = 0}: In this case both M and N are nil, and reflexivity yields that ⊢ nil = nil.

\underline{Induction step n > 0}: Assume that M and N have the forms:

M = ∑_{i} α_{i}; M_{i} + ∑_{k} γ_{k}; forked (C_{k})
N = ∑_{j} β_{j}; N_{j} + ∑_{l} δ_{l}; forked (D_{l})

As a step towards showing that ⊢ M = N, we shall show that for each summand of M, there is an equivalent summand of N, and vice versa. By definition 4.1, {|M; π|} ⌣ {|N; π|}. Now let {|M; π|} make a move. We get two cases depending on whether M choses an α_{i}; M_{i} alternative or an γ_{k}; forked (C_{k}) alternative.

Case 1 M  ↪^{α_{i}}  nil; M_{i}

and {|M; π|} ⟶^{α_{i}} {|nil; M_{i}; π|}, then since ⌣ is a bisimulation, {|N; π|} ⟶^{α_{i}} {|nil; N_{j}; π|} where {|nil; M_{i}; π|} ⌣ {|nil; N_{j}; π|}. Note that N cannot choose an δ_{l}; forked (D_{l}) alternative since it can never hold that {|nil; M_{i}; π|} ⌣ {|nil; forked (D_{l}); π|}. But then M ↪^{α_{i}} nil; M_{i} and N ↪^{α_{i}} nil; N_{j}, and nil; M_{i} ≡ nil; N_{j}. From the latter we can deduce that M_{i} ≡ N_{j} since equation (5.4) is known to be sound. Since M_{i} ≡ N_{j} the induction hypothesis yields that ⊢ M_{i} = N_{j} and therefore that ⊢ α_{i}; M_{i} = α_{i}; N_{j} due to the congruence property. So for every summand α_{i}; M_{i} of M, there is a summand α_{i}; N_{j} of N such that ⊢ α_{i}; M_{i} = α_{i}; N_{j}:

M = … + α_{i}; M_{i} + …
N = … + α_{i}; N_{j} + …

Case 2 M ↪^{γ_{k}} nil; forked (C_{k}) and {|M; π|} ⟶^{γ_{k}} {|nil; forked (C_{k}); π|}, then since ⌣ is a bisimulation, {|N; π|} ⟶^{γ_{k}} {|nil; forked (D_{l}); π|} where {|nil; forked (C_{k}); π|} ⌣ {|nil; forked (D_{l}); π|}. Note that N cannot choose an β_{j}; N_{j} alternative since it can never hold that {|nil; forked (C_{k}); π|} ⌣ {|nil; N_{j}; π|}. But then M ↪^{γ_{k}} nil; forked (C_{k}) and N ↪^{γ_{k}} nil; forked (D_{l}), and nil; forked (C_{k}) ≡ nil; forked (D_{l}). From the latter we can deduce that forked (C_{k}) ≡ forked (D_{l}) since equation (5.4) is known to be sound. Since forked (C_{k}) ≡ forked (D_{l}), lemma 5.16 yields that ⊢ forked (C_{k}) = forked (D_{l}) and therefore that ⊢ γ_{k}; forked (C_{k}) = γ_{k}; forked (D_{l}) due to the congruence property. So for every summand γ_{k}; forked (C_{k}) of M, there is a summand γ_{k}; forked (D_{l}) of N such that ⊢ γ_{k}; forked (C_{k}) = γ_{k}; forked (D_{l}):

M = … + γ_{k}; forked (C_{k}) + …
N = … + γ_{k}; forked (D_{l}) + …

From the above case analysis, we can conclude that for every summand S_{M} of M there exists a summand S_{N} of N such that ⊢ S_{M} = S_{N}. Similarly, for every summand of N there exists an equivalent summand of M.

We can now deduce that ⊢ M = M + N and ⊢ M + N = N and therefore by transitivity that ⊢ M = N. The technique for showing for example that ⊢ M = M + N is to apply the following transformation for each summand S_{N} of N. We know that there exists a summand S_{M} of M such that ⊢ S_{M} = S_{N}. Then we can perform the following deduction:

M =

M + S_{M} – axioms (5.7),(5.8) and (5.10)

=

M + S_{N} – ⊢ S_{M} = S_{N} and then congruence property

The completeness result we arrive at is limited in the sense that it only holds for process terms of FC(and not FC^{Φ}).

Proposition 5.18 (AS is limited Complete) For all p, q in FC,

Whenever p ≡ q then ⊢ p = q

Proof

Assume that p ≡ q. Now, due to proposition 5.15 there exist normal forms, say M and N such that ⊢ p = M and ⊢ q = N. Then, due to the soundness proposition 5.10, we deduce p ≡ M and q ≡ N. The initial assumption p ≡ q together with the latter two facts then yields M ≡ N by transitivity. But proposition 5.17 states completeness for normal forms, so ⊢ M = N. Now together with the facts that ⊢ p = M and ⊢ q = N, transitivity then yields the result ⊢ p = q.

Conclusion and Future Work

In this paper we have identified and axiomatized a congruence ≡ between FC–processes. Also, it has been demonstrated that ≡ is the congruence induced by a natural strong bisimulation equivalence ∼.

In practice, however, both ∼ and ≡ are too fine, as they are sensitive to internal computations. To obtain a more suitable equivalence, we may consider the weak bisimulation equivalence ≈ between processes, in which we abstract away from τ–transitions. Doing this, we will observe the same phenomena as we did for the strong equivalence: ≈ is not preserved by sequential composition. Applying the technique of this paper — i.e. defining p ≅ q if p; π ≈ q; π — we obtain the coarset equivalence contained in ≈ which is also preserved by ; (and fork ). However, ≅ will not quite be a congruence as it will not be preserved by the choice–operator. This is a classical problem [Mil89], and we conjecture that the classical techniques for overcoming this problem will apply to ≅. Also, we conjecture that the congruence obtained in this manner will be completely axiomatized by the axiomatization AS presented in this paper augmented with the classical τ–laws [Mil89].

As immediate future work we intend to investigate the FC–calculus extended with primitives for dynamic channel creation and communication of channels. A more long–term ambition is to extend our work to the full language of CML.

Further future work include design of appropriate (logical) specification languages for CML (and related/projected calculi). We consider the work presented in this paper of major importance for such future work: it should be shown that the designed specification language is adequate with respect to a suitable process– equivalence; i.e. two processes enjoys the same properties of the specification languages precisely when they are behaviourally equivalent. The work of the present paper provides a good candidate for such a behavioural equivalence.

Appendix A Proofs

The appendix contains proofs of properties used in the main text.

Lemma A.1

{|forked (p); q|} ⌣ {|p, q|}  (A.1)
{|forked (p)|} ⌣ {|p|}  (A.2)
P ∪ Q ⌣ Q ∪ P  (A.3)
P ∪ (Q ∪ R) ⌣ (P ∪ Q) ∪ R  (A.4)
P ∪ {|nil|} ⌣ P  (A.5)

Proof

Only the proof of (A.1) is presented here; the proofs of the other equations are left for the reader.

We show that {|forked (p); q|} ⌣ {|p, q|} by showing that if one of the programs can perform an action, then the other program can perform the same action, and the two resulting programs are equivalent.

Assume that {|forked (p); q|} ⟶^{α} S. Since forked (p); q ↪^{Φ(p)} nil; q we can conclude from the global semantics of the forked - operator that {|p, nil; q|} ⟶^{α} S. From this follows easely

that {|p, q|} ⟶^{α} S′ where S′ ⌣ S.

If we let the right hand side {|p, q|} move first, we can use the above argument in the reverse direction.

Proposition A.2 (AX is sound) The axiom system AX is sound with respect to strong process congruence.

Proof

For each equation t_{1} = t_{2} we must prove that t_{1} ≡ t_{2}, which due to the definition 4.1 of strong process congruence amounts to proving that {|t_{1}; π|} ⌣ {|t_{2}; π|}. We will only present the proofs of (5.11) and (5.12).

(5.11) fork (p) = τ; forked (p)

We will show, that the following relation S is a bisimulation:

S =^{def} {({|fork (p); π|}, {|τ; forked (p); π|}),
({|nil; π, p|}, {|nil; forked (p); π|})}
∪IdL_{p}^{Φ}

Here IdL_{p}^{Φ} = {(p, p) | p ∈ L_{p}^{Φ}}. We don’t need to

consider the pairs in IdL_{p}^{Φ} since this is obviously itself a

bisimulation. So we consider the other pairs in turn.

The pairs ({|fork (p); π|}, {|τ; forked (p); π|}):

Assume that {|fork (p); π|} ⟶^{τ} {|nil; π, p|}. But also {|τ; forked (p); π|} ⟶^{τ} {|nil; forked (p); π|} and ({|nil; π, p|}, {|nil; forked (p); π|}) ∈ S. The case where we start with {|τ; forked (p); π|} is similar.

The pairs ({|nil; π, p|}, {|nil; forked (p); π|}):

Assume that {|nil; π, p|} ⟶^{α} P. We know that

nil; forked (p); π ↪^{Φ(p)} nil; π and in combination with the assumption, the semantic rule Forked^{g} yields that {|nil; forked (p); π|} ⟶^{α} P. Since IdL_{p}^{Φ} ⊆ S,

(P, P) ∈ S.

The case where we start with {|nil; forked (p); π|} is similar.

(5.12) forked (forked (p)) = forked (p)

We  show  that

{|forked (forked (p)); π|} ⌣ {|forked (p); π|} by showing that if one of the programs can perform an action, then the other program can perform the same action, and the two resulting programs are equivalent.

Assume that {|forked (forked (p)); π|} ⟶^{α} P. We

know that forked (forked (p)); π ↪^{Φ(forked (p))} nil; π and in combination with the assumption, the semantic rule Forked^{g} (used backwards) yields that {|nil; π, forked (p)|} ⟶^{α} P. Since {|forked (p)|} ⌣ {|p|} (property (A.2)) the congruence property implies that {|nil; π, forked (p)|} ⌣ {|nil; π, p|} and therefore that {|nil; π, p|} ⟶^{α} P′ where P ⌣ P′. Now,

forked (p); π ↪^{Φ(p)} nil; π so the semantic rule Forked^{g} yields that {|forked (p); π|} ⟶^{α} P′.

The case where we start with {|forked (p); π|} is similar.

Proposition A.3 For all p, q in FC^{Φ},

Whenever p ≡ q then forked (p) ≡ forked (q).

Proof Let p and q be FC^{Φ} processes such that p ≡ q. We shall then prove that forked (p) ≡ forked (q). We show that {|forked (p); π|} ⌣ {|forked (q); π|} by showing that if one of the programs can perform an action, then the other program can perform the same action, and the two resulting programs are equivalent.

Assume that {|forked (p); π|} ⟶^{α} P. By the seman-

tic rules we additionally have that forked (p); π ↪^{Φ(p)} nil; π. Now applying the semantic rule (F orked^{g}) backwards, we get that {|p, nil; π|} ⟶^{α} P. Soundness of axiom (5.4) yields that nil; π ≡ π and the inclusion lemma 4.4 then yields {|nil; π|} ⌣ {|π|}. But then congruence yields that {|p, nil; π|} ⌣ {|p, π|}. Thus also

{|p, π|} ⟶^{α} P′ where P ⌣ P′. Now since p ≡ q the

inclusion lemma 4.4 yields that {|p|} ⌣ {|q|} and hence congruence gives {|p, π|} ⌣ {|q, π|}. But this means that also {|q, π|} ⟶^{α} Q′ where P′ ⌣ Q′. Now due to a reasoning similar to above {|q, nil; π|} ⌣ {|q, π|} so therefore also {|q, nil; π|} ⟶^{α} Q where Q′ ⌣ Q.

Since obviously (semantic rules) forked (q); π ↪^{Φ(q)} nil; π, applying the semantic rule (F orked^{g}) forwards gives {|forked (q); π|} ⟶^{α} Q. Transitivity finally yields that P ⌣ Q.

The case where we start with {|forked (q); π|} is similar.

Proposition A.4 (E_{1} is sound) The expansion law E_{1} is sound with respect to strong process congruence.

Proof We want to prove that forked (A); M ≡ A′ + B′ + C′ + D′+E′ which due to definition 4.1 follows if we can prove {|forked (A); M; π|} ⌣ {|(A′ + B′ + C′ + D′ + E′); π|}. Using property (A.1) in lemma A.1, we can bring the left hand side of this equation into a more convenient form: {|forked (A); M; π|} ⌣ {|A, M; π|}. So it remains to show {|A, M; π|} ⌣ {|(A′ + B′ + C′ + D′ + E′); π|}.

We show this by showing that if one of the programs can perform an action, then the other program can perform the same action, and the two resulting programs are equivalent. First, we let the left hand side {|A, M; π|} perform an action. There are three cases.

Case 1 {|A|} ⟶^{α_{i}} {|A_{i}|} and {|A, M; π|} ⟶^{α_{i}} {|A_{i}, M; π|}.

We also know that A′ ↪^{α_{i}} forked (A_{i}); M and therefore that {|(A′ + B′ + C′ + D′ + E′); π|} ⟶^{α_{i}} {|forked (A_{i}); M; π|}. Finally, property (A.1) yields that {|forked (A_{i}); M; π|} ⌣ {|A_{i}, M; π|}.

Case 2 M; π makes a move. In this case, since M is not nil, and since M = N + L, either N or L makes the move, thus giving two cases.

Case 2.1 {|M; π|} ⟶^{β_{j}} {|N_{j}; π|} and {|A, M; π|} ⟶^{β_{j}}

{|A, N_{j}; π|}.

We also know that B′ ↪^{β_{j}} forked (A); N_{j} and

therefore that {|(A′+B′+C′+D′+E′); π|} ⟶^{β_{j}} {|forked (A); N_{j}; π|}. Finally, property (A.1) yields that {|forked (A); N_{j}; π|} ⌣ {|A, N_{j}; π|}.

Case 2.2 {|M; π|} ⟶^{γ_{k}} {|forked (C_{k}); π|} and

{|A, M; π|} ⟶^{γ_{k}} {|A, forked (C_{k}); π|}. We also

know that C′ ↪^{γ_{k}} forked (A); forked (C_{k}) and therefore that {|(A′+B′+C′+D′+E′); π|} ⟶^{γ_{k}} {|forked (A); forked (C_{k}); π|}. Finally, property (A.1) yields that {|forked (A); forked (C_{k}); π|} ⌣ {|A, forked (C_{k}); π|}.

Case 3 A and M; π communicates. In this case, since M = N + L, either N or L communicates with A, thus giving two cases.

Case 3.1 {|A|} ⟶^{α_{i}} {|A_{i}|}, {|M; π|} ⟶^{β_{j}} {|N_{j}; π|}

where a_{i} = rev(b_{j}) and {|A, M; π|} ⟶^{τ}

{|A_{i}, N_{j}; π|}. we also know that D′ ↪^{τ} forked (A_{i}); N_{j} and therefore that {|(A′ + B′ +

C′+D′+E′); π|} ⟶^{τ} {|forked (A_{i}); N_{j}; π|}. Fi-

nally, property (A.1) yields that {|forked (A_{i}); N_{j}; π|} ⌣ {|A_{i}, N_{j}; π|}.

Case 3.2 {|A|} ⟶^{α_{i}} {|A_{i}|}, {|M; π|} ⟶^{γ_{k}}

{|forked (C_{k}); π|} where a_{i} = rev(c_{k}) and

{|A, M; π|} ⟶^{τ} {|A_{i}, forked (C_{k}); π|}. We also

know that E′ ↪^{τ} forked (A_{i}); forked (C_{k}) and therefore that {|(A′+B′+C′+D′+E′); π|} ⟶^{τ} {|forked (A_{i}); forked (C_{k}); π|}. Finally, property (A.1) yields that {|forked (A_{i}); forked (C_{k}); π|} ⌣ {|A_{i}, forked (C_{k}); π|}.

If we let the right hand side {|(A′ +B′ +C′ +D′ +E′); π|} move first, we can use the above argument in the reverse direction. The conclusion is that {|A, M; π|} ⌣ {|(A′ + B′ + C′ + D′ + E′); π|}, and we are done.

Proposition A.5 (E_{2} is sound) The expansion law E_{2} is sound with respect to strong process congruence.

Proof

We want to prove that forked (A); forked (B) ≡ forked (A′ + B′ + C′) which due to definition 4.1 follows if we can prove {|forked (A); forked (B); π|} ⌣ {|forked (A′ + B′ + C′); π|}. Using the property (A.1) in lemma A.1 and the congruence property of ⌣, we can bring the left hand side and right hand side of this equation into more convenient forms. Left hand side:

{|forked (A); forked (B); π|}
⌣ {|A, forked (B); π|}
⌣ {|A, B, π|}

and right hand side:

\begin{matrix}\{|forked (A′ + B′ + C′); π|\} \\ ⌣ \{|(A′ + B′ + C′), π|\} \end{matrix}

So the remaining job is to show {|A, B, π|} ⌣ {|(A′+B′+ C′), π|}. But, since ⌣ is a congruence, it will be enough to show that {|A, B|} ⌣ {|A′ + B′ + C′|} (Note how close this is to the CCS expansion law in [Mil89] page 96).

We show this by showing that if one of the programs can perform an action, then the other program can perform the same action, and the two resulting programs are equivalent. First, we let the left hand side {|A, B|} perform an action. There are three cases.

Case 1 {|A|} ⟶^{α_{i}} {|A_{i}|} and {|A, B|} ⟶^{α_{i}} {|A_{i}, B|}. We

also know that A′ ↪^{α_{i}} forked (A_{i}); forked (B) and

therefore  that  {|A′  +

B′ + C′|} ⟶^{α_{i}} {|forked (A_{i}); forked (B)|}. Property (A.1) yields that {|forked (A_{i}); forked (B)|} ⌣ {|A_{i}, forked (B)|} and property (A.2) further yields that {|A_{i}, forked (B)|} ⌣ {|A_{i}, B|}. So transitivity yields that {|forked (A_{i}); forked (B)|} ⌣ {|A_{i}, B|}.

Case 2 {|B|} ⟶^{β_{j}} {|B_{j}|} and {|A, B|} ⟶^{β_{j}} {|A, B_{j}|}. We

also know that B′ ↪^{β_{j}} forked (A); forked (B_{j}) and

therefore  that  {|A′  +

B′ + C′|} ⟶^{β_{j}} {|forked (A); forked (B_{j})|}. Property (A.1) yields that {|forked (A); forked (B_{j})|} ⌣ {|A, forked (B_{j})|} and property (A.2) further yields that {|A, forked (B_{j})|} ⌣ {|A, B_{j}|}. So transitivity yields that {|forked (A); forked (B_{j})|} ⌣ {|A, B_{j}|}.

Case 3 {|A|} ⟶^{α_{i}} {|A_{i}|}, {|B|} ⟶^{β_{j}} {|B_{j}|} where α_{i} =

rev(β_{j}) and {|A, B|} ⟶^{τ} {|A_{i}, B_{j}|}. We also know

that C′ ↪^{τ} forked (A_{i}); forked (B_{j}) and therefore that {|A′+B′+C′|} ⟶^{τ} {|forked (A_{i}); forked (B_{j})|}. Property (A.1) yields that {|forked (A_{i}); forked (B_{j})|} ⌣ {|A_{i}, forked (B_{j})|} and property (A.2) further yields that {|A_{i}, forked (B_{j})|} ⌣ {|A_{i}, B_{j}|}. So transitivity yields that {|forked (A_{i}); forked (B_{j})|} ⌣ {|A_{i}, B_{j}|}.

If we let the right hand side {|A′ + B′ + C′|} move first, we can use the above argument in the reverse direction. The conclusion is that {|A, B|} ⌣ {|A′ + B′ + C′|}, and we are done.

Lemma A.6 (Nested forked s) For any normal form N, there exists a simple normal form A such that:

⊢ forked (N) = forked (A)

Proof

We use induction on the depth n of N.

\underline{Base case n = 0:} In this case N = nil, and since nil is already on simple normal form, we have our A = nil, and surely ⊢ forked (nil) = forked (nil).

\underline{Induction step n > 0:} Assume that N has the form:

N = ∑_{i} α_{i}; N_{i} + ∑_{j} β_{j}; forked (B_{j})

Then we can perform the following deductions: forked (N) = forked (∑_{i} α_{i}; N_{i} + ∑_{j} β_{j}; forked (B_{j}))

– unfolding N

= forked (∑_{i} α_{i}; N_{i}) + forked (∑_{j} β_{j}; forked (B_{j}))

– axiom (5.13)

= L + R

– name the two summands L (left) and R (right)

We can now transform the summands L and R as follows. In the case of L we get:

L

=

forked (∑_{i} α_{i}; N_{i})

=

∑_{i} forked (α_{i}; N_{i})  – axiom (5.13)

=

∑_{i} forked (α_{i}; forked (N_{i})) – axiom (5.14)

=

∑_{i} forked (α_{i}; forked (A_{i}))

– induction hypothesis applied to

– forked (N_{i}). A_{i} is on

– simple normal form

=

∑_{i} forked (α_{i}; A_{i})  – axiom (5.14)

=

forked (∑_{i} α_{i}; A_{i})  – axiom (5.13)

In the case of R we get:

R = forked (∑_{j} β_{j}; forked (B_{j})) =

∑_{j} forked (β_{j}; forked (B_{j})) – axiom (5.13)

=

∑_{j} forked (β_{j}; B_{j})  – axiom (5.14)

=

forked (∑_{j} β_{j}; B_{j})  – axiom (5.13)

We can thus conclude that:

forked (N) = … = L + R = forked (∑_{i} α_{i}; A_{i}) + forked (∑_{j} β_{j}; B_{j}) = forked (∑_{i} α_{i}; A_{i} + ∑_{j} β_{j}; B_{j}) – axiom (5.13)

The latter argument to forked is on simple normal form, and so we are done.

Lemma A.7 (Sequential forked s) For any simple normal forms A and B, there exists a simple normal form C such that:

⊢ forked (A); forked (B) = forked (C)

Proof

Use induction on the sum n of depths of A and B. The base cases are those where the depth of either A or B is zero (A or B is nil).

\underline{Base case} n = depth(A) or n = depth(B) In case one of A or B is nil one can use axioms (5.15), (5.3) and (5.4) to obtain the result. For example if A is nil:

forked (A); forked (B)

=

forked (nil); forked (B) – unfolding of A

=

nil; forked (B)  – axiom (5.15)

=

forked (B)  – axiom (5.4)

\underline{Induction step} n > depth(A) and n > depth(B) In this case, neither A or B is nil. Use expansion law E_{2} (definition 5.8).

Let:

A = ∑_{i} α_{i}; A_{i}
B = ∑_{j} β_{j}; B_{j}

Then:

forked (A); forked (B) = forked (∑_{i} α_{i}; A_{i}); forked (∑_{j} β_{j}; B_{j})

– unfolding of A and B

= forked ( ∑_{i} α_{i}; forked (A_{i}); forked (B)+ ∑_{j} β_{j}; forked (A); forked (B_{j})+ ∑_{α_{i}=rev(β_{j})} τ; forked (A_{i}); forked (B_{j}))

– expansion law E_{2}

= forked ( ∑_{i} α_{i}; forked (C_{i})+ ∑_{j} β_{j}; forked (D_{j})+ ∑_{α_{i}=rev(β_{j})} τ; forked (E_{i,j}))

– induction hypothesis yielding new simple normal forms – C_{i}, D_{j} and E_{i,j}

= forked (∑_{i} α_{i}; forked (C_{i}))+ forked (∑_{j} β_{j}; forked (D_{j}))+ forked (∑_{α_{i}=rev(β_{j})} τ; forked (E_{i,j}))

– axiom (5.13)

= ∑_{i} forked (α_{i}; forked (C_{i}))+ ∑_{j} forked (β_{j}; forked (D_{j}))+ ∑_{α_{i}=rev(β_{j})} forked (τ; forked (E_{i,j}))

– axiom (5.13)

= ∑_{i} forked (α_{i}; C_{i})+ ∑_{j} forked (β_{j}; D_{j})+ ∑_{α_{i}=rev(β_{j})} forked (τ; E_{i,j})

– axiom (5.14)

= forked (∑_{i} α_{i}; C_{i})+ forked (∑_{j} β_{j}; D_{j})+ forked (∑_{α_{i}=rev(β_{j})} τ; E_{i,j})

– axiom (5.13)

= forked (∑_{i} α_{i}; C_{i} + ∑_{j} β_{j}; D_{j} + ∑_{α_{i}=rev(β_{j})} τ; E_{i,j})

– axiom (5.13)

Lemma A.8 (Normal forms for a subcategory) For any simple normal form A and normal form M (M different from nil), there exists a normal form N such that:

⊢ forked (A); M = N

Proof

Use induction on the sum n of the depth of A and M with the base cases where the depth of A is zero (recall that M is different from nil when applying this lemma, also in the inductive step).

\underline{Base case} n = depth(M) (depth(A) = 0):

forked (nil); M

=

nil; M  – axiom (5.15)

=

M  – axiom (5.4)

\underline{Induction step} n > depth(M) (depth(A) > 0):

Let:

A = ∑_{i} α_{i}; A_{i}
M = ∑_{j} β_{j}; M_{j} + ∑_{k} γ_{k}; forked (C_{k})

and:

A′ = ∑_{i} α_{i}; A′′
where A′′ = forked (A_{i}); M
B′ = ∑_{j} β_{j}; B′′
where B′′ = forked (A); M_{j}
C′ = ∑_{k} γ_{k}; C′′
where C′′ = forked (A); forked (C_{k})
D′ = ∑_{α_{i}=rev(β_{j})} τ; D′′
where D′′ = forked (A_{i}); M_{j}
E′ = ∑_{α_{i}=rev(γ_{k})} τ; E′′
where E′′ = forked (A_{i}); forked (C_{k})

Then using the expansion law E_{1} (definition 5.6) we get:

forked (A); M = A′ + B′ + C′ + D′ + E′

Now, each of the summands S′ is on the form ∑_{n} act_{n}; S′′. Due to the induction hypothesis, the summand A′′ reduces to a term on normal form. This is also the case for B′′ and D′′ in case M_{j} is different from nil. If M_{j} on the other hand is nil, B′′ and D′′ reduce to respectively forked (A) and forked (A_{i}) due to axiom (5.3). Finally, due to lemma 5.12, the summands C′′ and E′′ each reduce to a term of the form forked (G) where G is on simple normal form. To conclude, each S′′ reduces to a term in normal form or to a term on the form forked (G) where G is on simple normal form. Therefore the summation A′ + B′ + C′ + D′ + E′ reduces to a normal form.

Lemma A.9 (Normal forms for a subcategory) For any two normal forms M, N, there exists a normal form K such that:

⊢ M; N = K

Proof We use induction on the depth n (length of longest path a_{1}; a_{2}; …) of M.

\underline{Base case} n = 0:

M; N = nil; N – unfolding M = N – axiom (5.4)

\underline{Induction step} n > 0: Use the normal form lemma 5.13

M; N = (∑_{i} α_{i}; M_{i} + ∑_{k} γ_{k}; forked (C_{k})); N

– unfolding M which is on normal form

= ∑_{i} α_{i}; M_{i}; N + ∑_{k} γ_{k}; forked (C_{k}); N

– axiom (5.6)

= ∑_{i} α_{i}; K_{i} + ∑_{k} γ_{k}; forked (C_{k}); N

– induction hypothesis applied to M_{i}; N

– yielding normal form K_{i}

= ∑_{i} α_{i}; K_{i} + ∑_{k} γ_{k}; L_{k}

– normal form lemma applied to forked (C_{k}); N – yielding normal form L_{k}

Bibliography

[BMT92] D. Berry, R. Milner, and D.N. Turner. A Semantics for ML Concurrency Primitives. POPL, 1992.

[GV89] J. F. Groote and F. W. Vaandrager. Structured Operational Semantics and Bisimulation as a Congruence. Lecture Notes in Computer Science, 372, 1989.

[Mil89] R. Milner. Communication and Concurrency. International Series in Computer Science. Prentice Hall, 1989.

[Mol90] F. Moller. The Importance of the Left Merge Operator in Process Algebra. Lecture Notes in Computer Science, 443, 1990.

[MPW89] R. Milner, J. Parrow, and D. Walker. A Calculus of Mobile Processes, part I and II. Technical report, Department of Computer Science, University of Edinburgh, 1989. To appear in Information and Computation.

[PGM90] S. Prasad, A. Giacalone, and P. Mishra. Operational and Algebraic Semantics for Facile. Lecture Notes in Computer Science, 443, 1990. In Proceedings of ICALP90.

[Plo81] G. Plotkin. A Structural Approach to Operational Semantics. FN 19, DAIMI, Aarhus University, Denmark, 1981.

[Rep91] J.H. Reppy. An Operational Semantics of First–class Synchronous Operations. Technical Report TR 91–1232, Cornell University, Department of Computer Science, 1991.

[Tho89] B. Thomsen. A Calculus of Higher Order Communicating Systems. Proceedings of POPL, 1989.