Subject reduction for the chemical semantics (Theorem 1.1)

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':

an instance of rule Obj, followed by a sequence of Chemistry-Obj;
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 (A^j |- D' :: A_z)^{j z # D' Î
D} (2), A^y |- obj x = D init P in Q and (A^j |- P')^{j # P' Î P} (3), where A = È_{j z # D' Î D} A_z. A derivation of A^y |- obj x = D init P in Q must have the form:

[Object]

A^y |- self(x) D :: z(r)B ^W,Ø (4)

X = Gen (r, B, A^y) \ ctv(B|W) (5) A^y + x : " X. [r], x : " X. (B | F) |- P (7)

r = B | M (8) A^y+ x : " X. [r] |- Q (9)

A^y |- 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 = A^y + 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(A^y) È ctv(B|W))

X' = (ftv(B) È ftv(r)) \ (ftv(A'^y) È ctv(B|W))

Since A'^y is equal to A^y + x : " X. r and A^y 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 A_x = A'_x. Therefore, A'^{y x} is equal to A^{y 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 ||- P₁, P º stackrel ¾® D ||- P₂, 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 A^y |- P & Q and A^y |- P, A^y |- 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 A^y |- D :: A_x and A^y' |- x. m(u) (1). We must show that A^{y x} |- x.m (u_i ^{i Î I}) where u = u_i ^{i Î I}. A complete derivation of (1) must be of the form:

[Send]

[Message]

[Object-Var]

...

A^y' |- x : [ m : (t_i ^{i Î I}); r ]

A^y' |- x.m : (t_i ^{i Î I})

(

Object-Var

...

A^y' |- u_i : t_i

)

^{i Î I}

A^y' |- x.m (u_i ^{i Î I})

This derivation, which does not use any internal type assumption of A (any Private-Message rule), is not affected by replacing A^y' with A^{y x}. Thus, A^{y x} |- x.m (u_i ^{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 A^y |- D :: A_x and A^{y x y'} |- x. f(u) (1). We must show that A^{y x} |- x.f (u_i ^{i Î I}) where u = u_i ^{i Î I}. A complete derivation of (1) must be of the form:

[Send]

Private-Message

x : " X. (f : (t_i ^{i Î I}); B) Î A^{y x y'}

A^{y x y'} |- x.f : (t_i{a ¬ g_a^{a Î X}}^{i Î I})

(

Object-Var

...

A^{y x y'} |- u_i : t_i {a ¬ g_a^{a Î X}}

)

^{i Î I}

A^{y x y'} |- x.f (u_i ^{i Î I})

Note that, the only internal type assumption in the premise is on x, which remains in A^{y x}. Thus, as in case Public-Comm, we can replace A^{y x y'} by A^{y x} in this derivation and conclude that A^{y x} |- x. f(u_i ^{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Î I}l_i(x_i). 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} A_z) È A_x	(1)
(A^j \|- D'' :: A_z) ^{j z # D'' Î D}	(2)
A^y \|- D :: A_x	(3)
A^{y x} \|- x.(M s)	(4)
(A^j \|- P')^{j # P' Î P}	(5)

The derivation of (3) must end with rule Definition with the premises

	A_x = x : " X. [ r ], x : " X. (B \| F)	(6)
	r = B \| M	(7)
	X = Gen (r, B, A^y) \ ctv(B\|W)	(8)
	A^y \|- self(x) D :: z(r)B^W,Ø	(9)

To demonstrate |- ( D, y x # D ||- y x # (Ps), P) it suffices to show that A^y |- Ps. Note that A^{y x} = A^y + A_x follows from (1). The derivation of (4) must end with a rule Join-Parallel. Hence, for each message l_i (s (x_i)) of M s, we have A^y + A_x |- x.l_i (s(x_i)). In turn, this must be derived by rule Send with the premises A^y + A_x |- x.l_i : t_i (10) and A^y + A_x |- s(x_i) : t_i (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 t_i is an instance of the generic type " X. B(l_i), with a substitution h_i of domain in X Ç ftv(B(l_i)).

The derivation of (9) must contain a sub-derivation

Reaction

A' |- M :: B₀ (12) A^y+ x : [r], x :(B| F) + A' |- P (13) dom(A') = fn(M)

Sub

A^y + x : [r], x :(B| F) |- M |> P :: z(r)B₀^cl(M),Ø

A^y + x : [r], x :(B| F) |- M |> P :: z(r)B₀^W,Ø (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 B₀ 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' |- l_i(x_i) :: l_i : B(l_i) (16)

for every i Î I. By (15) and the definitions of cl(B) and ctv(B|W), we have ftv(B (l_i)) Ç ftv(B(l_j)) Í ctv(B|W), hence by (8), ftv(B (l_i)) Ç ftv(B(l_j)) Ç X = Ø, for every distinct i and j in I. Thus, the sets (X Ç ftv(B(l_i)))^{i Î I}, i.e. dom(h_i)^{i Î I} form a partition of X. Let h be the sum of substitutions Å^{i Î I} h_i. Observe that the domain of h is included in X and is thus disjoint from free type variables of A^y (17).

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