Polyregular equivalence is undecidable in higher-order types
arXiv:2604.119357.6h-index: 1
Predicted impact top 67% in PL · last 90 daysOriginality Incremental advance
AI Analysis
For researchers in automata theory and programming languages, this result establishes a fundamental undecidability boundary in higher-order string-to-string functions.
The paper proves that equivalence of higher-order polyregular functions is undecidable via a reduction from the tiling problem, extending the open decidability question for first-order polyregular functions.
It is open whether equivalence ( f = g ) is decidable for string-to-string polyregular functions. We consider their higher-order extension based on the λ-calculus definition of polyregular functions from Bojańczyk (2018). In this setting, equivalence is undecidable by reduction from the tiling problem.