On Strongest Algebraic Program Invariants

Decision problems for matrix semigroups have also been studied for many decades, independently of program analysis. One of the most prominent such is the Membership Problem, i.e., whether a given matrix belongs to a finitely generated semigroup of integer matrices. An early and striking result on this topic is due to Markov, who showed undecidability of the Membership Problem in dimension 6 in 1947 [31]. Later, Paterson [40] improved this result to show undecidability in dimension 3, while decidability in dimension 2 remains open. A breakthrough was achieved in 2017 by Potapov and Semukhin, who showed decidability of membership for semigroups generated by nonsingular integer \(2 \times 2\) matrices [41]. By contrast, the Membership Problem was shown to be polynomial-time decidable in any dimension by Babai et al. for commuting matrices over algebraic numbers [2]. As aptly noted by Stillwell, “noncommutative semigroups are hard to understand” [47]. Matrix semigroup theory also plays a central role in the analysis of weighted automata (such as probabilistic and quantum automata; see, e.g., References [4, 13]).

Algebraic invariants are stronger (i.e., more precise) than affine invariants. Various other types of domains have been considered in the setting of abstract interpretation, e.g., intervals, octagonal sets, and convex polyhedra (see, e.g., References [9, 10, 33] and references in Reference [5]). The precision of such domains in general is incomparable to that of algebraic invariants. Unlike with algebraic and affine invariants, there need not be a strongest convex polyhedral invariant for a given affine program. A natural decision problem in this setting is to ask for an inductive invariant that is disjoint from a given set of states (which one would like to show is not reachable). The version of this decision problem for convex invariants on affine programs was proposed by Monniaux [34] and remains open; if the convexity requirement is dropped, then the problem is shown to be undecidable in Reference [15].

The computation of semialgebraic invariants has also been considered in the context of discrete-time linear dynamical systems and linear loops (which can be viewed as highly restricted instances of affine programs); see, e.g., References [1, 16, 17].

Matrices. Let \(\mathbb {K}\) be a field. We denote by \(M_n(\mathbb {K})\) the semigroup of square matrices of dimension \(n\) with entries in \(\mathbb {K}\) . We write \(\operatorname{GL}_n(\mathbb {K})\) for the subgroup of \(M_n(\mathbb {K})\) comprising all invertible matrices. Given a set of matrices \(A \subseteq M_n(\mathbb {K})\) , we denote by \(\left\langle A \right\rangle\) the sub-semigroup of \(M_n(\mathbb {K})\) generated by \(A\) . The rank of a matrix \(a\) is denoted by \(\operatorname{rk}(a)\) , its kernel by \(\ker (a)\) , and its image by \(\operatorname{im}(a)\) . We denote by \(U\oplus V\) the direct sum of \(U\) and \(V\) .

Exterior Algebra and the Grassmannian. Given a vector space \(V\) over the field \(\mathbb {K}\) , its exterior algebra \(\Lambda ^{}{V}\) is a vector space that embeds \(V\) and is equipped with an associative, bilinear, and anti-symmetric mapWe can construct \(\Lambda ^{}{V}\) as a direct sumwhere \(\Lambda ^{r}{V}\) denotes the \(r\) th-exterior power of \(V\) for \(r\in \mathbb {N}\) , that is, the subspace of \(\Lambda ^{}{V}\) generated by \(r\) -fold wedge products \(v_1 \wedge \ldots \wedge v_r\) for \(v_1,\ldots ,v_r \in V\) . If \(V\) is finite dimensional, with basis \(e_1,\ldots ,e_n\) , then a basis of \(\Lambda ^{r}{V}\) is given by \(e_{i_1} \wedge \cdots \wedge e_{i_r}\) , \(1\le i_1 \lt \ldots \lt i_r \le n\) . Thus, \(\Lambda ^{r}{V}\) has dimension \(\binom{n}{r}\) (where \(\binom{n}{r}=0\) for \(r\gt n\) ).

A basic property of the wedge product is that given vectors \(u_1,\ldots ,u_r \in V\) , \(u_1 \wedge \ldots \wedge u_r \ne 0\) if and only if \(\lbrace u_1,\ldots ,u_r\rbrace\) is a linearly independent set. Furthermore, given \(w_1,\ldots ,w_r \in V\) , we have that \(u_1\wedge \ldots \wedge u_r\) and \(w_1\wedge \ldots \wedge w_r\) are scalar multiples of each other iff \(\operatorname{span}(u_1,\ldots ,u_r)= \operatorname{span}(v_1,\ldots ,v_r)\) .

The Grassmannian \(\operatorname{Gr}(r,n)\) is the set of \(r\) -dimensional subspaces of \(\mathbb {K}^n\) . By the above-stated properties of the wedge product there is an injective functionsuch that for any \(W\) , \(\iota (W)=v_1\wedge \cdots \wedge v_r\) where \(v_1,\ldots ,v_r\) is an arbitrarily chosen basis of \(W\) . Note that given two bases \(v_1,\ldots ,v_r\) and \(u_1,\ldots ,u_r\) of \(W\) , there exists \(\alpha \in \mathbb {K}\) such that \(v_1\wedge \cdots \wedge v_r=\alpha (u_1\wedge \cdots \wedge u_r)\) . In other words, the particular choice of a basis for \(W\) only changes the value of \(\iota (W)\) up to a constant. Given subspaces \(W_1,W_2 \subseteq V\) , we moreover have \(W_1\cap W_2 = 0\) iff \(\iota (W_1) \wedge \iota (W_2) \ne 0\) . We refer to Reference [39, Chapter 1.3] for more details about the Grassmannian.

In this section, we summarise some basic notions of algebraic geometry that will be used in the rest of the article.

Let \(\mathbb {K}\) be a field. An affine variety or algebraic set \(X\subseteq \mathbb {K}^n\) is the set of common zeros of a finite collection of polynomials, i.e., a set of the formwhere \(p_1,\ldots ,p_\ell \in \mathbb {K}[x_1,\ldots ,x_n]\) .³ Given a polynomial ideal \(I\subseteq \mathbb {K}[x_1,\ldots ,x_n]\) , by Hilbert’s basis theorem the setis a variety, called the variety of \(I\) . The two main varieties of interest to us are \(X=M_n(\mathbb {K})\) , which we identify with affine space \(\mathbb {K}^{n^2}\) in the natural way, and \(X=\operatorname{GL}_n(\mathbb {K})\) , which we identify with the variety

Given an affine variety \(X\subseteq \mathbb {K}^n\) , the Zariski topology on \(X\) has as closed sets the subvarieties of \(X\) , i.e., those sets \(A\subseteq X\) that are themselves affine varieties in \(\mathbb {K}^n\) . For example, \(\lbrace a \in M_n(\mathbb {K}) : \operatorname{rk}(a) \lt r\rbrace\) is a Zariski closed subset of \(M_n(\mathbb {K})\) , since for \(a\in M_n(\mathbb {K})\) we have \(\operatorname{rk}(a)\lt r\) iff all \(r\times r\) minors of \(a\) vanish. Given an arbitrary set \(S\subseteq X\) , we write \(\overline{S}^{}\) for its closure in the Zariski topology on \(X\) .

Given \(S \subseteq \mathbb {K}^n\) , let \(I\subseteq \mathbb {K}[x_1,\ldots ,x_n]\) be the ideal of polynomials that vanish on \(S\) . Observe that if the elements of \(S\) lie in a subfield \(\mathbb {F}\) of \(\mathbb {K},\) then the ideal \(I\) has a basis of polynomials with coefficients in \(\mathbb {F}\) . Indeed, if we fix a monomial ordering, then, by linear algebra, for every polynomial \(f \in \mathbb {K}[x_1,\ldots ,x_n]\) that vanishes on \(S\) there is a polynomial \(g \in \mathbb {F}[x_1,\ldots ,x_n]\) that also vanishes on \(S\) such that \(f\) and \(g\) have the same leading monomial. It follows that \(I\) has a Gröbner basis of polynomials in \(\mathbb {F}[x_1,\ldots ,x_n]\) (cf. [11, Chapter 5.2, Corollary 6]).

A set \(S \subseteq X\) is irreducible if for all closed subsets \(A_1,A_2\subseteq X\) such that \(S\subseteq A_1 \cup A_2\) , we have either \(S\subseteq A_1\) or \(S\subseteq A_2\) . It is well known that the Zariski topology on a variety is Noetherian. In particular, any closed subset \(A\) of \(X\) can be written as a finite union of irreducible components, where an irreducible component of \(A\) is a maximal irreducible closed subset of \(A\) .

The dimension of a variety \(X\) is defined to be the maximum number \(d \in \mathbb {N}\) such that there is a strictly increasing chain \(S_0 \subset S_1 \subset \cdots \subset S_{d}\) of non-empty irreducible closed subsets of \(X\) . A variety \(X\subseteq \mathbb {K}^n\) has dimension at most \(n\) .

The class of constructible subsets of a variety \(X\) is obtained by taking all Boolean combinations (including complementation) of Zariski closed subsets. Suppose that the underlying field \(\mathbb {K}\) is algebraically closed. Since the first-order theory of algebraically closed fields admits quantifier elimination, the constructible subsets of \(X\) are exactly the subsets of \(X\) that are first-order definable over \(\mathbb {K}\) in the language of rings, i.e., that are definable by first-order formulas with parameters from \(\mathbb {K}\) .

Suppose that \(X\subseteq \mathbb {K}^m\) and \(Y\subseteq \mathbb {K}^n\) are affine varieties. A function \(\varphi : X \rightarrow Y\) is called a regular map if it arises as the restriction of a polynomial map \(\mathbb {K}^m\rightarrow \mathbb {K}^n\) . Chevalley’s Theorem states that if \(\mathbb {K}\) is algebraically closed and \(\varphi : X \rightarrow Y\) is a regular map, then the image \(\varphi (A)\) of a constructible set \(A\subseteq X\) under \(\varphi\) is a constructible subset of \(Y\) . This result also follows from the fact that the theory of algebraically closed fields admits quantifier elimination.

A regular map of interest to us is matrix multiplication \(M_n(\mathbb {K}) \times M_n(\mathbb {K}) \rightarrow M_n(\mathbb {K})\) . In particular, we have that for constructible sets of matrices \(A,B \subseteq M_n(\mathbb {K})\) the set of productsis again constructible. Notice also that matrix inversion is a regular map \(\operatorname{GL}_n(\mathbb {K}) \rightarrow \operatorname{GL}_n(\mathbb {K})\) . Thus, if \(A\subseteq \operatorname{GL}_n(\mathbb {K})\) is a constructible set, then so is \(A^{-1} := \lbrace a^{-1} : a \in A\rbrace\) . Finally, the projection \((A,y) \mapsto A\) yields an injective regular map \(\operatorname{GL}_n(\mathbb {K}) \rightarrow M_n(\mathbb {K})\) . Via this map, we can identify \(\operatorname{GL}_n(K)\) with a constructible subset of \(M_n(\mathbb {K})\) .

On several occasions, we will use the facts that regular maps are continuous with respect to the Zariski topology and that the image of an irreducible set under a regular map is again irreducible. In particular, we have:

In this subsection, we briefly recall some algorithmic constructions on constructible subsets of a variety. We work over the field \(\overline{\mathbb {Q}}\) of algebraic numbers. Not only is this field algebraically closed, but there are also symbolic representations of algebraic numbers with respect to which arithmetic is effective (see Reference [7, Section 4.2]), which allows us to use standard algebraic-geometry algorithms, such as procedures for computing Gröbner bases, and so on.

Representing Constructible Sets. Consider a variety \(X\subseteq \overline{\mathbb {Q}}^n\) and let \(I \subseteq \overline{\mathbb {Q}}[x_1,\ldots ,x_n]\) be the ideal of polynomials that vanish on \(X\) . We represent Zariski closed subsets of \(X\) as zero sets of ideals in the coordinate ring \(\overline{\mathbb {Q}}[X]=\overline{\mathbb {Q}}[x_1,\ldots ,x_n]/I\) of \(X\) . The coordinate ring of \(M_n(\overline{\mathbb {Q}})\) is just \(\overline{\mathbb {Q}}[x_{1,1},\ldots ,x_{n,n}]\) while the coordinate ring of \(\operatorname{GL}_n(\overline{\mathbb {Q}})\) is

Unions and intersections of Zariski closed subsets of \(X\) , respectively, correspond to products and sums of the corresponding ideals in \(\overline{\mathbb {Q}}[X]\) . We furthermore represent constructible subsets of \(X\) as Boolean expressions over Zariski closed subsets.

Irreducible Components. Let \(A \subseteq X\) denote a Zariski closed set that is given as the variety of an ideal \(I\subseteq \overline{\mathbb {Q}}[X]\) . If \(I = P_1 \cap \cdots \cap P_m\) is an irredundant decomposition of \(I\) into primary ideals, then \(A=\mathbf {V}(P_1)\cup \ldots \cup \mathbf {V}(P_m)\) is a decomposition of \(A\) into irreducible components. One can compute the primary decomposition of an ideal using Gröbner basis techniques [3, Chapter 8].

Zariski Closure. At several points in our development, we will need to compute the Zariski closure of a constructible subset of a variety. Now, an arbitrary constructible subset of a variety \(X\) can be written as a union of differences of closed subsets of \(X\) . Thus, it suffices to be able to compute the closure of \(A\setminus B\) for closed sets \(A,B\subseteq X\) . Furthermore, by first computing a decomposition of \(A\) as a union of irreducible closed sets, we may also assume that \(A\) is irreducible. But \(A\subseteq \overline{A \setminus B}^{}\cup (A\cap B)\) ; thus, by irreducibility of \(A\) , we have \(\overline{A\setminus B}^{} = \emptyset\) if \(A\subseteq B\) and otherwise \(\overline{A\setminus B}^{} = A\) . An algorithm (when using the representation above) for computing the Zariski closure of a constructible set, essentially following this recipe, is given in Reference [26, Theorem 1].

Images under Regular Maps. One can use an algorithm for quantifier elimination for the theory of algebraically closed fields to compute the image of a constructible set under a regular map. An explicit algorithm for this task, using Gröbner bases, is given in Reference [45, Section 4].

Finding an Element in a Constructible Set. The problem of finding an element in a given non-empty constructible set \(A\subseteq \overline{\mathbb {Q}}^n\) is clearly computable in principle: Enumerate the elements of \(\overline{\mathbb {Q}}^n\) and check each one for membership in \(A\) . A more efficient procedure is to proceed by induction on the dimension \(n\) . In dimension one, a constructible set \(A\) is a Boolean combination of finite algebraic sets, thus, one can find a point of \(A\) among the elements of these sets plus one additional fresh element. In dimension \(n \ge 2\) , one can project \(A\) on the first \(n-1\) dimensions, find an algebraic point in the projection by induction, then substitute this point into the description \(A\) and reduce to the one-dimensional case.

Given integers \(n\) and \(r\) , let \(A\subseteq M_n(\overline{\mathbb {Q}})\) be a set of matrices of rank \(r\) . We define a labelled directed graph \(\mathcal {K}(A)\) as follows:

We note in passing that \(\mathcal {K}(A)\) can be seen as an edge-induced subgraph of the Karoubi envelope [46] of the semigroup \(M_n(\overline{\mathbb {Q}})\) .

A path in \(\mathcal {K}(A)\) is a non-empty sequence of consecutive edgesThe length of such a path is \(m\) and its label is the product \(a:=a_m \cdots a_1\) . Matrix \(a\) has rank \(r\) , since \(\ker (a_{i+1}) \cap \operatorname{im}(a_i)=0\) for \(i=1,\ldots ,m-1\) . It is moreover clear that \(\lbrace a\in \left\langle A \right\rangle : \operatorname{rk}(a)=r\rbrace\) is precisely the set of labels over all paths in \(\mathcal {K}(A)\) . We will denote that there is a path from \((U,V)\) to \((U^{\prime },V^{\prime })\) with label \(a\) by writing \((U,V) \xrightarrow{a} (U^{\prime },V^{\prime })\) .

The following sequence of propositions concerns the structure of the strongly connected components (SCCs) in \(\mathcal {K}(A)\) . The respective proofs make repeated use of the fact that for each vertex \((U,V)\) of \(\mathcal {K}(A)\) , we have \(\iota (U) \wedge \iota (V) \ne 0\) and that \(\dim \Lambda ^{r}{(}\overline{\mathbb {Q}}^n)=\binom{n}{r}\) (cf. Section 3). We say that an SCC of \(\mathcal {K}(A)\) is non-trivial if it contains a vertex \((U,V)\) such that there is a path from \((U,V)\) back to itself. Figure 1 summarises the structural results on \(\mathcal {K}(A)\) .

We now focus on individual SCCs within \(\mathcal {K}(A)\) . Let \(\mathcal {S}\) be such a non-trivial SCC. For each edge \((U,V) \xrightarrow{a} (U^{\prime },V^{\prime })\) in \(\mathcal {S}\) , define its pseudo-inverse to be a directed edge \((U^{\prime },V^{\prime }) \xrightarrow{a^{+}} (U,V)\) , where \(a^+\in M_n(\overline{\mathbb {Q}})\) is the unique matrix such that \(\ker (a^+)=U^{\prime }\) , \(\operatorname{im}(a^+)=V\) , \(a^+av=v\) for all \(v\in V\) , and \(aa^+v = v\) for all \(v\in V^{\prime }\) . We write \({\mathcal {S}^+}\) for the graph obtained from \(\mathcal {S}\) by adding pseudo-inverses of every edge in \(\mathcal {S}\) .

The graph \({\mathcal {S}^+}\) can be seen as the generator of a groupoid in which the above-defined pseudo-inverse matrices are genuine inverses. We do not develop this idea, except to observe that not only edges but also paths in \(\mathcal {S}\) have pseudo-inverses in \({\mathcal {S}^+}\) . Specifically, given a path \((U,V) \xrightarrow{a} (U^{\prime },V^{\prime })\) in \(\mathcal {S}\) , one obtains a path \((U^{\prime },V^{\prime }) \xrightarrow{a^+} (U,V)\) in \({\mathcal {S}^+}\) by taking the pseudo-inverse of each constituent edge. In the remainder of this section, we show that the pseudo-inverses of all paths in \(\mathcal {S}\) are already present in the Zariski closure \(\overline{\left\langle A \right\rangle }^{}\) .

Let \(\mathcal {S}\) be a non-trivial SCC in \(\mathcal {K}(A)\) . Write \(B \subseteq M_n(\overline{\mathbb {Q}})\) for the set of labels of all paths in \({\mathcal {S}^+}\) of length at most \(\binom{n}{r}+2\) . Moreover, fix a vertex \((U_*,V_*)\) in \({\mathcal {S}^+}\) and write \(B_*\) for the set of labels of all paths in \({\mathcal {S}^+}\) of length at most \(2{n\choose r}+3\) that are self-loops on \((U_*,V_*)\) .

Recall from Proposition 8 that the graph \(\mathcal {K}(A)\) has at most \(\binom{n}{r}\) non-trivial SCCs. Let \(\mathcal {S}_1,\ldots ,\mathcal {S}_\ell\) be a list of the non-trivial SCCs in \(\mathcal {K}(A)\) and write

Let \(R_r=\lbrace x\in M_n(\overline{\mathbb {Q}}):\operatorname{rk}(x)=r\rbrace\) , which is a constructible set, and \(R_{\lt r}=\lbrace x\in M_n(\overline{\mathbb {Q}}): \operatorname{rk}(x) \lt r\rbrace\) , which is closed.

We now present the main result of the article.

We conclude by filling in some details about how the generating graph \(\mathcal {K}(A)\) can be effectively represented and thereby how one enumerates the (finitely many) non-trivial SCCs and, given a representative of each SCC, computes the sets \(B\) and \(B^*\) described in Proposition 13. Throughout this section, by definable, we mean first-order definable by a formula in the language of rings with parameters from \(\overline{\mathbb {Q}}\) .

Let \(A \subseteq M_n(\overline{\mathbb {Q}})\) be a constructible set of matrices. Representing vector spaces by bases, the set of vertices of the generating graph \(\mathcal {K}(A)\) is a definable set. More precisely, since the same vector space has many different bases, the set of vertices is the quotient of a definable set by a definable equivalence relation. Then, for every fixed \(m\in \mathbb {N}\) , the binary relation of two vertices being connected in \(\mathcal {K}(A)\) by a path of length \(m\) is effectively definable if one already has a formula defining the set of matrices \(A\) : Indeed, there is a length- \(m\) path from \((U,V)\) to \((U^{\prime },V^{\prime })\) if there exist \(a_1,\ldots ,a_m \in A\) with \(\ker (a_m \cdots a_1)=U\) and \(\Im (a_m \cdots a_1)=V^{\prime }\) . Thanks to Propositions 9 and 10, it follows in turn that the binary reachability relation on \(\mathcal {K}(A)\) is also effectively definable and hence also the binary relation of two nodes being in the same SCC of \(\mathcal {K}(A)\) . Recall that Proposition 8 gives an upper bound on the number of SCCs of \(\mathcal {K}(A)\) . One can now enumerate a finite list of nodes of \(\mathcal {K}(A)\) that contains precisely one representative of each non-trivial SCC: Such a list can be constructed by an iterative process that at each stage maintains a formula defining all nodes lying in a non-trivial SCC other than the SCCs of the representatives found so far, and then uses the procedure described in Section 3.3 to pick an algebraic point in this set, which thus becomes a representative of a new SCC. Finally, given a representative node \((U_*,V_*)\) of an SCC \(\mathcal {S}\) , the sets \(B\) and \(B_*\) in Proposition 13 are also effectively definable, since they are labels of paths of bounded length. Note here that it is easy to include pseudo-inverses in the set \(B_*\) , since the property of being a pseudo-inverse is first-order definable.