强不变量很难：关于（概率）程序的最强多项式不变量的困难
摘要：计算具有多项式赋值的单路径循环的最强多项式不变量的问题至少与Skolem问题一样困难，这是一个有关可决定性的著名问题，几乎有一个世纪都没有解决。虽然对于仿射循环来说，最强多项式不变量是可计算的，但对于多项式循环来说，这个问题一直没有解决。作为一个独立感兴趣的中间结果，我们还证明了离散多项式动态系统的可达性问题也是Skolem难解的。此外，我们还推广了不变理想的概念，引入了概率程序的矩不变理想。利用这个工具，我们进一步证明了以下问题：（i）对于带有分支语句的概率循环，最强多项式矩不变是不可计算的；（ii）对于不带有分支语句的多项式概率循环，最强多项式矩不变是Skolem难解的。最后，我们确定了一类概率循环，其中最强多项式矩不变是可计算的，并提供了一个算法来计算它。
作者：Julian M"ullner and Marcel Moosbrugger and Laura Kov''acs
论文ID：2307.10902
分类：Programming Languages
分类简称：cs.PL
提交时间：2023-07-21