一句话:为任意实数线性递推的 Skolem、Positivity 与 Ultimate Positivity 问题构造近乎可判定的部分算法。
本文在比特模型实数计算下研究任意实数初值与系数的线性递推的 Skolem 问题、Positivity 问题与 Ultimate Positivity 问题的可判定性。作者构造了每个问题的正确部分算法:当问题答案在实例邻域内局部常值时算法停机,表明三者在该设定下已尽可能接近可判定。对于 Positivity 与 Ultimate Positivity,算法还相对于欧氏空间上的 Lebesgue 测度在几乎所有实例上停机。相比之下,系数为精确有理数或实代数数的同类问题目前仅对相当低阶的线性递推已知可判定。
We study the decidability of the Skolem Problem, the Positivity Problem, and the Ultimate Positivity Problem for linear recurrences with real number initial values and real number coefficients in the bit-model of real computation. We show that for each problem there exists a correct partial algorithm which halts for all problem instances for which the answer is locally constant, thus establishing that all three problems are as close to decidable as one can expect them to be in this setting. We further show that the algorithms for the Positivity Problem and the Ultimate Positivity Problem halt on almost every instance with respect to the usual Lebesgue measure on Euclidean space. In comparison, the analogous problems for exact rational or real algebraic coefficients are known to be decidable only for linear recurrences of fairly low order.