21.7 Regular Trees

---

21.7 Regular Trees

At this point, we have developed generic algorithms for checking membership in a set defined as the greatest fixed point of a generating function F, assuming that F is invertible and finite state; separately, we have shown how to define subtyping between infinite trees as the greatest fixed point of a particular generating function S. The obvious next step is to instantiate one of our algorithms with S. Of course, this concrete algorithm will not terminate on all inputs, since in general the set of states reachable from a given pair of infinite types can be infinite. But, as we shall see in this section, if we restrict ourselves to infinite types of a certain well-behaved form, so-called regular types, then the sets of reachable states will be guaranteed to remain finite and the subtype checking algorithm will always terminate.

21.7.1 Definition

A tree type S is a subtree of a tree type T if S = λσ. T(π,σ) for some π-that is, if the function S from paths to symbols can be obtained from the function T by adding some constant prefix π to the argument paths we give to T; the prefix π corresponds to the path from the root of T to the root of S. We write subtrees(T) for the set of all subtrees of T.

21.7.2 Definition

A tree type T Î T is regular if subtrees(T) is finite-i.e., if T has finitely many distinct subtrees. The set of regular tree types is written T_r.

21.7.3 Examples

1. Every finite tree type is regular; the number of distinct subtrees is at most the number of nodes. The number of distinct subtrees of a tree type can be strictly less than the number of nodes. For example, T = Top→(Top × Top) has five nodes but only three distinct subtrees (T itself, Top × Top, and Top).

2. Some infinite tree types are regular. For example, the tree

      T = Top × (Top × (Top × ...)) 

   has just two distinct subtrees (T itself and Top).

3. The tree type

      T = B × (A × (B × (A × (A × (B × (A × (A × (A × (B × ...) 

   where pairs of consecutive Bs are separated by increasingly many As, is not regular. Because T is irregular, the set reachable_s(T, T) containing all the subtyping pairs needed to justify the statement T<:T is infinite.

21.7.4 Proposition

The restriction S_r of the generating function S to regular tree types is finite state.

Proof: We need to show that for any pair (S, T)of regular tree types, the set is finite. Observe that ; the latter is finite, since both subtrees(S) and subtrees(T) are.

This means that we can obtain a decision procedure for the subtype relation on regular tree types by instantiating one of the membership algorithms with S. Naturally, for this to work in a practical implementation, regular trees must be represented by some finite structures. One such representation, μ-notation, is discussed in the next section.

---