We check that no case listed in
Definition 1 (Section 6.1)
can occur.
No free variables.
By definition of type judgments, since (1) hold,
every free object name in D, with y x # D Î D,
should appear as a leaf of the proof tree of Ay|- D :: Ax.
This leaf must be of the form Ay+ A' |- x : t. This implies
that x belongs to the domain of Ay because x is free in D.
Similarly, every class variable in D should belong to the domain of Ay,
which actually only contains object names.
The proof is similar for free names in P using (2).
where (5) is an instance of Private-Message. The premise
of (5) requires that x : " X.(l : (tii Î I); B') be in Ay. Therefore, by definition of Ay, variable x must
appear in y. Furthermore, by well-formedness of chemical solutions, a
name can have a unique prefix. Since y' is already a prefix of x, then
y must be of the form y' x y''.
(no undeclared label) We show that l Î dl(D).
Given (4), the judgment Ay' |- D :: Ax, where
Ax = x: " X. r, x: " X.(B | F ),
follows by rule Definition applied to (1) with the premises
below:
Since Ay|- x.l (u) by (2), either r is of the form [l : t; r'] or B is of the
form (l : t; B') depending on whether l is public or
private. In each case, using (7), l is in dom(B).
The conclusion follows by Lemma 7.
(no arity mismatch)
Let D be of the form [M |> P] where M is itself
of the form l(y) & J. We show that y and u have the
same arities.
For that purpose, it suffices to show that the type of u and
the type of y in A are instances of a same tuple type.
A leaf of (6) must be
dom(A') = fn(M) Ay' + x : [r], x : (B | F)+ A' |- P
Ay' + x : [r], x : (B | F) |- M |> P :: z(r)Bcl(M),Ø
Therefore, the type of y in A' is B(l). By rules
Chemical-Solution and Definition, A contains a
generalization of
x : [r], x : (B | F).
Thus,
the type of x.l in Ay is a generalization of B(l). The proof tree illustrated
in item 1 is required to prove Ay |- x.l (uii Î I).
Then, as a consequence of rule (5),
the type of u is an instance of the type of x.l in Ay, i.e. of the generalization of the type of y in A'.
No class rewriting failure.
Let y # P Î P, P = objx = CinitQinQ', rule
Class-Red does not apply to P, i.e. there is no C' such that C
|-x® C',
and P is not a refinement error. We show that P is not a failure;
namely, for every evaluation context E,
C ¹ E{c}, and c is free.
By (1), dom(A) only contains object names. Therefore, by (2),
P cannot contain free class names.
Let E {L} = C' orL (the case
E {L} = LorC' is similar). We demonstrate that, if A' |- C' orL
:: z(r)BW,V then L Í V.
By rule Abstract, A' |- L :: z(r)B1Ø,L(8).
Let A' |- C' :: z(r)B2W2,V2(9) and
V1' = L \( dom(B2) \ V2) (10) and
V2' = V2 \( dom(B1) \ L) (11).
Since there does not exists C'' such that C |-x® C'',
the rule Abstract-Cut cannot be applied.
This means that L = L \
dl(C') = L \ dom(B2), which implies V1' = L. By (8),
(9), (10), (11) and rule Disjunction we obtain
A' |- CorL :: z(r)(B1 Å B2)W1 È W2, L È
V2'(12).
On the other hand, by (2), a derivation of Ay|- P
must contain (P = objx = CinitQinQ')
