论文标题
Skolem遇到了Schanuel
Skolem Meets Schanuel
论文作者
论文摘要
著名的Skolem-Mahler-Lech定理指出，线性复发序列的零集是有限的集合和有限的许多算术进程的结合。相应的计算问题Skolem问题要求确定给定的线性复发序列是否为零项。尽管Skolem-Mahler-Lech定理已有近90年的历史，但Skolem问题的可决定性仍然开放。本文的主要贡献是解决简单线性复发序列（具有简单特征根）的Skolem问题的算法。每当算法终止算法时，它会产生其输出正确的独立证书 - 一组零以及一组不存在零零的证人的集合。我们给出证明，该算法始终终止假设两个经典的理论猜想：Skolem猜想（也称为指数局部 - 全球原则）和$ p $ -Adic-Adic Schanuel猜想。在工具\ textsc {skolem}内实现此算法的初步实验指出了该方法的实际适用性。
The celebrated Skolem-Mahler-Lech Theorem states that the set of zeros of a linear recurrence sequence is the union of a finite set and finitely many arithmetic progressions. The corresponding computational question, the Skolem Problem, asks to determine whether a given linear recurrence sequence has a zero term. Although the Skolem-Mahler-Lech Theorem is almost 90 years old, decidability of the Skolem Problem remains open. The main contribution of this paper is an algorithm to solve the Skolem Problem for simple linear recurrence sequences (those with simple characteristic roots). Whenever the algorithm terminates, it produces a stand-alone certificate that its output is correct -- a set of zeros together with a collection of witnesses that no further zeros exist. We give a proof that the algorithm always terminates assuming two classical number-theoretic conjectures: the Skolem Conjecture (also known as the Exponential Local-Global Principle) and the $p$-adic Schanuel Conjecture. Preliminary experiments with an implementation of this algorithm within the tool \textsc{Skolem} point to the practical applicability of this method.
