Regular => Subtree set finiteness => Termination of memoized algorithm

The termination argument behind the TAPL algorithm for subtyping of equirecursive types is not as scary as it sounds (or as it sounded to me, anyway). It's as simple as this: even though the subtyping rules generate bigger types when they substitute a recursive type into its own body, the fact that the types are regular means that there are only a finite number of distinct subterms in the infinite type tree--that's the definition of regular trees. So as long as you keep a cache of types you've looked at before and never have to look at the same pair of types twice, you can't do an infinite number of checks.

(Eventually, you run out of work.)

If I'm not mistaken, the syntactic restriction that types are contractive, i.e., recursive type variables have to appear under constructors, is sufficient to guarantee that the corresponding type trees are regular.