Algebra-Based Loop Synthesis

We present a method for synthesizing loops over affine assignments from polynomial invariants. It is complete when the number of auxiliary variables is bounded, thus serving as a foundation for strength reduction optimization that convert polynomial expressions into incremental affine computations. Our work has applications towards synthesizing loops satisfying a given polynomial loop invariant, program verification, as well as generating number sequences from algebraic relations. To understand viability of the methodology and heuristics for synthesizing loops with a large number of auxiliary variables, we implement and evaluate the method using the Absynth tool.