Linear loop synthesis: When d variables are not enough.

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.

$$**x**:= **s**; \; while \; true \; do \; **x** := M \cdot **x**;$$

Here, $**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.