# Type Assignement for Mobile Objects

Replace this ?le with prentcsmacro.sty for your meeting, or with entcsmacro.sty for your meeting. Both can be found at the ENTCS Macro Home Page.

Type Assignement for Mobile Objects

Franco Barbanera 1,3

Dipartimento di Matematica Universit` di Catania a Catania, Italy

Ugo de’Liguoro 2,4

Dipartimento di Informatica Universit` di Torino a Torino, Italy

Abstract We address the problem of formal reasoning about mobile code. We consider an Ambient Calculus, where process syntax includes constructs for object-oriented sequential programming. For the sake of concreteness, and because of practical relevance, we consider objects using message exchange to implement method invocation and overriding. The main contribution of the paper is an intersection type assignment system, obtained by a combination of systems introduced for the Calculus of Mobile Ambients and for the ?-calculus. We exploit in the mobility framework a typical feature of the intersection type discipline for object calculi, namely late typing of self. The proposed system is then checked against standard properties of related systems, establishing type invariance and a completeness theorem. Key words: objects, ambients, mobility, intersection, types.

1

Introduction

Any reasonable language for designing and programming mobile systems needs to have a sequential component. As a matter of fact languages designed for the network have a sequential core and primitives for communication, concurrency

1 2

Partially supported by MURST Co?n’01 NAPOLI Partially supported by MURST Co?n’01 COMETA and Co?n’02 PROTOCOLLO Projects, IST-2001-33477 DART Project and IST-2001-322222 MIKADO Project. The funding bodies are not responsible for any use that might be made of the results presented here. 3 Email: barba@dmi.unict.it 4 Email: deliguoro@di.unito.it

c 2003 Published by Elsevier Science B. V.

Barbanera, de’Liguoro

and mobility. Many theoretical models have been proposed to attack the urgent problem of understanding “global computing”, as it has been recently dubbed the scenario in which programmers have to cope with a plethora of computing devices and a great variety of interconnections, messages and code exchanges. These models, however, stemming from Milner π-calculus or from the Ambient Calculus of [CG00], do not directly take into account sequential procedures, which have to be simulated via heavy encodings. A possible reaction is the one pursued e.g. in [BCC01], were the formalization of object-oriented concepts, borrowed from calculi like the ?-calculus of [AC96], are strongly tied to the formalizations of distributed and mobile aspects, coming from the calculus of Mobile Ambients (MA). Another possible approach is to keep ambients and sequential code each other apart, as it is the case of the λ-terms inside ambients in [AKPG01]. The latter choice has the advantage of conceptual clarity, which is re?ected by the type system and (denotational) semantics. We shall describe a calculus where the sequential and the mobile/distributed components are loosely coupled, that is where objects and ambintes have different syntax and operational semantics; but, much as for “concurrent objects” in [Lan01], objects are allowed to interact with processes ant to drive mobility of ambients. The contribution of the paper, however, is not the calculus itself, but rather a type assignment system. This is mainly because what we intend to focus on is partial (semantical) information that one can get about programs, rather than ensuring global properties of the system (e.g. well-formedness, error freeness, etc.), which is typical of typed calculi a’ la Church. Therefore our calculus is type free, and types, which are better understood as predicates, are deduced for terms a posteriori. As a matter of fact we also try to partially re?ect in the type system the “loosely coupling” aspect of distributed/mobile and sequential features of the calculus, borrowing from type assignment systems for ?-calculus objects proposed in [dL01] and from the system for ambients introduced in [CD01]. The same approach should apply in the case of other sequential components of ambients, e.g. functional programs. From the work on type assignment for sequential objects, developed in works by the second author of the present paper [dL01,vBdL03] we retain the idea of “late typing of the self”. This consists in typing objects as records of methods; methods are typed by recording pre and post-conditions (the antecedent and the consequent of an arrow type respectively); it is only when a method is invoked that the system checks if the object satis?es the precondition of that particular method, which is actually a precondition of the self variable. This is contrasted to what we call the “early typing of the self”, consisting in the typing policy adopted in all type systems for objects, like those in [AC96], where all relevant information about the self variables needs to be checked in prior to any possible method invocation. Early typing of the 2

Barbanera, de’Liguoro

self leads to di?culties that have been faced in the literature by means of polymorphic types, as it is the case of the subtyping and matching polymorphism in [BCC01]. The main result in the paper is that types catch computational properties of terms because the system de?nes a model of the calculus. It is a logical model (namely a ?lter model), where each term denotes the sets of its properties, that is of its types; dually types denote sets of terms sharing certain relevant properties. This is the contents of our completeness theorem, which is also the basic tool to characterize the behavior of terms via their typings.

2

A calculus of Mobile Objects

De?nition 2.1 The set P of process terms of the Mobile Ambient calculus MA [CG00] is de?ned by the grammar: [ P, Q ::= 0 | (P | Q) | ! P | n[ P ] | M . P (by omitting restriction (νn)P ) where n ranges over a denumerable set of names, and M ::= in n | out n | open n Operational semantics of the MA calculus is given in terms of a structural congruence relation ≡, making | into an associative and commutative operator with unit 0 and such that ! P ≡ P | ! P , and a reduction relation. De?nition 2.2 Over P a reduction relation ?→ is de?ned by the following clauses: (R ? in ) (R ? out ) (R ? open ) (R ? P ar) (R ? Amb) (R? ≡) [ [ [ [ n[ in m . P | Q ] | m[ R ] ?→ m[ n[ P | Q ] | R ] [ [ [ [ m[ n[ out m . P | Q ] | R ] ?→ n[ P | Q ] | m[ R ] [ open n . P | n[ Q ] P ?→ Q P ?→ Q ?→ P |Q

=? P | R ?→ Q | R [ [ =? n[ P ] ?→ n[ Q ] P ?→ Q

P ≡ P , P ?→ Q, Q ≡ Q =?

In [CG00] the extension of MA with communication primitives amounts to the rede?nition the action part M in the pre?x operator by adding send and receive actions of the asynchronous π-calculus, and the proper clauses to the de?nition of the reduction relation. 3

Barbanera, de’Liguoro

To embody objects in the MA several possibilities are open. In [BCC01] objects are ambients with two ?elds: the ?rst one is a list of methods, the second is a process. Overriding is then implemented by means of the open primitive. To the other extreme one might follow [AKPG01], where MA is extended by rede?ning values that can be communicated to be (?rst order typed) λterms instead of plain names. It is not di?cult to do the same using terms from any ?-calculus in [AC96]. The calculus considered here sits in between: objects are considered as special processes, and we use pre?xing to exchange messages representing method invocation and overriding. Nevertheless objects retain their own syntax and operational semantics from the ?-calculus, and are not ambients. Instead, to make the calculus more expressive and allowing mobility primitives in the syntax of the “sequential” part, method bodies are processes themselves. This choice is closer to the “concurrent objects” in [Lan01]. De?nition 2.3 Terms P + of the MA calculus extended with objects are obtained by adding to de?nition 2.1 the following clauses: a ::= x | o | a.l | a.l ? ?(x)b b ::= a | P o ::= [li = ?(xi )bi

i∈I

]

P ::= . . . | o | l | l ? ?(x)b Operational semantics of the calculus is then given by extending de?nition 2.2 by:

(R ? 1) (R ? 2) (R ? 3) o| l o | l ? ?(x)b [li = ?(xi )bi

i∈I ].l j

?→ ?→ ?→

o.l o.l ? ?(x)b bj {[li = ?(xi )bi

i∈I ]/x } j

(R ? 4) [li = ?(xi )bi

i∈I ].l

j

? ?(y)b ?→ [li = ?(xi )bi

i∈I\{j} , l

j

= ?(y)b]

where in (R ? 3) and (R ? 4) we assume that j ∈ I.

3

A Type Assignment System

Our types, which could be more appropriately called predicates, are basically intersection types (see e.g. [DGdL98]). Their syntax comes from [CD01] for the MA terms, and from [dL01] for the ?-terms. 4

Barbanera, de’Liguoro

Γ Γ

P :σ

Γ (M ) Γ Γ

P :σ

Γ

Q:τ

M.P : M.σ Γ P :σ

P |Q:σ|τ P :σ Γ Γ !P : τ

(|)

Γ

[ [ n[ P ] : n[ σ ]

[ (n[ ] )

!P : σ | τ

(|)

Fig. 1. Type Inference Rules for Ambients

De?nition 3.1 The set T of types is the union of process types TP and functional types TF , which are de?ned by mutual induction according to the grammar: [ TP : σ, τ ::= ω | M . σ | n[ σ ] | (σ | τ ) | σ ∧ τ | {li : ?i TF : ?, ψ ::= σ → τ | ? ∧ ψ. The intended meaning of types is that of predicates, namely sets of terms sharing certain relevant property. More precisely types are seen as partial information about the “future” of process terms, so that whenever we say: “the meaning of the type σ is the set of processes such and such”, one should understand “the set of processes eventually reducing to something such and such” (among other possibilities). M . σ is the type of processes that may exhibit the capability M and then [ continue with something of type σ; n[ σ ] is the type of processes that are ambients named n, enclosing some process in σ; ?nally (σ | τ ) is the set of processes (equivalent to) (P | Q), where P and Q are in σ and τ respectively. The formal de?nition of our type inference rules for ambients is given in ?gure 1, where the statements Γ P : σ, for Γ = {x1 : σ1 , . . . , xk : σk }, have the standard meaning: P has type σ under the assumptions in the basis Γ. Types for the object part of the calculus have a similar meaning to types in [dL01] or predicates in [vBdL03]. {li : σi → τi i∈I } is the type of objects having at least methods labelled li such that, if the object itself satis?es σi (hence a precondition about the self), then the body will return a value satisfying τi (a postcondition of the method). We remark that this is a conditional statement, not involving any assumption about the actual properties of the object as a whole. This is also the basic tool to resolve the recursive nature of objects into simpler concepts. The rules for typing objects are in ?gure 2, where lj = ?(xj )bj ∈ a is de?ned as follows:

? ? i∈I

}| l | l? ? ,

j ∈ I =? lj = ?(xj )bj ∈ [li = ?(xj )bi l = ?(x)b ∈ a.l ? ?(x)b 5

i∈I

]

Barbanera, de’Liguoro

Γ, x : σ Γ Γ

b:τ

l = ?(x)b ∈ a

a : {l : σ → τ } Γ a:σ

({ }-I)

a : {l : σ → τ } Γ a.l : τ

({ }-E)

Fig. 2. Type Inference Rules for objects

?

l = ?(x)b ∈ a, l = l =? l = ?(x)b ∈ a.l ? ?(x )b

Types l and l ? ? are about communication; in particular if an update message of the shape l ? ?(x)b is sent, then the type l ? σ → τ records the pre and post conditions of the method implemented by the new body b. Rules for typing messages are in Figure 4. The type ω, arrow types and intersection types have their standard meaning: ω is the trivial predicate “true”, namely the whole set of terms; σ → τ is the type of functions (in the present case methods) sending anything of type σ into something of type τ (which is our understanding of pre and postconditions); σ ∧ τ is the property of any terms satisfying both σ and τ , so that extensionally it is the intersection of them. The typing rules dealing with intersection are given in the set of Logical Rules in Figure 3 in the style of the BCD type system [BCD83], where σ ≤ τ is logical implication of predicates, hence set inclusion extensionally. The relation ≤ is axiomatized in Figures 5 and 6.

4

Late versus Early Typing of Self

Before embarking in the technical treatment, let us pause on some relevant aspects of the assignment system we have proposed. The most apparent feature of the calculus is that at ?rst glance we regard objects as records of methods. This is the content of the following rule, which

Γ, x : σ Γ a:σ Γ

x:σ Γ

(Var) Γ Γ a:ω

(ω)

a:τ

a:σ∧τ

(∧-I)

a:σ Γ

σ≤τ

a:τ

(≤)

Fig. 3. Logical Type Inference Rules

6

Barbanera, de’Liguoro

Γ

l : l

(MsgSel) Γ

Γ, x : σ

b:τ

l ? ?(x)b : l ? σ → τ

(MsgUpdate)

Fig. 4. Type Inference Rules for Communication

is admissible in the system: xj : σj Γ [li = ?(xi )bi bi : τj

i∈I

?j ∈ J

j∈J

] : {lj : σj → τj

}

(J ? I)

Note that the σj do not need to be the same, not even equivalent each other. The admissibility follows since ?(xj )bj ∈ [li = ?(xi )bi i∈I ] for all j ∈ J, so that using rule ({ }-intro) and rule (∧-I) repeatedly we eventually get Γ [li = ?(xi )bi i∈I ] : j∈J σj → τj , which is equivalent to {lj : σj → τj j∈J }, so that we conclude by rule (≤). Reasoning in the same way we see that also the following rule is admissible: Γ Γ a : {li : ?i

i∈I

} x:σ

i∈I\{k}

b:τ , lk : σ → τ }

a.lk ? ?(x)b : {li : ?i

This has the obvious advantage that we can treat uniformly the typing of an object and of the overriding operation, so that e.g. we can give the same types, say {l0 : σ0 → τ0 , l1 : σ1 → τ1 , l2 : σ2 → τ2 }, both to o = [l0 = ?(x0 )b0 , l1 = ?(x1 )b1 , l2 = ?(x2 )b2 ] and to o = ([l0 = ?(x0 )b0 , l1 = ?(x1 )b1 , ] l1 ? ?(x1 )b1 ) l2 ? ?(x2 )b2 where o ?→ o, given that xi : σi bi : τi for i = 0, 1, 2. Beside observe that we may allow for the overriding of a method which is not in the object, namely for object extension, which is not possible in the ?-calculus. It would be surely uncorrect to step from a : {li : σi → τi i∈I } to a.li : τi , since we have never checked that a : σi , that is a (the object itself) satis?es the precondition of its method li . In [dL01,vBdL03] the same di?culty is solved by a late typing of the self, that is by checking the object against the precondition of the selected method just before method invocation: Γ a : {li : σi → τi Γ

i∈I ?

} Γ

a : σk

a.lk : τk

(k ∈ I)

This should be contrasted to the type systems of the ?-calculus in [AC96], where e.g. the rule to type an object [li = ?(xi )bi i∈I ] by A = [lk : Bk k∈I ] is 7

Barbanera, de’Liguoro

?

Commutativity and distributivity of |

(| 1) σ | τ τ |σ (| 2) (σ | τ ) | γ σ | (τ | γ)

?

Axioms for ω

(ω1) σ ≤ ω (ω2) σ σ|ω (ω3) σ → ω ≤ ω → ω

?

Distributivity of ∧

[ [ (a[ ] ∧) a[ σ ∧ τ ] (.∧) m .(σ ∧ τ ) [ [ a[ σ ] ∧ a[ τ ] m .σ ∧ m .τ ({ }∧2) {li : σi

i∈I } i∈I {li

(| ∧)

σ | (τ ∧ γ)

(σ | τ ) ∧ (σ | γ)

({ }∧1) {l : σ} ∧ {l : τ } ≤ {l : σ ∧ τ } (

?

: σi }

∧)

l ?σ ∧ l ?τ ≤ l ?σ∧τ

Sequentialization

(. |1 ) m .σ | τ ≤ m .(σ | τ ) (. |2 ) m .σ | n .τ m .(σ | n .τ ) ∧ n .(m .σ | τ )

?

Reduction

[ [ [ [ (in) a[ in b.σ | τ ] | b[ γ ] ≤ b[ a[ σ | τ ] | γ ] [ [ [ [ (|) a[ b[ out a.σ | τ ] | γ ] ≤ a[ γ ] | b[ σ | τ ] [ (open) open a.σ | a[ τ ] ≤ σ | τ (out-in) in a.out a.in a.σ ≤ in a.σ (in-out) out a.in a.out a.σ ≤ out a.σ (comm-1)({l : σ → τ } ∧ σ) | l ≤ τ (comm-2){li : ?i

i∈I }

| lk ? ? ≤ {li : ?i

i∈I\{k} , l

k

: ?}

Fig. 5. Type Entailment Rules, Part I

E, xi : A

bi : Bi

?i ∈ I

E [li = ?(xi )bi i∈I ] : [lk : Bk k∈I ] That is: all relevant information has to be assumed of the self variables xi , and it is coded in their type A which has to be the same as that of the object 8

Barbanera, de’Liguoro

?

Congruence

σ≤τ [ (cg ? M[ ]) [ [ a[ σ ] ≤ a[ τ ] σ≤γ (cg? |) τ ≤γ (cg ? ) (cg ? act) σ≤τ m .σ ≤ m .τ σ≤τ l?σ ≤ l?τ

σ|τ ≤γ|γ σ≤τ

(cg ? { })

{l : σ} ≤ {l : τ }

?

Transitivity

σ≤τ (trans) τ ≤γ σ≤γ

?

Logical

(∧ ? id) (∧ ? r) (∧? ≤) σ ≤σ∧σ σ∧τ ≤τ σ≤σ τ ≤τ (∧ ? l) (→ ?) (→ ?) σ∧τ ≤σ (σ → τ ) ∧ (σ → τ ) ≤ σ → (τ ∧ τ ) σ≥σ τ ≤τ

σ∧τ ≤σ ∧τ

σ→τ ≤σ →τ

Fig. 6. Type Entailment Rules, Part II

(hence the same for all i). We call this an early typing of the self. This choice makes it clear what the self variables stay for, and that objects are in fact recursive records, but causes lots of troubles when dealing with object modi?cation and extension, which are essential features of object based languages in practice. Such problems become even more apparent when mobility is involved, since we cannot know in advance in which ambient the methods of an object will be actually invoked, nor whether the object will be modi?ed before the invocation. Consequently, the impact of early typing of the self in such cases would be very restrictive. As it is the case of [CD01], the essential properties of typing are invariance under structural equivalence and, more importantly, subject expansion. Now a | l ?→ a.l, and suppose that we have a.l : τ since a : {l : σ → τ } ∧ σ; this implies that we can type a | l by ({l : σ → τ } ∧ σ) | l . This forces to us the type inequality: ({l : σ → τ } ∧ σ) | l ≤ τ which implies a | l : τ by (≤). Similarly for overriding we have the schema: {li : ?i

i∈I

} | lk ? ? ≤ {li : ?i 9

i∈I\{k}

, lk : ?}.

Barbanera, de’Liguoro

5

Invariance under Congruence and Expansion

To establish the invariance of types under congruence and expansion we need a ?rst lemma, essentially reversing the derivation rules. Lemma 5.1 (Generation Lemma) (i) Γ (ii) Γ (iii) Γ (iv) Γ 0 : σ i? σ ω; m . P : σ i? Γ [ a[ P ] : σ i? Γ P | Q : σ i? Γ P : τ and m . τ ≤ σ for some τ ; [ P : τ and a[ τ ] ≤ σ for some τ ; P : τ, Γ Q : ρ and τ | ρ ≤ σ for some τ, ρ;

(v) Γ !P : σ i? Γ τ1 , . . . , τ n .

P : τi for (1 ≤ i ≤ n) and τ1 | . . . | τn ≤ σ for some bj : τj , and {lj : σj → τj

j∈J

(vi) Γ [li = ?(xi )bi i∈I ] : σ i? Γ, xj : σj for some J ? I, σj and τj ; (vii) Γ a.l : τ i? Γ

} ≤ σ,

a : {l : σ → τ } ∧ σ and τ ≤ τ , for some σ and τ ; b : τ and

(viii) Γ a.lk ? ?(x)b : σ i? Γ a : {li : σi i∈I }, Γ, x : σ {li : σi i∈I\{k} , lk : σ → τ } ≤ σ, for some I, σi , σ and τ ; (ix) γ (x) γ l : σ i? l ≤σ l ? ?(x)b : σ i? Γ, x : σ

b : τ where l ? σ → τ ≤ σ.

Lemma 5.1 is proved using similar techniques as in the λ-calculus case, e.g. in [BCD83], because rule (≤) does not commute with the arrow introduction in rule ({ }-I). By the way we cannot have in the present setting a conjunctive normal form of normal types as it happens in [CD01], where only the ambient part of the calculus is dealt with. Lemma 5.2 (Subject Congruence) If P ≡ Q and Γ P : σ then Γ Q : σ Proof. By induction on the de?nition of ≡, using Lemma 5.1. Theorem 5.3 (Subject Expansion) ? If P ?→ Q and Γ Q : σ then Γ P : σ. Proof. By induction on the de?nition of ?→, using Lemma 5.1 and Lemma 5.2. 2 [ We observe that subject reduction does not hold: n[ 0 ] | open n . 0 has [ type n[ ω ] (among others), but it reduces to 0 | 0 ≡ 0 which is only typable by ω or equivalent types. 10 2

Barbanera, de’Liguoro

6

Type Semantics and Completeness Theorem

Given that P 0 is the set of closed terms, and P[x] the set of terms whose free variables are included in {x}, we de?ne a type interpretation which is essentially based on the concept of saturated sets used e.g. in [Kri90]. They are subsets of P 0 , closed under expansion. This happens to be the same interpretation of types given in [dL01] to characterize convergence in the ?calculus, and in [CD01] to model the MA calculus. The following de?nition is a bit more involved because we do not have λ-abstractions in the syntax to interpret arrow types, namely types in TF , which occur in the typing of objects. De?nition 6.1 We de?ne by mutual induction the maps [[ ]]P : TP → ?(P 0 ) and [[ ]]F : TF × Var → ?( x∈Var P[x]) as follows: (i) [[ω]]P = P 0 (ii) [[σ ∧ τ ]]P = [[σ]]P ∩ [[τ ]]P (iii) [[M . σ]]P = {P ∈ P 0 : ?Q ∈ [[σ]]P . P ?→ M . Q} [ [ (iv) [[n[ σ ] ]]P = {P ∈ P 0 : ?Q ∈ [[σ]]P , R ∈ P 0 . P ?→ n[ Q ] | R} (v) [[(σ | τ )]]P = {P ∈ P 0 : ?Q ∈ [[σ]]P , R ∈ [[τ ]]P . P ?→ Q | R} (vi) [[ l ]]P = {P ∈ P 0 : P ?→ l } (vii) [[ l ? ? ]]P = {P ∈ P 0 : ? ?(x)b. P ?→ l ? ?(x)b , b ∈ [[?]]F (x)} (viii) [[{li : ?i i∈I }]]P ? = {P ∈ P 0 : ?o. P ?→ o & ? i ∈ I ? li = ?(xi )bi ∈ o. bi ∈ [[?i ]]F (xi )} (ix) [[σ → τ ]]F (x) = {b ∈ P[x] : ?P ∈ [[σ]]P . b{P/x} ∈ [[τ ]]P } (x) [[? ∧ ψ]]F (x) = [[?]]F (x) ∩ [[ψ]]F (x) Lemma 6.2 (i) For all σ, τ ∈ TP , if σ ≤ τ then [[σ]]P ? [[τ ]]P . (ii) For all ?, ψ ∈ TF , if ? ≤ ψ then [[?]]F (x) ? [[ψ]]F (x), for all x ∈ Var. De?nition 6.3 Let Γ = {x1 : σ1 , . . . , xk : σk }, P ∈ P. σ ∈ TP and ? : Var → P 0 is a substitution, and P ? is the result of substituting ?(x) for x in P for each free variable x of P , avoiding variable clashes by renaming bound variables. Then we de?ne: (i) ? |= Γ if ?(xi ) ∈ [[σi ]]P , for all 1 ≤ i ≤ k; (ii) Γ |= P : σ if for all ? such that ? |= Γ, it is the case that P ? ∈ [[σ]]P . Lemma 6.4 (Soundeness) If Γ P : σ then Γ |= P : σ. P : σ, using theorem 5.3 and 2

? ? ? ? ?

Proof. By induction on the derivation of Γ lemma 6.2. 11

Barbanera, de’Liguoro

Theorem 6.5 (Completeness) Γ P : σ ? Γ |= P : σ.

Proof. The only if part is lemma 6.4. To prove the if part we reason by induction on the size of σ. We report some interesting cases only (the others are either immediate consequence of the induction hypothesis, or they are similar to the proofs of analogous results in [dL01,CD01]) Case l ? ? : given any closed substitution ? such that ? |= Γ, we know ? that P ? ?→ l ? ?(x)b , for some b ∈ [[?]]F (x). Now ? = j∈J (σj → τj ), and clearly [[?]]F (x) = [[σj → τj ]]F (x),

j∈J

being J ?nite, so that b ∈ [[σj → τj ]]F (x) for all j ∈ J. Let Q ∈ [[σJ ]]P be arbitrarily chosen, and ? be the same as ? but for ? (x) = Q. Then ? |= Γ, x : σj and that b? = b{Q/x} ∈ [[τJ ]]P , namely that Γ, x : σj b : τj by induction, since the size of τj has to be smaller than the size of ?. By this we deduce Γ l ? ?(x)b : l ? σj → τj for all j ∈ J by rule (MsgUpdate), and eventually Γ l ? ?(x)b : l ? ? by rules (∧-I) and (≤). The thesis then follows by theorem 5.3. Case {li : ?i i∈I }: in this case we have that P ? ?→ o and that bi ∈ [[?i ]]F (xi ) for all li = ?(xi )bi ∈ o. By reasoning in a similar way as in the previous case, this time using rule ({ }-I), we conclude that Γ o : {li : ?i } for all i ∈ I, end hence Γ o : {li : ?i i∈I } by rules (∧-I) and (≤). Again the thesis follows by 5.3. 2 The completeness theorem has relevant consequences. First we have a model, properly a ?lter model, of the calculus. Closed terms P ∈ P 0 denote ?lters of types, namely upward sets closed under ∧, by setting [[P ]] = {σ ∈ TP : P ∈ [[σ]]P }. By theorem 6.5 we have that [[P ]] = {σ ∈ TP : P : σ}

?

By introducing the notion of environments ξ, assigning ?lters to term variables, and setting ξ |= Γ if σ ∈ ξ(x) whenever x : σ ∈ Γ, we have for arbitrary terms P ∈ P: [[P ]]ξ = {σ ∈ TP : ?Γ. ξ |= Γ & Γ P : σ}. Second we have a framework to logically characterize the capabilities that a process term P exhibits in one of its reducts by inspecting its typings. In fact it is not di?cult to de?ne a convergence predicate ? by combining 12

Barbanera, de’Liguoro

the de?nitions in [dL01] and [CD01], and then use theorem 6.5 to show that [ P : n[ ω ] if and only if P ? n (namely it reduces to a parallel of processes having at top level an ambient named n), or that P : {l : ω → ω} if and ? only if P ? l (that is P ?→ o and o is an object that reacts to the message l ).

7

Conclusion

The type assignment systems for ?-calculus and the MA calculus smoothly combine into a system for a calculus of mobile objects. Essential properties, namely type invariance under expansion of subjects, completeness and adequacy of the assignments system with respect to an observational semantics based on capabilities of reducts, the construction of a logical model of properties, are retained by the resulting system. Full abstraction remains to be investigated (but then we need something like the self-open capability of [CD01], at least). More interesting would be a study of general methods to compose sequential and mobile/concurrent calculi in such a way that their assignment systems compose, namely their semantics.

Acknowledgements

The authors are very grateful to Pia and Daniela for their support.

References

[AC96] M. Abadi, L. Cardelli, A Theory of Objects, Springer 1996. [AKPG01] T. Amtoft, A.J. Kfoury, S.M. Pericas-Geertsen, “What are Polymorphically-Typed Ambients?”, LNCS 2028, 2001, pp. 206–224 [BCC01] M. Bugliesi, G. Castagna, S. Crafa, “Subtyping and Matching for Mobile Objects”, LNCS 2202, 2001, pp 235–255. [BCD83] H.P. Barendregt, M. Coppo, M. Dezani, “A Filter Lambda Model and the Completeness of Type Assignment”, JSL 48, 1983, 931-940. [vBdL03] S. van Bakel, U. de’Liguoro, “Logical Semantics for the First Order ?Calculus”, LNCS 2841, 2003, 202–215. [CD01] M. Coppo and M. Dezani-Ciancaglini “A fully abstract model for mobile ambients” ENTCS 62, 2002. [CG00] L. Cardelli, A.D. Gordon, “Mobile Ambients”, TCS 240/1, 2000, pp 177– 213. [DGdL98] M. Dezani, E. Giovannetti, U. de’ Liguoro, “Intersection types, λ-models and B¨hm trees”, in M. Takahashi, M. Okada, M. Dezani eds., Theories of o Types and Proofs, Mathematical Society of Japan, vol. 2, 1998.

13

Barbanera, de’Liguoro

[Lan01] C. Laneve, “Inheritance in Concurrent Objects”, in Formal Methods for Distributed Processing, An Object Oriented Approach H. Bowman, J. Derrick eds. Cambridge University Press, 2001. [dL01] U. de’ Liguoro “Characterizing convergent terms in object calculi via intersection types” LNCS 2044, 2001, 315–328. [Kri90] J.L. Krivine, Lambda-calcul, types et mod`les, Masson 1990. e

14