A.14 Lemma Term Substitution Preserves Typing

 < Free Open Study > 



A.14 Lemma [Term Substitution Preserves Typing]

If Г, and , where , then for some C <: D.

Proof: By induction on the derivation of Г, . The intuitions are exactly the same as for the lambda-calculus with subtyping; details vary a little, of course. The most interesting cases are the last two.

Case T-VAR:

t = x

x:D Î Г

If , then the result is trivial since . On the other hand, if x = xi and D = Bi, then, since , letting C = Ai finishes the case.

Case T-FIELD:

t = t0.fi

Г,

D = Ci

By the induction hypothesis, there is some C0 such that and C0 <: D0. It is easy to check that for some . Therefore, by T-FIELD, .

Case T-INVK:

By the induction hypothesis, there are some C0 and such that:

By Lemma A.13, . Moreover, by the transitivity of <:. Therefore, by T-INVK, .

Case T-NEW:

By the induction hypothesis, for some with . We have by the transitivity of <:. Therefore, by T-NEW, .

Case T-UCAST:

t = (D)t0

Г,

C <: D

By the induction hypothesis, there is some E such that and E <: C. We have E <: D by the transitivity of <:, which yields by T-UCAST.

Case T-DCAST:

t = (D)t0

Г,

D <: C

D C

By the induction hypothesis, there is some E such that and E <: C. If E <: D or D <: E, then by T-UCAST or T-DCAST, respectively. On the other hand, if both D : E and E : D, then (with a stupid warning) by T-SCAST.

Case T-SCAST:

t = (D)t0

Г,

D : C

C : D

By the induction hypothesis, there is some E such that and E <: C. This means that E D. (To see this, note that each class in FJ has just one super class. It follows that, if both E <: C and E <: D, then either C <: D or D <: C.) So (with a stupid warning), by T-SCAST.



 < Free Open Study > 



Types and Programming Languages
Types and Programming Languages
ISBN: 0262162091
EAN: 2147483647
Year: 2002
Pages: 262

flylib.com © 2008-2017.
If you may any questions please contact us: flylib@qtcs.net