A.10 Lemma

---

A.10 Lemma

If L <: S and L <: T, then S ∧ T = M for some M.

Proof: By induction on the size of S (or, equivalently, T), with a case analysis on the shapes of S and T. If either S or T is Top, then one of the first two cases in the definition applies, and the result is either T or S, respectively. The cases where S and T have different shapes cannot occur, since the inversion lemma for the subtype relation (15.3.2) would make inconsistent demands on the shape of L; for example, if S is an arrow, then so must L be, but if T is a record, then so is L^[1] So we have three cases left.

If both S and T are Bool, then the third case in the definition applies and we are finished.

Suppose instead that S = S₁→S₂ and T = T₁→T₂. The totality of the V algorithm tells us that the first recursive call returns some type J₁. Also, by the inversion lemma, L must have the form L₁→L₂ with L₂ <: S₂ and L₂ <: T₂. That is, L₂ is a common lower bound of S₂ and T₂, so the induction hypothesis applies and tells us that S₂ ∧ L₂ does not fail, but rather returns a type M₂. So S ∧ T = J₁→M₂.

Finally, suppose that S = {k_j:S_j ^jÎl..m} and T = {l_i:T_i ^iÎi..n}. By the inversion lemma, L must be a record type whose labels include all the labels that occur in either of S and T. Moreover, for each label in both S and T, the inversion lemma tells us that the corresponding field in L is a common subtype of the fields in S and T. This assures us that the recursive calls to the ∧ algorithm for the common labels all succeed.

Now let us verify that these definitions calculate joins and meets. The argument is divided into two parts: Proposition A.11 shows that the calculated meet is a lower bound of S and T and the join is an upper bound; Proposition A.12 shows that the calculated meet is greater than every common lower bound of S and T and the join less than every common upper bound.

^[1]Strictly speaking, Lemma 15.3.2 did not deal with Bool. The additional case for Bool just says that the only subtype of Bool is Bool itself.

---