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难计算的。最后，我们确定了一类概率循环，其最强多项式矩不变量是可计算的，并为此类循环提供了相应算法。