7.6PLApr 13
Polyregular equivalence is undecidable in higher-order typesMikołaj Bojańczyk, Grzegorz Fabiański, Rafał Stefański
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.