21.9 Counting Subexpressions

< Free Open Study >

Instantiating the generic algorithm gfp^t (21.6.4) with the specific support function for the subtype relation on μ-types (21.8.4) yields the sub-typing algorithm shown in Figure 21-4. The argument in Section 21.6 shows that the termination of this algorithm can be guaranteed if is finite for any pair of μ-types (S, T). The present section is devoted to proving that this is the case (Proposition 21.9.11).

Figure 21-4: Concrete Subtyping Algorithm for μ-Types

At first glance, the property seems almost obvious, but proving it rigorously requires a surprising amount of work. The difficulty is that there are two possible ways of defining the set of "closed subexpressions" of a μ-type. One, which we call top-down subexpressions, directly corresponds to the subexpressions generated by . The other, called bottom-up subexpressions, supports a straightforward proof that the set of closed subexpressions of every closed μ-type is finite. The termination proof proceeds by defining both of these sets and showing that the former is a subset of the latter (Proposition 21.9.10). The development here is based on Brandt and Henglein's (1997).

21.9.1 Definition

A μ-type S is a top-down subexpression of a μ-type T, written S ⊑ T, if the pair (S,T) is in the least fixed point of the following generating function:

TD(R)	=	{(T,T) \| T Î T_m}
	È	{(S,T₁ × T₂) \| (S,T₁) Î R}
	È	{(S,T₁ × T₂) \| (S,T₂) Î R}
	È	{(S,T₁ → T₂) \| (S,T₁) Î R}
	È	{(S,T₁ → T₂) \| (S,T₂) Î R}
	È	{(S,μX.T) \| (S,[X ↦ μX.T]T), Î R}

21.9.2 Exercise [⋆]

Give an equivalent definition of the relation S ⊑ T as a set of inference rules.

From the definition of it is easy to see that, for any μ-types S and T, all the pairs contained in are formed from top-down subexpressions of S and T:

21.9.3 Lemma

If (S′,T′) Î , then either S′ ⊑ S or S′ ⊑ T, and either T′ ⊑ S or T′ ⊑ T.

Proof: Straightforward inspection of the definition of .

Also, the top-down subexpression relation is transitive:

21.9.4 Lemma

If S ⊑ U and U ⊑ T, then S ⊑ T.

Proof: The statement of the lemma is equivalent to "U, T. U ⊑ T ⇒ ("S. S ⊑ U ⇒ S ⊑ T).In other words, we must show that μ (TD) ⊆ R, where R = {(U,T) | "S. S ⊑ U ⇒ S ⊑ T}. By the induction principle, it suffices to show that R is TD-closed-that is, that TD(R) ⊆ R. So suppose (U,T) Î TD(R). Proceed by cases on the clauses in the definition of TD.

Case:

(U,T) = (T,T)

Clearly, (T,T) Î R.

Case:

(U,T) = (U,T₁ × T₂) and (U,T₁) Î R

Since (U,T₁) Î R, it must be the case that S ⊑ U ⇒ S ⊑ T₁ for all S. By the definition of ⊑, it must also be the case that S ⊑ U ⇒ S ⊑ T₁ × T₂ for all S. Thus, (U,T) = (U,T₁ × T₂) Î R, by the definition of R.

Other cases:

Similar.

Combining the two previous lemmas gives us the proposition that motivates the introduction of top-down subexpressions:

21.9.5 Proposition

If (S′,T′) Î , then S′ ⊑ S or S′ ⊑ T, and T′ ⊑ S or T′ ⊑ T.

Proof: By induction on the definition of , using transitivity of ⊑.

The finiteness of will follow (in Proposition 21.9.11) from the above proposition and the fact that any μ-type U has only a finite number of top-down subexpressions. Unfortunately, the latter fact is not obvious from the definition of ⊑. Attempting to prove it by structural induction on U using the definition of TD does not work because the last clause of TD breaks the induction: to construct the subexpressions of U = μX.T, it refers to a potentially larger expression [X ↦ μX.T]T.

The alternative notion of bottom-up subexpressions avoids this problem by performing the substitution of μ-types for recursion variables after calculating the subexpressions instead of before. This change will lead to a simple proof of finiteness.

21.9.6 Definition

A μ-type S is a bottom-up subexpression of a μ-type T, written S ≼ T, if the pair (S,T) is in the least fixed point of the following generating function:

BU(R)	=	{(T,T) \| T Î T_m}
	È	{(S,T₁ × T₂) \| (S,T₁) Î R}
	È	{(S,T₁ × T₂) \| (S,T₂) Î R}
	È	{(S,T₁ → T₂) \| (S,T₁) Î R}
	È	{(S,T₁ → T₂) \| (S,T₂) Î R}
	È	{([X ↦ μX.T]S,μX.T) \| (S,T) Î R}

This new definition of subexpressions differs from the old one only in the clause for a type starting with a μ binder. To obtain the top-down subexpressions of such a type, we unfolded it first and then collected the subexpressions of the unfolding. To obtain the bottom-up subexpressions, we first collect the (not necessarily closed) subexpressions of the body, and then close them by applying the unfolding substitution.

21.9.7 Exercise [⋆⋆]

Give an equivalent definition of the relation S ≼ T as a set of inference rules.

The fact that an expression has only finitely many bottom-up subexpressions is easily proved.

21.9.8 Lemma

{S | S ≼ T} is finite for each T.

Proof: Straightforward structural induction on T, using the following observations, which follow from the definition of BU and ≼:

if T = Top or T = X then {S | S ≼ T} = {T};
if T = T₁ × T₂ or T = T₁→T₂ then {S | S ≼ T} = {T} È {S | S ≼ T₁} È {S | S ≼ T₂};
if T = μX.T′ then {S | S ≼ T} = {T} {[X ↦ T]S | S ≼ T′}.

To prove that the bottom-up subexpressions of a type include its top-down subexpressions, we will need the following lemma relating bottom-up subexpressions and substitution.

21.9.9 Lemma

If S ≼ [X ↦ Q]T, then either S ≼ Q or else S = [X ↦ Q]S′ for some S′ with S′ ≼ T.

Proof: By structural induction on T.

Case:

T = Top

Only the reflexivity clause of BU allows Top as the right-hand element of the pair, so we must have S = Top. Taking S′ = Top yields the desired result.

Case:

T = Y

If Y = X, we have S ≼ [X ↦ Q]T = Q, and the desired result holds by assumption. If Y ≠ X, we have S = [X ↦ Q]T = Y. Only the reflexivity clause of BU can justify this pair, so we must have S = Y. Take S′ = Y to get the desired result.

Case:

T = T₁ × T₂

We have S ≼ [X ↦ Q]T = [X ↦ Q]T₁ × [X ↦ Q]T₂. According to the definition of BU, there are three ways in which S can be a bottom-up subexpression of this product type. We consider each in turn.

Subcase:

S = [X ↦ Q]T

Then take S′ = T.

Subcase:

S ≼ [X ↦ Q]T₁

By the induction hypothesis, either S ≼ Q (in which case we are done) or else S = [X ↦ Q]S′ for some S′ ≼ T₁. The latter alternative implies the desired result S′ ≼ T₁ × T₂ by the definition of BU.

Subcase:

S ≼ [X ↦ Q]T₂

Similar.

Case:

T = T₁→T₂

Similar to the product case.

Case:

T = μY.T′

We have S ≼ [X ↦ Q]T = μY.[X ↦ Q]T′. There are two ways in which S can be a bottom-up subexpression of this μ-type.

Subcase:

S = [X ↦ Q]T

Take S′ = T

Subcase:

S = [Y ↦ μY.[X ↦ Q]T′]S₁

with S₁ ≼ [X ↦ Q]T′

Applying the induction hypothesis gives us two possible alternatives:

S₁ ≼ Q. By our conventions on bound variable names, we know that Y ∉ FV(Q), so it must be that Y ∉ FV(S₁). But then S = [Y ↦ μY.[X ↦ Q]T′]S₁ = S₁, so S ≼ Q.
S₁ = [X ↦ Q]S₂ for some S₂ such that S₂ ≼ T′. In this case, S= [Y ↦ μY.[X ↦ Q]T′]S₁ = [Y ↦ μY.[X ↦ Q]T′][X ↦ Q]S₂ = [X ↦ Q][Y ↦ μY.T′]S₂. Take S′ = [Y ↦ μY.S′]S₂ to obtain the desired result.

The final piece of the proof establishes that every top-down subexpression of a μ-type can be found among its bottom-up subexpressions.

21.9.10 Proposition

If S ⊑ T, then S ≼ T.

Proof: We want to show that μTD ⊆ μBU. By the principle of induction, this will follow if we can show that μBU is TD-closed-that is, TD(μBU) ⊆ μBU. In other words, we want to show that (A, B) Î TD(μBU) implies (A, B) Î μBU = BU(μBU). The latter will be true if every clause of TD that could have generated (A, B) from μBU is matched by a clause of BU that also generates (A, B) from μBU. This is trivially true for all the clauses of TD except the last, since they are exactly the same as the corresponding clauses of BU. In the last clause, (A, B) = (S, μX.T) Î TD(μBU) and (S, [X ↦ μX.T]T) Î μBU or, equivalently, S ≼ [X ↦ μX.T]T. By Lemma 21.9.9, either S ≼ μX.T, which is (S, μX.T) Î μBU, what is needed, or S = [X ↦ μX.T]S′ for some S′ with (S′,T) Î μBU.The latter implies (S, μX.T) Î BU(μBU) = μBU, by the last clause of BU.

Combining the facts established in this section gives us the final result.

21.9.11 Proposition

For any μ-types S and T, the set is finite.

Proof: For S and T, let Td be the set of all their top-down subexpressions, and Bu be the set of all their bottom-up subexpressions. According to Proposition 21.9.5, . By Proposition 21.9.10, Td × Td ⊆ Bu × Bu. By Lemma 21.9.8, the latter set is finite. Therefore, is finite.

< Free Open Study >