28.6 Joins and Meets

 < Free Open Study > 



28.6 Joins and Meets

We saw in §16.3 that a desirable property of languages with subtyping is the existence of a join for every pair of types S and Tthat is, a type J that is minimal among all the common supertypes of S and T. We show in this section that the subtype relation of kernel F<: does indeed have a join for every S and T, as well as a meet for every S and T with at least one subtype in common, by giving algorithms for calculating them. (On the other hand, both of these properties fail for full F<:; see Exercise 28.6.3.)

We write Г S V T = J for "J is the join of S and T in context Г" and Г S T = M for "M is the meet of S and T in Г." The algorithms for calculating these relations are defined simultaneously, in Figure 28-5. Note that some of the cases in each definition overlap; to read the definitions as deterministic algorithms, we stipulate that the first clause that applies is always chosen.


Figure 28-5: Join and Meet Algorithms for Kernel F<:

It is easy to check that V and are total functions, in the sense that V always returns a type and either returns a type or fails. We just observe that the total weight (cf. Definition 28.3.4) of S and T with respect to Г is always reduced in recursive calls.

Now let us verify that these definitions actually calculate joins and meets. The argument is divided into two parts: Proposition 28.6.1 shows that the calculated join is an upper bound of S and T and the meet (when it exists) is a lower bound; Proposition 28.6.2 then shows that the calculated join is less than every common upper bound of S and T and that the meet is greater than every common lower bound (and exists whenever S and T have a common lower bound).

28.6.1 Proposition:

  1. If Г S V T = J, then Г S <: J and Г T <: J.

  2. If Г S T = M, then Г M <: S and Г M <: T.

Proof: By a straightforward induction on the size of a derivation of Г S V T = J or Г S T = M (i.e., the number of recursive calls needed to calculate J or M).

28.6.2 Proposition:

  1. If Г S <: V and Г T <: V, then Г S V T = J for some J with Г J <: V.

  2. If Г L <: S and Г L <: T, then Г S T = M for some M with Г L <: M.

Proof: It is easiest to prove the two parts by simultaneous induction on the total sizes of algorithmic derivations of and for part 1 and of and for part 2. (Theorem 28.3.3 assures us that these algorithmic counterparts of the given derivations always exist.)

  1. If either of the two derivations is an instance of SA-Top, then V = Top and the desired result, is immediate.

    If the derivation of is an instance of SA-REFL-TVAR, then T = V. But then the first given derivation tells us that Г S <: V = T, so the first clause in the definition of the join applies, giving us Г S V T = T and satisfying the requirements. Similarly, if the derivation of is an instance of SA-REFL-TVAR, then S = V. But then the second given derivation tells us that Г T <: V = S, so the second clause in the definition of the join applies, giving us Г S V T = S and again satisfying the requirements.

    If the derivation of ends with an instance of SA-TRANS-TVAR, then we have S = X with X<:U Î Г and a subderivation of Г U V T = J. The third clause in the definition of the join gives us Г S V T = J, and the induction hypothesis yields Г J <: V. Similarly if the derivation of ends with SA-TRANS-TVAR.

    It is now easy to check, from the form of the algorithmic subtyping rules, that the only remaining possibilities are that both of the given derivations end with either SA-ARROW or SA-ALL.

    If both end with SA-ARROW, then we have S = S1S2, T = T1T2, and V = V1V2, with , , , and . By part (2) of the induction hypothesis, Г S1 T1 = M1 for some M1 with Г V1 <: M1, and by part (1), Г S2 V T2 = J2 for some J2 with Г J2 <: V2. The fifth clause in the definition of joins gives us Г S1S2 V T1T2 = M1J2, and we obtain Г M1J2 <: V1V2 by S-ARROW.

    Finally, if both of the given derivations end with SA-ALL, then we have S = "X<:U1 .S2, T = "X<:U1T2, and V = "X<:U1 .V2, with Г, and Г, . By part (1) of the induction hypothesis, Г, X<:U1 S2 V T2 = J2 with Г, . The sixth clause in the definition of joins gives us J = "X<:U1 .J2, and we obtain Г "X<:U1 .J2 <: "X<:U1 .V2 by S-ALL.

  2. If the derivation of ends in SA-TOP, then T is Top, so Г S <: T and, from the first clause of the definition of the meet, Г S T = S. But, from the other given derivation, we know that Г L <: S, so we are finished. Similarly if the derivation of ends in SA-TOP.

    If the derivation of ends in SA-REFL-TVAR, then L = S and the other given derivation tells us Г L = S <: T, from which the definition of the meet yields Г S T = S and we are done. Similarly if the derivation of ends in SA-REFL-TVAR.

    The only remaining possibilities are that both of the given derivations end with SA-TRANS-TVAR, SA-ARROW, or SA-ALL.

    If both derivations end with SA-TRANS-TVAR, then we have L = X with X<:U Î Г and two subderivations and . By part (2) of the induction hypothesis, Г U <: M, from which we obtain Г L <: M from S-TVAR and transitivity.

    If both derivations end with SA-ARROW, then we have S = S1S2, T = T1T2, and L = L1L2, with , , , and . By part (1) of the induction hypothesis, Г S1 V T1 = J1 for some J1 with Г J1 <: L1, and by part (2), Г S2 T2 = M2 for some M2 with Г L2 <: M2. The definition of meets tells us that Г S1S2 T1T2 = J1M2, and we obtain Г L1L2 <: J1M2 by S-ARROW.

    The case where both derivations end with SA-ALL is similar.

28.6.3 Exercise [Recommended, ⋆⋆⋆]:

Consider the pair of types (due to Ghelli, 1990) S = "X<:YZ.YZ and T = "X<:Y′→Z.Y′→Z and the context Г = Y<:Top, Z<:Top, Y<:Y, Z<:Z. (1) In full F<:, how many types are there that are subtypes of both S and T under Г? (2) Show that, in full F<:, the types S and T have no meet under Г. (3) Find a pair of types that has no join under Г in full F<:.



 < 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