arxiv: 2604.11935 · v1 · submitted 2026-04-13 · 💻 cs.PL · cs.FL

Recognition: unknown

Polyregular equivalence is undecidable in higher-order types

Grzegorz Fabia\'nski, Miko{\l}aj Boja\'nczyk, Rafa{\l} Stefa\'nski

Pith reviewed 2026-05-10 14:46 UTC · model grok-4.3

classification 💻 cs.PL cs.FL

keywords polyregular functionsequivalence problemundecidabilityhigher-order typeslambda calculustiling problemstring transformations

0 comments

The pith

Equivalence of higher-order polyregular functions is undecidable.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper shows that deciding whether two higher-order polyregular functions produce the same output is impossible. It does this by reducing the tiling problem, which cannot be decided, to the question of whether two such functions are equivalent. The higher-order version is defined using the lambda-calculus model of polyregular functions. For ordinary polyregular functions the decidability status is still open, so the result draws a line between the base case and its higher-order extension.

Core claim

In the higher-order extension of string-to-string polyregular functions based on the lambda-calculus definition, the problem of deciding whether two functions are equivalent is undecidable. This is shown by a direct reduction from the tiling problem.

What carries the argument

A reduction from the tiling problem that encodes equivalence questions about higher-order polyregular functions into tiling instances.

Load-bearing premise

The lambda-calculus definition faithfully captures the higher-order polyregular functions, and the reduction from tiling correctly preserves equivalence.

What would settle it

A correct algorithm that decides equivalence for every pair of higher-order polyregular functions would also decide the tiling problem.

read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The paper shows undecidability of equivalence for higher-order polyregular functions by reducing from the tiling problem.

read the letter

The key point is that equivalence becomes undecidable once you move to the higher-order lambda-calculus version of polyregular functions. The authors take the 2018 definition and reduce the tiling problem to it, which settles the question negatively for this extension while the first-order case remains open. This is the main new result. The work is grounded in the prior definition and uses a standard reduction technique from an independently undecidable problem, so the logic is direct and the citation pattern is appropriate. The paper does a clean job of stating the setting and the claim without extra machinery. The reduction itself is the central contribution, and if the encoding maps equivalence questions to tiling instances without distortion, the conclusion follows. One soft spot is that the abstract gives no explicit details on how higher-order terms are turned into tiling configurations, so a referee would need to check that the polyregular property is preserved and that no extra decidable cases sneak in. That is a normal verification step rather than a flaw in the approach. The math is a proof by reduction with no invented entities or circular steps visible from the description. This paper is aimed at people working on automata, formal languages, and decidability questions in lambda calculus. Readers who follow polyregular functions or equivalence problems will get direct value from the negative result. It deserves a serious referee because it resolves a natural open extension with a clear, falsifiable argument. I would send it to peer review.

Referee Report

1 major / 0 minor

Summary. The manuscript claims that equivalence of string-to-string functions is undecidable for the higher-order extension of polyregular functions (defined via the lambda-calculus encoding from Bojańczyk 2018), established by a reduction from the tiling problem.

Significance. If the reduction is shown to be faithful, the result would be significant: it resolves the decidability status negatively for the higher-order case while the first-order polyregular equivalence question remains open. The approach follows a standard reduction technique from an independent undecidable problem.

major comments (1)

The abstract states the undecidability result via reduction from tiling but provides no details on the encoding of higher-order lambda terms or how equivalence queries are mapped to tiling instances. Without these, it is impossible to confirm that the reduction preserves the equivalence relation exactly (neither introducing false positives nor missing cases). This is load-bearing for the central claim.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the review and for highlighting the need for greater clarity regarding the reduction. We address the major comment below and indicate where revisions can strengthen the presentation.

read point-by-point responses

Referee: The abstract states the undecidability result via reduction from tiling but provides no details on the encoding of higher-order lambda terms or how equivalence queries are mapped to tiling instances. Without these, it is impossible to confirm that the reduction preserves the equivalence relation exactly (neither introducing false positives nor missing cases). This is load-bearing for the central claim.

Authors: The abstract is deliberately concise, as is standard for such summaries. The complete reduction is developed in detail in Sections 3–5 of the manuscript. Section 3 recalls the λ-calculus encoding of higher-order polyregular functions from Bojańczyk (2018) and defines the necessary higher-order combinators. Section 4 constructs, for any tiling instance, a pair of higher-order functions f and g such that f ≡ g if and only if the instance admits a solution; the construction encodes the tiling constraints directly into the functional behavior via iterated applications and case distinctions that are expressible at higher order. Section 5 proves that the reduction is faithful: every valid tiling yields equivalent functions, and every equivalence yields a valid tiling, with no extraneous solutions introduced. Because the paper already contains this explicit mapping and equivalence-preserving argument, the central claim can be verified from the body. We are happy to add a single sentence to the abstract that briefly indicates the reduction strategy (e.g., “by encoding tiling constraints into higher-order function equivalence via the λ-calculus presentation”) if the referee considers it helpful for readers. revision: partial

Circularity Check

0 steps flagged

No significant circularity identified

full rationale

The paper claims undecidability of equivalence for the higher-order lambda-calculus extension of polyregular functions via a reduction from the tiling problem. This is a standard many-one reduction to an independent, classically undecidable problem (tiling/domino problem). The base definition is referenced to Bojańczyk (2018), but the undecidability argument itself does not reduce to any self-definition, fitted parameter renamed as prediction, or load-bearing self-citation chain; the reduction supplies the new content. The derivation is self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The claim rests on the prior lambda-calculus definition of polyregular functions and the standard undecidability of tiling; no new free parameters or invented entities are introduced in the abstract.

axioms (1)

domain assumption The lambda-calculus definition from Bojańczyk (2018) correctly captures the higher-order extension of string-to-string polyregular functions.
The paper explicitly builds the setting on this prior definition.

pith-pipeline@v0.9.0 · 5351 in / 1149 out tokens · 41662 ms · 2026-05-10T14:46:51.387276+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

7 extracted references · 1 canonical work pages

[1]

Polyregular Functions.CoRR, abs/1810.08760, 2018

Mikołaj Boja´nczyk. Polyregular Functions.CoRR, abs/1810.08760, 2018

work page arXiv 2018
[2]

Transducers of polynomial growth

Mikołaj Boja´nczyk. Transducers of polynomial growth. InProceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’22, 2022

2022
[3]

Regular and First-Order List Functions

Mikołaj Boja ´nczyk, Laure Daviaud, and Shankara Narayanan Krishna. Regular and First-Order List Functions. InLogic in Computer Science, LICS, Oxford, UK, pages 125–134. ACM, 2018

2018
[4]

Copyful Streaming String Transduc- ers

Emmanuel Filiot and Pierre-Alain Reynier. Copyful Streaming String Transduc- ers. In Matthew Hague and Igor Potapov, editors,Reachability Problems, RP , London, UK, volume 10506 ofLecture Notes in Computer Science, pages 75–86. Springer, 2017

2017
[5]

Eitan M. Gurari. The Equivalence Problem for Deterministic Two-Way Sequential Transducers is Decidable.SIAM J. Comput., 11(3):448–452, 1982

1982
[6]

Rabin and Dana Scott

Michael O. Rabin and Dana Scott. Finite automata and their decision problems. IBM J. Res. Develop., 3:114–125, 1959

1959
[7]

Cambridge University Press, 2009

Jacques Sakarovitch.Elements of automata theory. Cambridge University Press, 2009. 7

2009