21.8 -Types

---

21.8 μ-Types

This section develops the finite μ-notation, defines subtyping on μ-expressions, and establishes the correspondence between this notion of subtyping and the subtyping on tree types.

21.8.1 Definition

Let X range over a fixed countable set {X₁, X₂,...} of type variables. The set of raw μ-types is the set of expressions defined by the following grammar:

•  

  T

  ::=

  X

  Top

  T × T

  T→T

  μX.T

The syntactic operator μ is a binder, and gives rise, in the standard way, to notions of bound and free variables, closed raw μ-types, and equivalence of raw μ-types up to renaming of bound variables. FV(T) denotes the set of free variables of a raw μ-type T. The capture-avoiding substitution [X ↦ S]T of a raw μ-type S for free occurrences of X in a raw μ-type T is defined as usual.

Raw μ-types have to be restricted a little to achieve a tight correspondence with regular trees: we want to be able to "read off" a tree type as the infinite unfolding of a given μ-type, but there are raw μ-types that cannot be reasonably interpreted as representations of tree types. These types have subexpressions of the form μX.μX₁...μX_n.X, where the variables X₁ through X_n are distinct from X. For example, consider T = μX.X. Unfolding of T gives T again, so we cannot read off any tree by unfolding T. This leads us to the following restriction.

21.8.2 Definition

A raw μ-type T is contractive if, for any subexpression of T of the form μX.μX₁...μX_n .S, the body S is not X. Equivalently, a raw μ-type is contractive if every occurrence of a μ-bound variable in the body is separated from its binder by at least one → or ×.

A raw μ-type is called simply a μ-type if it is contractive. The set of μ-types is written T_m.

When T is a μ-type, we write μ-height(T) for the number of μ-bindings at the front of T.

The common understanding of μ-types as finite notation for infinite regular tree types is formalized by the following function.

21.8.3 Definition

The function treeof, mapping closed μ-types to tree types, is defined inductively as follows:

•  

  treeof (Top)(*)	=	Top
  treeof (T1→T2)(*)	=	→
  treeof (T1→T2)(i,π)	=	treeof(Ti)(π)
  treeof(T1 × T2)(*)	=	×
  treeof (T1 × T2)(i,π)	=	treeof(Ti)(π)
  treeof (μX.T)(π)	=	treeof([X ↦ μX.T]T)(π)

To verify that this definition is proper (i.e., exhaustive and terminating), note the following:

1. Every recursive use of treeof on the right-hand side reduces the lexicographic size of the pair(|π|, μ-height(T)):the cases for S→T and S × T reduce |π| and the case for μX.T preserves |π| but reduces μ-height(T).

2. All recursive calls preserve contractiveness and closure of the argument types. In particular, the type μX.T is contractive and closed iff its unfolding [X ↦ μX.]T is. This justifies the unfolding step in the definition of treeof (μX.T).

The treeof function is lifted to pairs of types by defining treeof (S, T) = (treeof (S), treeof (T)).

An sample application of treeof to a μ-type is shown in Figure 21-3.

Figure 21-3: Sample treeof Application

The subtype relation for tree types was defined in §21.3 as the greatest fixed point of the generating function S. In the present section, we extended the syntax of types with μ-types, whose behavior is intuitively described by the rules of (right and left, correspondingly) μ-folding:

Formally, we define subtyping for μ-types by giving a generating function S_m, with three clauses identical to the definition of S and two additional clauses corresponding to the μ-folding rules.

21.8.4 Definition

Two μ-types S and T are said to be in the subtype relation if (S, T) Î vS_m, where the monotone function S_m Î P (T_m × T_m) → P(T_m × T_m) is defined by:

•  

  Sm(R)	=	{(S, Top) | S Î Tm}
  	È	{(S1 × S2, T1 × T2) | (S1, T1), (S2, T2) Î R}
  	È	{S1→S2, T1→T2) | (T1, S1), (S2, T2) Î R}
  	È	{S, μX.T) | (S, [X → μX.T]T) Î R}
  	È	{(μX.S, T) | ([X → μX.S]S, T) Î R, T ≠ Top, and T ≠ μY.T1}.

Note that this definition does not embody precisely the μ-folding rules above: we have introduced an asymmetry between its final and penultimate clauses to make it invertible (otherwise, the clauses would overlap). However, as the next exercise shows, S_m generates the same subtype relation as the more natural generating function^[4] S_d whose clauses exactly correspond to the inference rules.

21.8.5 Exercise [⋆⋆⋆]

Write down the function S_d mentioned above, and demonstrate that it is not invertible. Prove that vS_d = vS_m.

The generating function S_m is invertible because the corresponding support function is well-defined:

The subtype relation on μ-types so far has been introduced independently of the previously defined subtyping on tree types. Since we think of μ-types as just a way of representing regular types in a finite form, it is necessary to ensure that the two notions of subtyping correspond to each other. The next theorem (21.8.7) establishes this correspondence. But first, we need a technical lemma.

21.8.6 Lemma

Suppose that R ⊆ T_m × T_m is S_m-consistent. For any (S, T) Î R, there is some (S′, T′) Î R such that treeof (S′, T′) = treeof (S, T) and neither S′ nor T′ starts with μ.

Proof: By induction on the total number of μs at the front of S and T. If neither S nor T starts with μ, then we can take (S′, T′) = (S, T). On the other hand, if (S, T) = (S, μX.T₁), then by the S_m-consistency of R, we have (S, T) Î S_m(R), so (S″, T″) = (S, [X ↦ μX.T₁]T₁) Î R. Since T is contractive, the result T″ of unfolding T has one fewer μ at the front than T does. By the induction hypothesis, there is some (S′, T′) Î R such that neither S′ nor T′ starts with μ and such that treeof(S″, T″) = (S′, T′). Since, by the definition of treeof, treeof (S, T) = treeof (S″, T″), the pair (S′, T′) is the one we need. The case where (S, T) = (μX.S₁, T) is similar.

21.8.7 Theorem

Let (S, T) Î T_m × T_m. Then (S, T) Î vS_m iff treeof (S, T) Î vS.

Proof: First, let us consider the "only if" direction-that (S, T) Î vS_m implies treeof (S, T) Î vS_m. Let (A, B) = treeof (S, T) Î T × T. By the coinduction principle, the result will follow if we can exhibit an S-consistent set Q Î T × T such that (A, B) Î Q. Our claim is that Q = treeof (vS_m) is such a set. To verify this, we must show that (A′, B′) Î S(Q) for every (A′, B′) Î Q.

Let (S′, T′) Î vS_m be a pair of μ-types such that treeof (S′, T′) = (A′, B′). By Lemma 21.8.6, we may assume that neither S′ nor T′ starts with μ. Since vS_m is S_m-consistent, (S′, T′) must be supported by one of the clauses in the definition of S_m-i.e., it must have one of the following shapes.

Case:

(S′, T′) = (S′, Top)

Then B′ = Top, and (A′, B′) Î S(Q) by the definition of S.

Case:

(S′, T′) = (S₁ × S₂, T₁ × T₂)

with

(S₁, T₁), (S₂, T₂) Î vS_m

By the definition of treeof, we have B′ = treeof(T′)= B₁ × B₂, where each B_i = treeof(T_i). Similarly, A′ = A₁ × A₂, where A_i = treeof (S_i). Applying treeof to these pairs gives (A₁, B₁), (A₂, B₂) Î Q. But then, by the definition of S, we have (A, B) = (A₁ × A₂, B₁ × B₂) Î S(Q).

Case:

(S′, T′) = (S₁→S₂, T₁→T₂)

with

(T₁, S₁), (S₂, T₂) Î vS_m Similar.

Next, let us check the "if" direction of the theorem-that treeof (S, T) Î vS implies (S, T) Î vS_m. By the coinduction principle, it suffices to exhibit an S_m-consistent set R Î T_m × T_m with (S, T) Î R. We claim that R = {(S′ T′) Î T_m × T_m | treeof(S′, T′) Î vS}. Clearly, (S, T) Î R. To finish the proof, we must now show that (S′, T′) Î R implies (S′, T′) Î S_m(R).

Note that, since vS is S-consistent, any pair (A′, B′) Î vS must have one of the forms (A′, Top), (A₁ × A₂, B₁ × B₂), or (A₁→A₂, B₁→B₂). From this and the definition of treeof , we see that any pair (S′ T′) Î R must have one of the forms (S′, Top), (S₁ × S₂, T₁ × T₂), (S₁→S₂, T₁→T₂), (S′, μX.T₁), or (μX.S₁, T′). We consider each of these cases in turn.

Case:

(S′, T′) = (S′, Top)

Then (S′, T′) Î S_m(R) immediately, by the definition of S_m.

Case:

(S′, T′) = (S₁ × S₂, T₁ × T₂)

Let (A′, B′) = treeof (S′ T′). Then (A′, B′) = (A₁ × A₂, B₁ × B₂), with A_i = treeof (S_i) and B_i = treeof(T_i). Since (A′, B′) Î vS, the S-consistency of vS implies that (A_i, B_i) Î vS, which in turn yields (S_i, T_i) Î R, by the definition of R. The definition of S_m yields (S′, T′) = (S₁ × S₂, T₁ × T₂) Î S_m(R).

Case:

(S′, T′) = (S₁→S₂, T₁→T₂)

Similar.

Case:

(S′, T′) = (S′, μX.T₁)

Let T″ = [X ↦ μX.T₁]T₁. By definition, treeof (T″) = treeof (T′). Therefore, by the definition of R, we have (S′, T″) Î R, and so (S′, T′) Î S_m(R), by the definition of S_m.

Case:

(S′, T′) = (μX.S₁, T′)

If T′ = Top or T′ starts with μ, then one of the cases above applies; otherwise, the argument is similar to the previous one.

The correspondence established by the theorem is a statement of soundness and completeness of subtyping between μ-types, as defined in this section, with respect to the ordinary subtype relation between infinite tree types, restricted to those tree types that can be represented by finite μ-expressions.

^[4]The "d" in S_d is a reminder that the function is based on the "declarative" inference rules for μ-folding, in contrast to the "algorithmic" versions used in S_m.

---