Document Open Access Logo

On the Existential Theory of the Reals Enriched with Integer Powers of a Computable Number

Authors Jorge Gallego-Hernández , Alessio Mansutti

PDF
Thumbnail PDF

File

LIPIcs.STACS.2025.37.pdf
  • Filesize: 0.88 MB
  • 18 pages

Document Identifiers

Author Details

Jorge Gallego-Hernández
  • IMDEA Software Institute, Madrid, Spain
  • Universidad Politécnica de Madrid, Spain
Alessio Mansutti
  • IMDEA Software Institute, Madrid, Spain

Funding

This work is part of a project that is partially funded by the Madrid Regional Government (César Nombela grant 2023-T1/COM-29001), and by MCIN/AEI/10.13039/501100011033/FEDER, EU (grant PID2022-138072OB-I00).

Acknowledgements

We would like to thank Michael Benedikt and Dmitry Chistikov for the insightful discussions on the paper [Avigad and Yin, Theor. Comput. Sci., 2007], and Andrew Scoones and James Worrell for providing guidance through the number theory literature. We are also grateful to the anonymous referees for comments and corrections.

Cite As Get BibTex

Jorge Gallego-Hernández and Alessio Mansutti. On the Existential Theory of the Reals Enriched with Integer Powers of a Computable Number. In 42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 327, pp. 37:1-37:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.STACS.2025.37

Abstract

This paper investigates ∃ℝ(ξ^ℤ), that is the extension of the existential theory of the reals by an additional unary predicate ξ^ℤ for the integer powers of a fixed computable real number ξ > 0. If all we have access to is a Turing machine computing ξ, it is not possible to decide whether an input formula from this theory is satisfiable. However, we show an algorithm to decide this problem when  
- ξ is known to be transcendental, or 
- ξ is a root of some given integer polynomial (that is, ξ is algebraic).  In other words, knowing the algebraicity of ξ suffices to circumvent undecidability. Furthermore, we establish complexity results under the proviso that ξ enjoys what we call a polynomial root barrier. Using this notion, we show that the satisfiability problem of ∃ℝ(ξ^ℤ) is  
- in ExpSpace if ξ is an algebraic number, and 
- in 3Exp if ξ is a logarithm of an algebraic number, Euler’s e, or the number π, among others.
To establish our results, we first observe that the satisfiability problem of ∃ℝ(ξ^ℤ) reduces in exponential time to the problem of solving quantifier-free instances of the theory of the reals where variables range over ξ^ℤ. We then prove that these instances have a small witness property: only finitely many integer powers of ξ must be considered to find whether a formula is satisfiable. Our complexity results are shown by relying on well-established machinery from Diophantine approximation and transcendental number theory, such as bounds for the transcendence measure of numbers.
As a by-product of our results, we are able to remove the appeal to Schanuel’s conjecture from the proof of decidability of the entropic risk threshold problem for stochastic games with rational probabilities, rewards and threshold [Baier et al., MFCS, 2023]: when the base of the entropic risk is e and the aversion factor is a fixed algebraic number, the problem is (unconditionally) in Exp.

Subject Classification

ACM Subject Classification
  • Computing methodologies → Symbolic and algebraic algorithms
Keywords
  • Theory of the reals with exponentiation
  • decision procedures
  • computability

Metrics

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

Related Versions

References

  1. Melanie Achatz, Scott McCallum, and Volker Weispfenning. Deciding polynomial-exponential problems. In ISSAC, pages 215-222, 2008. URL: https://doi.org/10.1145/1390768.1390799.
  2. Shaull Almagor, Dmitry Chistikov, Joël Ouaknine, and James Worrell. O-minimal invariants for discrete-time dynamical systems. ACM Trans. Comput. Log., 23(2), 2022. URL: https://doi.org/10.1145/3501299.
  3. Hirokazu Anai and Volker Weispfenning. Deciding linear-trigonometric problems. In ISSAC, pages 14-22, 2000. URL: https://doi.org/10.1145/345542.345567.
  4. Jeremy Avigad and Yimu Yin. Quantifier elimination for the reals with a predicate for the powers of two. Theor. Comput. Sci., 370(1-3):48-59, 2007. URL: https://doi.org/10.1016/J.TCS.2006.10.005.
  5. Christel Baier, Krishnendu Chatterjee, Tobias Meggendorfer, and Jakob Piribauer. Entropic risk for turn-based stochastic games. In MFCS, volume 272, pages 15:1-15:16, 2023. URL: https://doi.org/10.4230/LIPICS.MFCS.2023.15.
  6. David H. Bailey, Peter B. Borwein, and Simon Plouffe. On the rapid computation of various polylogarithmic constants. Math. Comput., 66:903-913, 1997. URL: https://doi.org/10.1090/S0025-5718-97-00856-9.
  7. Gilles Barthe, Rohit Chadha, Paul Krogmeier, A. Prasad Sistla, and Mahesh Viswanathan. Deciding accuracy of differential privacy schemes. Proc. ACM Program. Lang., 5(POPL):1-30, 2021. URL: https://doi.org/10.1145/3434289.
  8. Saugata Basu, Richard Pollack, and Marie-Françoise Roy. On the combinatorial and algebraic complexity of quantifier elimination. J. ACM, 43(6):1002-1045, 1996. URL: https://doi.org/10.1145/235809.235813.
  9. Sylvain Bruiltet. D'une mesure d'approximation simultanée à une mesure d'irrationalité: le cas de Γ(1/4) et Γ(1/3). Acta Arith., 104(3):243-281, 2002. URL: https://doi.org/10.4064/aa104-3-3.
  10. Yann Bugeaud. Approximation by Algebraic Numbers. Cambridge Tracts in Mathematics. Cambridge University Press, 2004. URL: https://doi.org/10.1017/CBO9780511542886.
  11. Jin-yi Cai, Richard J. Lipton, and Yechezkel Zalcstein. The complexity of the A B C problem. SIAM J. Comput., 29(6):1878-1888, 2000. URL: https://doi.org/10.1137/S0097539794276853.
  12. John Canny. Some algebraic and geometric computations in PSPACE. In STOC, pages 460-467, 1988. URL: https://doi.org/10.1145/62212.62257.
  13. Dmitry Chistikov, Stefan Kiefer, Andrzej S. Murawski, and David Purser. The big-o problem. Log. Methods Comput. Sci., 18(1), 2022. URL: https://doi.org/10.46298/LMCS-18(1:40)2022.
  14. Mohan Dantam and Amaury Pouly. On the decidability of reachability in continuous time linear time-invariant systems. In HSCC, 2021. URL: https://doi.org/10.1145/3447928.3456705.
  15. Laure Daviaud, Marcin Jurdziński, Ranko Lazić, Filip Mazowiecki, Guillermo A. Pérez, and James Worrell. When are emptiness and containment decidable for probabilistic automata? JCSS, 119:78-96, 2021. URL: https://doi.org/10.1016/j.jcss.2021.01.006.
  16. Andreas Dolzmann and Thomas Sturm. REDLOG: computer algebra meets computer logic. SIGSAM Bull., 31(2):2-9, 1997. URL: https://doi.org/10.1145/261320.261324.
  17. Lou van den Dries. The field of reals with a predicate for the powers of two. Manuscripta Math., 54:187-196, 1986. URL: https://doi.org/10.1007/BF01171706.
  18. Lou van den Dries and Ayhan Günaydin. The fields of real and complex numbers with a small multiplicative group. Proc. Lond. Math. Soc., 93(1):43-81, 2006. URL: https://doi.org/10.1017/S0024611506015747.
  19. Teemu Hankala, Miika Hannula, Juha Kontinen, and Jonni Virtema. Complexity of neural network training and ETR: extensions with effectively continuous functions. In AAAI, pages 12278-12285, 2024. URL: https://doi.org/10.1609/AAAI.V38I11.29118.
  20. Philipp Hieronymi. Defining the set of integers in expansions of the real field by a closed discrete set. Proc. Am. Math. Soc., 138(6):2163-2168, 2010. URL: https://doi.org/10.1090/S0002-9939-10-10268-8.
  21. Omri Isac, Yoni Zohar, Clark W. Barrett, and Guy Katz. DNN verification, reachability, and the exponential function problem. In CONCUR, pages 26:1-26:18, 2023. URL: https://doi.org/10.4230/LIPICS.CONCUR.2023.26.
  22. A. G. Khovanskii. Fewnomials. Transl. Math. Monogr., 88, 1991. Translated by Smilka Zdravkovska. URL: https://doi.org/10.1090/mmono/088.
  23. Arjen K Lenstra, Hendrik Willem Lenstra, and László Lovász. Factoring polynomials with rational coefficients. Math. Ann., 261:515-534, 1982. URL: https://doi.org/10.1007/bf01457454.
  24. Angus Macintyre and Alex 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
  25. Kurt Mahler. Zur Approximation der Exponentialfunktion und des Logarithmus. Teil I. Journal für die reine und angewandte Mathematik, 166:118-150, 1932. Google Scholar
  26. David Marker. Model Theory: An Introduction. Graduate Texts in Mathematics. Springer, 2002. URL: https://doi.org/10.1007/b98860.
  27. D. W. Masser. Linear relations on algebraic groups, pages 248-262. Cambridge University Press, 1988. Google Scholar
  28. Scott McCallum and Volker Weispfenning. Deciding polynomial-transcendental problems. J. Symb. Comput., 47(1):16-31, 2012. URL: https://doi.org/10.1016/J.JSC.2011.08.004.
  29. J. Popken. Zur Transzendenz von e. Mathematische Zeitschrift, 29:525-541, 1929. Google Scholar
  30. Q. I. Rahman and G. Schmeisser. Analytic Theory of Polynomials. Oxford University Press, September 2002. URL: https://doi.org/10.1093/oso/9780198534938.001.0001.
  31. H. G. Rice. Recursive real numbers. Proc. Am. Math. Soc., 5(5):784-791, 1954. URL: https://doi.org/10.2307/2031867.
  32. Walter J. Savitch. Relationships between nondeterministic and deterministic tape complexities. JCSS, 4(2):177-192, 1970. URL: https://doi.org/10.1016/S0022-0000(70)80006-X.
  33. Michel Waldschmidt. Transcendence measures for exponentials and logarithms. J. Aust. Math. Soc., 25(4):445-465, 1978. URL: https://doi.org/10.1017/S1446788700021431.
  34. Volker Weispfenning. The complexity of almost linear diophantine problems. J. Symb. Comput., 10(5):395-404, 1990. URL: https://doi.org/10.1016/S0747-7171(08)80051-X.
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 About DROPS Imprint Privacy Contact