The membership and threshold problems for recurrence sequences are fundamental open decision problems in automated verification. The former problem asks whether a chosen target is an element of a sequence, whilst the latter asks whether every term in a sequence is bounded from below by a given value. A rational-valued sequence $\langle u_n \rangle_n$ is hypergeometric if it satisfies a first-order linear recurrence of the form $p(n)u_{n+1} = q(n)u_{n}$ with polynomial coefficients $p,q\in\mathbb{Z}[x]$. In this note we establish decidability results for the aforementioned problems for restricted classes of hypergeometric sequences. For example, we establish decidability for the aforementioned problems under the assumption that the polynomial coefficients $p,q\in\mathbb{Z}[x]$ are monic and split over an imaginary rational extension of $\mathbb{Q}$. We also establish conditional decidability results; that is, conditional on Schanuel's conjecture, when the irreducible factors of the monic polynomial coefficients $p,q\in\mathbb{Z}[x]$ are either linear or quadratic.
翻译:递推序列的成员资格问题和阈值问题是自动验证中基本的开放决策问题。前者询问给定目标是否为序列中的某个元素,而后者则询问序列中每一项是否都不小于某个给定值。若一个有理值序列$\langle u_n \rangle_n$满足形如$p(n)u_{n+1} = q(n)u_{n}$的一阶线性递推关系,其中多项式系数$p,q\in\mathbb{Z}[x]$,则该序列称为超几何序列。本文针对受限类别的超几何序列,建立了上述问题的可判定性结果。例如,我们证明了当多项式系数$p,q\in\mathbb{Z}[x]$为首一且可在$\mathbb{Q}$的虚有理扩张上分裂时,上述问题可判定。此外,我们还建立了条件性可判定性结果:即当首一多项式系数$p,q\in\mathbb{Z}[x]$的不可约因子为线性或二次时,在Schanuel猜想成立条件下的可判定性。