Does Types and Programming Languages use a recursive equation to define a recursive type or its generator?
You've stumbled across the difference between isorecursive and equirecursive types.

Equi-recursive types say "types are (possibly) infinite trees, and a recursive type is the solution to a recursive equation". Specifically, $\mu x\ldotp T = [\mu x \ldotp T/x]T$. These are conceptually simple, but in practice difficult to work with, since deciding whether two types are equal (or worse, subtypes of one another) or not is tricky.

Conversely, isorecursive types say that recursive types are just syntax. You are allowed to unroll them according to the equation above, but $\mu x\ldotp T$ and $ [\mu x \ldotp T/x]T$ are fundamentally different types, and must use the explicit fold and unfold instructions.

If you keep reading Pierce, he will explain this in the book.

Answering your specific questions:


The "loop" is that the definition on the RHS or the = is allowed to reference the name defined on the left. This is awkward for theory, because we don't want to treat top-level definitions as special.
Yes, $\mu$ is similar to $\lambda$ in the sense that they both bind variables. However, it's different in that there's always a very specific thing that gets plugged in for the bound variable with $\mu$, whereas $\lambda$ is useful precisely because we can plug the variable with anything. Also, the bound variable of $\mu$ denotes a type, whereas with $\lambda$ it denotes a term.
Yes, and that's the point of the $\mu$ operator. It says "I am the syntax that takes the generator for a type, and turns it into an actual type you can use like any other type in your program." And it make explicit the role of $X$ in the equation your outline.
Again, this is the job of $\mu$ by definintion. It is the piece of syntax that says "given the generator, tie the knot and make it an actual type."


The thing is, you can't really understand $\mu$-types on their own. Otherwise it's just syntax. The key is in the type rules for $\mu$ types. For isorecursive types, there are fold and unfold rules that allow us to "run the generator" one step. For equirecursive types, there are special rules in how type equality is determined that allow us to treat $\mu x \ldotp T$ as actually being the solution generated by the recurrence equation. But, these type rules will change depending on the specific language or calculus you're using.