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猜想的条件下可判定。