Rational polynomial solvability linked to semilinear set stratifiability decision
Rational polynomial solvability reduces to stratifiability of semilinear sets
Formal Languages and Automata TheoryLogic in Computer Science
Summary
Deciding if certain sets built from simple repeating patterns can be nicely broken down is connected to finding rational solutions to polynomial equations with integer coefficients. The authors show that checking for rational solutions to polynomials can be transformed into deciding this breaking-down problem for these sets. This connection also relates to classic problems in language theory about certain structured languages. If recent claims about the difficulty of solving rational polynomial equations are true, then the authors’ work would finally answer a long-open question in the study of semilinear sets.
What this means in practice
- •For automata engineers: Clarify which structured languages specified by semilinear sets can be automatically recognized or decided using connection to rational polynomial solvability.
- •For formal verification teams: Inform formal verification tools about limits and capabilities when reasoning about systems modeled by semilinear sets and polynomial equations.
A theory result. No direct application yet.
Authors
Michaël Cadilhac
Abstract
A semilinear set is stratifiable if it is a finite union of linear sets whose periods have at most two nonzero coordinates, with no two periods in one component connecting alternating pairs of coordinates. We give a computable many-one reduction from the existence of a rational zero of an integer polynomial to deciding stratifiability. After the classical reduction to quadratic systems, we reduce rational solvability of these systems to a problem we call finite separation by Cartesian products of rational linear forms. Its input consists of rational subspaces $D_1,\ldots,D_k\le\mathbb Q^r\times\mathbb Q^r$. A separator is a map $(\boldsymbol x,\boldsymbol y)\mapsto(u(\boldsymbol x),v(\boldsymbol y))$, where $u,v\colon\mathbb Q^r\to\mathbb Q$ are nonzero rational linear forms. The problem asks whether finitely many separators suffice so that every pair outside $\bigcup_iD_i$ receives, from some separator, a value attained at no pair in that union. We then reduce this problem to stratifiability. Ginsburg and Spanier's characterization of letter-bounded context-free languages} also induces a reduction from rational polynomial solvability to context-freeness of letter-bounded languages specified by semilinear exponent sets. An OpenAI preprint claims undecidability of rational polynomial solvability; if correct, our result settles the decidability of general stratifiability, a problem open since 1966.