Algebraic Closure of Matrix Sets Recognized by 1-VASS

TL;DR

The work investigates when the Zariski closure of matrix sets $\varphi(L)$ is computable, focusing on languages $L$ beyond regular, including one-counter languages and indexed grammars. It develops a novel adaptation of Simon's factorization forests to infinite matrix monoids and introduces factorization trees to bound complexity, enabling reductions of closure problems to regular-language settings. The authors provide explicit procedures to compute vanishing ideals for $\varphi(L)$ when $L$ is a $1$-VASS coverability or reachability language and prove undecidability for indexed languages, highlighting both decidability boundaries and fundamental limits. The results advance interprocedural program analysis and algebraic invariants by linking automata-theoretic representations with algebraic-geometry closures, offering a framework for analyzing polynomial invariants in affine systems and beyond.

Abstract

It is known how to compute the Zariski closure of a finitely generated monoid of matrices and, more generally, of a set of matrices specified by a regular language. This result was recently used to give a procedure to compute all polynomial invariants of a given affine program. Decidability of the more general problem of computing all polynomial invariants of affine programs with recursive procedure calls remains open. Mathematically speaking, the core challenge is to compute the Zariski closure of a set of matrices defined by a context-free language. In this paper, we approach the problem from two sides: Towards decidability, we give a procedure to compute the Zariski closure of sets of matrices given by one-counter languages (that is, languages accepted by one-dimensional vector addition systems with states and zero tests), a proper subclass of context-free languages. On the other side, we show that the problem becomes undecidable for indexed languages, a natural extension of context-free languages corresponding to nested pushdown automata. One of our main technical tools is a novel adaptation of Simon's factorization forests to infinite monoids of matrices.

Figures (5)

• Figure 1: Two recursive procedures in which all variables are global. The wildcard (*) evaluates non-deterministically either to true or false. An execution of the procedure $P$ on the left can be summarized by the assignment $\boldsymbol x:= B^nA^n \boldsymbol x$ for some $n\in \mathbb N$. An execution of the procedure $Q$ on the right results in assignment $\boldsymbol x:=M\boldsymbol x$ where the matrix $M$ is a product of a string of $A$'s and $B$'s that is well-matched in the sense of the Dyck language.
• Figure 2: factorization tree of $M_{j_k}, \dots, M_{j_{\ell}-1}$ with height at most 2
• Figure 3: Fragment of Stratum 0, showing two products $N_1$ and $N_2$ paired into a parent node $P_1$.
• Figure 4: Decomposition $w=xw_1yw_2$, where $x$ is the shortest prefix of $w$ with weight in $\{-\eta(d),\eta(d)\}$, the infix $xw_1y$ is the shortest weight-zero prefix of $w$ that extends $x$, and $y$ is the shortest suffix of $xw_1y$ with weight $\omega(y)=-\omega(x)$.
• Figure 5: Depiction of the word $W_2$, where the vertical axis represents the prefix weight. The parts in blue represent symbols $(\varepsilon,\sigma_i,\varepsilon,\varepsilon)$ or $(\varepsilon,\varepsilon,\varepsilon,\xi_i)$. These are interleaved with words $(u,\varepsilon,\varepsilon,\varepsilon)$ and $(\varepsilon,\varepsilon,v,\varepsilon)$ so as to keep the weight in the range $\{-2\eta(d),\ldots,2\eta(d)\}$.

Theorems & Definitions (51)

• Example 1
• Example 2
• Example 3
• Proposition 0
• Proposition 1
• proof
• Example 4
• Proposition 1
• Proposition 1
• Theorem 2