Tree Equivalence of Higher-Order Recursion Schemes Is Undecidable

Mingkun Xiao, Yixuan Sun

Higher-order recursion schemes (HORS) are finite, simply typed recursive programs that generate potentially infinite trees. Their monadic second-order model-checking problem is dec…