Undecidability of tree equivalence for some recursive program-generated trees
Tree Equivalence of Higher-Order Recursion Schemes Is Undecidable
Formal Languages and Automata TheoryLogic in Computer Science
Summary
Some computer programs called higher-order recursion schemes (HORS) can produce infinitely large tree-shaped structures. The authors show that deciding whether two such deterministic HORS generate the exact same tree is impossible with any algorithm, a problem called undecidable. They prove this even for fairly simple HORS of order four using clever encodings of machines that count and compare numbers. This means some verification tasks comparing these program outputs cannot be fully automated.
What this means in practice
- •For program verification teams: Avoid relying on automatic equivalence checks for higher-order recursion scheme outputs, as this problem is undecidable for some cases.
- •For formal methods engineers: Design verification tools that handle infinite trees generated by HORS but do not attempt full equivalence checking due to its undecidability.
A theory result. No direct application yet.
Authors
Mingkun Xiao, Yixuan Sun
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$.