Polyregular equivalence is undecidable in higher-order types

TL;DR

The paper proves that determining equivalence of higher-order polyregular functions, based on lambda calculus, is undecidable, extending known results to a more complex setting.

Contribution

It establishes the undecidability of equivalence for higher-order polyregular functions, a significant extension of prior work on first-order cases.

Findings

Equivalence is undecidable for higher-order polyregular functions.

The proof uses a reduction from the tiling problem.

Extends undecidability results to a lambda calculus-based setting.

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.