Previous Up Next
B.2 Subject reduction for the chemical semantics (Theorem 1.1)

Proof:
Let |- ( D ||- P) and D ||- P   stackrel   D' ||- P'. We demonstrate that |- ( D' ||- P'). According to the rules in Figure 6, there are two cases for the proof of D ||- P   stackrel   D' ||- P':
  1. an instance of rule Obj, followed by a sequence of Chemistry-Obj;

  2. an instance of one of the rules Par, Nil, Public-Comm, Private-Comm, Red, followed by a sequence of Chemistry.
We discuss the two cases separately.

Case 1.
The reduction is D ||- y   #  obj x = D init P in Q,   P D, y x   #  D ||- y x   #  P, y   #  Q,   P, where x fn( D) fn( P).


On the one hand, if |- ( D ||- y   #  obj x = D init P in Q,   P(1) and rule Chemical-Solution, we obtain (Aj |- D' :: Az)j z   #  D' D (2), Ay |- obj x = D init P in Q and (Aj |- P')j   #  P' P (3), where A = j z   #  D' D   Az. A derivation of Ay |- obj x = D init P in Q must have the form:
[Object]
Ay |- self(xD :: z(r)B W, (4)
X = Gen (r, B, Ay) \ ctv(B|W(5)      Ay + x : " X. [r], x : " X. (B | F) |- P (7)
r = B | M (8)      Ay+ x : " X. [r] |- Q (9)
Ay |- obj x = D init P in Q
On the other hand, if |- ( D, y x   #  D ||- y x   #  P, y   #  Q,   P(10) and rule Chemical-Solution, we obtain (A'j |- D' :: A'z)j z   #  D' D (11), A'y |- D :: A'x, A'y x |- P (12), A'y |- Q (13) and (A'j |- P')j   #  P' P (14) where A' = (j z   #  D' D   A'z) A'x. A derivation of A'y |- D :: A'x must have the form:
[Definition]
A'y |- self(xD :: z(r') B'W',  (15)
r' = B' | M (16)      X' = Gen (r', B', A'y) \ ctv(B'|W') (17)
A'y |- D :: A'x
where A'x = x : " X'. [ r ] x : " X'. (B' | F).

Note that, by definition, A does not bind x because x fn( D). Therefore, by Lemma 2, if either (1) or (10) hold, then we can always choose A or A' such that A' = A + A'x, the judgments (2) and (11) be equivalent, as well as the judgments (3) and (14). We now focus on the other judgments.

Then, since A'y = Ay + x : " X'.   [r'], the following premises can be made equivalent to one another: To conclude, if (1) holds, then (10) holds by taking A + x : " X. [ r ], x : " X. (B | F) for A', and conversely, if (10) holds, then (1) holds by taking A' \ x for A.

Case 2.
The reduction is D ||- P1,   P stackrel D ||- P2,   P. There are several subcases, according to the leaf node in the proof tree.

Nil.
The equivalence is D ||- y   #  0, P D ||- P. Indeed the judgment A |- y   # 0 is always true, for any environment A.

Par.
The equivalence is D ||- y   # (P & Q), P D ||- y   #  P, y   #  Q, P. We apply rule Chemical-Solution, then it suffices to prove that the two judgments Ay |- P & Q and Ay |- P, Ay |- Q are equivalent. This follows by rules Parallel and Chemical-Solution.

Join.
This is similar to the above case, and relies on rules Chemical-Solution, Parallel and Join-Parallel.

Public-Comm.
The reduction is D, y x   # D ||- y'   #  x. m(u), P D, y x   # D ||- y x   #  x. m(u), P. Let us assume that Ay |- D :: Ax and Ay' |- x. m(u(1). We must show that Ay x |- x.m (ui i I) where u = ui i I. A complete derivation of (1) must be of the form:
[Send]
[Message]
[Object-Var]
...
Ay' |- x : [ m : (ti i I); r ]
Ay' |- x.m : (ti i I)
     (
Object-Var    
...
Ay' |- ui : ti
) i I
Ay' |- x.m (ui i I)
This derivation, which does not use any internal type assumption of A (any Private-Message rule), is not affected by replacing Ay' with Ay x. Thus, Ay x |- x.m (ui i I) holds.

Private-Comm.
The reduction is D, y x   # D ||- y x y'   #  x. f(u), P D, y x   # D ||- y x   #  x. f(u), P. Let us assume that Ay |- D :: Ax and Ay x y' |- x. f(u(1). We must show that Ay x |- x.f (ui i I) where u = ui i I. A complete derivation of (1) must be of the form:
[Send]
Private-Message    
x : " X. (f : (ti i I); B) Ay x y'
Ay x y' |- x.f : (ti{a gaa X}i I)
     (
Object-Var    
...
Ay x y' |- ui : ti {a gaa X}
) i I
Ay x y' |- x.f (ui i I)
Note that, the only internal type assumption in the premise is on x, which remains in Ay x. Thus, as in case Public-Comm, we can replace Ay x y' by Ay x in this derivation and conclude that Ay x |- x. f(ui i I).

Red.
The reduction is D, y x   #  D ||- y x   #  x.(Ms), P D, y x   #  D ||- y x   #  (Ps), P, where D is of the form M |> P or D' and M is of the form &i Ili(xi). A derivation of |- ( D, y x   #  D ||- y x   #  x.(Ms), P) must follow from rule Chemical-Solution with the following premises:
A = (j z   #  D'' D Az) Ax (1)
(Aj |- D'' :: Az) j z   #  D'' D (2)
Ay |- D :: Ax (3)
Ay x |- x.(M s) (4)
(Aj |- P')j   #  P' P (5)
The derivation of (3) must end with rule Definition with the premises
  Ax = x : " X. [ r ], x : " X. (B | F) (6)
  r = B | M (7)
  X = Gen (r, B, Ay) \ ctv(B|W) (8)
  Ay |- self(xD :: z(r)BW, (9)
To demonstrate |- ( D, y x   #  D ||- y x   #  (Ps), P) it suffices to show that Ay |- Ps. Note that Ay x = Ay + Ax follows from (1). The derivation of (4) must end with a rule Join-Parallel. Hence, for each message li (s (xi)) of M s, we have Ay + Ax |- x.li (s(xi)). In turn, this must be derived by rule Send with the premises Ay + Ax |- x.li : ti (10) and Ay + Ax |- s(xi) : ti (11). The judgment (10) is derived by either rule Private-Message or Message, depending on whether l is private or public. In both cases, each tuple ti is an instance of the generic type " X. B(li), with a substitution hi of domain in X ftv(B(li)).

The derivation of (9) must contain a sub-derivation
Reaction
A' |- M :: B0 (12)      Ay+ x : [r], x :(B| F) + A' |- P (13)      dom(A') = fn(M)
Sub    
Ay + x : [r], x :(B| F) |- M |> P :: z(r)B0cl(M),
Ay + x : [r], x :(B| F) |- M |> P :: z(r)B0W, (14)
where cl(M) W (15) (the judgment (14) is then combined with other judgments for other reaction rules of D by a sequence of Disjunction rules, followed by a rule Self, to end up with (9)). The internal type B0 is therefore a subset of B. As regards the premise (12), it is derived by a combination of rules Synchronization, Message-Pattern, and Empty-Pattern. Hence, we have:
A' |- li(xi) :: li : B(li(16)
for every i I. By (15) and the definitions of cl(B) and ctv(B|W), we have ftv(B (li)) ftv(B(lj)) ctv(B|W), hence by (8), ftv(B (li)) ftv(B(lj)) X = , for every distinct i and j in I. Thus, the sets (X ftv(B(li)))i I, i.e. dom(hi)i I form a partition of X. Let h be the sum of substitutions i I hi. Observe that the domain of h is included in X and is thus disjoint from free type variables of Ay (17).

Applying Lemma 3 to (13), we have h (Ay + x : [r], x :(B| F)) + h (A') |- P, that is, Ay + x : [h(r)], x : h (B| F) + h (A') |- P. By Lemma 4, we can let x be used polymorphically, i.e. Ay + Ax + h (A') |- P. Similarly, we have (Ay + Ax |- s(xi) : h(ti')) xi : ti' A' by Lemmas 3 and 4 successively applied to the collection of judgments (11). Thus, by Lemma 5, we derive Ay + Ax |- Ps.



Previous Up Next