Equivariant ideals of polynomials
This work solves a foundational problem in symbolic computation for infinite-variable polynomial ideals, with implications for verification of data-driven systems.
The paper provides a necessary and sufficient condition for a countable logical structure to guarantee that every equivariant polynomial ideal is finitely generated, and extends Buchberger's algorithm to compute Gröbner bases for such ideals, enabling decidability of membership. Applications include register automata and Petri nets with data.
We study existence and computability of finite bases for ideals of polynomials over infinitely many variables. In our setting, variables come from a countable logical structure A, and embeddings from A to A act on polynomials by renaming variables. First, we give a sufficient and necessary condition for A to guarantee the following generalisation of Hilbert's Basis Theorem: every polynomial ideal which is equivariant, i.e. invariant under renaming of variables, is finitely generated. Second, we develop an extension of classical Buchberger's algorithm to compute a Gröbner basis of a given equivariant ideal. This implies decidability of the membership problem for equivariant ideals. Finally, we sketch upon various applications of these results to register automata, Petri nets with data, orbit-finitely generated vector spaces, and orbit-finite systems of linear equations.