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(x)  D :: 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(x)  D :: 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:
• (4)º (15): By Lemma 2 and identifying B' with B, r' with r, and W' with W.

• (5)º (17): By definition, we now have
 X = (ftv(B) È ftv(r)) \ (ftv(Ay) È ctv(B|W))

 X' = (ftv(B) È ftv(r)) \ (ftv(A'y) È ctv(B|W))
Since A'y is equal to Ay + x : " X. r and Ay does not bind x, we have X' Í X. Conversely, we have X \ X' Í ftv(" X. r). Since by definition ftv(" X.r) does not intersect X, it follows that X \ X' is empty, thus X Í X'.

• (7)º (12): Using the previous equivalences, we now have Ax = A'x. Therefore, A'y x is equal to Ay x.
• (9)º (13): Same reasoning as the previous case.
• (8)º (16): The two equalities are now identical.
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(x)  D :: 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.