Polyregular equivalence is undecidable in higher-order types
Programming Languages
2026-04-15 v1 Formal Languages and Automata Theory
Abstract
It is open whether equivalence ( f = g ) is decidable for string-to-string polyregular functions. We consider their higher-order extension based on the {\lambda}-calculus definition of polyregular functions from Boja\'nczyk (2018). In this setting, equivalence is undecidable by reduction from the tiling problem.
Cite
@article{arxiv.2604.11935,
title = {Polyregular equivalence is undecidable in higher-order types},
author = {Mikołaj Bojańczyk and Grzegorz Fabiański and Rafał Stefański},
journal= {arXiv preprint arXiv:2604.11935},
year = {2026}
}