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

0
下载
关闭预览

相关内容

【2023新书】使用Python进行统计和数据可视化,554页pdf
专知会员服务
130+阅读 · 2023年1月29日
Linux导论,Introduction to Linux,96页ppt
专知会员服务
82+阅读 · 2020年7月26日
专知会员服务
162+阅读 · 2020年1月16日
机器学习入门的经验与建议
专知会员服务
94+阅读 · 2019年10月10日
Hierarchically Structured Meta-learning
CreateAMind
27+阅读 · 2019年5月22日
Transferring Knowledge across Learning Processes
CreateAMind
29+阅读 · 2019年5月18日
强化学习的Unsupervised Meta-Learning
CreateAMind
18+阅读 · 2019年1月7日
无监督元学习表示学习
CreateAMind
27+阅读 · 2019年1月4日
Unsupervised Learning via Meta-Learning
CreateAMind
44+阅读 · 2019年1月3日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
18+阅读 · 2018年12月24日
【推荐】ResNet, AlexNet, VGG, Inception:各种卷积网络架构的理解
机器学习研究会
20+阅读 · 2017年12月17日
【推荐】RNN/LSTM时序预测
机器学习研究会
25+阅读 · 2017年9月8日
【推荐】SVM实例教程
机器学习研究会
17+阅读 · 2017年8月26日
【推荐】(Keras)LSTM多元时序预测教程
机器学习研究会
25+阅读 · 2017年8月14日
国家自然科学基金
1+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
1+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
Arxiv
0+阅读 · 2023年6月24日
Arxiv
10+阅读 · 2022年3月18日
VIP会员
最新内容
学习数据的几何:形状空间分析数学综述
专知会员服务
0+阅读 · 12分钟前
定向能反无人机系统最新发展动态
专知会员服务
3+阅读 · 今天13:50
从燃煤战舰到算法战争:水面指挥的永恒要求
专知会员服务
2+阅读 · 今天13:33
相关资讯
Hierarchically Structured Meta-learning
CreateAMind
27+阅读 · 2019年5月22日
Transferring Knowledge across Learning Processes
CreateAMind
29+阅读 · 2019年5月18日
强化学习的Unsupervised Meta-Learning
CreateAMind
18+阅读 · 2019年1月7日
无监督元学习表示学习
CreateAMind
27+阅读 · 2019年1月4日
Unsupervised Learning via Meta-Learning
CreateAMind
44+阅读 · 2019年1月3日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
18+阅读 · 2018年12月24日
【推荐】ResNet, AlexNet, VGG, Inception:各种卷积网络架构的理解
机器学习研究会
20+阅读 · 2017年12月17日
【推荐】RNN/LSTM时序预测
机器学习研究会
25+阅读 · 2017年9月8日
【推荐】SVM实例教程
机器学习研究会
17+阅读 · 2017年8月26日
【推荐】(Keras)LSTM多元时序预测教程
机器学习研究会
25+阅读 · 2017年8月14日
相关基金
国家自然科学基金
1+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
1+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
Top
微信扫码咨询专知VIP会员