一句话：证明单路径多项式循环的最强多项式不变式计算至少与 Skolem 问题同难，并推广到概率程序的矩不变式。
本文研究（概率）程序中强多项式不变式的可计算性。作者证明，对带多项式赋值的单路径循环，计算最强多项式不变式至少与 Skolem 问题同难，而后者的可判定性已开放近百年；作为中间结果，离散多项式动力系统的可达性也是 Skolem-hard。方法上，作者推广不变式理想，并为概率程序引入矩不变式理想。借助该工具，他们证明：带分支的概率循环的最强多项式矩不变式不可计算；无分支的多项式概率循环则 Skolem-hard。最后给出一类可计算情形及算法。
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.
@article{paperbot2617,
title = {Strong Invariants Are Hard: On the Hardness of Strongest Polynomial Invariants for (Probabilistic) Programs},
author = {Julian Müllner and Marcel Moosbrugger and Laura Kovács},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {POPL},
year = {2024},
doi = {10.1145/3632872}
}