paperbot · PL 论文追踪

全部论文 待读 收藏

P2 On Robustness for the Skolem, Positivity and Ultimate Positivity Problems

论 Skolem、正性与最终正性问题的鲁棒性
LMCS vol.Volume 20, Issue 22024匹配度 2/10 · 该论文研究线性递归序列的 Skolem、正性与最终正性问题的鲁棒变体,属于逻辑与自动机、形式化可判定性理论,与用户核心方向(LLM/Agent 与静态分析、浮点程序分析、贝叶斯程序分析)没有直接关联;仅在形式化验证的理论背景上存在非常弱的间接联系。引用 0 inbox
S. Akshay, Hugo Bazille, Blaise Genest, Mihir Vahanwala
crossref: 2026-09-10

AI 速览

一句话:研究线性递归序列在初始配置邻域内规避零或负值的鲁棒变体,刻画其可判定性与复杂度边界。

本文研究线性递归序列(LRS)的 Skolem、正性与最终正性问题的鲁棒变体。经典 Skolem 问 LRS 能否从给定初始配置到达 0,正性问是否始终保持正;初始化版本长期未决,未初始化版本已有多项式时间算法。作者考察介于两者之间的问题:给定初始配置,判断其某个邻域内的所有初始配置是否都能避开 0(或负数)。结果表明:若邻域作为输入给出,鲁棒 Skolem 与鲁棒正性是 Diophantine 难的;若改为询问是否存在这样的邻域,则问题可判定且属于 PSPACE。对最终正性,非一致界变体在开邻域下即使邻域作为输入也可 tractable 求解。

问题
经典 Skolem 与正性问题对带固定初始配置的线性递归序列长期未决,而未初始化版本较易;本文研究二者之间的鲁棒版本:给定初始配置,其邻域内所有配置是否都能避开 0 或负值。
方法
将鲁棒 Skolem/正性以及最终正性的不同邻域与界变体形式化,利用 Diophantine 逼近与复杂度分析进行归约和判定。
评估
通过可判定性与复杂度结果评估:邻域给定时的 Diophantine 难性、邻域存在时的 PSPACE 可判定性,以及最终正性非一致界变体在开邻域下的 tractable 性。
原文摘要(Abstract)

The Skolem problem is a long-standing open problem in linear dynamical systems: can a linear recurrence sequence (LRS) ever reach 0 from a given initial configuration? Similarly, the positivity problem asks whether the LRS stays positive from an initial configuration. Deciding Skolem (or positivity) has been open for half a century: the best known decidability results are for LRS with special properties (e.g., low order recurrences). But these problems are easier for "uninitialized" variants, where the initial configuration is not fixed but can vary arbitrarily: checking if there is an initial configuration from which the LRS stays positive can be decided in polynomial time (Tiwari in 2004, Braverman in 2006). In this paper, we consider problems that lie between the initialized and uninitialized variants. More precisely, we ask if 0 (resp. negative numbers) can be avoided from every initial configuration in a neighborhood of a given initial configuration. This can be considered as a robust variant of the Skolem (resp. positivity) problem. We show that these problems lie at the frontier of decidability: if the neighbourhood is given as part of the input, then robust Skolem and robust positivity are Diophantine hard, i.e., solving either would entail major breakthroughs in Diophantine approximations, as happens for (non-robust) positivity. However, if one asks whether such a neighbourhood exists, then the problems turn out to be decidable with PSPACE complexity. Our techniques also allow us to tackle robustness for ultimate positivity, which asks whether there is a bound on the number of steps after which the LRS remains positive. There are two variants depending on whether we ask for a "uniform" bound on this number of steps. For the non-uniform variant, when the neighbourhood is open, the problem turns out to be tractable, even when the neighbourhood is given as input.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@article{paperbot2757,
  title = {On Robustness for the Skolem, Positivity and Ultimate Positivity Problems},
  author = {S. Akshay and Hugo Bazille and Blaise Genest and Mihir Vahanwala},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 20, Issue 2},
  year = {2024},
  doi = {10.46298/lmcs-20(2:11)2024}
}