This is how SMT solvers deal with bounded quantifiers.

In theory? Absolutely; unrolling a loop is exactly what it sounds like. Recursion is just a fancy loop. But there's a reason no one does that, and why no compilers emit that as code.

Fancy in the sense of being a loop with an implicit stack. Or maybe just some registers if TCO.

And yet the machines we can actually build are far closer to LBAs than TMs.