Linear loops (or linear dynamical systems) are an established computational model in our community. We typically understand under a linear loop a simple while loop with a single linear update as shown next.
\[\textbf{x}:= \textbf{s}; \; while \; true \; do \; \textbf{x} := M \cdot \textbf{x};\]
Here, \(\textbf{x} = (x_1, \dots, x_d)\) is a vector of rational-valued loop variables and the matrix \(M \in \mathbb{Q}^{d \times d}\) denotes a linear transformation of \(\mathbb{Q}^d\).
In the loop synthesis problem, a polynomial \(p \in \mathbb{Q}[x_1, \dots, x_d]\) in \(d\) variables is given. The goal is to generate a linear loop (that is, both the update matrix \(M\) and the initialisation vector \(s\)) such that \(p(x_1(n), \dots, x_d(n)) = 0\) holds after \(n\)-th iteration of the loop for all \(n \in \mathbb{N}\).
It is natural to start investigations by assuming the same number of variables \(d\) in the loop as in the desired polynomial invariant \(p(x_1, \dots, x_d) = 0\). However, as can be seen from the following example, linear loops with \(s > d\) variables are more expressive. \[ (x,y,z):= (1,2,-1);
while \; true \; do \; x:= 2x; y:= 8y+4z; z:= 4z; endwhile; \] This linear loop with \(s=3\) variables satisfies a polynomial invariant \(x^3+x^2-y = 0\). While doing so, the loop produces an infinite set of distinct values for \((x(n), y(n))\). We refer to this as a \(non-trivial\) linear loop in 3 variables for \(p = x^3+x^2-y\). Nevertheless, one can prove that no non-trivial linear loop with \(d=2\) variables \(\{x,y\}\) satisfying \(p(x,y)=0 \) exists.
Question: Let \(p\) be an arbitrary polynomial in \(d\) variables. Does there exist an upper bound \(N\) such that if a non-trivial linear loop satisfying \(p=0\) exists, then there exists a non-trivial linear loop with at most \(N\) variables satisfying the same invariant?
If such an upper bound exists and can be computed, a known template-based loop synthesis approach can be used to synthesise all loops satisfying an invariant, provided such loops exist.
From the observation above, if \(N\) exists, then \(N \geq d+1 \). The challenge to improve the lower bound on \(N\) is the lack of techniques to prove that no loop with fixed number of variables satisfies a given invariant. The techniques that we seek for may be rooted in the theory of C-finite sequences and their algebraic properties: allowing additional variables widens the class of C-finite sequences generated by the loop.
Another way to see this is to consider loops with \(d\) variables but affine updates of the form \[x_i \gets a_1x_1 + \dots + a_dx_d + a_0.\] Affine loops can be simulated by linear loops with an additional variable \(x_0\) which is constantly set to 1. Polynomial invariants of an affine loop with \(d\) variables are thus the invariants in terms of \(x_1, \dots, x_d\) in a linear loop with variables \(x_0, x_1, \dots, x_d\). However, some of those invariants may not have a linear loop with only \(d\) variables that satisfies them.