9512.net

甜梦文库

甜梦文库

当前位置：首页 >> >> # A Filter Model for Mobile Processes

A Filter Model for Mobile Processes

Dipartimento di Informatica - Universita di Torino Corso Svizzera 185 - 10149 Torino (Italy) e-mail: fdamiani,dezani,gianninig@di.unito.it Received 13 November 1997

Math. Struct. in Comp. Science (1993), vol. 11, pp. 1{000. Printed in the United Kingdom c 1993 Cambridge University Press

y

F E R R U C C I O D A M I A N I, M A R I A N G I O L A D E Z A N I - C I A N C A G L I N I and P A O L A G I A N N I N I

This paper presents a lter model for -calculus, and shows its full abstraction with respect to a \may" operational semantics. The model is introduced in the form of a type assignment system. Types are related by a preorder which mimics the operational behaviour of terms. A subject expansion theorem holds. Terms are interpreted as lters of types: this interpretation is compositional. The proof of full abstraction relies on a notion of realizability of types, and on the construction of terms, which test when an arbitrary term has a xed type.

Introduction

Process algebras are among the most successful formalisms for reasoning about concurrent processes. The starting point for the study of process algebras is the CCS formalism, introduced in (Milner 1980) (see also (Milner 1989) and (Hennessy 1988)). Inspired by the -calculus (Barendregt 1984), CCS is based on a small set of basic actions and primitive constructors that are meant to characterize the behaviour of communicating processes. Even though CCS allows for dynamic creation of processes, the topology of the possible interactions between processes is xed by their syntax. So mobile systems, that is systems with a dynamically-changing pattern of communications, cannot be expressed. Various extensions have been proposed to overcome this problem. On one side there is the -calculus (Milner et al. 1992), see also (Milner 1991), (Milner 1992), and (Sangiorgi 1992). In the -calculus channels are passed as values in communications. The restriction operator models static binding in the sense that: 1 the property of being a bound or a free channel is invariant under reduction of terms, and 2 each bound channel refers to the same binder during reduction. On the other side there are various versions of higher-order process calculi. In these languages processes are explicitly passed as values in communications. Process-passing languages have been studied with respect to both the static and the dynamic binding of

y

This work was partly supported by NATO Grant HTECH.LG960875.

F. Damiani, M. Dezani-Ciancaglini and P. Giannini

2

channels. For example, Plain CHOCS (Thomsen 1990), and HO (Sangiorgi 1992) have static binding. Instead, CHOCS (Thomsen 1990), and the languages studied in (Hennessy 1994a) and (Hennessy 1994b) have the dynamic binding. The semantics of CCS and of its extensions was originally given in an operational way by bisimulation techniques. In (Milner et al. 1993) a characterization of early and late bisimulation for the calculus via modal logics is presented. The authors introduce a set of modal formulas and a satisfaction relation for processes based on the labelled transition system. Such satisfaction relation produces an axiomatic semantics. In (Amadio and Dam 1996) this axiomatic approach is extended using a richer logic. The logical language considered: a version of the -calculus, is shown to be su ciently expressive to characterize the nite behaviour of processes. Moreover the authors present an algorithm that checks that processes satisfy a speci cation expressed in the logical language. Their proof system is quite similar to ours. The main advantage of our approach is that of giving at the same time a complete proof system and a fully abstract model. In (De Nicola and Hennessy 1984), and more extensively in (Hennessy 1988), operational semantics for CCS based on \may" and \must" preorders are introduced. The \may" and \must" operational semantics test respectively the possibility and the necessity of performing communications. Moreover (Hennessy 1988) presents a denotational semantics that is fully abstract with respect to these operational preorders. Denotational semantics can be given through a \logical" description of domains. Such an approach goes back to (Scott 1982), and has been advocated in (Abramsky 1991a) as a general paradigm unifying, among other things, type assignment, logic of programs and logical characterizations of behaviour of concurrent processes such as Hennessy-Milner logic. The semantics can be introduced through a type assignment system, with types ordered by an inclusion relation. The interpretation of a term is the lter of types that can be assigned to it. This produces a denotational model in the sense that the denotation of a term is given by means of the denotations of its components. This has been used in (Barendregt et al. 1983) and (Abramsky and Ong 1991) for -calculus. In the same line are the studies concerning extensions of -calculus by means of operators with concurrent features like (Ong 1993; Boudol 1994; Dezani et al. 1996; Dezani et al. 1997). In (Abramsky 1991b) it is given a denotational model of SCCS based on a domain of synchronization trees. This domain is described through a domain logic related to it by Stone duality. (Hennessy 1994a) presents the rst denotational model of higher-order concurrent processes based on a compromise between type systems and modal logic. Here type-formulas are built using arrows, (implicit) conjunction and pre xing connectors, expressing the ability to communicate (which are a kind of indexed modalities as in Hennessy-Milner logic). The resulting lter model turns out to be fully abstract with respect to an operational semantics based on a notion of testing and \may" convergency. This semantics is equivalent to trace semantics. The restriction operator on channels models dynamic binding. Indeed a process sent from one process to another can escape a

A Filter Model for Mobile Processes

3

restriction or can be captured by a restriction. (Hennessy 1994b) builds a lter model for higher-order processes which is adequate but not complete with respect to the \must" testing. The scoping of variables is again dynamic. One of the important issues about process algebras is the study of the possible behaviourial equivalences. -calculus processes are usually compared either by bisimulation (Milner et al. 1993) or by testing (Boreale and De Nicola 1995). In the case of bisimulation, one needs to distinguish between early and late bisimulation, according to the fact that an input transition may or may not correspond to one atomic event, see (Milner et al. 1993). A well know problem shared by early, late bisimulation and testing for -calculus is that the equivalence between processes obtained is not a congruence. In (Boreale and Sangiorgi 1996) some general results about the limitations that must be imposed on the language to show that some bisimilarities are congruences are studied. In particular they prove that, in order to turn ground bisimulation into a congruence, matching must be removed, and either the output pre x must be limited or the bisimilarity has to take into account also the causality of actions. The main problem arises from matching. For example, we have that x = y]ab:0 is equivalent to 0, since both processes o er no communication, however a(x): x = y]ab:0 di ers from a(x):0. In fact, a(x): x = y]ab:0 can communicate with ay:0 yielding the process ab:0, while only 0 is the result of the communication between a(x):0 and ay:0. To overcome this problem, (Sangiorgi 1996) proposes the open bisimulation which compares processes under all possible substitutions. With the substitution assigning x to y (or vice versa) we can discriminate between 0 and x = y]ab:0, which becomes ab:0. More generally, open bisimulation induces an equivalence between processes which is a congruence. Along a similar line, we de ne our observational equivalence. That is, we test processes allowing rst substitutions, which may satisfy the matchings involved. In this way we obtain a congruence. In our model the interpretation of a process P is bigger than the interpretation of its restriction with respect to any channel name, i.e., xP for all x. This would no longer be true for a language including the mismatch operator (as shown in (Boreale and De Nicola 1995)). The calculus studied in this paper is the version of -calculus with replication of processes (instead of constants) and matching, and without the \sum" (external choice) operator. We de ne a \may" operational semantics and a logically characterized denotational semantics. In particular the denotation of a term is the lter of types (properties) assignable to the term. This interpretation is compositional in the sense that the interpretation of a term (the lter of types that can be assigned to it) is uniquely determined by the interpretation of its subterms. It is not sensible to add the external choice to our language, since the -calculus can simulate the internal choice (as de ned in (De Nicola and Hennessy 1987)) and since the internal and external choices have an identical behaviour in a \may" perspective (Milner 1980). The main problem we solved is the interpretation of the restriction on channels, since restriction obeys a static binding discipline. We quote from (Hartonas and Hennessy 1997):

F. Damiani, M. Dezani-Ciancaglini and P. Giannini

4

\Thus the major challenges are to extend the mathematical framework so that a proper scoping of channel names can be properly modelled : : :"

Unfortunately, the present paper did not win this challenge, since it gives a program logic modelling static binding, but id does not provide the underlying domain construction. The contribution of this paper is methodological. We show that the technique of providing a logical model for a language based on lters of assignable properties can be applied also to languages, like the -calculus, including channel communication and static scoping of names. For this reason, our priority has been to keep both the process language and the operational semantics as simple as possible. So we considered the \may" testing and a restricted version of the -calculus which does not include many interesting process constructors, notably the mismatch. As a matter of fact, following the approach of (Hennessy 1994b) we can build a lter model which is adequate with respect to the \must" testing. To be coherent with the present approach, a logic describing must behaviours needs two type constructors, to model respectively the internal and the external choices. As shown in (Dezani et al. 1996; Dezani et al. 1997) the union of types corresponds in a natural way to the internal choice in a must perspective. The type constructor mimicking the external choice would be rather \ad hoc". Instead there are problems (already discussed in (Hennessy 1994b)) in obtaining a complete model in this case. Essentially test terms (see De nition 54) would require a quite unnatural extension of the -calculus. We conjecture that we can model also mismatch by adding environments (mirrored by basis in the type assignment system) which state equalities and disequalities of names. We notice that the above extensions would increase considerably the (already nonelementary) present treatment. Types express operational behaviours of processes and therefore our type inference system is a proof system to argue about properties of programs. Since the model de ned is fully abstract, this proof system is both correct and complete. Terms not containing replication have a principal type that is dependent on their syntax. So we can de ne algorithms checking the observational behaviours of terms. The de nition of the language and its operational semantics are given in Section 1. The operational semantics is presented in two stages. First we de ne the reduction relation. Then we de ne a \may" convergency predicate that expresses the capability of a process of o ering a communication along a given channel. We consider an observational preorder based on testing enriched by substitutions. In Section 2 we introduce the type syntax and the preorder on types. The channel restriction corresponds in a natural way to a binding operator on channels and the matching operator of processes to a matching operator of types. The matching operator plays a central role in the de nition of the equivalence between types (properties) and in the full abstraction result. Types form a preordered structure whose lters are meant to be the elements of a domain, ordered by subset inclusion. Section 3 gives the type assignment system and proves its properties.

A Filter Model for Mobile Processes

5

In Section 4 we present an interpretation of terms as the lters of types that can be assigned to them in the type assignment system. This is the logical semantics of our calculus. We show, by means of a realizability interpretation and of test terms, that we can characterize the convergency properties of terms by means of the types which can be deduced for them. This implies the full abstraction of our semantics, i.e., that the inclusion between interpretations of terms coincides with the \may" observational preorder. Section 5 contains some further comparisons with related papers.

1. The language

In this section we introduce the -calculus without the \sum" operator. This choice was justi ed in the introduction and will be discussed further in Remark 10. The most primitive entity of -calculus is a name or channel. Names, ranged over by x, y, z , : : :, and a, b, : : : have no structure. The class of -calculus processes, ranged over by P , Q, R, M , N , : : :, is built from names and the null process 0 using the operators of pre xing, parallel composition, restriction, matching and replication, as follows. De nition 1. Let N be an in nite set of names. Processes are de ned by the following grammar M ::= 0 :M M jM x M x = y]M !M where is called pre x and can be either an input or an output : ::= x(y)

xy:

The symbol 0 denotes the inactive process. An input-pre xed process x(y):M waits for a name on the channel x and then behaves like the process M in which y is substituted by the name received. An output-pre xed process xy:M sends the names y on the channel x and then behaves like the process M . The matching x = y]M is used to test the equality of x and y. Such a process behaves like M when x is equal to y and it is inactive otherwise. The restriction construct x M declares x as a new name local to M . The parallel composition P jQ means that P and Q are concurrently active, so they can act independently and also communicate. The replication !M means M jM j , an arbitrary number of times. So there can be an arbitrary number of M executing concurrently. Free names of a term M , fn(M ), are de ned in the usual way, taking into account that, in both the input-pre xed process y(x):M and in the restriction x M , the name x is local to M , and bound in the whole term. In the following we shall be working modulo -conversion. We can assume that bound names are di erent from free names and from each other (this can always be achieved by -conversion). We say that a process M is mono if and only if fn(M ) contains at most one name. The substitution of x for y in P is denoted by P fx=yg, i.e., P fx=yg denotes the term obtained by replacing x to all the free occurrences of y in P . A suitable renaming of bound names is intended to avoid capturing the free name x. ? ! ??? ! We use a = b] to denote a sequence of matchings a1 = b1 ] am = bm ] (m 0), ?c

F. Damiani, M. Dezani-Ciancaglini and P. Giannini

to denote a sequence of restrictions c1 cn (n 0). Moreover x 62 a = b] is short for x 62 fa1 ; : : : ; am ; b1 ; : : : ; bmg, and x 62 ~ is short for x 62 fc1; : : : ; cn g. c A context is a term with a hole . Contexts will be denoted by C and C M is the term obtained by lling the hole with M . We adopt the following precedence among syntactic forms, in decreasing order: substitution precedes restriction, pre xing, matching, and replicator, that precede parallel composition. Now, following (Milner 1992) and (Sangiorgi 1992), we give the operational semantics of our calculus. We rst de ne the structural congruence between terms and then the reduction rules for terms. De nition 2. The structural congruence between terms, , is the smallest congruence that satis es: 1 P Q if P is -convertible to Q 2 Abelian monoid laws for j:

? ! ???

6

P j0 P P jQ QjP P j(QjR) (P jQ)jR 3 x0 0 x yP y xP x P jQ x (P jQ) if x 62 Q 4 x = x]P P !P P j!P .

We now give the reduction rules of the calculus. De nition 3. The reduction relation ?! is the smallest relation that satis es: COM : x(y):P jxz:Q ?! P fz=ygjQ PAR : RES :

P ?! P 0 P jQ ?! P 0 jQ

+ + We de ne ?! to be ?! , where ?! is the transitive closure of ?!. ?! Since is a congruence, if M ?! N , then there are Mi , 1 i n such that ?!

P ?! P 0 x P ?! x P 0 0 0 0 STRUCT : Q P P ?! P 0 P Q Q ?! Q

M M1 ?! M2 M3 ?!

?! Mn N:

The restriction operator models static binding on names. In fact, if two processes are willing to communicate, and one of them has a channel bound by , rst this binding is extended to both processes using the third congruence of De nition 2.3 and then the communication may be established (see also the discussion after De nition 4). The behaviour of processes that we analyze is their ability to o er input or output

A Filter Model for Mobile Processes

7

communications on a given channel. That is the \may" convergency (see (Hennessy 1988; Hennessy 1994a)). This convergency predicate tells whether there is a possible evolution of the process that leads to o er a communication on a given channel. De nition 4. The may convergency predicates are de ned by: | M +may if M ?! ?c (x(y):P jQ) for some ~, y, P , Q, where x 62 ~. ?! ! c c x may if M ?! ?c (xy:P jQ) for some ~, y , P , Q, where x 62 ~. | M +x ?! ! c c The previous de nition is motivated by the observation that the behaviour of a parallel composition is the sum of the behaviours of its components plus the possible interaction between them. So in considering the may convergency predicates we have to consider reductions to parallel processes one of whose components o ers the required communication. Moreover a process c x(y):N , where c 6= x, may o er an (input) communication on x. In fact if we consider a process that does an output on x, say xz:M , then ( c x(y):N )jxz:M with the third congruence of De nition 2.3 gives c (x(y):N jxz:M ) that causes the process to o er the input communication. So the presence of a possible restriction in the reduced term. We compare processes through open testing, i.e., a preorder based on the idea of considering processes under all possible substitutions on names. We call it open testing preorder since it is similar to open bisimulation (Sangiorgi 1996). In the present setting a testery is any process E which may use a new distinguished name w and such that every occurrence of w in E is in a subterm of the shape v wv:0. To test a process M means to put a substitution instance of M in parallel with a tester. We say that the test is successful if it o ers the output communication w. The condition above on the occurrences of w in E expresses the fact that the name w can only be used to report success. De nition 5. (Open testing preorder) Let M; N be processes. M vOT N if for every tester E , for every substitution on names s, may may s(M )jE +w implies s(N )jE +w : Two other standard operational preorders (see (Hennessy 1994a)) are de ned by means of contexts and testers. The rst is the observational preorder and it is based on the notion of distinguishing two terms if there is a context in which they behave di erently. De nition 6. (Observational preorder) Let M , N be processes. M vO N if for all contexts C , for all names c,

may C M +c implies C N +may : c

y Testers are usually called observers: we prefer testers to avoid confusion with the observational

preorder.

F. Damiani, M. Dezani-Ciancaglini and P. Giannini

8

C

Remark 7. In the de nition above we choose as behaviour of the terms the +may conc vergency. Choosing +may would be equivalent, in fact for all processes M , for all contexts c

, for all names c, we have that may | C M +c if and only if d ( c (C M jc(v):d(x):0)jdy:c(z ):0) +may , and c may | C M +may if and only if d ( c (C M jcv:d(x):0)jdy:cz:0) +c , c where d; v; x; y; z 62 fn(C M ). Proposition 8. M vO N implies M vOT N . Proof. For every substitution on names s we can consider its restriction to fn(M ) fn(N ), say s0 = fa1 =b1; : : : ; an =bng (n 1), and de ne a context Cs = d (d(b1 ): d(bn ): jda1 : dan :E ); where d is a fresh name. The context above when lled by M reduces to d(s(M )jE ): (Similarly for N ). The full abstraction result of Section 4 will show that the observational preorder and the open testing preorder are indeed the same preorder.

0

The second preorder is the testing preorder (see (Hennessy 1991), (Boreale and De Nicola 1995)). De nition 9. (Testing preorder) Let M; N be processes. M vT N if for every tester E,

may may M jE +w implies N jE +w : It is clear that if M vOT N then M vT N . The reverse implication does not hold

in general, but from the full abstraction result of Section 4 we have that it holds for a subset of which includes the set of mono terms and the set of terms that do not contain matchings, j and !. Remark 10. It is well know that the internal choice (the operator in (De Nicola and Hennessy 1987)) can be simulated in -calculus. In fact, it is easy to verify that the process M x (xy:P jxy:Qjx(z ):0) (where x 62 fn(P ) fn(Q)) and the internal choice between P and Q are strongly bisimilar. It is also easy to see that, w.r.t. \may" preorders like the one considered in this paper, the internal choice and both the external choices (the operator ] in (De Nicola and Hennessy 1987) and the operator + in (Milner 1980)) have an identical behaviour. These facts motivates our choice of process constructors.

2. The set of types

In this section we introduce the types and show some of their properties. In type assignment systems for polymorphic -calculus, types are properties of type free objects rather than domains in which objects live. This is common to many formalisms used in the theory of programming languages, and in particular to Hennessy-Milner logic

A Filter Model for Mobile Processes

9

for concurrency theory. In (Hennessy 1994a) a logic for processes that combines the functional arrow and an (implicit) intersection with indexed modalities is given. We present our process logic as a standard type assignment system in which intersection appears explicitly. Instead of modalities, we use types to represent the interaction capabilities of a process. Moreover, we have type constructors corresponding to the channel binder and to the matching over channels. De nition 11. The set T of types, ranged over by , and , is generated by the following grammar: ::= ! h i

o

x

x = y]

^

where h i is called pre x and can be either an input or an output: ::= x(y) xy: The type ! can be assigned to every process (it is the \true" constant). A type h i is the type of a process that may o er the corresponding communication. For example, hx(y)i can be assigned to a process that may o er an input communication on channel x and that, after the communication, becomes a process having type , in which the name received is substituted for y. Parallel composition of processes is represented by the type constructor o. Finally the ^ operator represents the logical \and" of formulas. So a process having type 1 ^ 2 behaves as a process having both the types 1 and x(y):yy:0 and 2 . Consider, for instance, the process M de ned by P jQ, where P Q xz:0. The process M has type o where is a type of P and a type of Q. The process P o ers the input communication hx(y)i, and Q the output communication hxz i. Moreover P and Q may communicate yielding a process that o ers the communication hzz i. So among the types we can assign to M we have hx(y)i!, hxz i!, and hzz i!. We can also have any intersection of such types. The intersection operator does not correspond to any syntactic construct of the process language. But, as we will see in Remark 33, it corresponds to the internal choice operator as de ned in (De Nicola and Hennessy 1987). In the following we will use hx z = (y)]i for hx(y)i z = y], and hx(y)i for yhxyi. We call hx z = (y)]i a matched input and hx(y)i a bounded output. will range over inputs, matched inputs, outputs and bounded outputs. Syntactic equality between types (modulo the above shortcuts) will be denoted by \=". Free and bound names of types are de ned as for processes; fn( ) will denote the set of free names occurring in . The substitution of x for y in is denoted by fx=yg. In writing types, we assume the convention that substitution precedes channel binder, pre xing, and matching, that precede parallel composition o, that precedes intersection. We note that there is a one-one correspondence between process constructors and type constructors with the exceptions of ! and ^. Types are related by a preorder which represents logical implication, if they are thought of as properties, or, equivalently, subset inclusion, if they are thought of as sets (the extensions of properties). Such a preorder induces an equivalence between types.

F. Damiani, M. Dezani-Ciancaglini and P. Giannini

10

Type inclusion is intended to model the behaviour of processes roughly in the following sense. Let , , and be the properties that characterize the processes M , P , and Q, respectively. If M is structurally congruent to P , then we assume that and are equivalent. Instead, if M in any context behaves either like P or like Q, we assume the equivalence of and ^ . Other type equivalences are postulated, since there are processes that cannot be distinguished by any context. For example, if x 6= y; z , then x y(z ):M and y(z ): x M never exhibit a di erent behaviour. So we assume the equivalence between the types x hy(z )i and hy(z )i x . The type inclusion relation , together with the induced equivalence relation ', is de ned as the least binary relation on T that satis es the axioms and rules presented in the following. Axioms are grouped according to their meanings, to facilitate their explanations. In the following axiom A2.3 will stand for the third axiom of the group A2, and similarly.

Structural equivalence axioms A1 ' if is -convertible to A2 Abelian monoid laws for o: o!' o ' o o( o )'( o )o A3 x y ' y x x o ' x ( o ) if x 62 fn( ) A4 x = x] ' .

The set of \structural equivalences" mirrors the congruence of terms, see De nition 2. Axiom A2.3 states the associativity of o: so we can omit parentheses in writing parallel compositions of types. Notably axiom x ! ' ! is missing, since it can be derived from the \may" inclusion axioms A11.

Behavioural equivalence axioms A5 x h i ' h i x if x 62 fn( ) x y = z ] ' y = z ] x if x = y and x 6= z 6 A6 x = y] ' y = x] x = y] a = b] ' a = b] x = y] x = y] y = z ] ' x = y] y = z ] x = z ] x = y] ' x = y] fx=yg x = y]( o ) ' x = y] o x = y] A7 x hx(y)i ' ! x hxyi ' ! x x = y] ' ! if x = y. 6

The previous equivalences establish properties that cannot be distinguished in any reasonable model of -calculus. Namely, equivalences in A5 re ect the fact that the binder can be moved in and out pre xes and matchings (as along as they do not mention the quanti ed name).

A Filter Model for Mobile Processes

11

The equivalences in A6 say that matchings induce an equivalence relation on names. Moreover, for the process P ' x = y]M , the matching x = y] can be considered a guard. Whenever the process P is in a context in which x is equal to y, it behaves like M . So, in this context, M behaves also as the process M 0 , where M 0 is obtained from M by substituting some of the x's by y's and vice versa. The axiom A6.4 mimics this behaviour. In a context in which x is di erent from y (for instance, they could be bound by two di erent restriction operators) P is the inactive process. Equivalences A7 say that communications on local channels (bound by ) cannot be o ered and also matchings with local names cannot be satis ed.

\May" equivalence axioms ??? ??? ??? ??? ??? ??? A8 ? =!]h 1i o ? = !]h 2i ' ? =!]h 1 i( o ? = !]h 2 i ) ^ ? = !]h 2i(? =!]h 1i o ) a b c d a b c d c d a b where either 1 is t1 z1 and 2 is t2 z2 ? ! ??? ? ! ??? or 1 is x1 (y1 ) and 2 is x2 (y2 ), y1 62 fn( c = d]h 2 i ) and y2 62 fn( a = b]h 1 i )

where 1 is x(y), 2 is tz and y 62 fn( c = d]h 2 i ). A9 ha(b)i x = y] ' ha(b)i! ^ x = y]ha(b)i if b 6= x and b 6= y habi x = y] ' habi! ^ x = y]habi

)z

? =!]h i o ? = !]h i ' ??? ??? a b 1 c d 2 ? =!]h i( o ? = !]h i ) ^ ? = !]h i(? =!]h i o ) ^ ? =!]? = !] x = t]( fz=yg o ??? ??? ??? ??? ??? ??? a b 1 c d 2 c d 2 a b 1 a b c d

? ! ???

The \may equivalences" characterize the behaviour of parallel processes (note the similarity between the axioms A8 and the expansion law in (Milner et al. 1992)). Consider for instance the equivalence A8.2. As already mentioned, this says that the behaviour of a parallel process is the \and" of the behaviours of the individual processes and the result of their interaction (when the interaction is possible). Interaction is possible when we have a process o ering a communication and a process expecting one. The fact that the input and output channels have to be the same is forced by the use of the matching operator. We can see also that the equivalence is given for types preceded by matchings. This is because matchings cannot be moved in or out of pre xes. Without matchings in the left-hand side, the equivalence A8.2 rewrites as hx(y)i o htz i ' hx(y)i( o htz i ) ^ htz i(hx(y)i o ) ^ x = t]( fz=yg o ): There are also equivalences characterizing the logical operator ^. For a process M to have property ^ means that M has both property and property . As already said, ^ corresponds to the internal choice. The meaning of the equivalence A9.1 is that

z Here and in the following we avoid parentheses since, as proved in Remark 12, ^ is associative.

A10 ' ^ h i( ^ ) ' h i ^ h i o( ^ )' o ^ o x( ^ ) ' x ^ x x = y]( ^ ) ' x = y] ^ x = y] :

F. Damiani, M. Dezani-Ciancaglini and P. Giannini

12

a(b): x = y]M certainly o ers the input communication on a, so it has property ha(b)i!. Moreover, if x is equal to y, it o ers the input communication on a followed by M , so it has type x = y]ha(b)i , if characterizes a property of M . So it behaves like the internal choice between the processes a(b):0 and x = y]a(b):M . The equivalence A9.2

can be explained similarly. The equivalences in A10 say that ^ is idempotent and it distributes over restrictions, matchings, pre xes and parallel compositions.

\May" inclusion axioms A11 ! fy=xg x

. The axioms for inclusion tell us when a process behaves better than another in a \may" perspective. First every process o ers more communications than the one that o ers none. The second axiom means that restricting a process by produces a process that o ers less communications. The reason for having fy=xg instead of is that this is true also when the captures only some of the occurrences of y. For example hyyi! xhyxi! by choosing to be hyxi!. Also restricting a process by a matching produces a worse process (third axiom). We also have the basic logical property of ^. Note that from these inclusions we immediately derive ! ' x! ' x = y]!.

^ ^

x = y]

Rules R1

and imply . The rules extend inclusions (and so also equivalences) to the various syntactic forms. Remark 12. We can prove that ^ is associative, i.e., ^ ( ^ ) ' ( ^ ) ^ . We rst show that ^ ( ^ ) ( ^ ) ^ . 1 ^( ^ ) using A11.4, 2 ^ ( ^ ) ^ from A11.4, and ^ again from A11.4, and ^ using A11.5. Therefore from rule R2 we have (a) ^ ( ^ ) , and (b) ^ ( ^ ) . 3 From Points 1, and 2a, we derive that ^ ( ^ ) ^ , using A10.1 and R1.5. Finally from this, and 2b, again using A10.1 and R1.5, we get ^ ( ^ ) ( ^ ) ^ . The other inclusion ( ^ ) ^ ^ ( ^ ) can be proved in a similar way. It is not di cult (but quite cumbersome) to verify that is a decidable relation. We do not do this, since it is not relevant for our development.

R2

0 implies h i h i0 0 implies x x 0 0 implies x = y] x = y] 0 0 and 0 imply o 0o 0 0 and 0 imply ^ 0^ 0

A Filter Model for Mobile Processes

13

It is easy to see that is a precongruence and that ' is a congruence over types. Moreover implies that fy=xg fy=xg. Due to axioms A8 we have that any equivalence class of ' contains a type in which the parallel composition o does not occur. Indeed the behaviour of a parallel process can be given in terms of the intersection of the behaviours of its components. Moreover the axioms A10 say that the ^ operator can always be pulled out of the various syntactic forms, i.e., any type is equivalent to an intersection of types which do not contain any occurrence of o and ^. Looking at the axioms A7 we can see that subtypes of types can be replaced by ! when they correspond to behaviours not o ering any communication. Moreover axioms A4 and A6 allow us to erase super uous matchings and to choose a representative for each induced equivalence class of names. So types can be shortened obtaining equivalent types. The fourth axiom of A6 allows us to have types in which the names occurring on the right of = in a matching do not occur anywhere else. Lastly the axioms A5 allow us to move the binder in and out pre xes and matchings that do not involve the bound variable. These considerations lead us to formulate the notions of bodies and normal types. 1 A normal sequence of matchings is inductively de ned by: | the empty sequence of matchings is normal, ? ! ??? ? ! ??? | x = y] a = b] is a normal sequence of matchings, if and only if a = b] is normal, ? ! ??? x 6= y, y 62 a = b], and x 62 ~. b 2 The set of bodies B is inductively de ned by: | !2B | hx(y)i ; hxyi 2 B if 2 B | hx z = (y)]i 2 B if z 6= y, 2 B and y 62 fn( ) | hx(y)i 2 B if x 6= y and 2 B 3 A type is normal if and only if | either = !, ? ! ??? ? ! ??? | or = a = b] , where a = b] is a normal sequence of matchings, 6= ! is a body, and ~ 62 fn( ). b ? ! ??? A sequence of matchings induces an equivalence relation on names: E ( a = b]) will ? ! ??? denote the equivalence relation induced by a = b]. A normal sequence is a standard representation of an equivalence relation. Notice that a normal sequence is always a minimal representation of an equivalence relation, in the sense that it contains a minimal number of matchings. When the matching x = y] belongs to a normal sequence we say that x is the representative of the equivalence class of y.

De nition 13. (Normal types)

Proposition 14. ? ! ? ! ??? ??? ? ! ??? 1 Let a = b] and x = y] be sequences of matchings, and let be a type. E ( a = b]) = ??? ??? ??? E (? = !]) implies ? =!] ' ? = !] . x y a b x y

F. Damiani, M. Dezani-Ciancaglini and P. Giannini

2 If x = y] is a sequence of matchings, then there is a normal sequence a = b] such ? ! ??? ? ! ??? that E ( x = y]) = E ( a = b]). Proof. ? ! ??? ? ! ??? ? ! ??? 1 Observe that E ( a = b]) = E ( x = y]) and z = t] 2 x = y] imply that there are c0 ; : : : ; cn (n 1) such that: | c0 = z ; ? ! ??? | ci = ci+1 ] or ci+1 = ci ] 2 a = b]; | cn = t. ? ! ? !? ! ??? ??? ??? Therefore we get a = b] ' a = b] x = y] using the rst three equivalences in A6. ? ! ? !? ! ??? ??? ??? ? !? ! ??? ??? Symmetrically we get x = y] ' x = y] a = b] . Lastly by A6.2 we get a = b] x = y] ' ? = !]? =!] . Therefore, by transitivity of ' (rule R2), ? =!] ' ? = !] . ??? ??? ??? ??? x y a b a b x y ? ! ? ! ??? ??? ? ! ??? 2 By structural induction on x = y]. If x = y] = z = t] u = v] then by induction there ? ! ??? ? ! ??? ? ! ??? is a normal sequence of matchings c = d] such that E ( u = v]) = E ( c = d]). Now ? ! ??? if z = t 2 E ( u = v]) (in particular we can have z identical to t) then we choose ? =!] = ? = !]. Otherwise if z 62 d and t 62 ? = !] then we choose ? =!] = z = ??? ??? ??? ??? ~ a b c d c d a b ? ! ??? ~ t] c = d]. If z; t 2 d, let e; f be the representative of the corresponding equivalence ? = !]) implies e 6= f . We choose ? =!] = e = f ](? = !]fe=f g). ??? ??? ??? classes. z = t 62 E ( u v a b c d ? ! ??? ? ! ??? ~ If z; t 2 ~, we choose a = b] = z = t]( c = d]fz=tg). If z 2 ~ and t 2 d we choose c c ? =!] = z = e](? = !]fz=eg), where e is the representative of the equivalence class ???b ???d a c of t. The remaining cases have z and t interchanged, so we can do similar choices. Observe that normal types represent traces of communications that may be o ered by a process, namely a match speci es a condition on names, i.e., on the context in which the process is embedded, necessary for the process to satisfy the speci cation that follows the match. A pre x speci es when the corresponding communication may be o ered. Moreover a pre x hx(y)i speci es that a new name is created, and a pre x hx z = (y)]i speci es a condition on the received name necessary for the process to satisfy the specication that follows the pre x. The results that follow will show that every type can be expressed as an intersection of normal types. This is consistent with the intuition that the behaviour of a process is determined by all the possible traces of communications that it may o er. Note that, in spite of this, our semantics is not a trace semantics, since we compare types by means of an inclusion relation which takes into account the behaviour of processes in contexts. In the following we give a de nition of substitutions (normal substitutions) and bindings (normal bindings) mapping normal types into normal types. Note that, if is a body, then fx=yg is a body, but normal does not imply fx=yg normal. For example, if is x = y]h i!, then fx=yg = x = x]h i! which is not normal. Moreover x is

? ! ???

? ! ???

14

A Filter Model for Mobile Processes

15

not in general normal also when is a body. In order to de ne normal substitutions we need to force a given name, say x, to be the representative of the equivalence class (of the equivalence relation) induced by a sequence of matchings. This is done by the following mapping rep(x; ). ? ! ??? ? ! ??? Let a = b] ? x = y] denote the sequence of matchings obtained from a = b] by erasing x = y], if it occurs. ??? De nition 15. Let = ? =!] be a normal type, where is a body. a b 1 ( ? ! ??? ? ! ??? rep(x; ) = x = c](( a = b] ? c = x]) )fx=cg if c = x] 2 a = b] otherwise. 2 To de ne the normal substitution of x for y in , rst let us de ne fx=ygR. In the de nition of fx=ygR we assume that both x and y are the representative of their equivalence classes in , if their equivalence classes are di erent, otherwise x is the representative of the common equivalence class. fx=ygR is inductively de ned as follows: | fx=ygR = fx=yg, | ( x = y] 0 )fx=ygR = 0 , | ( z = a] 0 )fx=ygR = x = a]( 0 fx=ygR), for z = x or z = y, and a 6= x; y, | ( a = b] 0 )fx=ygR = a = b]( 0 fx=ygR), for a 6= x; y and b 6= x; y. Now de ne the normal substitution of x for y in , fx=ygN, to be (rep(x; rep(y; )))fx=ygR . 3 The normal binding of x in , N x , is inductively de ned as follows: | N x ! = !, | N x h i = h i N x , for x 62 fn( ), | N x h i = !, for 2 fx(y); xy; x z = (y)]; x(y)g, | N x hyxi = hy(x)i , for x 6= y, | N x hy x = (z )]i8 = hy(z )i!, for x 6= y, ? ! ??? ? ! < ??? for x 2 a = b] or N x = ! | N x a = b] = : !??? ? =!] N x otherwise: a b The de nition of normal substitution is justi ed by observing that, in rep(x; rep(y; )), both x and y are the representative of their equivalence classes in , if x and y are in di erent equivalence classes, and x is the representative, when they both belong to the same class. Normal substitutions and normal bindings behave respectively like standard substitutions and standard bindings modulo type equivalence. De nition 15 allows us to state some equivalences between types and intersections of normal types which can be shown easily and will be useful in the following. ??? Lemma 16. Let = ? =!] be normal, where is a body. Then the following equivaa b lences hold and each right-hand side is an intersection of normal types whose free names

F. Damiani, M. Dezani-Ciancaglini and P. Giannini

16

are a subset of the free names of the corresponding left-hand side. 1 2

We can now prove that every type can be expressed as a nite intersection of normal types. Proposition 17. For every type there is n 1 and there are n normal types 1 ; : : : ; n such that ' 1 ^ ^ n and fn( ) fn( 1 ^ ^ n ): Proof. By induction on . All the cases except for o are by induction hypothesis and Lemma 16. 0 0 For o, let be o 0 . By the induction hypothesis ' 1 ^ ^ m , and 0 ' 1 ^ ^ n , 0 ; ; n are normal types. Then 0 where 1 ; ; m ; 1

' rep(x; ). fx=yg ' 8 x=ygN. f ? ! ??? ??? < hx(y)i! ^ ? =!]hxf~ =~g(y)i a b ab if y 62 a = b] 3 hx(y)i ' : ??? ??? hx(y)i! ^ ? = !]hxf~=dg z = (y)]i( fz=yg) if z = y] or y = z ] 2 ? =!] c d c ~ a b ? ! ? ! ??? ??? where c = d] = ( a = b] ? z = y] ? y = z ])fz=yg. ? ! ??? 4 hxyi ' hxyi! ^ a = b]hxyif~ =~g . ab N x( . 5 x ' ! if = ! 6 x = y] ' N ) otherwise: x = y]( fx=yg ? ! ??? ? ! ??? ? ! ??? Proof. We only show Point 3. If y 62 a = b], then hx(y)i a = b] ' hx(y)i!^ a = b]hx(y)i ? ! ??? ? ! ??? by repeated applications of axiom A9.1. Moreover a = b]hx(y)i ' a = b](hx(y)i f~ =~g) ab ? =!]hxf~ =~g(y)i , since by de nition of normal ???b a b by axiom A6.4, and hx(y)i f~ =~g = a ab type ~ 62 fn( ). b ? ! ? ! ? ! ??? ??? ??? ? ! ??? If z = y] 2 a = b], let c = d] = a = b]? z = y]. By A6.2 and A9.1 we get hx(y)i a = b] ' ??? hx(y)i! ^ ? = !]hx(y)i z = y] . By notational convention hx(y)i z = y] = hx z = (y)]i , c d ? ! ??? ? ! c~ ??? so we conclude as in previous case c = d]hx z = (y)]i ' c = d]hxf~=dg z = (y)]i , since ? ! ??? ~ d; y 62 fn( ). Notice that in this case y 62 c = d]. ? ! ??? ? ! ??? ? ! ??? If y = z ] 2 a = b], Proposition 14.1 and axiom A6.4 imply hx(y)i a = b] ' hx(y)i(( a = b]? ? ! ??? y = z ])fz=yg) z = y]( fz=yg), and therefore as in previous cases hx(y)i(( a = b] ? y = ? ! c~ ??? ? ! ? ! ??? ??? z ])fz=yg) z = y]( fz=yg) ' c = d]hxf~=dg z = (y)]i( fz=yg), where c = d] = ( a = b] ? y = z ])fz=yg .

o 0'

^

So we have to show that, for all normal types and 0 , o 0 is equivalent to an intersection of normal types. The proof is by induction on the number of pre xes in and 0 . If either ' ! or 0 ' ! the result is obvious. Otherwise we consider the most

1 i m;1 j n

0 i o j:

A Filter Model for Mobile Processes

di cult case = a = b]hx(y)i and 0 = c = d]hv (t)i . We have: ??? ??? ??? ??? a b c d a b c d o ' ? =!]hx(y)i( o ) ^ ? = !]hv(t)i( o ) ^ ? =!]? = !] x = v] t ( ft=yg o ): As already noticed, ft=yg is a body, and therefore it is also a normal type. So applying the induction hypothesis to the three parallel compositions ( o 0 , o , and ft=yg o ), the equivalences A10 (that pull out the ^ operator) and Lemma 16 (to add the matchings and the restrictions) we get the result. Remark 18. Looking at the previous proposition a natural question arises. Why did not we consider only normal types? This is, as it will be clear from the following section, because the de nition of the type assignment system and the proofs of its properties would be much more di cult when restricted to normal types. In the remaining of the present section we will relate the preorder on types with the decomposition in normal types (Theorem 24). To this aim it is useful to characterize in a structural way the inclusion relation between normal types.

0 0

? ! ???

? ! ???

17

De nition 19. (Inclusion relation for normal types)

1 The normal inclusion relation, N , between normal types is inductively de ned by: | N! | N , if is -convertible to | hx(y)i N hx z = (y)]i fz=yg, for z 6= y | hxz i fz=yg N hx(y)i , for y 6= x | ; 2 B and N imply { hx(y)i N hx(y)i { hxyi N hxyi { hx y = (z )]i fz=yg N hx y = (z )]i fz=yg, for z 6= y { hx(y)i N hx(y)i , for y 6= x | N x = y] fx=ygN | N imply x = y] fx=ygN N x = y] fx=ygN | 1 N 2 , and 2 N 3 imply 1 N 3 . 2 'N is the equivalence relation induced by N . From the previous de nition it follows that two 'N equivalent normal types can only di er for -conversion, the order of the initial matchings and the choice of the representative of the equivalence classes in the initial sequences of matchings. To relate the type inclusion, , and the normal type inclusion, N , between normal types, we de ne for any normal type a context ? ;w , where w is a fresh name, that discriminates types less than or equal to . First we associate to any body a test body = ;w which o ers the communications \complementary" to those o ered by . Then if ? ! ??? ? ! ??? rst satis es the matchings a = b] and then puts the = a = b] , the context ? ;w hole in parallel with = ;w .

De nition 20.

F. Damiani, M. Dezani-Ciancaglini and P. Giannini

18

1 Let be a body, and w 62 fn( ). The test body = ;w for is de ned by induction on . | =!;w = hw(v)i! | =hx(y)i ;w = hx(y)i= ;w | =hx z=(y)]i ;w = hxz i= ;w | =hxyi ;w = hx y = (z )]i= ;w | =hx(y)i ;w = hx(y)i= ;w : ? ! ??? 2 Let = a = b] and w 62 fn( ). De ne ? ;w as d (hd(b1 )i hd(bn )i o hda1 i hdan i= ;w ) where d 6= w and d 62 fn( ). ??? Lemma 21. Let = ? =!] and be normal types, ~ fn( ) fn( ) and w 62 ~. a b c c ?c ? ;w 6' ! implies N , and ! 1 ! hw(v)i!. 2 implies ?c ? ;w Proof. 1 By induction on . If = !, then ' !, so it is trivial. Let 6= !. Note that axioms A8.2, A7.1, and A7.2 imply ! ?c ? ;w ' ?c d( f~ =~g o = ;w ): ! ab () ! ab First observe that ?c ? ;w 6' ! implies that f~ =~g is a body. This is because if 0 and = ;w = h i 0 , then f~ =~g = e = f ] ab ! ?c ? ;w ! ' ?c d( e = f ] 0 o h i 0 ) by ( ) ?c d e = f ] 1 ^ ?c dh i 2 for some 1 and 2 by axioms A8 ! ! ' '! by axioms A7 since e, f , and the free names in are all included in ~. c Let = hx(y)i , then = ;w = hx(y)i= ;w and ! ?c ? ;w ' ?c d( f~ =~g o hx(y)i= ;w ) by ( ): ! ab ! ab For ?c ? ;w 6' ! it must be that f~ =~g = hx(z )i for some such that ! ! ?c ? ;w ' ?c d( fy=z g o = ;w ) = ?c ? ;w fy=z g 6' !: ! By the induction hypothesis fy=z g N . So f~ =~g = hx(z )i 'N hx(y)i fy=z g N hx(y)i = using De nition 19. Since ab ??? ??? N ? =!] f~ =~g, then N ? =!] by the same de nition. a b ab a b ! Let = hx z = (y)]i , then = ;w = hxz i= ;w . For ?c ? ;w 6' ! it must be that either f~ =~g = hx(t)i or f~ =~g = hx z = (t)]i for some . In both cases ab ab f~ =~g N hx z = (t)]i and ab ?c ? ;w ' ?c d( fz=tg o = ;w ) = ?c ? ;w fz=tg 6' !: ! ! !

A Filter Model for Mobile Processes

19

By the induction hypothesis fz=tg N . So hx z = (t)]i fz=tg N hx z = (y)]i (since y 62 fn( ) by de nition of normal type). As for the previous case we can now ? ! ??? deduce that N a = b] . ! 6' ! it must be that Let = hxyi , = ;w = hx y = (z )]i= ;w . For ?c ? ;w f~ =~g = hxyi for some . Indeed if f~ =~g were hxti , or hx(t)i , then the matching ab ab y = z ] in = ;w after the communication would become y = t] with t bound by an ! external , and therefore ?c ? ;w would be !. So we have that

derive the result. 2 Let , then since

! ! ' ?c d( o = ;w ) = ?c ? ;w 6' !: By the induction hypothesis N . So hxyi N hxyi and, as for the previous cases, ? ! ??? we can conclude that N a = b] . ! Let = hx(y)i , = ;w = hx(y)i= ;w . For ?c ? ;w 6' ! it must be that either f~ =~g = hxz i or f~ =~g = hx(z )i for some . In both cases ab ab ! ! ?c ? ;w ' ?c z x d( o = ;w fz=yg) = ?c z ? fz=yg;w 6' !; ! since = ;w fz=yg = = fz=yg;w . By the induction hypothesis we derive N fz=yg. If f~ =~g = hx(z )i observe that hx(z )i N hx(z )i fz=yg. Since hx(z )i fz=yg is ab convertible to under the condition z 62 fn( ), we can derive the result. If f~ =~g = hxz i observe that hxz i N hxz i fz=yg N hx(y)i = and we can ab ?c ? !

;w

! ! ab Moreover ?c ? ;w ' ?c d( o = ;w ) by ( ), since f~ =~g = . It is easy to see that ! ! hw(v)i!. hw(v)i! and therefore ?c ? ;w o = ;w hw(v)i!. So ?c ? ;w

From the previous lemma we get the coincidence of and N on normal types. Corollary 22. Let and be normal types. if and only if N . Proof. The (if) implication is by induction on the de nition of N and the (only if) implication follows directly from Lemma 21. De ne to be a prime type if and only if for all and 0 , if ^ 0 then either 0 , or . The following theorem shows that the set of normal types coincides with the set of prime types (modulo equivalence).

is a precongruence, we have that ?c ? ;w : ! ?c ? ;w !

Theorem 23.

1 Any normal type is prime. 2 Any prime type is equivalent to a normal type. Proof.

x If f~ =~ g = hxzi we get z 2 ~, so this binding is super uous. a b c

F. Damiani, M. Dezani-Ciancaglini and P. Giannini

20

1 Let be a normal type, and and 0 be types. By Proposition 17, ' 1 ^ ^ m 0 0 0 0 andV 0 ' 1 ^ ^V n , where 1 ; ; m ; 1 ; ; n are normal types. Let ~ = c 0 ) fn( ). Assume that ^ 0 06 . , 6 and fn( 1 i m i ) fn( 1 j n j N , and for all j (1 j n) j 6 N . This, by 0 Then for all i (1 i m) i 6 ?c ? ;w i ' !, and for all j , 1 j ! Lemma 21.1, implies that for all i (1 i m) V V ! ! ! n, ?c ? ;w j0 ' !. Therefore 1 i m ?c ? ;w i ^ 1 j n ?c ? ;w j0 ' !. This is V V ! ! 0 a contradiction since ^ 0 implies 1 i m ?c ? ;w i ^ 1 j n ?c ? ;w j ' ?c ? ;w ^ 0 ?c ? ;w , and ?c ? ;w 6' !. ! ! ! 2 Let be a prime type. By Proposition 17, ' 1 ^ ^ m where 1 ; ; m are normal types. The primality of implies that i for some i (1 i m). Moreover since ' 1 ^ ^ m j for all j , 1 j m, also i . Therefore ' i . Now we can prove the key relations between subtyping and normal subtyping. Theorem 24. Let ' 1 ^ ^ m and ' 1 ^ ^ n, where 1; ; m; 1 ; ; n are normal types. if and only if for all i (1 i n) there is j (1 j m) such that j N i . Proof. The (if) implication is obvious. For the (only if ) let 1 ^ ^ m 1 ^ ^ n . Then given any i (1 i n), we have that 1 ^ ^ m i . By Theorem 23.1 for N i. some j (1 j m), j We say that types 1 ; : : : ; n are incomparable if for no i 6= j (1 i; j n), i j . Corollary 25. The decomposition of a type as an intersection of incomparable normal types is unique modulo 'N . Proof. Let 1 ^ ^ m and 1 ^ ^ n be two intersections of incomparable, normal types. From Theorem 24 we have that: 1 ^ ^ n ' 1 ^ ^ m implies m = n and for all i (1 i m) there is j (1 j m) such that i 'N j .

3. The type assignment system

In this section we de ne the type assignment system characterizing the -calculus, and we prove the property of subject expansion.

De nition 26. (The type assignment system)

(!) P : !

P (h i I) x(y):P ::hx(y)i (o Ij ) PP :jQ : Qo : P ( I) x P :: x

( ) P:P: P (h i I) xy:P ::hxyi (o I! ) P !:P : !P : o P: ( ]I) x = y]P : x = y]

A Filter Model for Mobile Processes

21

We write ` P : if the statement P : can be derived from the axioms and rules of De nition 26. We call deductions in which the rule ( ) is not used -free deductions, and with `? we denote derivation in the system without the rule ( ). As we can see, the system has only introduction rules for the various constructors. Elimination of pre xes and parallel composition is done using the inclusion rule ( ). Such a rule acts also as an ^ introduction and elimination (cf. Proposition 37). Example 27. The two main features of -calculus are the mobility, that is the ability of passing channel names, and the creation of names. As an example of name creation consider: M ! a ba:0. The process M can generate in nite new names. To M we can assign all the normal types hb(a1 )i hb(an )i! for any n 0. Clearly these types express the property of giving as outputs on channel b a nite but unbounded number of local names. The axioms and rules for type inclusion A11 and R1 allow us to postpone the use of the rule ( ) till the end of deductions. Therefore every deduction can be transformed into a deduction in which the rule ( ) is used exactly once and it is the last applied rule.

Proposition 28. ( -free deduction property) 1 ` P : imply `? P : for some . 2 `? P : implies fn( ) fn(P ).

Proof. Both points can be proved by induction on deductions. For 1, if the last rule applied is (h i I), then we have Q (h i I) x(y):Q ::hx(y)i : By the induction hypothesis `? Q : 0 for some 0 . So by (h i I) we get `? x(y):Q : hx(y)i 0 , where hx(y)i 0 hx(y)i . The other cases are similar. The proof of 2 is immediate. If P is a process that does not contain !, it is easy to de ne its principal type, i.e., a type }(P ) such that ` P : }(P ) and for all types , ` P : implies }(P ) . Really, P admits a unique -free deduction which derives its principal type. De nition 29. (Principal type) Let P be a process not containing !. We de ne }(P ) by structural induction: }(0) = ! }( :M ) = h i}(M ) }(M jN ) = }(M ) o }(N ) }( xM ) = x}(M ) }( x = y]M ) = x = y]}(M ): Proposition 30. (Principal type property) Let P be a process not containing !. Then

F. Damiani, M. Dezani-Ciancaglini and P. Giannini

22

1 `? P : }(P ), and 2 ` P : implies }(P ) . Proof. 1 By structural induction on P . 2 From Proposition 28 `? P : for some deduction of `? P : .

. The proof is by induction on the

Remark 31. From the principal type property, and the decidability of (see Remark 12)

we get the decidability of our type assignment system for processes without occurrences of !. Of course this does not holds for the whole set of processes. The given type assignment system has the obvious structural properties which can be shown by simple induction on derivations.

Lemma 32. (Structural properties of deductions) 1 ` 0 : if and only if ! ' , 2 ` x(y):P : if and only if for some , `? P : and hx(y)i , 3 ` xy:P : if and only if for some , `? P : and hxyi , 4 ` P jQ : if and only if for some , , `? P : , `? Q : and o , 5 ` x P : if and only if for some , `? P : and x , 6 ` x = y]P : if and only if for some , `? P : and x = y] , 7 ` !P : if and only if for some 1 ; : : : ; n (n 1), `? P : 1 , : : :, `? P : o n . 1o

n and

Proof. All cases follow easily from Proposition 28.1. The most interesting one is Point 7. Let ` !P : . By Proposition 28.1, `? !P : for some . Let m be the number of applications of rule (o I! ), with !P as subject of the conclusion, that occur at the end of a -free deduction of !P : . We prove, by induction on m, that is of the form 1 o o m o ! and `? P : 1 , : : :, `? P : m . The case m = 0 is trivial, in fact in this case we can use only rule (!). If m 1, then is of the form 1 o for some 1 ; such that `? P : 1 and there is a -free deduction of !P : that has exactly m ? 1 applications of rule (o I!) at the end. By induction hypothesis is of the form 2 o o m o ! and `? P : 2 ; : : : ; `? P : m . Lemma 32 says that the types of a term can be obtained in a uniform way from the types of its subterms, and this will guarantee the compositionality of the lter model we will build in the next section. Remark 33. As noticed at the beginning of Section 2, the intersection operator corresponds to the internal choice operator (see Remark 10). In fact if M x (xy:P jxy:Qjx(z ):0) (where x 62 fn(P ) fn(Q)) it is straightforward to verify using Lemma 32 that M has type if and only if ' ^ , where is a type of P and is a type of Q. The crucial observation is that whenever 0 ^ 0 we can nd ; such that 0 , 0 , and ^ ' . This can be easily proved by taking the prime decomposition of ; ; and by using Theorem 24. We state now some properties of deductions which will be useful in the following.

A Filter Model for Mobile Processes

23

Lemma 34. 1 ` P : implies ` P fy=xg : fy=xg. 2 `? P fy=xg : implies that is of the form fy=xg, for some such that `? P : . 3 ` P fy=xg : fy=xg implies ` P : x = y] .

Since we are in a \may" perspective, it is natural that a process P o er all the communications o ered by one of its reducts Q (may be more). At the type assignment level this means that types are preserved under subject expansion. Of course subject reduction should not hold, since reducing P with the rule COM may produce a process that o ers less communications (so with less types). Lemma 35. (Subject congruence) ` P : and P Q imply ` Q : . Proof. By cases on the de nition of (De nition 2), using Lemma 32. The only interesting case is the third axiom of A3. In one direction we have to show that ` x P jQ : implies ` x (P jQ) : under the condition x 62 fn(Q). By Lemma 32, we have `? P : , `? Q : and x o . By (o Ij ) and ( I) we get ` x (P jQ) : x ( o ). Now by Lemma 28.2 x 62 fn( ), which implies (by axiom A3.2) x ( o ) ' x o . So by rule ( ) we conclude ` x (P jQ) : . Similarly we can prove that ` x (P jQ) : implies ` x P jQ : . Theorem 36. (Subject expansion) ` P : and Q?! P imply ` Q : . ?! + + Proof. Remember that by de nition ?! = ?! ?! , where ?! is the transitive closure of ?!. + If Q P , then the results follows by Lemma 35. If Q ?! P , then the proof is by induction on the length of the expansion sequence. The only non trivial case is rule COM. Let x(y):M jxz:N ?! M fz=ygjN . By Lemma 32.4 there are 0 ; such that `? M fz=yg : 0 , `? N : and 0 o . By Lemma 34.2, 0 can be written as fz=yg where is such that `? M : . From `? M : , by (h i I), we get `? x(y):M : hx(y)i , and from `? N : , by (h i I), we get xz:N : hxz i . Then by (o Ij ) we deduce `? x(y):M jxz:N : hx(y)i o hxz i . Finally by ( ), observing that hx(y)i o hxz i fz=yg o by axioms A8.2 and A11.3, we conclude `? x(y):M jxz:N : . It is interesting to notice that the standard rule of intersection introduction is admissible in our system. Proposition 37. For the type assignment system of De nition 26, the rule : P (^I) P P : ^ : is an admissible rule. Proof. We prove that ` P : and ` P : imply ` P : ^ by induction on the structure of P .

`? P fy=xg : with fy=xg by Proposition 28.1. By Point 2 this implies that is of the form fy=xg, for some such that `? P : . Now x = y] ' x = y]( fy=xg) x = y]( fy=xg) ' x = y] by axioms A11.3, A6.4, and rule R1.3, so we conclude ` P : x = y] .

Proof. Points 1 and 2 can be shown by induction on deductions. For Point 3, we have

F. Damiani, M. Dezani-Ciancaglini and P. Giannini

24

Let P be x(y):Q. By Lemma 32.2 there are 0 ; 0 such that ` Q : 0 , ` Q : 0 and hx(y)i 0 , hx(y)i 0 . By induction ` Q : 0 ^ 0 , which implies ` x(y):Q : hx(y)i( 0 ^ 0 ) by rule (h i I). By axiom A10.2 and rule R1.5 we have hx(y)i( 0 ^ 0 ) ' hx(y)i 0 ^ hx(y)i 0 ^ . Let P be !Q. By Lemma 32.7 there are 1 ; : : : ; m such that ` Q : i (1 i m) and 1 o o m . Again by Lemma 32.7 there are 1 ; : : : ; n such that ` Q : j (1 j n) and 1 o o n . By induction ` Q : i ^ j (1 i m; 1 j n), which imply ` !Q : o1 i m; 1 j n ( i ^ j ) by rule (o I! ). Using axioms A10.3, A11.4, and A2.3 it is easy to check that o1 i m; 1 j n ( i ^ j ) ( 1 o o m ) ^ ( 1 o o n ). So we can conclude ` !Q : ^ by ( ). All other cases are similar to the case of the input pre x. We end this section by introducing a subclass of processes which are characterized by bodies. Lemma 39 shows that this class contains interesting processes, in particular all mono processes. Remember that, by de nition, a process P is mono if and only if it contains at most one free name. De nition 38. (Body processes) We say that a process P is a body process if `? P : implies ' 1 ^ ^ n (n 1), where 1 ; ; n are bodies.

Lemma 39.

1 Every process that does not contain matchings, parallel compositions, and replications is a body process. 2 Every mono process is a body process. Proof. 1 Let P be a process that does not contain matchings, parallel compositions, and replications. Assume that `? P : , it is easy to show by induction on the deduction that is a body. 2 Let P be a mono process. Assume that `? P : , then by Proposition 28.2, fn( ) contains at most one name. By Proposition 17 ' 1 ^ ^ m and fn( ) fn( 1 ^ ^ m ) where 1 ; ; m are normal types. But a normal type with at most one free name is a body and therefore each i is a body.

4. The lter model

In this section we rst introduce the lter model for the -calculus de ned in Section 1 and then we prove its adequacy and full abstraction with respect to the operational semantics. Let hD; vi be a preorder. A subset L of D is a lter if L is a non-empty upper set, i.e., l 2 L and l v l0 imply l0 2 L, and every nite subset of L has a lower bound in L. Consider the set T of types with the inclusion de ned in Section 2. The lower bound of a nite non-empty set of types is the intersection of the types in the set. We can observe that the set F (T ) of lters over T is a model of in the following sense. For all M de ne M ]] = f 2 T ` M : g:

A Filter Model for Mobile Processes

25

From rules (!); ( ) and the admissibility of (^I) we have that M ]] 2 F (T ) for all M . Subject expansion can now be rephrased into the following statement: if M ?! N then M ]] N ]]: ?! The lter model is naturally ordered by subset inclusion. The inclusion on lters induces an ordering on terms. De nition 40. Let M; N 2 . M vF N if and only if M ]] N ]]. The order relation vF can be easily characterized by means of the deducibility of types as follows. Proposition 41. Let M; N 2 . M vF N if and only if, for all , ` M : implies `N : . We will prove that the lter model exactly mirrors the operational semantics, i.e., that it is adequate and fully abstract. The adequacy proof requires a double induction on types and deductions. Following a standard methodology, we split this induction by introducing a realizability interpretation of types as sets of terms. The underlying idea is that a term M belongs to the interpretation of a type if and only if can be derived for M . First we give an interpretation of normal types, and then we build the interpretation of all types, taking into account Theorem 24 and Corollary 25. The interpretation of normal types is given by structural induction. De nition 42. If is a normal type, the realizability of is de ned by: !]] = hx(y)i ]] = fM 2 M ?! ?c (x(y):P jQ) for some P; Q;~ such that ?! ! c ?c (P jQ) 2 ]] and x 62 ~ g ! c hxyi ]] = fM 2 M ?! ?c (xy:P jQ) for some P; Q;~ such that ?! ! c ?c (P jQ) 2 ]] and x; y 62 ~ g ! c hx z = (y)]i ]] = fM 2 M ?! ?c (x(y):P jQ) for some P; Q;~ such that ?! ! c ?c (P jQ)fz=yg 2 ]] and x; z 62 ~ g ! c hx(y)i ]] = Sz2N hxz i( fz=yg)]] fM 2 M ?! y?c (xy:P jQ) for some P; Q;~ such that ?! ! c ?c (P jQ) 2 ]] and x 62 ~ g ! c x = y] ]] = fM 2 M fx=yg 2 ]]g: To de ne the realizability of an arbitrary type we need the soundness of the normal type inclusion relation with respect to the interpretation of normal types (Theorem 44). To prove it we relate the interpretation of with that of fx=ygN.

Lemma 43.

1 If x = y] is normal, then x = y] ]] = y = x]( fy=xg)]]. 2 If x = y] a = b] is normal, then x = y] a = b] ]] = a = b] x = y] ]]. 3 If is normal, then ]] = rep(x; )]].

F. Damiani, M. Dezani-Ciancaglini and P. Giannini

26

4 If is a body, then fx=yg]] = fM fx=yg j M 2 ]]g. 5 If is normal, then fx=ygN]] = fM fx=yg j M 2 ]]g. Proof. 1 Observe rst that y = x]( fy=xg) is normal. It is easy to prove by induction on that M fx=yg 2 ]] if and only if M fy=xg 2 fy=xg]]. Then M 2 x = y] ]] () (by de nition) M fx=yg 2 ]] () M fy=xg 2 fy=xg]] () (again by de nition) M 2 y = x]( fy=xg)]]. 2 Notice that by de nition of normal type y 6= a; b and x 6= b, therefore M fx=ygfa=bg M fa=bgfx=yg. So we conclude the result using the de nition of realizability of matching (last case). ? ! ??? ? ! ??? 3 Let = a = b] . If rep(x; ) = the result is obvious. Otherwise c = x] 2 a = b]. ? ! ??? Let = ( a = b] ? c = x]) . By de nition rep(x; ) = x = c] fx=cg. Therefore by Point 2, ]] = c = x] ]] and by Point 1, c = x] ]] = x = c] fx=cg]]. 4 Easy by structural induction on . 5 Let = rep(x; rep(y; )). By Point 3 we have ]] = ]]. So it is su cient to prove, by structural induction on and using the inductive de nition of f = gR (De nition 15), that: M 2 ]] () M fx=yg 2 fx=ygR]]. | If is a body, then the result follows by Point 4. | If = x = y] 0 , then fx=ygR = 0 . Moreover M 2 ]] () (by de nition) M fx=yg 2 0 ]] = fx=ygR]]. | The other cases follow immediately from the induction hypothesis.

Theorem 44. Let and be normal types.

N implies ]] ]]. N . We consider Proof. The proof is by induction on the length of the derivation only the interesting cases. | hx(y)i N hx z = (y)]i fz=yg where z 6= y. ! If M 2 hx(y)i ]] then M ?! ?c (x(y):P jQ) for some P; Q;~ such that ?c (P jQ) 2 ]] ?! ! c and x 62 ~. We can assume that z 62 ~. c c ?c (P jQ) 2 ]] implies ?c (P jQ)fz=yg 2 fz=yg]] by Lemma 43.4. By de nition we ! ! conclude M 2 hx z = (y)]i fz=yg]]. | N x = y]( fx=ygN). If M 2 ]] then M fx=yg 2 fx=ygN]] by Lemma 43.5. Then by de nition M 2 x = y] fx=ygN]].

Now we can de ne the interpretation of all types. De nition 45. If is a type, then the realizability of is \ ]] = i ]]; where i (1 i n) are incomparable normal types such that ' 1 ^ ^ n . Notice that, as shown in Corollary 25, the decomposition of a type as an intersection

1 i n

A Filter Model for Mobile Processes

27

of incomparable normal types is unique modulo 'N . This together with Theorem 44 assures that ]] is well de ned, in the sense that it does not depend on the choice of the incomparable normal types i (1 i n) such that ' 1 ^ ^ n . Moreover from Theorem 44 we derive that we do not need a decomposition in incomparable types. This is because, for any 0i (1 i m) normal, and i (1 i n) normal, such that ' 01 ^ ^ 0m , and ' 1 ^ ^ n , we have that \ \ 0 ]]: i ]] = i implies ]] ]]. Proof. Easy from De nition 45 and Theorems 24 and 44. It is easy to prove that realizability sets are closed under subject expansion and under parallel composition.

Theorem 46. Let and be any types. Then

1 i n

1 i m

Lemma 47. 1 If N 2 ]] and M ?! N then M 2 ]]. ?! 2 M 2 ]] implies that M jN 2 ]] for all N .

Proof. By De nition 45 it is su cient to consider the case of normal types. Both proofs are by structural induction on normal types. 1 All cases follow from the transitivity of ?! and from induction. For the last case ?! notice that if M ?! N then M fx=yg?! N fx=yg. ?! ?! ! 2 If = hx(y)i , then M ?! ?c (x(y):P jQ) for some P; Q;~ such that ?c (P jQ) 2 ]] ?! ! c ! and x 62 ~. By induction ?c (P jQ)jN 2 ]]. We can assume that ~ 62 fn(N ). So c c ?c (P jQjN ) 2 ]] by Point 1, since ?c (P jQ)jN ?c (P jQjN ). Now M jN ?! ?c (x(y):P jQjN ) ! ! ! ?! ! implies M jN 2 ]]. ! If = hx z = (y)]i , then M ?! ?c (x(y):P jQ) for some P; Q;~ such that ?c (P jQ)fz=yg 2 ?! ! c ! ]] and x; z 62 ~. By induction ?c (P jQ)fz=ygjN fz=yg 2 ]]. We can assume that c ?c (P jQjN )fz=yg 2 ]] by Point 1, since ?c (P jQ)fz=ygjN fz=yg ! ! ~ 62 fn(N ). So c ?c (P jQjN )fz=yg. Now M jN ?! ?c (x(y):P jQjN ) implies M jN 2 ]]. ! ! ?! If = x = y] then M fx=yg 2 ]]. By induction hypothesis M fx=ygjN fx=yg 2 ]]. So, since M fx=ygjN fx=yg (M jN )fx=yg, also (M jN )fx=yg 2 ]] by Point 1. Therefore M jN 2 x = y] ]]. The proofs of the other cases are similar to the proof of the rst one.

According to De nition 42, some reduction properties characterize the processes that belong to the interpretations of normal types. We can extend this result to all types only partially, since we are able to give su cient but not necessary conditions for the membership of processes to the interpretation of a (non-normal) type.

Lemma 48. ! 1 M ?! ?c (x(y):P jQ) for some P; Q;~ such that ?c (P jQ) 2 ]], and x 62 ~ imply ?! ! c c M 2 hx(y)i ]]. ! 2 M ?! ?c (xy:P jQ) for some P; Q;~ such that ?c (P jQ) 2 ]], and x; y 62 ~ imply ?! ! c c M 2 hxyi ]].

F. Damiani, M. Dezani-Ciancaglini and P. Giannini

28

3 M ?! xN for some N such that N 2 ]] implies M 2 x ]]. ?! Proof. By Theorem 46 it is su cient to prove all points for normal types, observing that if ' 1 ^ ^ n , then h i ' h i 1 ^ ^ h i n , and x ' x 1 ^ ^ x n , by R1.1 and R1.2. ? ! ??? ! ! 1 Let = a = b] where is a body. If ?c (P jQ) 2 ]] then ?c (P jQ)f~ =~g 2 ]] by ab ?c (P jQ) 2 !]], ! De nition 42. Moreover since M 2 hx(y)i!]]: () Now we have two di erent cases according to y 62 a = b] or y 2 a = b]. ? ! ??? ? ! ab ??? i) If y 62 a = b], then hx(y)i ' hx(y)i! ^ a = b]hxf~ =~g(y)i by Lemma 16.3. ? ! ab ??? By ( ) and Theorem 46 it is su cient to prove M 2 a = b]hxf~ =~g(y)i ]]. Now ?c (P jQ)f~ =~g 2 ]] implies ?c (x(y):P jQ)f~ =~g 2 hx(y)i ]] by de nition, so we ! ! ab ab ???b a b ?c (x(y):P jQ) 2 ? =!]hxf~ =~g(y)i ]] again by de nition. Then we ! have that a ? =!]hxf~ =~g(y)i ]] by Lemma 47.1. ???b a b conclude M 2 a ? ! ? ! ? ! ??? ??? ??? ii) If z = y] or y = z ] 2 a = b], let d = e] = ( a = b] ? z = y] ? y = z ])fz=yg. Then ??? hx(y)i ' hx(y)i! ^ ? =!]hxfd=~g z = (y)]i( fz=yg) by Lemma 16.3. d e ~e ? ! ~e ??? By ( ) and Theorem 46 it is su cient to prove M 2 d = e]hxfd=~g z = (y)]i fz=yg]]. ! ! ~e ~e First observe that ?c (P jQ)fd=~gfz=yg 2 fz=yg]] implies ?c (x(y):P jQ)fd=~g 2 ~e hx z = (y)]ifd=~g fz=yg]] by de nition. So, again by de nition, we have that ??? ??? ?c (x(y):P jQ) 2 ? =!]hxfd=~g z = (y)]i fz=yg]]. Then we conclude M 2 ? =!]hxfd=~g z = ! d e ~e d e ~e (y)]i fz=yg]] by Lemma 47.1. 2 As the rst case of Point 1 using Lemma 16.4. 3 The more interesting case is = hyxi . In this case N x hyxi = hy(x)i and x 6= y. If N 2 hyxi ]] then, by de nition, N ?! ?c (hyxi:P jQ) for some ~, P , Q such that ?! ! c ?c (P jQ) 2 ]] and x; y 62 ~. This implies M ?! x?c (hyxi:P jQ). Therefore by de ! ! c ?! nition, M 2 x: ]].

? ! ???

? ! ???

Lemma 49. 1 fx=yg]] = fM fx=yg j M 2 ]]g. 2 M fx=yg 2 ]] implies M 2 x = y] ]]. ? !? ! ??? ??? 3 M f~ =~gjN f~=f g 2 ]] implies M jN 2 a = b] e = f ] ]]. ab e ~

Proof. By Theorem 46 it is su cient to prove the rst two points for normal types, observing that if ' 1 ^ ^ n , then fx=yg ' 1 fx=yg ^ ^ n fx=yg, and x = y] ' x = y] 1 ^ ^ x = y] n , by R1.3. 1 Immediate from Lemmas 43.5, 16.2 and Theorem 46. 2 M fx=yg 2 ]] =) (by Lemma 43.5) M fx=yg (M fx=yg)fx=yg 2 fx=ygN]] =) (by De nition 42, axiom A6.4, Lemma 16.2, and Theorem 46) M 2 x = y]( fx=ygN)]] = x = y] ]].

A Filter Model for Mobile Processes

3 Let u = v] be a normal{ sequence such that E ( u = v]) = E ( a = b] e = f ]) (Propo? ! ??? sition 14.2 assures the existence of u = v]). By Point 1, M f~ =~gjN f~=f g 2 ]] implies (M f~ =~gjN f~=f g)f~ =~ g 2 f~ =~ g]]. ab e ~ ab e ~ uv uv ~gjN f~=f g)f~ =~ g, we have that (M jN )f~ =~ g 2 f~ =~ g]]. ~ uv Since (M jN )f~ =~ g (M f~ =b uv a e uv uv ? = !] ]] by Point 2. We conclude M jN 2 ? =!]? = !] ]] ???v ???b e???f So we obtain M jN 2 u a by Proposition 14.1 and Theorem 46. The next lemma states the key properties of realizability interpretation needed to prove the soundness of realizability. Lemma 50. Let M 2 ]], 1 x(y):M 2 hx(y)i ]], 2 xy:M 2 hxyi ]], 3 x M 2 x ]], 4 x = y]M 2 x = y] ]], 5 N 2 ]] implies M jN 2 o ]]. Proof. Points 1, 2, and 3 follow immediately from the corresponding Points of Lemma 48. 4 M 2 ]] =) (by Lemma 49.1) M fx=yg 2 fx=yg]] =) (since ( x = y]M )fx=yg M fx=yg) ( x = y]M )fx=yg 2 fx=yg]] =) (by Lemma 49.2) x = y]M 2 x = y] fx=yg]] =) (by axiom A6.4 and Theorem 46) x = y]M 2 x = y] ]]. 5 Let ' 1 ^ ^ m , ' 1 ^ ^ n where i (1 i m), T (1 j n) are j normal. Then o ' ^1 i m;1 j n ( i o j ). Therefore o ]] = 1 i m;1 j n i o j ]] by Theorem 46. So we will prove that M 2 ]] and N 2 ]] imply M jN 2 o ]] when and are normal. This proof is by structural induction on and . We consider only the more interesting cases. ? ! ??? ? ! ??? (a) Let = a = b]hy g = (x)]i and = e = f ]htz i . Then by axiom A8.2 ??? ??? o ' (? =!]hy(x)i( g = x] o )) ^ (? = !]htzi( o ))^ a b e f ? =!]? = !] y = t]( g = z] fg=zg o fy=tg)): ???b e f ??? (a So we have to prove ? ! ??? | M jN 2 a = b]hy(x)i( g = x] o )]], ? ! ??? | M jN 2 e = f ]htz i( o )]], and ? !? ! ??? ??? | M jN 2 a = b] e = f ] y = t]( g = z ] fg=xg o fy=tg)]]. If M 2 ]], then M f~ =~g 2 hy g = (x)]i ]], i.e., M f~ =~g?! ?c (y(x):P jQ), and ab a b ?! ! ?c (P jQ)fg=xg 2 ]] for some P; Q;~, by De nition 42. Moreover N 2 ]] im! c ! plies N f~=f g 2 htz i ]], i.e., N f~=f g?! ?d(tz:RjS ) and ?d(RjS ) 2 ]] for some e ~ e ~ ?! !

? ! ???

? ! ???

? !? ! ??? ???

29

???v { We require ? = !] to be normal, since this assures us that the substitution f~ =~ g is well-de ned. u u v

F. Damiani, M. Dezani-Ciancaglini and P. Giannini

30

~ R; S; d, by the same de nition. ? ! ??? Proof of M jN 2 a = b]hy(x)i( g = x] o )]]. ! ! From ?c (P jQ)fg=xg 2 ]] we get by de nition ?c (P jQ) 2 g = x] ]]. Now ?c (P jQ) 2 g = x] ]] and N 2 ]] imply ?c (P jQ)jN 2 g = x] o ]] by in! ! ! ! duction. We can assume ~ 62 fn(N ), so we get ?c (P jQ)jN ?c (P jQjN ) and c ?c (P jQjN ) 2 g = x] o ]] by Lemma 47.1. By Lemma 48.1, this implies ! M f~ =~gjN 2 hy(x)i( g = x] o )]], since M f~ =~gjN ?! ?c (y(x):P jQjN ). We ab a b ?! ! ? =!]hy(x)i( g = x] o )]]. ???b conclude, by Lemma 49.3, that M jN 2 a ? ! ??? The proof of M jN 2 e = f ]htz i( o )]] is similar. ? !? ! ??? ??? Proof of M jN 2 a = b] e = f ] y = t]( g = z ] fg=xg o fy=tg)]]. ?c (P jQ)fg=xg 2 ]] =) ?c (P jQ)fg=xgfg=zg 2 fg=zg]] by Lemma 43.4 ! ! ?c (P jQ)fz=xgfg=zg 2 fg=zg]] =) ! ! =) ?c (P jQ)fz=xg 2 g = z] fg=zg]] by De nition 42 ( ) ?d(RjS ) 2 ]] ! ?d(RjS )fy=tg 2 fy=tg]] by Lemma 43.4 =) ! ( )

! ! ( ) and ( ) =) ?c (P jQ)fz=xgj?d(RjS )fy=tg 2 g = z] fg=zg o fy=tg]] by induction =) M f~ =~gjN f~=f gfy=tg 2 g = z] fg=zg o fy=tg]] by Lemma 47.1 since ab e ~ ? ! M f~ =~ gjN f~=f gfy=tg?! ?c (P jQ)fz=xgj d(RjS )fy=tg ab e ~ ?! ! ? =!]? = !] y = t]( g = z] fg=xg o fy=tg)]] ???b e f ??? =) M jN 2 a by Lemma 49.3:

(b) Let = a = b]hy(x)i and = e = f ]ht(z )i . Then by axiom A8.2 ??? ??? o ' (? =!]hy(x)i( o )) ^ (? = !]ht(z)i( o ))^ a b e f ? !? ! ??? ??? ( a = b] e = f ] y = t] z ( fz=xg o fy=tg)):

? ! ???

? ! ???

So we have to prove ? ! ??? | M jN 2 a = b]hy(x)i( o )]], ? ! ??? | M jN 2 e = f ]ht(z )i( o )]], and ? !? ! ??? ??? | M jN 2 a = b] e = f ] y = t] z ( fz=xg o fy=tg)]]. ! If M 2 ]], then M f~ =~g 2 hy(x)i ]], i.e., M f~ =~g?! ?c (y(x):P jQ) and ?c (P jQ) 2 ab a b ?! ! ]] for some P; Q;~, by De nition 42. Moreover N 2 ]] implies N f~=f g 2 c e ~ ht(z )i ]]. Again, by De nition 42, this implies that: either ! (i) N f~=f g 2 htgi fg=z g]] for some g, i.e., N f~=f g?! ?d(tg:RjS ) and ?d(RjS ) 2 e ~ e ~ ?! ! ~ fg=z g]] for some R; S; d, or ! ~ (ii)N f~=f g?! z ?d(tz:RjS ) and ?d(RjS ) 2 ]] for some R; S; d. e ~ ?! ! ? ! ??? In both cases, (i) and (ii), the proof of M jN 2 a = b]hy(x)i( o )]] is similar to

A Filter Model for Mobile Processes

31

the proof of case (a). ? ! ??? Proof of M jN 2 e = f ]ht(z )i( o )]]. ! Case (i). In this case N f~=f g?! ?d(tg:RjS ) and ?d(RjS ) 2 fg=z g]]. Now M 2 e ~ ?! ! ! ! ]] and ?d(RjS ) 2 fg=z g]] imply M j?d(RjS ) 2 o fg=z g]] by induction. We ! ! ! ~ can assume d 62 fn(M ), so we get M j?d(RjS ) ?d(M jRjS ) and ?d(M jRjS ) 2 o fg=z g]] by Lemma 47.1. By Lemma 48.1 this implies M jN f~=f g 2 htgi( o e ~ ?d(M jtg:RjS ). So we have M jN f~=f g 2 ht(z )i( o ! fg=z g)]], since M jN f~=f g?! e ~ ?! e ~ )]] by Theorem 46, since htgi( o fg=z g) = htgi( o )fg=z g ht(z )i( o ) by A11.2 (we can assume z 6= t and z 62 fn( )). We conclude by Lemma 49.3 that ? ! ??? M jN 2 e = f ]ht(z )i( o )]]. ! Case (ii). In this case N f~=f g?! z ?d(tz:RjS ) and ?d(RjS ) 2 ]]. e ~ ?! ! ! ! Now M 2 ]] and ?d(RjS ) 2 ]] imply M j?d(RjS ) 2 o ]] by induc! ! ~ 62 fn(M ), so we get M j?d(RjS ) ?d(M jRjS ) and tion. We can assume d ?d(M jRjS ) 2 o ]] by Lemma 47.1. By Lemma 48.1 this implies ?d(M jtz:RjS ) 2 ! ! htz i( o )]]). We get M jN f~=f g 2 z htz i( o )]] by Lemma 48.3, since e ~ ??? ?d(M jtz:RjS ). We conclude by Lemma 49.3 that M jN 2 ? = !]ht(z )i( o ! M jN f~=f g?! z e ~ ?! e f )]]. ? !? ! ??? ??? Proof of M jN 2 a = b] e = f ] y = t] z ( fz=xg o fy=tg)]]. Case (i). ?c (P jQ) 2 ]] ! ! =) ?c (P jQ)fg=xg 2 fg=xg]] by Lemma 43.4 () ?d(RjS ) 2 fg=zg]] =) ?d(RjS )fy=tg 2 fg=zgfy=tg]] by Lemma 43.4 ( ) ! ! ! ! ( ) and ( ) =) ?c (P jQ)fg=xgj?d(RjS )fy=tg 2 fg=xg o fg=zgfy=tg]]

by induction =) M f~ =~gjN f~=f gfy=tg 2 fg=xg o fg=zgfy=tg]] by Lemma 47.1 since ab e ~ ? ! M f~ =~ gjN f~=f gfy=tg?! ?c (P jQ)fg=xgj d(RjS )fy=tg ab e ~ ?! ! =) M f~ =~gjN f~=f gfy=tg 2 z( fz=xg o fy=tg)]] ab e ~ by Theorem 46, since fg=xg o fg=zgfy=tg = ( fz=xg o fy=tg)fg=zg (we can assume z 62 fn( )) z ( fz=xg o fy=tg) by axiom A11.2, ? =!]? = !] y = t]( fg=xg o fg=zgfy=tg)]] ???b e f ??? =) M jN 2 a by Lemma 49.3

Case (ii). ?c (P jQ) 2 ]] =) ?c (P jQ)fz=xg 2 fz=xg]] by Lemma 43.4 ( ) ! ! ?d(RjS ) 2 ]] =) ?d(RjS )fy=tg 2 fy=tg]] by Lemma 43.4 ( ) ! ! ! ! ( ) and ( ) =) ?c (P jQ)fy=xgj?d(RjS )fy=tg 2 fz=xg o fy=tg]] by induction =) M f~ =~gjN f~=f gfy=tg 2 z( fz=xg o fy=tg)]] by Lemma 48.3 since ab e ~ ? ! M f~ =~ gjN f~=f gfy=tg?! z (?c (P jQ)fz=xgj d(RjS )fy=tg) ab e ~ ?! ! ??? ??? =) M jN 2 ? =!]? = ! y = t] z( fz=xg o fy=tg)]] by Lemma 49.3: a b e f]

F. Damiani, M. Dezani-Ciancaglini and P. Giannini

32

From Theorem 46 and Lemma 50 we get the main property of our realizability interpretation. Theorem 51. (Soundness and completeness) ` M : if and only if M 2 ]]. Proof. Soundness is proved by induction on the derivation of ` M : . The base of the induction is ` M : !, that is trivial. In the induction case we look at the last rule of the derivation. For rule ( ) we apply Theorem 46. For all the other rules we apply the induction hypothesis and the corresponding clause of Lemma 50. As for completeness, assume that M 2 ]], then for all i, 1 i n, M 2 i ]], where ' 1 ^ ^ n and each i is normal. So we only have to show that if M 2 ]] then ` M : , when is normal. This proof is by structural induction on . ! | If = hx(y)i , then M 2 ]] implies M ?! ?c (x(y):N jQ) for some ?c (N jQ) 2 ]] ?! ! ?c (N jQ) : . This implies by ! where x 62 ~. We can assume that y 62 ~. By induction ` c c ! Lemmas 32.4 and 32.5 that ` N : , ` Q : , for some ; such that ?c ( o ) . So using rule (h i I) we have ` x(y):N : hx(y)i and then by rules (o Ij ) and ( I) we ! ! ! can deduce ` ?c (x(y):N jQ) : ?c (hx(y)i o ). We get by rule ( ) ` ?c (x(y):N jQ) : ?c (hx(y)i o ) ' hx(y)i?c ( o ) hx(y)i by axiom A5.1 and rule ! ! hx(y)i , since R1.1. By the invariance of typing under subject expansion (Theorem 36) we conclude ` M : hx(y)i . ! | If = hx z = (y)]i , then M 2 ]] implies M ?! ?c (x(y):N jQ) for some ?c (N jQ)fz=yg 2 ?! ! ?c (N jQ)fz=yg : . This ! ]] where x; z 62 ~. We can assume that y 62 ~. By induction ` c c ! implies by Lemmas 28.1 and 34.2 that ` ?c (N jQ) : for some such that fz=yg . Then by Lemmas 32.4 and 32.5 we have that ` N : , and ` Q : , for some ; ! ! such that ?c ( o ) . As in the previous case we can deduce ` ?c (x(y):N jQ) : ?c (hx(y)i o ). So, by rule ( ), we get that ` ?c (x(y):N jQ) : hx z = (y)]i , since ! ! ?c (hx(y)i o ) ' hx(y)i?c ( o ) hx(y)i hx z = (y)]i ' hx z = (y)]i fz=yg ! ! hx z = (y)]i by axioms A5.1, A11.3, A6.4, and rules R1.1, R1.3. By the invariance of typing under subject expansion (Theorem 36) we conclude ` M : hx z = (y)]i . | If = hx(y)i , then M 2 ]], and M 2 ]] implies that: either M ?! ?c (xz:N jQ) ?! ! ?c (N jQ) 2 fz=yg]], or M ?! y?c (xy:N jQ) for some ?c (N jQ) 2 ]], ! ! ! for some ?! where x; z 62 ~. We can assume that y 62 ~. c c ! In the rst case by induction ` ?c (N jQ) : fz=yg. This implies by Lemmas 32.4 ! and 32.5 ` N : , ` Q : , for some ; such that ?c ( o ) fz=yg. So using rule (h i I) we have ` xz:N : hxz i , and then by (o Ij ) and ( I) we can deduce ! ! ! ` ?c (xz:N jQ) : ?c (hxz i o ). Then applying rule ( ), we get ` ?c (N jQ) : hx(y)i , ! ! since ?c (hxz i o ) ' hxz i?c ( o ) hxz i fz=yg hx(y)i by axiom A5.1, rule R1.1, and axiom A11.2. By the invariance of typing under subject expansion (Theorem 36) we conclude ` M : hx(y)i . ! In the second case by induction ` ?c (N jQ) : . This implies, by Lemmas 32.4 and ! 32.5, that ` N : , ` Q : , for some ; such that ?c ( o ) . As in the ?c (xy:N jQ) : ?c (hxyi o ). So, by rule ( I), we ! ! previous case we can deduce ` ! ! ! get that ` y?c (xy:N jQ) : y?c (hxyi o ). Therefore ` y?c (N jQ) : hx(y)i by ?c (hxyi o ) ' hx(y)i?c ( o ) hx(y)i by axiom A5.1, and rule ! ! rule ( ), since y

A Filter Model for Mobile Processes

33

R1.1. By the invariance of typing under subject expansion (Theorem 36) we conclude ` M : hx(y)i . | If = x = y] , then M 2 ]] implies M fx=yg 2 ]]. By induction ` M fx=yg : , which implies ` M : x = y] by Lemma 34.3, taking into account that y 62 fn( )

since x = y] is normal. Now we are able to characterize convergency by means of typing and of proving the adequacy of the lter model.

Theorem 52. (Resource property)

For all M : may 1 ` M : hx(y)i! for some y 6= x if and only if M +x , and may . 2 ` M : hx(y)i! for some y if and only if M +x Proof. 1 (Only if) Suppose ` M : hx(y)i! (y 6= x). By Theorem 51 it follows that M 2 hx(y)i!]]. By De nition 42 we can have two cases: either M ?! ?c (xz:P jQ) for ?! ! may some z , or M ?! y?c (xy:P jQ), where x 62 ~. So in both cases M +x since ?! ! c x 62 ~. c may (If) Suppose M +x for a term M . This means that M ?! ?c (xz:P jQ) for some ~, ?! ! c z , P , Q, where x 62 ~. Since ` xz:P : hxz i! and ` Q : !, we have, by rule (o Ij ), c that ` xz:P jQ : hxz i! o !, which implies ` xz:P jQ : hxz i!, since by axiom A2.1 ! ! hxz i! o ! ' hxz i!. Therefore ` ?c (xz:N jQ) : ?c hxz i! by rule ( I). If z 62 ~ c ?c hxz i! ' hxz i?c ! hxz i! z hxz i! ' hx(y)i!, by axioms A5.1, ! ! we have ! ! A11.1, A11.2, and A1, where x 6= y. If z 2 ~ we have ?c hxzi! ' z ?d hxzi! ' c ! ~ c z hxz i?d ! hx(y)i!, by axioms A3.1, A5.1, A11.1 and A1, where d = ~ ? z ?c (xz:N jQ) : hx(y)i!. So by ! and x 6= y. In both cases using rule ( ) we get ` Theorem 36 we conclude ` M : hx(y)i!. 2 Similarly. The adequacy of the lter model with respect to the open testing preorder means that the congruence induced does not consider equivalent programs that can be distinguished by some substitution and tester. We rst prove the adequacy with respect to the observational preorder, the other equivalences will follow easily.

Theorem 53. (Adequacy) 1 If M vF N then M vO N . 2 If M vF N then M vOT N . 3 If M vF N then M vT N .

Proof. 1 First we show that for all terms M and N it holds that may may if (M vF N and M +x ) then N +x : () may . Then ` M : hx(y )i! for some Let M; N 2 and assume that M vF N and M +x

F. Damiani, M. Dezani-Ciancaglini and P. Giannini

34

2 Easy consequence of Point 1 and Proposition 8. 3 Immediate from Point 2.

y 6= x by Theorem 52.1. By M vF N we also have that ` N : hx(y)i! and again by may Theorem 52.1 we get that N +x . Moreover, note that (by Lemma 32) M vF N implies that C M vF C N for all contexts C . So, if M vF N then for every context C we have, by ( ), that may may C M +x implies C N +x : Therefore M vO N .

To prove full abstraction, let us consider a normal type = a = b] , where is a body. We associate to each body a test term T ;w , where w is a name which does not occur in . Then to discriminate using type we will equate channels according to ? =!] and put the obtained process in parallel with T . ??? a b ;w The test terms are de ned by induction on bodies: they o er the communications \complementary" to the pre xes of the bodies. The test terms look similar to the test bodies (De nition 20.1). Notably, the test bodies turn out to be the principal types of the test terms. De nition 54. Let be a body and w be a name which does not occur in . We de ne the test term T ;w by structural induction on : 1 T!;w = v wv:0 2 Thx(y)i ;w = y xy:T ;w 3 Thx z=(y)]i ;w = xz:T ;w 4 Thxyi ;w = x(z ): y = z ]T ;w where z 62 fn(hxyi ) 5 Thx(y)i ;w = x(y):T ;w . From Proposition 30, each T ;w has a principal type, since ! does not occur in it. More precisely Proposition 55. Let be a body and w be a name which does not occur in . Then }(T ;w ) = = ;w . Proof. By structural induction on , using the de nition of principal type (De nition 29). The following property of = ;w is crucial for our proof. Lemma 56. Let be a body, be a type, and w be a name such that w 62 fn( ), w 62 fn( ). Then o = ;w hw(v)i! if and only if . Proof. (If) implies o = ;w o = ;w by rule R1.4. Moreover o = ;w hw(v)i! can be easily proved by induction on . To prove the (Only if) assume that o = ;w hw(v)i! and 6 : By De nition 20, ? ;w ' ] o = ;w . Let ' 1 ^ ^ n , where 1 ; ; n are normal

? ! ???

A Filter Model for Mobile Processes

35

types. If 6 then for all i n, i 6 N ,S Theorem 24. Then, by Lemma 21.1, we have by ?c ? ;w i ' ! for all i n, where ~ = i n fn( i ) fn( ). From o = ;w hw(v)i! ! c V ! !V we get ? ;w ' i n ? ;w i hw(v)i! and also ?c ( i n ? ;w i ) ?c hw(v)i! hw(v)i! by rule R1.2 and axioms A5.1, A11.1. So we get a contradiction. ??? Lemma 57. Let = ? =!] be a normal type, where is a body. Then a b ` M : if and only if ` M f~ =~g : . ab Proof. Observe that ' f~ =~g. The (Only if) derives from Lemma 34.1, and the ab (If) from Lemma 34.3. ??? Theorem 58. (Characterization theorem) Let = ? =!] be a normal type, where a b is a body, and let w be a name which does not occur in . may 1 Let N be a process that does not contain w. Then N jT ;w +w if and only if ` N : . may ~gjT ;w +w if and only if 2 Let M be a process that does not contain w. Then M f~ =b a `M : . Proof. may 1 By Theorem 52, N jT ;w +w if and only if ` N jT ;w : hw(y)i!. By Lemma 32.4 we get ` N : and ` T ;w : for some ; such that o hw(y)i!. By Propositions 30 and 55, ` T ;w : implies = ;w . So we get o = ;w hw(y)i! by rule R1.4. By Lemma 56 and rule ( ) we can conclude that ` N : : 2 Immediate from Point 1 and Lemma 57.

Theorem 59. (Full abstraction) 1 M vOT N implies M vF N .

Now we can prove our full abstraction result.

2 Let M be a body process. Then M vT N implies M vF N . Proof. 1 Assume that M 6vF N , say ` M : and 6` N : for some type . Then by Proposition ? ! ??? 17 and rule ( ) there is a normal type = a = b] , where is a body, such that may ` M : and 6` N : . We have, by Theorem 58.2, that M f~ =~gjT ;w +w but not ab may (where w is a name not occurring in M; N ). So we can conclude N f~ =~gjT ;w +w ab that M 6vOT N . 2 Let ` M : and 6` N : be as in the proof of Point 1. By Proposition 28.1 we can nd such that `? M : . Clearly 6` N : . By De nition 38, ' 1 ^ ^ n (n 1) where 1 ; : : : ; n are body types, since M is a body process. So there is a body 2 f 1 ; : : : ; n g such that ` M : and 6` N : . Then Theorem 58.1 implies may may that M jT ;w +w holds but N jT ;w +w does not hold. So we can conclude that M 6vT N .

As an immediate consequence we have that the open testing preorder and the observational preorder coincide, moreover, for body processes, open testing coincides with testing.

F. Damiani, M. Dezani-Ciancaglini and P. Giannini

36

Corollary 60. 1 M vOT N if and only if M vO N .

2 Let M be a body process. Then M vOT N if and only if M vT N . For example, let P = xy:0 and Q = y xy:0. It it easy to see that Q vF P and P 6vF Q. In fact, for hxyi! we have ` P : and 6` Q : . Now, according to Theorem 59, we can build the test term T ;w and the substitution s may may such that s(P )jT ;w +w and not s(Q)jT ;w +w , where w is a name not occurring in P; Q. Indeed, T ;w = x(z ): y = z ] vwv:0 and the empty substitution are the required test term and substitution. Remark 61. Corollary 60 shows that vOT is a congruence, and clearly vOT implies vT . As a matter of fact, vOT is the biggest congruence included in vT . To see this, take M; N such that M 6vOT N , but M vT N . By de nition there is a context C such that C M 6vT C N , so we cannot extend vOT preserving the closure under contexts.

5. Related papers

The literature related to the present paper has partially been quoted in the introduction. We add here comparisons and remarks which require the development of the lter model presented in previous sections. Two papers deeply related to our are (Hennessy 1991) and (Boreale and De Nicola 1995). Both papers describe denotational semantics of -calculus which are fully abstract with respect to a \must" operational semantics. The models described are term models and the completeness proofs rely on the existence of head normal forms. The language considered in (Hennessy 1991) is quite expressive, since it includes an if{then{ else construct. The fully abstract model is build using a proof system based on a set of inequations between processes. The compact elements of the domain turn out to be the nite processes which have a \ nite" behaviour on input actions. Also the language of (Boreale and De Nicola 1995) is richer than ours since it includes mismatch. The axioms and rules of (Boreale and De Nicola 1995) for comparing nite processes are a subset of our axioms and rules for comparing types (modulo the correspondence between types and processes). There is also a similarity between the strong normal forms of (Boreale and De Nicola 1995) and our normal types. The main feature of our approach, with respect to the one of (Boreale and De Nicola 1995), is that the meanings of :P and xP , that is the set of types that can be assigned to :P and xP , are de ned from the meaning of P in a uniform way. For instance if P ]] is the lter of types that can be assigned to P , xP ]] = f j x for some 2 P ]]g. In (Boreale and De Nicola 1995), instead, the interpretation of pre xes and restrictions is done, by using, in a suitable way, the equivalence class of the strong normal form of the term itself. For instance xP ]] = snf ( xP )], where snf ( xP ) is the strong normal form of xP . So the de nition of the model in (Boreale and De Nicola 1995) requires strong normal forms. Our normal types are only a tool for proving adequacy and full abstraction of the lter model.

A Filter Model for Mobile Processes

37

A number of interpretations of the -calculus based on functor categories have been proposed, see (Stark 1996; Fiore et al. 1996; Hennessy 1996). Such interpretations are parameterized on the set of names used by a process. Let I be the category of nite sets of names with injections. The functor category considered for the interpretation is the category of functors from I to the category of SFP in (Stark 1996) and the category of functors from I to Cpo (and Set) in (Fiore et al. 1996). In such interpretations we have to consider the meaning of processes indexed by a set of names that may change as the process does input actions or restrictions. The bound output is modelled by N (N ? P ); where N is the functor injecting I into the chosen category (SFP or Cpo). The functor N ? P is such that (N ? P )s = P (s + 1) where s is a nite set of names and s + 1 is obtained adding a new name to s. (In the category of nite sets with injections s + 1 does not depend on which element we add.) The fact that ? is a functor implies that the interpretation of the bound output does not depend on the name chosen (the name is fresh). The input is modelled by N (N ! P ); where the functor ! is such that (N ! P )s = (P s)s P (s + 1): (P s)s speci es the behaviour of the function for inputs in s, and P (s + 1) speci es the value of the function when the input is not in s. In this second case, as for the ? functor, the result is independent from the particular element chosen. In these models we can interpret faithfully restriction and input, and we can express the fact that the restriction operator introduces a new name that should not interfere with the free names of other processes. The models presented in (Fiore et al. 1996; Stark 1996) are shown to be fully abstract w.r.t. strong late bisimilarity. A similar technique is used in (Hennessy 1996) to presents two fully abstract term models for the \may" and \must" testing. It is also outlined that the model for the \may" testing is also fully abstract w.r.t. the more general equivalence that compares the \may" behaviour of processes in all contexts. None of these functorial models, however, has a logical presentation. The full abstraction of the model in (Hennessy 1996), that is the closest to ours, is provided similarly to (Hennessy 1988) by associating both to terms and to elements of the domain the sets of acceptances (similar to strong normal forms). In the rst case the set of acceptances of a term determines its operational behaviour, and in the second the set of acceptances of an element of the domain determines completely the element (it is the set of its nite approximations). So, as normal types for our work, also for this work acceptances are a device to prove completeness (and not essential to the de nition of the model). A drawback of the functorial interpretation, that was already noticed for the interpretation of block structures for which the functorial approach was rst introduced in (Oles 1985), is

F. Damiani, M. Dezani-Ciancaglini and P. Giannini

38

that it is not clear how to extend it to higher-types. (Hartonas and Hennessy 1997) present a model of a subset of the language FACILE (mini-FACILE) which is fully abstract w.r.t. the \may" observational preorder that compares the behaviour of terms in all contexts. The technique used for the proof of full abstraction is similar to the one of the present paper. That is the logic of the model is speci ed through a type assignment system. Moreover a notion of satisfaction for types that coincide with our realizability is given. The type assignment provides a correct and complete proof system for the \may" properties expressed by the types. The language modelled, mini-FACILE, is a typed -calculus with a type proc for processes that are speci ed with a value passing CCS-like syntax. The part of the language modelled does not, however, contain the local scoping operator (that correspond to the -calculus restriction operator), and adding static scoping is left as future work. It is hinted that static scoping could be modelled via functor categories. Even though papers like the previous (Stark 1996; Fiore et al. 1996; Hennessy 1996) show that this is the case, the di culty with these interpretations is to get a logical characterization of the domains through a type assignment system. Indeed at the moment we do not know of anyone. We instead model static scoping via the inclusion (and equivalence) relation between types.

Acknowledgments

We thank Rocco De Nicola, Eugenio Moggi and Michele Boreale for enlightening discussions about the subject of this paper, and Andrea Pederiva for his comments on drafts of this paper. The present version of this paper has strongly bene ted from comments and remarks by the Anonymous Referees. During the elaboration of the nal version of this paper Mariangiola Dezani-Ciancaglini was visiting the Tokyo Institute of Technology. She would like to thank her host Masako Takahashi-Horai and the whole Department of Mathematical and Computing Sciences for the ideal working conditions they provided.

References

Abramsky, S. (1991) Domain Theory in Logical Form. Annals of Pure and Applied Logic 51, 1{77. Abramsky, S. (1991) A Domain Equation for Bisimulation. Information and Computation 92 (2), 161{218. Abramsky, S. and Ong, C. -H. L. (1993) Full Abstraction in the Lazy Lambda Calculus. Information and Computation 105 (2),159{267. Amadio, R. M. and Dam, M. (1996) Toward a modal theory of types for the -calculus. In Formal Techniques in Real-Time and Fault-Tolerant Systems, Lecture Notes in Computer Science 1135, 347{365. Springer-Verlag. Barendregt, H. P. (1984) The -Calculus. Its Syntax and Semantics. North-Holland.

A Filter Model for Mobile Processes

39

Barendregt, H. P., Coppo, M. and Dezani-Ciancaglini, M. (1983) A Filter Lambda Model and the Completeness of Type Assignment. Journal of Symbolic Logic 48 (4), 931{940. Boreale M. and De Nicola R. (1995) Testing Equivalence for Mobile Processes Information and Computation 120 (2), 279{303. Boreale M. and Sangiorgi D. (1996) Some Congruence Properties for -calculus Bisimilarities. Technical Report RR-2870, INRIA-Sophia Antipolis. Boudol G. (1994) A Lambda Calculus for (Strict) Parallel Functions. Information and Computation 108 (1), 51{127. Dam M. (1993) Model Checking Mobile Processes. In CONCUR'93, Lecture Notes in Computer Science 715, 22{36, Springer-Verlag. De Nicola R. and Hennessy M. (1984) Testing Equivalences for Processes. Theoretical Computer Science 34 (1-2), 83{133. De Nicola R. and Hennessy M. (1987) CCS without 's. In TAPSOFT'87, Lecture Notes in Computer Science 249, 138{152. Springer-Verlag. Dezani-Ciancaglini M., de'Liguoro U. and Piperno A.(1996) Filter Models for ConjunctiveDisjunctive -calculi. Theoretical Computer Science 170(1-2), 83{128. Dezani-Ciancaglini M., de'Liguoro U. and Piperno A.(1997) A Filter Model for Concurrent -calculi. SIAM Journal on Computing, to appear. Fiore M. P., Moggi E. and Sangiorgi D. (1996) A Fully Abstract Model for the -calculus. In LICS'96, IEEE Comp.Soc. Press. Hartonas T. and M. Hennessy M. (1997) Full Abstractness for a Functional/Concurrent Language with Higher-Order Value-Passing. Computer Science Technical Report 97:01, School of Cognitive and Computing Sciences, University of Sussex. An Extended Abstract in CSL'97. Hennessy M.(1988) Algebraic Theory of Processes. MIT Press. Hennessy M.(1991) A Model for the -calculus. Computer Science Technical Report 91:08, School of Cognitive and Computing Sciences, University of Sussex. Hennessy M.(1994) A Fully Abstract Denotational Model for Higher-Order Processes. Information and Computation 112 (1), 55{95. Hennessy M.(1994) Higher-order Processes and their Models. In ICALP '94, Lecture Notes in Computer Science 820, 286{303. Springer-Verlag. Hennessy M.(1996) A Fully Abstract Denotational Semantics for the -calculus. Computer Science Technical Report 96:04, School of Cognitive and Computing Sciences, University of Sussex. Milner R. (1980) A Calculus of Communicating Systems. Lecture Notes in Computer Science 92, Springer-Verlag. Milner R. (1989) Communication and Concurrency. Prentice-Hall. Milner R. (1991) The Polyadic -calculus: A Tutorial. Technical Report ECS-LFCS-91-180, Edinburgh Univ. Also in Logic and Algebra of Speci cation, Springer-Verlag, Berlin, 1993. Milner R. (1992) Functions as Processes. Mathematical Structures in Computer Science 2(2), 119{141. Milner R., Parrow J. and Walker D. (1992) A Calculus of Mobile Processes, I and II. Information and Computation 100 (1), 1{77. Milner R., Parrow J. and Walker D. (1993) Modal Logics for Mobile Processes. Theoretical Computer Science 114 (1), 149{171. Oles F. J. (1985) Type Algebras, Functor Categories and Block Structures. In Algebraic Methods in Semantics, 543{573. Cambridge University Press. Ong C. -H. L. (1993) Non-Determinism in a Functional Setting. In LICS '93, IEEE Comp.Soc. Press, 275{286.

F. Damiani, M. Dezani-Ciancaglini and P. Giannini

40

Sangiorgi D. (1992) Expressing Mobility in Process Algebras: First-Order and Higher-Order Paradigms. Ph.D.Thesis, University of Edinburgh. Sangiorgi D. (1996) A Theory of Bisimulation for the -calculus. Acta Informatica 33 (1), 68{97. Scott D. (1982) Domains for Denotational Semantics. In ICALP'82, Lecture Notes in Computer Science 140, 577{613. Springer-Verlag. Stark I. (1996) A Fully Abstract Domain Model for the -calculus. In LICS'96, IEEE Comp.Soc. Press, 36{42. Thomsen B. (1990) Calculi for Higher-Order Communicating Systems. Ph.D.Thesis, Imperial College.

赞助商链接

- Human resource management and performance _Stephen_Wood(30)
- IMPACT OF HUMAN RESOURCE MANAGEMENT
- A business process approach to human resource management
- Human Resource Management in a Project
- Human Resource Management
- A filter model for mobile processes FERRUCCIO DAMIANI, MARIANGIOLA DEZANI-CIANCAGLINI
- A statistical model for land mobile
- A multiple model multiple hypothesis filter for Markovian switching systems
- ABSTRACT A New Analysis Model for Data Mining Processes in Higher Educational Systems
- A parametric model for the analysis of mobile ambients. Full version with proofs
- A Generic Model for NFC-based Mobile Commerce
- First experiences with a mobile platform for flexible 3d model acquisition in indoor and ou
- A Complete Order-theoretic Model for the Algebra of Communicating Processes
- Important configurations for NN processes in a Goldstone boson exchange model
- A Kalman Filter Model for GPS Navigation of Land Vehicles

更多相关文章：
更多相关标签：