The inclusion problem for monadic recursion schemes
The inclusion problem for the class of monadic recursion schemes is shown to be undecidable. The proof illustrates the close relationship between monadic recursion schemes and deterministic pushdown automata. The proof is extended to show that both the weak equivalence problem for the class of monadic recursion schemes and the weak equivalence problem for the class of free schemes without identity are undecidable.
Friedman, E. P.↗