Tree Equivalence of Higher-Order Recursion Schemes Is Undecidable

Abstract

Higher-order recursion schemes (HORS) are finite, simply typed recursive programs that generate potentially infinite trees. Their monadic second-order model-checking problem is decidable. We prove that tree equivalence of deterministic HORS is undecidable and, more precisely, $Π^0_1$-complete under total computable many-one reductions. The lower bound holds for safe, productive schemes of order at most four over the fixed ranked alphabet $Σ_2=\{e:0,d:2\}$, consisting of one nullary and one binary symbol. Adapting the counter-guard witness of Boiret, Piorkowski, and Schmude, we generate all candidate executions of a two-counter machine by producing both continuations at every counter test. An integer weight is nonzero exactly on legal prefixes. Functions at fixed simple types represent the polynomial of growing degree. A shift recurrence updates them without storing a separate step counter, allowing the witness to be implemented by safe applicative HORS rules. At candidate halts, the intermediate schemes generate unary observation subtrees whose lengths encode the two natural-number components of the signed weight. Invalid candidates give matching observations; a legal halt produces a finite discrepancy. Fixed constructor contexts encode these intermediate trees over $Σ_2$. For the upper bound, a finite monotone semantics decides head convergence and supports an algorithm computing exact tree prefixes at any prescribed finite depth, including positions labelled $\bot$.