We show that computing the strongest polynomial invariant for single-path loops with polynomial assignments is at least as hard as the Skolem problem, a famous problem whose decidability has been open for almost a century. While the strongest polynomial invariants are computable for affine loops, for polynomial loops the problem remained wide open. As an intermediate result of independent interest, we prove that reachability for discrete polynomial dynamical systems is Skolem-hard as well. Furthermore, we generalize the notion of invariant ideals and introduce moment invariant ideals for probabilistic programs. With this tool, we further show that the strongest polynomial moment invariant is (i) uncomputable, for probabilistic loops with branching statements, and (ii) Skolem-hard to compute for polynomial probabilistic loops without branching statements. Finally, we identify a class of probabilistic loops for which the strongest polynomial moment invariant is computable and provide an algorithm for it.

翻译：我们证明，对于具有多项式赋值的单路径循环，计算其最强多项式不变式至少与Skolem问题（一个近一个世纪以来其可判定性悬而未决的著名问题）一样困难。虽然仿射循环的最强多项式不变式是可计算的，但对于多项式循环而言，该问题仍然完全开放。作为一个具有独立意义的中介结果，我们证明离散多项式动力系统的可达性同样是Skolem困难的。此外，我们推广了不变理想的概念，并为概率程序引入了矩不变理想。借助这一工具，我们进一步证明：（i）对于带有分支语句的概率循环，其最强多项式矩不变式是不可计算的；（ii）对于不含分支语句的多项式概率循环，其最强多项式矩不变式的计算是Skolem困难的。最后，我们确定了一类概率循环，其最强多项式矩不变式是可计算的，并为此给出了相应算法。