Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Jorge Gallego-Hernández, Alessio Mansutti

TL;DR

This work analyzes the existential theory of the reals enriched with integer powers of a fixed computable base $\xi>0$, denoted $\exists\mathbb{R}(\xi^{\mathbb{Z}})$. It introduces the root-barrier framework to obtain decidability and precise complexity bounds that depend on the barrier exponent and on whether $\xi$ is algebraic or transcendental, achieving $\text{ExpSpace}$ for algebraic bases and $\text{3Exp}$ for a broad class of transcendental bases (including $\pi$ and $e$). The authors provide a constructive procedure that reduces general satisfiability to a small witness over integer powers, along with a quantifier-elimination-like technique and a relativisation argument that yield a small-model property. As a by-product, they remove reliance on Schanuel’s conjecture from certain entropic risk threshold results, obtaining unconditional decidability in $\text{ExpTime}$ for bases $e$ (and algebraic) when the aversion is fixed algebraic. These results advance understanding of decidability boundaries for extended real-analytic theories and have implications for stochastic games and related decision problems.

Abstract

This paper investigates $\exists\mathbb{R}(r^{\mathbb{Z}})$, that is the extension of the existential theory of the reals by an additional unary predicate $r^{\mathbb{Z}}$ for the integer powers of a fixed computable real number $r > 0$. If all we have access to is a Turing machine computing $r$, it is not possible to decide whether an input formula from this theory satisfiable. However, we show an algorithm to decide this problem when: 1. $r$ is known to be transcendental, or 2. $r$ is a root of some given integer polynomial (that is, $r$ is algebraic). In other words, knowing the algebraicity of $r$ suffices to circumvent undecidability. Furthermore, we establish complexity results under the proviso that $r$ enjoys what we call a polynomial root barrier. Using this notion, we show that the satisfiability problem of $\exists\mathbb{R}(r^{\mathbb{Z}})$ is 1. in NEXPTIME if $r$ is a natural number, 2. in EXPSPACE if $r$ is an algebraic number, and 3. in 3EXP if $r$ belongs to a family of transcendental numbers including $π$ and Euler's $e$. 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'23]: when the base of the entropic risk is Euler's $e$ and the aversion factor is a fixed algebraic number, the problem is in EXP.

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

TL;DR

This work analyzes the existential theory of the reals enriched with integer powers of a fixed computable base , denoted . It introduces the root-barrier framework to obtain decidability and precise complexity bounds that depend on the barrier exponent and on whether is algebraic or transcendental, achieving for algebraic bases and for a broad class of transcendental bases (including and ). The authors provide a constructive procedure that reduces general satisfiability to a small witness over integer powers, along with a quantifier-elimination-like technique and a relativisation argument that yield a small-model property. As a by-product, they remove reliance on Schanuel’s conjecture from certain entropic risk threshold results, obtaining unconditional decidability in for bases (and algebraic) when the aversion is fixed algebraic. These results advance understanding of decidability boundaries for extended real-analytic theories and have implications for stochastic games and related decision problems.

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 . If all we have access to is a Turing machine computing , it is not possible to decide whether an input formula from this theory satisfiable. However, we show an algorithm to decide this problem when: 1. is known to be transcendental, or 2. 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 1. in NEXPTIME if is a natural number, 2. in EXPSPACE if is an algebraic number, and 3. in 3EXP if belongs to a family of transcendental numbers including and Euler's . 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'23]: when the base of the entropic risk is Euler's and the aversion factor is a fixed algebraic number, the problem is in EXP.

Paper Structure

This paper contains 42 sections, 7 theorems, 90 equations, 1 figure, 1 table, 2 algorithms.

Table of Contents

  1. Introduction
  2. Approaching complexity bounds with root barriers
  3. Preliminaries
  4. Sets, vectors, and basic functions.
  5. Integer polynomials.
  6. Computable numbers, and algebraic and transcendental numbers.
  7. The theory $\exists\mathbb{R}\xspace({\xi\xspace}^{\mathbb{Z}\xspace}\xspace)$.
  8. Refined representation for fixed algebraic numbers
  9. An algorithm for deciding the existential theory
  10. Step I (lines \ref{['algo:line1']}--\ref{['algo:line6']}): reducing the variables to integer powers of the base
  11. Step II (lines \ref{['algo:line7']} and \ref{['algo:line8']}): solving the existential theory over integer powers of the base
  12. Step III (line \ref{['algo:line9']}): polynomial sign evaluation
  13. Handling small bases
  14. Correctness of Algorithm \ref{['algo:main-procedure']} (Proof of \ref{['theorem:result-root-barrier']}.\ref{['theorem:result-root-barrier:point3']})
  15. Running time (Proof of \ref{['theorem:general-result-root-barrier']})
  16. ...and 27 more sections

Key Result

Lemma 4.1

Let $p(x)$ be an integer polynomial, and let ${r \in \mathbb{R}\xspace}$ with $\left|r\right|\xspace \leq K$ for some $K \geq 1$. Consider $L,M \in \mathbb{N}\xspace$ satisfying $M\geq L + \log(\textup{h}\xspace(p)+1) + 2 \deg(p) \cdot \log(K+1)$. For every $r^* \in \mathbb{R}\xspace$, if $\left|r-r

Figures (1)

  • Figure 1: High-level idea of the quantifier elimination procedure. Dashed rectangles are intervals corresponding to the set of solutions over $\mathbb{R}\xspace$ of a (univariate) formula $\varphi\xspace$. To search for a solution over ${\xi\xspace}^{\mathbb{Z}\xspace}\xspace$, it suffices to look for elements of ${\xi\xspace}^{\mathbb{Z}\xspace}\xspace$ that are close to the endpoints of these intervals. At each endpoint, a polynomial in $\varphi\xspace$ must evaluate to zero (since around endpoints the truth of $\varphi\xspace$ changes), so it suffices to look for integer powers of $\xi\xspace$ that are close to roots or polynomials in $\varphi\xspace$.

Theorems & Definitions (59)

  • Conjecture 2.1
  • Definition 2.2
  • proof
  • proof
  • Lemma 4.1
  • proof
  • proof
  • proof
  • proof
  • proof
  • ...and 49 more