Document Open Access Logo

Skolem Meets Schanuel

Authors Yuri Bilu , Florian Luca , Joris Nieuwveld, Joël Ouaknine , David Purser , James Worrell

PDF
Thumbnail PDF

File

LIPIcs.MFCS.2022.20.pdf
  • Filesize: 0.75 MB
  • 15 pages

Document Identifiers

Author Details

Yuri Bilu
  • Institut de Mathématiques de Bordeaux, Université de Bordeaux and CNRS, Talence, France
Florian Luca
  • School of Mathematics, University of the Witwatersrand, Johannesburg, South Africa
  • Research Group in Algebraic Structures & Applications, King Abdulaziz University, Saudi Arabia
  • Centro de Ciencias Matemáticas UNAM, Morelia, Mexico
  • Max Planck Institute for Software Systems, Saarland Informatics Campus, Germany
Joris Nieuwveld
  • Max Planck Institute for Software Systems, Saarland Informatics Campus, Germany
Joël Ouaknine
  • Max Planck Institute for Software Systems, Saarland Informatics Campus, Germany
David Purser
  • University of Warsaw, Poland
James Worrell
  • Department of Computer Science, University of Oxford, UK

Funding

  • Bilu, Yuri: Supported by ANR project JINVARIANT, by the Max Planck Institute for Software Systems, Saarland Informatics Campus, Germany, and by the Max Planck Institute for Mathematics, Bonn, Germany.
  • Ouaknine, Joël: Also affiliated with Keble College, Oxford as http://emmy.network/ Fellow, and supported by DFG grant 389792660 as part of TRR 248 (see https://perspicuous-computing.science).

Cite AsGet BibTex

Yuri Bilu, Florian Luca, Joris Nieuwveld, Joël Ouaknine, David Purser, and James Worrell. Skolem Meets Schanuel. In 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 241, pp. 20:1-20:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.MFCS.2022.20

Abstract

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 Skolem point to the practical applicability of this method.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • Skolem Problem
  • Skolem Conjecture
  • Exponential Local-Global Principle
  • p-adic Schanuel Conjecture

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. M. Agrawal, S. Akshay, B. Genest, and P. S. Thiagarajan. Approximate verification of the symbolic dynamics of Markov chains. J. ACM, 62(1):2:1-2:34, 2015. Google Scholar
  2. S. Akshay, T. Antonopoulos, J. Ouaknine, and J. Worrell. Reachability problems for Markov chains. Inf. Process. Lett., 115(2):155-158, 2015. Google Scholar
  3. S. Almagor, T. Karimov, E. Kelmendi, J. Ouaknine, and J. Worrell. Deciding ω-regular properties on linear recurrence sequences. Proc. ACM Program. Lang., 5(POPL), 2021. Google Scholar
  4. C. Baier, F. Funke, S. Jantsch, T. Karimov, E. Lefaucheux, F. Luca, J. Ouaknine, D. Purser, M. A. Whiteland, and J. Worrell. The Orbit Problem for parametric linear dynamical systems. In 32nd International Conference on Concurrency Theory, CONCUR 2021, volume 203 of LIPIcs, pages 28:1-28:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. Google Scholar
  5. G. Barthe, C. Jacomme, and S. Kremer. Universal equivalence and majority of probabilistic programs over finite fields. In LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, pages 155-166. ACM, 2020. Google Scholar
  6. B. Bartolome, Y. Bilu, and F. Luca. On the exponential local-global principle. Acta Arith., 159(2):101-111, 2013. Google Scholar
  7. Cs. Bertók and L. Hadju. A Hasse-type principle for exponential Diophantine equations and its applications. Math. Comput., 85:849-860, 2016. Google Scholar
  8. Cs. Bertók and L. Hadju. A Hasse-type principle for exponential Diophantine equations over number fields and its applications. Monatshefte Math., 187:425-436, 2018. Google Scholar
  9. V. Blondel and J. Tsitsiklis. A survey of computational complexity results in systems and control. Automatica, 36(9):1249-1274, 2000. URL: https://doi.org/10.1016/S0005-1098(00)00050-9.
  10. V. D. Blondel and N. Portier. The presence of a zero in an integer linear recurrent sequence is NP-hard to decide. Linear Algebra and Its Applications, 351-352, 2002. Google Scholar
  11. A. Brumer. On the units of algebraic number fields. Mathematika, 14:121-124, 1967. Google Scholar
  12. F. Calegari and B. Mazur. Nearly ordinary Galois deformations over arbitrary number fields. J. Inst. Math. Jussieu, 8(1):99-177, 2009. Google Scholar
  13. K. Chatterjee and L. Doyen. Stochastic processes with expected stopping time. In 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS, pages 1-13. IEEE, 2021. Google Scholar
  14. V. Chonev, J. Ouaknine, and J. Worrell. The Polyhedron-Hitting Problem. In Proceedings of the Twenty-Sixth Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 2015, pages 940-956. SIAM, 2015. Google Scholar
  15. G. Everest, A. van der Poorten, I. Shparlinski, and T. Ward. Recurrence Sequences. American Mathematical Society, 2003. Google Scholar
  16. N. Fijalkow, J. Ouaknine, A. Pouly, J. Sousa Pinto, and J. Worrell. On the decidability of reachability in linear time-invariant systems. In Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2019, pages 77-86. ACM, 2019. Google Scholar
  17. F. Gouvea. p-adic Numbers: An Introduction, Second Edition. Universitext. Springer, 1997. Google Scholar
  18. T. Karimov, E. Lefaucheux, J. Ouaknine, D. Purser, A. Varonka, M. A. Whiteland, and J. Worrell. What’s decidable about linear loops? Proc. ACM Program. Lang., 6(POPL), 2022. Google Scholar
  19. J. C. Lagarias and A. M. Odlyzko. Effective versions of the Chebotarev density theorem. Academic Press, London, 1977. Google Scholar
  20. S. Landau. Factoring polynomials over algebraic number fields. SIAM Journal on Computing, 14(1):184-195, 1985. Google Scholar
  21. Serge Lang. Introduction to Transcendental Numbers. Addison-Wesley, 1966. Google Scholar
  22. R. Lipton, F. Luca, J. Nieuwveld, J. Ouaknine, D. Purser, and J. Worrell. On the Skolem Problem and the Skolem Conjecture. To appear, Proceedings of the 37th Annual ACM/IEEE Symposium on Logic and Computer Science, LICS'22, 2022. Google Scholar
  23. A. Macintyre and A. J. Wilkie. On the decidability of the real exponential field. In Piergiorgio Odifreddi, editor, Kreiseliana. About and Around Georg Kreisel, pages 441-467. A K Peters, 1996. Google Scholar
  24. N. Mariaule. p-adic exponential ring, p-adic Schanuel’s conjecture and decidability. PhD Thesis, University of Manchester, 2014. Google Scholar
  25. D. W. Masser. Linear relations on algebraic groups. In New Advances in Transcendence Theory. Cambridge University Press, 1988. Google Scholar
  26. M. Mignotte, T. N. Shorey, and R. Tijdeman. The distance between terms of an algebraic recurrence sequence. Journal für die reine und angewandte Mathematik, 349, 1984. Google Scholar
  27. J. Ouaknine and J. Worrell. On linear recurrence sequences and loop termination. ACM SIGLOG News, 2(2):4-13, 2015. Google Scholar
  28. J. Piribauer and C. Baier. On Skolem-hardness and saturation points in Markov decision processes. In 47th International Colloquium on Automata, Languages, and Programming, ICALP 2020, volume 168 of LIPIcs, pages 138:1-138:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. Google Scholar
  29. G. Rozenberg and A. Salomaa. Cornerstones of Undecidability. Prentice Hall, 1994. Google Scholar
  30. A. Schinzel. Abelian binomials, power residues and exponential congruences. Acta Arith., 32(3):245-274, 1977. Google Scholar
  31. A. Schinzel. On the congruence u_n ≡ c (mod p) where u_n is a recurring sequence of the second order. Acta Acad. Paedagog. Agriensis Sect. Math., 30:147-165, 2003. Google Scholar
  32. Th. Skolem. Anwendung exponentieller Kongruenzen zum Beweis der Unlösbarkeit gewisser diophantischer Gleichungen. Avhdl. Norske Vid. Akad. Oslo I, 12:1-16, 1937. Google Scholar
  33. M. Soittola. On D0L synthesis problem. In A. Lindenmayer and G. Rozenberg, editors, Automata, Languages, Development. North-Holland, 1976. Google Scholar
  34. N. K. Vereshchagin. The problem of appearance of a zero in a linear recurrence sequence (in Russian). Mat. Zametki, 38(2), 1985. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact