Solvability of orbit-finite systems of linear equations
Arka Ghosh, Piotr Hofman, Sławomir Lasota
TL;DR
The paper addresses the decidability of solvability for orbit-finite systems of linear equations over atom-based sets (nominal sets) by establishing an Orbit-Finite Basis Theorem and reducing solvability to finitely many finite systems. The core approach constructs an orbit-finite basis for $\mathrm{Lin}(B)$ when $B$ is orbit-finite, enabling a finite representation of solutions via tight orbits and canonical bases, and then reduces the general solvability problem $Solv(\mathbb{K})$ to the finitary case $Fin-Solv(\mathbb{K})$. The reduction yields a singly-exponential blowup in atom-dimension, with polynomial-time solvability for fixed atom-dimension over $\mathbb{Q}$ or $\mathbb{Z}$, and a broad decidability result for arbitrary effective rings $\mathbb{K}$. The results generalize prior work on data-enriched models and have potential applications to reachability questions in data-bearing Petri nets and related automata; they also open questions about full solution sets, non-finitary solutions, and nonnegativity constraints. Overall, the work provides fundamental tools for algorithmically handling linear-algebraic problems in nominal settings with atoms.
Abstract
We study orbit-finite systems of linear equations, in the setting of sets with atoms. Our principal contribution is a decision procedure for solvability of such systems. The procedure works for every field (and even commutative ring) under mild effectiveness assumptions, and reduces a given orbit-finite system to a number of finite ones: exponentially many in general, but polynomially many when atom dimension of input systems is fixed. Towards obtaining the procedure we push further the theory of vector spaces generated by orbit-finite sets, and show that each such vector space admits an orbit-finite basis. This fundamental property is a key tool in our development, but should be also of wider interest.