# On the Decidability of Monadic Second-Order Logic with Arithmetic Predicates

Valérie Berthé, Toghrul Karimov, Joris Nieuwveld, Joël Ouaknine, Mihir

Vahanwala, James Worrell

► To cite this version:

Valérie Berthé, Toghrul Karimov, Joris Nieuwveld, Joël Ouaknine, Mihir Vahanwala, et al.. On the Decidability of Monadic Second-Order Logic with Arithmetic Predicates. LICS '24: 39th Annual ACM/IEEE Symposium on Logic in Computer Science, Jul 2024, Tallinn, Estonia. pp.1-14, 10.1145/3661814.3662119 . hal-04768908

HAL Id: hal-04768908

https://hal.science/hal-04768908v1

Submitted on 6 Nov 2024

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
<figure><img src="image_2.png" /></figure>

# On the Decidability of Monadic Second-Order Logic with Arithmetic Predicates

Valérie Berthé

berthe@irif.fr

Université Paris Cité, IRIF, CNRS

Paris, France

Toghrul Karimov

Joris Nieuwveld

Joël Ouaknine

Mihir Vahanwala

toghs@mpi-sws.org

jnieuwve@mpi-sws.org

joel@mpi-sws.org

mvahanwa@mpi-sws.org

Max Planck Institute for
Software Systems

Saarbrücken, Germany

James Worrell

jbw@cs.ox.ac.uk

University of Oxford, Department of
Computer Science

Oxford, United Kingdom

## ABSTRACT

We investigate the decidability of the monadic second-order (MSO) theory of the structure $⟨N; <, P₁, ..., P_k⟩$, for various unary predicates $P₁, ..., P_k ⊆ N$. We focus in particular on ‘arithmetic’ predicates arising in the study of linear recurrence sequences, such as fixed-base powers $Pow_k = {k^n : n ∈ N}$, k-th powers $N_k = {n^k : n ∈ N}$, and the set of terms of the Fibonacci sequence $Fib = {0, 1, 2, 3, 5, 8, 13, ...}$ (and similarly for other linear recurrence sequences having a single, non-repeated, dominant characteristic root). We obtain several new unconditional and conditional decidability results, a select sample of which are the following:

* The MSO theory of $⟨N; <, Pow₂, Fib⟩$ is decidable;

* The MSO theory of $⟨N; <, Pow₂, Pow₃, Pow₆⟩$ is decidable;

* The MSO theory of $⟨N; <, Pow₂, Pow₃, Pow₅⟩$ is decidable assuming Schanuel’s conjecture;

* The MSO theory of $⟨N; <, Pow₄, N₂⟩$ is decidable;

* The MSO theory of $⟨N; <, Pow₂, N₂⟩$ is Turing-equivalent to the MSO theory of $⟨N; <, S⟩$, where S is the predicate corresponding to the binary expansion of $\sqrt{2}$. (As the binary expansion of $\sqrt{2}$ is widely believed to be normal, the corresponding MSO theory is in turn expected to be decidable.)

These results are obtained by exploiting and combining techniques from dynamical systems, number theory, and automata theory.

The full version of this paper can be found in [8].

## CCS CONCEPTS

* Theory of computation → Logic and verification.

## KEYWORDS

Monadic second-order logic, linear recurrence sequences, toric words, cutting sequences, decidability

<figure><img src="image_3.png" /></figure>

This work is licensed under a Creative Commons Attribution International 4.0 License.
LICS '24, July 8–11, 2024, Tallinn, Estonia

© 2024 Copyright held by the owner/author(s).

ACM ISBN 979-8-4007-0660-8/24/07

https://doi.org/10.1145/3661814.3662119

## ACM Reference Format:

Valérie Berthé, Toghrul Karimov, Joris Nieuwveld, Joël Ouaknine, Mihir Vahanwala, and James Worrell. 2024. On the Decidability of Monadic Second-Order Logic with Arithmetic Predicates. In *39th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS '24)*, July 8–11, 2024, Tallinn, Estonia. ACM, New York, NY, USA, 14 pages. https://doi.org/10.1145/3661814.3662119

## 1 INTRODUCTION

Büchi’s seminal 1962 paper [10] established the decidability of the monadic second-order (MSO) theory of the structure $⟨N; <⟩$, and in so doing brought to light the profound connections between mathematical logic and automata theory. Over the ensuing decades, considerable work has been devoted to the question of which expansions of $⟨N; <⟩$ retain MSO decidability. In other words, for which unary predicates $P₁, ..., P_k$ is the MSO theory of $⟨N; <, P₁, ..., P_k⟩$ decidable?<fnref n="1" /> Here by unary predicate we mean a fixed set of non-negative integers $P ⊆ N$. Taking, for example, $P$ to be the set of prime numbers, Büchi and Landweber [11] observed in 1969 that a proof of decidability of the MSO theory of $⟨N; <, P⟩$ would “seem very difficult”, as it would *inter alia* enable one (at least in principle) to settle the twin prime conjecture. (Decidability was subsequently established assuming Schinzel’s hypothesis H [5].)

The set of prime numbers is, of course, highly intricate. In 1966, Elgot and Rabin [17] considered a large class of simpler predicates of ‘arithmetic’ origin, such as, for any fixed $k$, the set $Pow_k = \{k^n : n \in N\}$ of powers of $k$, and the set $N_k = \{n^k : n \in N\}$ of $k$-th powers. For any such predicate $P$, they systematically established decidability of the MSO theory of $⟨N; <, P⟩$ by using (in modern parlance) a notion of *effective profinite ultimate periodicity* (essentially an automata-theoretic concept). Many years later, the theory was substantially developed and extended by Carton and Thomas [14], Rabinovich [30], and Rabinovich and Thomas [31], among others. A related key concept is that of *effective almost periodicity*, introduced in the 1980s by Semënov [35], and recently brought to bear in the MSO model checking of linear dynamical systems [22].

It is notable that whilst Elgot and Rabin establish separately the decidability of the MSO theories, for example, of $⟨N; <, Pow₂⟩$ and

<footnote n="1">¹The restricted focus on unary (or monadic) predicates is justified by the fact that most natural non-unary predicates immediately lead to undecidability [32].</footnote>
(N; <, Pow₃), they remain resolutely silent on the obvious joint expansion (N; <, Pow₂, Pow₃). This in hindsight is wholly unsurprising: there are various statements that one can express in the above theory whose truth values are highly non-trivial to determine: for example, for given fixed a, b, the assertion that there exist infinitely many powers of 3 whose distance to the next power of 2 is congruent to a modulo b. An immediate corollary of our first main result, Thm. 5.1, is that the MSO theory of (N; <, Pow₂, Pow₃) is indeed decidable. Although this is new, we should mention that decidability of the first-order theory of (N; <, Pow₂, Pow₃) has been known for over forty years, an important result of Semënov [34].

Looking over the last several decades' worth of research work on monadic second-order expansions of the structure (N; <), it is fair to say that the bulk of the attention has focused on the addition of a single predicate P. The obvious reason is that whilst, in general, the decidability of single-predicate expansions of (N; <) can usually be handled with automata-theoretic techniques alone, by reasoning about individual patterns in isolation, this is not the case when multiple predicates are at play simultaneously. Such collections of predicates can exhibit highly complex interaction patterns, which existing approaches are ill-equipped to handle.

In this paper, we show that key aspects of such interactions can be modelled in the theory of *dynamical systems*, and in particular via the notion of *toric words* [7]. In addition, we make use of number-theoretic tools to ensure effectiveness at various junctures of our algorithms. Some of our results are conditional: whereas Baker's theorem on linear forms in logarithms (alongside other tools) underpins the decidability of the MSO theory of (N; <, Pow₂, Pow₃), we are only able to show decidability of the MSO theory of (N; <, Pow₂, Pow₃, Pow₅) subject to Schanuel's conjecture, a central hypothesis in transcendental number theory. Intuitively, the reason is that whilst Baker's theorem suffices to handle interaction patterns of powers of 2 and powers of 3, the injection of powers of 5 into the mix exceeds the limits of contemporary number-theoretic knowledge.

Our paper contains two main results. Theorem 5.1 considers predicates arising from the sets of values achieved by certain linear recurrence sequences, generalising the predicates considered above. A simplified version of that result is as follows:

**THEOREM 1.1.** Let $\rho_1, \dots, \rho_d > 1$ be natural numbers.

(1) The MSO theory of $\langle N; <, \mathrm{Pow}_{\rho_1}, \dots, \mathrm{Pow}_{\rho_d} \rangle$ is decidable assuming Schanuel's conjecture.

(2) If $1/\log(\rho_1), \dots, 1/\log(\rho_d)$ are linearly independent over $\mathbb{Q}$, then the decidability is unconditional.

(3) If each triple of distinct $\rho_i, \rho_j, \rho_k$ is multiplicatively dependent, then the decidability is unconditional.

Item (3) captures, for example, the decidability of the MSO theory of $\langle N; <, \mathrm{Pow}_2, \mathrm{Pow}_3, \mathrm{Pow}_6 \rangle$. Our second main result is Thm. 6.4, restated here:

**THEOREM 1.2.** Let $p, q, b, d$ be natural numbers such that $\eta = \sqrt[d]{p/q}$ is irrational, $P_1 = \{qn^d: n \in N\}$, and $P_2 = \{pb^{nd}: n \in N\}$. The decidability of the MSO theory of $\langle N; <, P_1, P_2 \rangle$ is Turing-equivalent to that of the MSO theory of the base-$b$ expansion of $\eta$.<fnref n="2" />

The underlying dynamical system here is of a symbolic nature: it consists of the base-$b$ expansion of the irrational number $\eta$, which is a $d$-th root of a rational number. Such expansions are widely conjectured to be normal, and a *fortiori* weakly normal: every finite pattern of digits should occur infinitely often. As the MSO theory of any weakly normal word is decidable (Thm. 4.16), we obtain a conditional decidability result.

Note that when $\eta$ is rational, we obtain unconditional decidability (Thm. 6.3), thanks to a composition result (Thm. 4.11) which we believe may be of independent interest. Here we state a simple corollary of Thm. 6.3:

**COROLLARY 1.3.** For any positive integers $b$ and $d$, the MSO theory of $\langle N; <, \mathrm{Pow}_{b^d}, N_d \rangle$ is decidable.

For example, we recover from the above the decidability of the MSO theory of $\langle N; <, \mathrm{Pow}_4, N_2 \rangle$, mentioned in the abstract.

# 2 PRELIMINARIES

## 2.1 Words and Automata

By an alphabet $\Sigma$ we mean a finite non-empty set of letters. The sets of finite, non-empty, and infinite words over $\Sigma$ are denoted $\Sigma^*$, $\Sigma^+$, and $\Sigma^\omega$ respectively. For a finite or infinite word $\alpha$ and $n \in N$, we write $\alpha(n)$ for the nth letter of $\alpha$. Thus $\alpha = \alpha(0)\alpha(1)\dots$. We define $\alpha[n, m) := \alpha(n) \cdots \alpha(m-1)$, and assuming $\alpha$ is infinite, $\alpha[n, \infty) := \alpha(n)\alpha(n+1)\dots$. We denote the length of a finite word $w$ by $|w|$. A finite word $w \in \Sigma^*$ occurs at a position $n$ in $\alpha$ if $\alpha[n, n + |w|) = w$. Such $w$ is called a *factor* of $\alpha$. We will often factorise $\alpha \in \Sigma^\omega$ as $\alpha = u_0u_1\dots$, where $u_i \in \Sigma^*$ for all $i \in N$. Such a factorisation is uniquely determined by an increasing sequence $\langle k_n \rangle_{n=0}^\infty$ over $N$ such that $u_i = \alpha[k_i, k_{i+1})$ for all $i$. Finally, consider $\alpha_i \in \Sigma_i^\omega$ for $1 \le i \le d$. The *product word* $\alpha := \alpha_1 \times \dots \times \alpha_d$ is defined by $\alpha(n) = (\alpha_1(n), \dots, \alpha_d(n)) \in \Sigma_1 \times \dots \times \Sigma_d$ for all $n$.

Let $\alpha \in \Sigma^\omega$. We say that $\alpha$ is

(a) *effective* if for any $n \in N$, $\alpha(n)$ can be effectively computed,

(b) *weakly normal* if for every $w \in \Sigma^+$, $w$ occurs as a factor of $\alpha$ infinitely often, and

(c) *uniformly recurrent* if for every $w \in \Sigma^+$, either $w$ does not occur in $\alpha$, or there exists $R(w) \in N$ such that $w$ occurs in every factor of $\alpha$ of length $R(w)$. Equivalently, if $w$ occurs in $\alpha$, then there exists an integer $R(w)$ such that for all $N \in N$, $w$ occurs in $\alpha[N, N + R(w))$.

Prominent examples of uniformly recurrent words include the Thue-Morse word [2, Chap. 1] and all Sturmian words [24, Chap. 2].

A deterministic finite Muller automaton $\mathcal{A}$ over an alphabet $\Sigma$ is given by a tuple $(Q, q_{\mathrm{init}}, \delta, \mathcal{F})$, where $Q$ is the (finite) set of states, $q_{\mathrm{init}}$ is the initial state, $\delta: Q \times \Sigma \to Q$ is the transition function, and $\mathcal{F}$ is the acceptance condition consisting of subsets of $Q$. We denote by $\mathcal{A}(\alpha)$ the *run* of $\mathcal{A}$ on $\alpha$, which is the sequence of states visited when $\mathcal{A}$ reads $\alpha$. A word $\alpha \in \Sigma^\omega$ is accepted by $\mathcal{A}$ if the set $S$ of states appearing infinitely often in $\mathcal{A}(\alpha)$ is present in $\mathcal{F}$.

A deterministic finite transducer $\mathcal{B}$ over an input alphabet $\Sigma$ and an output alphabet $\Gamma$ is given by $(R, r_{\mathrm{init}}, \sigma)$, where $R$ is the (finite) set of states, $r_{\mathrm{init}}$ is the initial state, and $\sigma: R \times \Sigma \to R \times \Gamma^*$ is the transition function. At every step, $\mathcal{B}$ reads a letter from the input

<footnote>we mean the MSO theory of the structure $\langle N; <, P_0, \dots, P_{b-1} \rangle$, where each $P_i$ is the unary predicate $\{n \in N: \alpha(n) = i\}$.</footnote>

<footnote n="2">²The representation of $\eta$ in the base-$b$ number system is an infinite word $\alpha$ over the finite alphabet $\Sigma = \{0, 1, \dots, b-1\}$ of digits. By the MSO theory of an infinite word</footnote>
alphabet $\Sigma$, transitions to the next state, and outputs a finite word over the output alphabet $\Gamma$. We define $\sigma_R: R \times \Sigma \to R$ to be the function that returns the next state, and $\sigma_{\Gamma^*}: R \times \Sigma \to \Gamma^*$ to be the function that returns the output word. We denote by $\mathcal{B}(\alpha)$ the (possibly finite) word over $\Gamma$ output by $\mathcal{B}$ upon reading $\alpha \in \Sigma^\omega$.

Let $\mathcal{A}$ be a finite automaton as above. By a journey on $\mathcal{A}$ we mean an element of $J := Q \times Q \times 2^Q$. A path $q_0q_1q_2 \cdots q_n \in Q^{n+1}$ makes the journey $(q_0, q_n, V)$ where $V$ is the set of states occurring in the proper suffix $q_1q_2 \cdots q_n$. If $n \ge 1$, then $q_n \in V$ necessarily, but $q_0$ may not belong to $V$. The unique journey a word $w \in \Sigma^*$ makes starting in $q \in Q$, denoted by journey$(w, q)$, is the journey made by $q_0 \cdots q|_w|$, where $q_{i+1} = \delta(q_i, w(i))$ for $1 \le i < |w|$. The empty word makes journeys of the form $(q, q, \emptyset)$. If $v$ makes the journey $(q_1, q_3, V_1)$ and $w$ makes the journey $(q_3, q_2, V_2)$, then $vw$ makes the journey $(q_1, q_2, V_1 \cup V_2)$.

Next, we define the equivalence relation $\sim_{\mathcal{A}}$ as follows. Two words $v, w \in \Sigma^*$ are equivalent, denoted $v \sim_{\mathcal{A}} w$, if and only if the sets of journeys they can undertake (starting from various states) are identical. The equivalence is moreover a congruence: if $v \sim_{\mathcal{A}} w$ and $x \sim_{\mathcal{A}} y$, then $vx \sim_{\mathcal{A}} wy$. Observe that $\sim_{\mathcal{A}}$ is not the classical congruence associated with the automaton $\mathcal{A}$. Our choice, however, will be more convenient for technical reasons.

Since there are only finitely many equivalence classes of $\sim_{\mathcal{A}}$, the quotient of $\Sigma^*$ by $\sim_{\mathcal{A}}$ is a finite monoid $M$. We use $h$ to denote the natural morphism from $\Sigma^*$ into $M$. The morphism $h$ maps each letter to its equivalence class modulo $\sim_{\mathcal{A}}$. We also extend the function journey to take inputs from $M \times Q$: For equivalence class $m = [w]$ and state $q$, we define journey$(m, q) = \text{jour}(w, q)$. Finally, we will need the following lemma, whose proof is immediate.

**LEMMA 2.1.** Let $\mathcal{A}$ be an automaton as above and $\alpha \in \Sigma^\omega$ with factorisation $\alpha = u_0u_1 \cdots \in \Sigma^\omega$, where $u_n \in \Sigma^*$ for all $n$. Then the word $\mathcal{A}(\alpha)$ can be decomposed as the concatenation of journeys

$$ (q_0, q_1, V_0)(q_1, q_2, V_1)(q_2, q_3, V_2)\cdots $$

where $q_0 = q_{\text{init}}$, journey$(u_n, q_n) = (q_n, q_{n+1}, V_n)$ for all $n$, and for every $q \in Q$, the state $q$ appears infinitely often in $\mathcal{A}(\alpha)$ if and only if $q \in V_n$ for infinitely many $n \in \mathbb{N}$.

## 2.2 Monadic Second-Order Logic

Monadic second-order logic (MSO) is an extension of first-order logic that allows quantification over subsets of the universe. Such subsets can be viewed as unary (that is, monadic) predicates. We will only be interpreting MSO formulas over expansions of the structure $\langle \mathbb{N}; \langle \cdot, \cdot \rangle \rangle$. For a general perspective on MSO, see [9].

Let $\mathcal{S} = \langle \mathbb{N}; \langle P_1, \dots, P_m \rangle \rangle$ be a structure where each $P_i \subseteq \mathbb{N}$ is a unary predicate. We associate a language $\mathcal{L}_{\mathcal{S}}$ of terms and formulas with $\mathcal{S}$ as follows. The terms of $\mathcal{L}_{\mathcal{S}}$ are the countably many constant symbols $\{0, 1, 2, \dots\}$, lowercase variable symbols that stand for elements of $\mathbb{N}$, and uppercase variable symbols that denote subsets of $\mathbb{N}$. The formulas of $\mathcal{L}_{\mathcal{S}}$ are the well-formed statements constructed from the built-in equality ($=$) and membership ($\in$) symbols, logical connectives, quantification over elements of $\mathbb{N}$ (written $Qx$ for a quantifier $Q$), and quantification over subsets (written $QX$ for a quantifier $Q$). The MSO theory of the structure $\mathcal{S}$ is the set of all sentences belonging to $\mathcal{L}_{\mathcal{S}}$ that are true in $\mathcal{S}$. The MSO theory

of $\mathcal{S}$ is decidable if there exists an algorithm that, given a sentence $\varphi \in \mathcal{L}_{\mathcal{S}}$, decides if $\varphi$ belongs to the MSO theory of $\mathcal{S}$.

As an example, consider $\mathcal{S} = \langle \mathbb{N}; \langle \cdot, \cdot \rangle \rangle$ where $P$ is the set of all primes. Let $s(\cdot)$ be the successor function defined by $s(x) = y$ if and only if

$$ x < y \wedge \forall z. x < z \Rightarrow y \le z. $$

That is, $s(x) = x + 1$. Further let

$$ \varphi(X) := 1 \in X \wedge 0, 2 \notin X \wedge \forall x. x \in X \Leftrightarrow s(s(x)) \in X, $$

$$ \psi := \exists X: \varphi(X) \wedge \forall y. \exists z > y: z \in X \wedge P(z). $$

The formula $\varphi$ defines the subset $\{n: n \equiv 1 \pmod 3\}$ of $\mathbb{N}$, and $\psi$ is the sentence "there are infinitely many primes congruent to 1 modulo 3", which is the case. At the time of writing, it is not known whether the MSO theory of the structure $\mathcal{S}$ above is decidable.

The Acceptance Problem for an infinite word $\alpha$, denoted $\text{Acc}_\alpha$, is to determine, given a deterministic Muller automaton $\mathcal{A}$, whether $\mathcal{A}$ accepts $\alpha$. Let $P_1, \dots, P_d \subset \mathbb{N}$ be predicates and $\Sigma = \{0, 1\}^d$.

**Definition 2.2.** The characteristic word of $(P_1, \dots, P_d)$, written $\alpha := \text{Char}(P_1, \dots, P_d) \in \Sigma^\omega$, is defined by $\alpha(n) = (b_{n,1}, \dots, b_{n,d})$ where $b_{n,i} = 1$ if $n \in P_i$ and $b_{n,i} = 0$ otherwise.

The following is a seminal result of Büchi, through which he showed decidability of the MSO theory of $\langle \mathbb{N}; \langle \cdot, \cdot \rangle \rangle$.

**THEOREM 2.3 ([36, THMS. 5.4 AND 5.9]).** The decision problem of the MSO theory of the structure $\langle \mathbb{N}; \langle \cdot, \cdot \rangle, P_1, \dots, P_d \rangle$ is Turing-equivalent to $\text{Acc}_\alpha$, where $\alpha$ is the characteristic word of $(P_1, \dots, P_d)$.

## 2.3 Algebraic Numbers

A complex number $\lambda$ is algebraic if there exists $p \in \mathbb{Q}[x]$ such that $p(\lambda) = 0$. The set of algebraic numbers is denoted by $\overline{\mathbb{Q}}$. The unique irreducible monic polynomial that has $\lambda$ as a root is called the minimal polynomial of $\lambda$. A canonical representation of an algebraic number $\lambda$ consists of its minimal polynomial $p$ and sufficiently accurate rational approximations of the real and imaginary parts of $\lambda$ to distinguish it from the other roots of $p$. All arithmetic operations can be performed effectively on canonical representations of algebraic numbers [15, Sec. 4.2].

By a multiplicative relation of $(\lambda_1, \dots, \lambda_d) \in \mathbb{C}^d$ we mean $\mathbf{k} = (k_1, \dots, k_d) \in \mathbb{Z}^d$ such that $\lambda_1^{k_1} \cdots \lambda_d^{k_d} = 1$. We write

$$ G := G_M(\lambda_1, \dots, \lambda_d) $$

for the set of all multiplicative relations of $(\lambda_1, \dots, \lambda_d)$, which is a free abelian group under addition. If $G = \{(0, \dots, 0)\}$, we say that $X = \{\lambda_1, \dots, \lambda_d\}$ is multiplicatively independent. The rank of $G$ is the cardinality of a largest multiplicatively independent subset of $X$. If $\text{rank}(G) = m$, then $G$ has a basis $B = \{v_1, \dots, v_m\} \subseteq \mathbb{Z}^d$ that is linearly independent over $\mathbb{Q}$ with the property that every $z \in G$ can be written as an integer linear combination of $v_1, \dots, v_m$. If $\lambda_1, \dots, \lambda_d$ are algebraic, we can compute a basis of $G$ using a deep result of Masser [26].

**THEOREM 2.4 ([13]).** Given $\lambda_1, \dots, \lambda_d \in \overline{\mathbb{Q}}$, one can compute a basis for $G_M(\lambda_1, \dots, \lambda_d)$.

Finally, for $\lambda_1, \dots, \lambda_d$ as above, we define the group of additive relations as

$$ G_A(\lambda_1, \dots, \lambda_d) := \{(k_1, \dots, k_d) \in \mathbb{Z}^d : k_1\lambda_1 + \dots + k_d\lambda_d \in \mathbb{Z}\}. $$
Observe that $G_A(\lambda_1, \dots, \lambda_d) = G_M(e^{i2\pi\lambda_1}, \dots, e^{i2\pi\lambda_d})$.

## 2.4 Linear Recurrence Sequences

A sequence $\langle u_n \rangle_{n=0}^{\infty}$ is a linear recurrence sequence (over $\mathbb{Z}$) if $u_n \in \mathbb{Z}$ for all $n \in \mathbb{N}$ and there exist $d > 0$ and $c_1, \dots, c_d \in \mathbb{Z}$ and

$$u_{n+d} = c_1 u_{n+d-1} + \dots + c_d u_n \quad (1)$$

for all $n \in \mathbb{N}$. We assume that the recurrence (1) is minimal, i.e. $c_d \neq 0$. The characteristic polynomial of this sequence is $p(x) = x^d - \sum_{i=1}^d c_i x^{d-i}$. Suppose $\langle u_n \rangle_{n=0}^{\infty}$ is an LRS whose characteristic polynomial has the (distinct) roots $\lambda_1, \dots, \lambda_m \in \overline{\mathbb{Q}}$, called the characteristic roots of $\langle u_n \rangle_{n=0}^{\infty}$. Then there exist unique non-zero polynomials $q_1, \dots, q_m \in \overline{\mathbb{Q}}[x]$ such that

$$u_n = q_1(n)\lambda_1^n + \dots + q_m(n)\lambda_m^n \quad (2)$$

for all $n \in \mathbb{N}$. Eq. (2) is known as the exponential-polynomial form of $\langle u_n \rangle_{n=0}^{\infty}$. For a given characteristic root $\lambda_i$, the polynomial $q_i$ is the coefficient of $\lambda_i$. A characteristic root $\lambda_i$ is called simple if $q_i$ is constant and dominant when $|\lambda_i| \ge |\lambda_j|$ for all $1 \le j \le m$. We refer the reader to the book [18] for a detailed account of LRS.

Next we give two straightforward lemmas about LRS. First, the exponential-polynomial form (2) immediately implies an exponential upper bound on $|u_n|$, formalised below.

**LEMMA 2.5.** Let $\langle u_n \rangle_{n=0}^{\infty}$ be an LRS, $r, R > 0$ be real algebraic, and suppose $R > |\lambda_i|$ for any characteristic root $\lambda_i$ of $\langle u_n \rangle_{n=0}^{\infty}$. We can compute $N \in \mathbb{N}$ such that $|u_n| \le rR^n$ for all $n \ge N$.

From (1) it follows that an integer-valued LRS is ultimately periodic modulo any $m \in \mathbb{N}$.

**LEMMA 2.6.** Let $\langle u_n \rangle_{n=0}^{\infty}$ be an LRS and $m$ be a positive integer. We can effectively compute $N$, $p \in \mathbb{N}$ such that $u_n \equiv u_{n+p} \pmod m$ for all $n \ge N$.

## 2.5 Schanuel's Conjecture

A set $X = \{\alpha_1, \dots, \alpha_d\}$ of complex numbers is algebraically independent over $\mathbb{Q}$ if $p(\alpha_1, \dots, \alpha_d) \neq 0$ for any non-zero polynomial $p \in \mathbb{Q}[x_1, \dots, x_d]$. The transcendence degree of $X$ is the size of a largest subset of $X$ that is algebraically independent over $\mathbb{Q}$. Below we state Schanuel's conjecture, a classical conjecture in transcendental number theory with far-reaching implications [23].

**CONJECTURE 2.7 (SCHANUEL'S CONJECTURE).** If $\alpha_1, \dots, \alpha_d \in \mathbb{C}$ are linearly independent over $\mathbb{Q}$, then the transcendence degree of $\{\alpha_1, \dots, \alpha_d, \exp(\alpha_1), \dots, \exp(\alpha_d)\}$ is at least $d$.

We will use Schanuel's conjecture in two ways. First, consider the structure $\mathbb{R}_{\exp} := \langle \mathbb{R}; <, +, -, \exp(-), 0, 1 \rangle$ of real numbers equipped with arithmetic and (real) exponentiation. By the first-order theory of $\mathbb{R}_{\exp}$ we mean the set of all well-formed first-order sentences in a suitable language $\mathcal{L}_{\exp}$ that are true in $\mathbb{R}_{\exp}$. In [25], Macintyre and Wilkie show that the first-order theory of the structure $\mathbb{R}_{\exp}$ is decidable assuming Schanuel's conjecture.

**THEOREM 2.8.** Assuming Schanuel's conjecture, given a sentence $\varphi \in \mathcal{L}_{\exp}$, we can decide whether $\varphi$ holds in $\mathbb{R}_{\exp}$.

We will also use Schanuel's conjecture to prove the following.

**LEMMA 2.9.** Let $\lambda_1, \dots, \lambda_d \in \mathbb{R}_{>0} \cap \overline{\mathbb{Q}}$. Assuming Schanuel's conjecture, a basis for $G_A(1/\log(\lambda_1), \dots, 1/\log(\lambda_d))$ can be computed.

The proof is in [8, App. A.1].

## 2.6 Baker's Theorem

By a $\mathbb{Q}$-affine form we mean $h(x_1, \dots, x_d) = a_0 + \sum_{i=1}^d a_i x_i$, where $a_i \in \mathbb{Q}$ for all $0 \le i \le d$. We recall Baker's celebrated theorem on $\mathbb{Q}$-affine forms in logarithms.

**THEOREM 2.10 (THM. 1.6 IN [37]).** Let $\lambda_1, \dots, \lambda_d \in \mathbb{R}_{>0} \cap \overline{\mathbb{Q}}$ be multiplicatively independent. Then the numbers $1, \log(\lambda_1), \dots, \log(\lambda_d)$ are linearly independent over $\overline{\mathbb{Q}}$.

We will use Baker's theorem to prove the following results.

**LEMMA 2.11.** Let $d \ge 2$, $\lambda_1, \dots, \lambda_d \in \mathbb{R}_{>0} \cap \overline{\mathbb{Q}}$ be pairwise multiplicatively independent, and suppose

$$\mathrm{rank}(G_M(\lambda_1, \dots, \lambda_d)) \ge d - 2.$$

Then $1/\log(\lambda_1), \dots, 1/\log(\lambda_d)$ are linearly independent over $\mathbb{Q}$.

The proof of the lemma above is in [8, App. A.2].

**LEMMA 2.12.** Given $\lambda_1, \dots, \lambda_d \in \overline{\mathbb{Q}}$ and $a_0, \dots, a_d \in \mathbb{Q}$, we can effectively determine the sign of $a_0 + \sum_{i=1}^d a_i \log(\lambda_i)$.

**PROOF.** By computing the multiplicative relationships among the $\lambda_i$ using Thm. 2.4, we can rewrite this expression as $b_0 + \sum_{i=1}^d b_i \log(\lambda_i)$. Here, we relabeled the $\lambda_i$ such that $\lambda_1, \dots, \lambda_e$ is a maximum multiplicatively independent subset of $\lambda_1, \dots, \lambda_d$, and $b_0, \dots, b_e \in \mathbb{Q}$ are explicitly computed. By Thm. 2.10, this expression is 0 if and only if all $b_i$ are 0. If this expression is non-zero, we can compute it up to arbitrary precision and test whether it is positive or not. $\square$

Multiple effective versions of Baker's theorem exist, which give a lower bound on the magnitude of $\Lambda := h(\log(\rho_1), \dots, \log(\rho_d))$ for a $\mathbb{Q}$-affine form $h$, assuming $\Lambda \neq 0$. We use Matveev's version [27] to prove the following; See [8, App. A.3].

**THEOREM 2.13.** Let $b_1, b_2, c_1, c_2, \rho_1, \rho_2, R_1, R_2$ be positive real algebraic numbers such that $\rho_1 > R_1 > 0$ and $\rho_2 > R_2 > 0$. Then, one can compute $N \in \mathbb{N}$ such that for all $n_1, n_2 \ge N$,

$$|c_1\rho_1^{n_1} - c_2\rho_2^{n_2}| \le b_1R_1^{n_1} + b_2R_2^{n_2} \quad (3)$$

implies that $c_1\rho_1^{n_1} = c_2\rho_2^{n_2}$.

## 2.7 Toric Words

Denote by $\mathbb{T}$ the abelian group $\mathbb{R}/\mathbb{Z}$, viewed as the interval $[0, 1)$. For $x \in \mathbb{R}$, let $\{x\} := x - \lfloor x \rfloor$ be the fractional part of $x$. A word $\alpha \in \Sigma^\omega$ is toric if there exist $d > 0$, $s = (s_1, \dots, s_d) \in \mathbb{T}^d$, a translation $g: \mathbb{T}^d \to \mathbb{T}^d$ given by

$$(x_1, \dots, x_d) \to (\{x_1 + \delta_1\}, \dots, \{x_d + \delta_d\}) \quad (4)$$

for $\delta_1, \dots, \delta_d \in \mathbb{T}$, and a collection $S = \{S_b : b \in \Sigma\}$ of subsets of $\mathbb{T}^d$ such that for all $n \in \mathbb{N}$ and $b \in \Sigma$,

$$\alpha(n) = b \iff g^{(n)}(s) \in S_b. \quad (5)$$

Here $g^{(n)}(s)$ denotes the result of iteratively applying $g$ to $s$ a total of $n$ times. That is, $\alpha$ is the coding (with respect to $S$) of the
trajectory of the discrete-time dynamical system on $T^d$ defined by $(g, s)$. Observe that $g^{(n)}(s) = (\{s_1 + n\delta_1\}, \dots, \{s_d + n\delta_d\})$. The word $\alpha$ belongs to the subclass $\mathcal{T}_O$ of toric words if there exist $d > 0$, $s_1, \delta_1, \dots, s_d, \delta_d \in T$ as above and a collection $\{S_b : b \in \Sigma\}$ of open subsets of $T^d$ such that (5) holds for all $n \in \mathbb{N}$ and $b \in \Sigma$. See [7] for a discussion of various subclasses of toric words.

Let $s, \delta \in T^d$, $G = G_A(\delta)$, and $g: T^d \to T^d$ be as in (4). Define $T_\delta = \{z \in T^d : G_A(z) \subseteq G_A(\delta)\} \subseteq T^d$. The following is a rephrasing of Kronecker's theorem in Diophantine approximation [20]. In the language of dynamical systems, it states that the dynamical system (on $T_\delta$) obtained by restricting $g$ to $T_\delta$ is minimal.

**THEOREM 2.14.** *The orbit $\langle g^{(n)}(0) \rangle_{n=0}^\infty$, where $0 = (0, \dots, 0) \in T^d$, is dense in $T_\delta$. Moreover, for every open subset $O$ of $T_\delta$ there exist infinitely many $n \in \mathbb{N}$ such that $g^{(n)}(0) \in O$.*

Let $v_1, \dots, v_m \in \mathbb{Z}^d$ be a basis of $G_A(\delta)$, where $m < d$. Write $v_i = (v_{i,1}, \dots, v_{i,d})$ for $1 \le i \le m$ and let $C = \max_i ||v_i||_\infty$, noting that $|v_i \cdot z| \le Cd$ for all $z \in T^d$. We have that $z \in T_\delta$ if and only if $v_i \cdot z \in \mathbb{Z}$ for all $i$, which is equivalent to

$$ \bigwedge_{i=1}^{d} \bigvee_{|k| \le Cd} v_i \cdot z = k. $$

That is, $T_\delta$, viewed as a subset of $\mathbb{R}^d$, is an intersection of $T^d$ with a union of affine subspaces of $\mathbb{R}^d$ with integer parameters. We can now define $T_{\delta,s} := \{(\{s_1 + z_1\}, \dots, \{s_d + z_d\}) \mid (z_1, \dots, z_d) \in T_\delta\}$. Applying Thm. 2.14, we obtain the following.

**THEOREM 2.15.** *The orbit $\langle g^{(n)}(s) \rangle_{n=0}^\infty$ is dense in $T_{\delta,s}$, and for every open subset $O$ of $T_{\delta,s}$ there exist infinitely many $n \in \mathbb{N}$ such that $g^{(n)}(s) \in O$.*

To prove the first main result of this paper, we will need to show that $\text{Acc}_\alpha$ is decidable for certain $\alpha \in \mathcal{T}_O$. The following well-known fact will play an important role in this; See [7] for a proof.

**THEOREM 2.16.** Every $\alpha \in \mathcal{T}_O$ is uniformly recurrent.

## 2.8 Fourier-Motzkin Elimination

Let $\Phi(x_1, \dots, x_m)$ be a Boolean combination of atomic formulas of the form $h(x_1, \dots, x_m) \sim 0$, where $h$ is a $\mathbb{Q}$-affine form and $\sim$ is a (strict or non-strict) inequality symbol. Let $1 \le l \le m$, and consider the formula $\exists x_1, \dots, x_l \in \mathbb{R} : \Phi(x_1, \dots, x_m)$. Using the Fourier-Motzkin Elimination [16], we can compute a formula $\Psi(x_{l+1}, \dots, x_m) = \bigvee_{j \in J} \wedge_{k \in K} h_{j,k}(x_{l+1}, \dots, x_m) \sim_{j,k} 0$ such that

(a) each $\sim_{j,k}$ is an inequality and $h_{j,k}$ is a $\mathbb{Q}$-affine form, and

(b) for all $z_{l+1}, \dots, z_m \in \mathbb{R}$, the sentence

$$ \exists x_1, \dots, x_l \in \mathbb{R} : \Phi(x_1, \dots, x_l, z_{l+1}, \dots, z_m) $$

holds if and only if $\Psi(x_{l+1}, \dots, x_m)$ holds.

# 3 SYNOPSIS OF OUR TECHNIQUES

Our central problem is as follows:

For unary predicates $P_1, \dots, P_d$, establish the decidability of the MSO theory of $\langle \mathbb{N} ; <, P_1, \dots, P_d \rangle$.

In this section, we give a high-level overview of our approach.

The predicates we consider in this paper have arithmetic origins, e.g. $\text{Pow}_2 = \{2^n : n \in \mathbb{N}\}$. In order to exploit their mathematical

properties, we view the problem from the equivalent automata-theoretic perspective (Thm. 2.3). Recall the characteristic word from Def. 2.2, and let $\alpha = \text{Char}(P_1, \dots, P_d) \in (\{0, 1\}^d)^\omega$.

We have that $\alpha(n) = (b_{n,1}, \dots, b_{n,d})$, where for all $n \in \mathbb{N}$ and $1 \le i \le d$, $b_{n,i} = 1$ if $n \in P_i$ and $b_{n,i} = 0$ otherwise. Our problem is thus restated:

For $\alpha = \text{Char}(P_1, \dots, P_d)$, establish the decidability of the automaton acceptance problem $\text{Acc}_\alpha$.

We let $0$ denote the letter $(0, \dots, 0)$ and express

$$ \alpha = \mathbf{0}^{k_0} \alpha(k_0) \mathbf{0}^{k_1} \alpha(k_0 + k_1 + 1) \cdots \mathbf{0}^{k_n} \alpha(k_0 + \cdots + k_n + n) \cdots \quad (6) $$

where each letter between the blocks of $0$'s is not $0$. Characteristic words defined by a single predicate (e.g. $\text{Pow}_2$, the powers of 2) are much better studied than those defined by multiple predicates (e.g. $\text{Pow}_2$, $\text{Pow}_3$). Intuitively, this is because in the latter case, one needs to capture additional element of interaction between predicates. To do this, we define order words.

*Definition 3.1 (Order Word).* For unary predicates $P_1, \dots, P_d$ with $\alpha = \text{Char}(P_1, \dots, P_d) \in (\{0, 1\}^d)^\omega$, their order word

$$ \alpha' = \text{Ord}(P_1, \dots, P_d) \in (\{0, 1\}^d)^\omega $$

is obtained by deleting all occurrences of $(0, \dots, 0)$ from $\alpha$.

In compressing the characteristic word $\alpha$ to the order word $\alpha'$, one only retains partial information, i.e. a particular aspect of the interaction between predicates. Not surprisingly (by Lem. 4.5), $\text{Acc}_\alpha'$ always reduces to $\text{Acc}_\alpha$. Remarkably however, under certain circumstances, the interaction captured by order words is the essence of the decision problem $\text{Acc}_\alpha$: For certain well-behaved tuples of predicates, given an automaton $\mathcal{A}$, one can use the order word $\alpha'$ to recover sufficient information about the interspersed $0$'s, and hence about $\alpha$ itself, to decide whether $\mathcal{A}$ accepts $\alpha$.

Let us intuit why this could be so. We rewrite (6) in terms of the order word $\alpha$:

$$ \alpha = \mathbf{0}^{k_0} \alpha'(0) \cdots \mathbf{0}^{k_n} \alpha'(n) \cdots $$

An automaton $\mathcal{A}$ is crucially finite, and consequently one can compute $K, p > 0$ such that for all $n \ge K$, it cannot distinguish $\mathbf{0}^n$ from $\mathbf{0}^{n+p}$. Provided that $k_n$ is persistently larger than $K$, it suffices to only keep track of $k_n$ modulo $p$. We will show that if $\langle \mathbf{0}^{m_n} \rangle_{n=0}^\infty$, where each $m_n$ is indistinguishable from $k_n$ to $\mathcal{A}$, can be inserted back into $\alpha'$ using a transducer, then $\text{Acc}_\alpha$ reduces to $\text{Acc}_\alpha'$.

In Sec. 4, we develop the automata-theoretic machinery required to prove that $\text{Acc}_\alpha$ (the acceptance problem of the characteristic word) reduces to $\text{Acc}_\alpha'$ (the acceptance problem of the order word) assuming the predicates $(P_1, \dots, P_d)$ meet certain technical conditions.

In Sec. 5, we invoke Baker's theorem to argue that the predicates defined by LRS with one simple dominant root indeed meet the sufficient conditions identified in Sec. 4.

We devote Sec. 5.2 to proving decidability of $\text{Acc}_\alpha'$ for the order word $\alpha'$ defined by tuples of LRS with one simple dominant root. We do so by showing that $\alpha'$ can be generated as a toric word. Toric words enjoy a crucial combinatorial property: they are almost-periodic. It is known that if a word $\beta$ is effectively almost-periodic,
then $Acc_β$ is decidable (Thm. 4.2). Through number-theoretic arguments, we establish when the order word $α'$ is indeed effectively almost-periodic.

Below is a summary of our strategy to solve our central problem:

(1) Identify sufficient conditions to reduce $Acc_α$ (the acceptance problem of the characteristic word) to $Acc_{α'}$ (the acceptance problem of the order word). (Sec. 4)

(2) Prove that the predicates under consideration meet these conditions. (Sec. 5)

(3) Generate $α'$ as the trace of a toric dynamical system, and exploit the underlying model to decide $Acc_{α'}$. (Sec. 5.2)

In Sec. 6, we follow a similar approach to analyze $Char(P_1, P_2)$ for $P_1 = \{qn^d : n \in \mathbb{N}\}$ and $P_2 = \{pb^{nd} : n \in \mathbb{N}\}$. The difference is that the underlying dynamical systems are driven by *numeration systems* [24, Chap. 7].

# 4 PROVING MSO DECIDABILITY

## 4.1 Classical Results

We recount various classes of words whose automaton acceptance problem is known to be decidable. Recall that a word $α$ is effective if its letters can be effectively computed. Seménov considered the class of (effectively) almost-periodic words in [35].

**Definition 4.1.** A word $α \in \Sigma^ω$ is almost-periodic, if for every $u \in \Sigma^+$, there exists $R(u) \in \mathbb{N}$ such that the word $u$ either

(a) does not occur in $α[R(u), \infty)$, or

(b) occurs in every factor of $α$ of length $R(u)$.

If, moreover, $α$ is effective and a *return time* $R(u)$ as above is computable given $u$, then $α$ is said to be *effectively almost-periodic*.

**THEOREM 4.2 (THEOREM 3 IN [28]).** If $α \in \Sigma^ω$ is effectively almost-periodic, then $Acc_α$ is decidable.

Carton and Thomas [14] introduced the class of profinitely ultimately periodic words as a framework to generalise the thematic *contraction methods* of Elgot and Rabin [17].

**Definition 4.3.** Let $Σ$ be an alphabet.

(a) A sequence of finite words $\langle u_n \rangle_{n \in \mathbb{N}}$ is effectively profinitely ultimately periodic if for any morphism $h$ from $Σ^*$ into a finite monoid $M$, we can compute $N$ and $p$ such that for all $n \ge N$, $h(u_n) = h(u_{n+p})$.

(b) An infinite word $α$ is called *effectively profinitely ultimately periodic* if it can be effectively factorised as an infinite concatenation $u_0u_1 \cdots$ of finite non-empty words forming an effectively profinitely ultimately periodic sequence.

**THEOREM 4.4.** Let $α \in \Sigma^*$. The problem $Acc_α$ is decidable if and only if $α$ is effectively profinitely ultimately periodic.

The if direction is due to Carton and Thomas [14], and the converse is due to Rabinovich [30]. Every infinite word is profinitely ultimately periodic, as a close inspection of the use of Ramsey's theorem in Rabinovich's proof reveals. The effectiveness distinguishes words whose automaton acceptance problem is decidable.

A comprehensive class of predicates whose characteristic words $(α \in \{0, 1\}^ω)$ are effectively profinitely ultimately periodic is identified by [14, Thm. 5.2]. This class includes fixed base powers $Pow_k = \{k^n : n \in \mathbb{N}\}$ as well as $k$-th powers $N_k = \{n^k : n \in \mathbb{N}\}$.

## 4.2 Closure Properties

We now define a few constructs under which the set of infinite words with a decidable automaton acceptance problem is closed.

**LEMMA 4.5 (TRANSDUCTION).** Let $α \in \Sigma^ω$, $B$ be a deterministic finite transducer with input alphabet $Σ$ and output alphabet $Γ$, and $β = B(α) \in Γ^ω$. The problem $Acc_β$ reduces to $Acc_α$.

**PROOF.** Given an instance $A = (Q, q_{init}, \delta, \mathcal{F})$ of $Acc_β$, we shall construct $A'$ whose run on $α$ simulates the run of $A$ on $β$. Write $B = (R, r_{init}, \sigma)$. The automaton $A'$ must simulate what $B$ would do upon reading $α$, and furthermore, what $A$ would do upon reading each output block of $B(α)$.

In order to do so, we express $β = u_0u_1 \cdots$ such that $B$ outputs $u_n$ upon reading the $n$th letter of $α$ and correspondingly decompose the run of $A$ on $β$ as the concatenation of journeys $(q_{init}, q_1, V_0)(q_1, q_2, V_1) \cdots$. In order to construct this decomposition, we define the set of states, initial state, and transition function of $A'$ as

$$ 
\begin{align*}
Q' &= Q \times 2^Q \times R; \\
q'_{init} &= (q_{init}, \emptyset, r_{init}); \\
\delta'((q_{now}, V_{last}, r), a) &= (q_{next}, V, \sigma_R(r, a))
\end{align*}
$$

such that the invariant $jour(\sigma_{Γ^*}(r, a), q_{now}) = (q_{now}, q_{next}, V)$ holds. By construction, the run $(q_{init}, \emptyset, r_{init})(q_1, V_0, r_1)(q_2, V_1, r_2) \cdots$ of $A'$ on $α$ corresponds to the above concatenation of journeys.

By Lem. 2.1, a state $q$ is visited infinitely often in $A$ if and only if a state $(p, V, r)$ with $q \in V$ is visited infinitely often in $A'$. We thus have our acceptance condition

$$ F' \in \mathcal{F}' \iff \left( \bigcup_{(p,V,r) \in F'} V \right) \in \mathcal{F} $$

and the reduction is hence complete. $\square$

<figure><img src="image_4.png" /></figure>

In fact, we can even use the construction to detect whether $β$ is an infinite word at all: $β$ is infinite if and only if the run of $A'$ on $α$ visits a state $(q, V, r)$ with $V \neq \emptyset$ infinitely often.

Next, we give our primary closure property. Here we have two words $α$ and $β$ such that $α$ is a “compressed” version of $β$. We show that $Acc_β$ reduces to $Acc_α$ assuming we can dilate $α$ into (a word equivalent to) $β$. As expected, Thm. 4.6 further generalises the frameworks of Elgot and Rabin [17] as well as Carton and Thomas [14]. Below, by computing a factorisation $β = u_0u_1 \cdots$ we mean giving an algorithm that on every $n \in \mathbb{N}$, returns a finite word $u_n$ such that $β$ is the concatenation of $\langle u_n \rangle_{n=0}^\infty$.

**THEOREM 4.6.** Let $α \in \Sigma^ω$ and $β \in Γ^ω$ be such that for any morphism $h$ from $Γ^*$ into a finite monoid $M$, we can construct a deterministic finite transducer $B$ (with input alphabet $Σ$ and output alphabet $M$) and compute a factorisation $u_0u_1 \cdots$ of $β$ such that $γ = B(α) = γ(0)γ(1) \cdots \in M^ω$ satisfies $h(u_n) = γ(n)$ for all $n \in \mathbb{N}$. Then $Acc_β$ reduces to $Acc_α$.

**PROOF.** Given a deterministic finite automaton $A$ as an instance of $Acc_β$, we will use the natural morphism $h$ into the finite quotient monoid $M = Γ^*/\sim_A$ to reduce it to an instance of $Acc_α$.

For $h, M$ chosen thus, consider the transducer $B$, factorisation $u_0u_1 \cdots$ of $β$, and word $γ = B(α) \in M^ω$ from the premise. We have
that for all $n$, $h(u_n) = \gamma(n)$. Since the morphism $h$ maps each word in $\Gamma^*$ to the equivalence class of words that undertake the same set of journeys, the equivalence class $\gamma(n) \in M$ contains all the information about the journeys that $u_n$ can undertake, i.e. for all $n \in \mathbb{N}$, $q \in Q$, $jour(u_n, q) = \text{jour}(\gamma(n), q) \in J$.

It is straightforward to construct a transducer $\mathcal{B}'$ such that $\mathcal{B}'(y) = \zeta = j_0 j_1 \cdots \in J^\omega$ has the following properties:

(1) $j_0 = \text{jour}(\gamma(0), q_{\text{init}}) = \text{jour}(u_0, q_{\text{init}}) = (q_{\text{init}}, q_1, V_0)$;

(2) $j_n = \text{jour}(\gamma(n), q_n) = \text{jour}(u_n, q_n) = (q_n, q_{n+1}, V_n)$ for $n \ge 1$.

We will now show how to decide $\text{Acc}_\beta$, which is equivalent to deciding whether the run of $\mathcal{A}$ on $\beta$ visits a state $q$ infinitely often.

To that end, observe that the infinite word $\zeta \in J^\omega$ is indeed a decomposition of the run of $\mathcal{A}$ on $\beta$. By Lem. 2.1, the latter visits a state $q \in Q$ infinitely often if and only if $q \in V_n$ of $j_n$ for infinitely many $n$. This is easily seen to be an instance of $\text{Acc}_\zeta$. By Lem. 4.5, $\text{Acc}_\zeta$ reduces to $\text{Acc}_\gamma$, which itself reduces to $\text{Acc}_\alpha$. $\square$

**COROLLARY 4.7 (DILATION).** Let $\Sigma = \{1, \dots, b\}$, $\Sigma_0 = \Sigma \cup \{0\}$, and $\alpha \in \Sigma^\omega$. Suppose $\beta \in \Sigma_0^\omega$ and $\beta = 0^{k_0}\alpha(0)0^{k_1}\alpha(1) \cdots$ is such that for any finite monoid $M$ and morphism $h: \Sigma_0^* \to M$, we can construct a transducer $\mathcal{B}$ with the following property. Its output $\gamma := \mathcal{B}(\alpha) \in M^\omega$ upon reading $\alpha$ satisfies $h(0^{k_n}\alpha(n)) = \gamma(n)$ for all $n$. Then $\text{Acc}_\beta$ reduces to $\text{Acc}_\alpha$.

**COROLLARY 4.8 (INTERLEAVING).** Let $\alpha \in \Sigma^\omega$, $\langle v_n \rangle_{n \in \mathbb{N}}$ be an effectively profinitely ultimately periodic sequence of words in $\Sigma^*$, and $\beta = v_0\alpha(0)v_1\alpha(1) \cdots \in \Sigma^\omega$. The problem $\text{Acc}_\beta$ reduces to $\text{Acc}_\alpha$.

**PROOF.** We will show that for any morphism $h$ into a finite monoid $M$, we can construct a transducer $\mathcal{B}$ such that $\gamma := \mathcal{B}(\alpha) = \gamma(0)\gamma(1) \cdots \in M^\omega$ satisfies $h(v_n\alpha(n)) = \gamma(n)$ for all $n \in \mathbb{N}$. The conclusion then follows immediately from Thm. 4.6.

Since the sequence $\langle v_n \rangle_{n \in \mathbb{N}}$ is effectively profinitely ultimately periodic, we can compute $N, p \in \mathbb{N}$ with $p > 0$ such that $h(v_n) = h(v_{n+p})$ for all $n \ge N$. Define $\gamma(n) = h(v_n\alpha(n)) = h(v_n) \cdot h(\alpha(n))$ for $n < N + p$, and $\gamma(N + qp + r) = h(v_{N+r}) \cdot h(\alpha(N + qp + r))$ for $q > 0$ and $0 < r < p$. It is straightforward to construct a transducer $\mathcal{B}$ that outputs $h(v_0\alpha(0))h(v_1\alpha(1)) \cdots$ upon reading $\alpha$. $\square$

## 4.3 Predicates Corresponding to Functions

Recall that we associate to a tuple of predicates $(P_1, \dots, P_d)$ its characteristic word $\alpha \in \Sigma^\omega$, where $\Sigma = \{0, 1\}^d$ and $\alpha(n)$ records which of the predicates hold for $n$. The order word $\alpha'$ only records the order in which the predicates hold: it is obtained by deleting all occurrences of $(0, \dots, 0)$ from the characteristic word $\alpha$.

**Definition 4.9.** Let $\mathcal{F}$ be the class of strictly increasing functions $f: \mathbb{N} \to \mathbb{N}$ such that the characteristic word $\alpha$ of the predicate $P = \{f(n) : n \in \mathbb{N}\}$ can be factorised as $0^{k_0} 10^{k_1} 1 \cdots$ where $\langle 0^{k_n} \rangle_{n=0}^\infty$ is an effectively profinitely ultimately periodic sequence of words.

The following readily follows from Thm. 4.4.

**LEMMA 4.10.** Suppose $\alpha$ is the characteristic word of a predicate $P = \{f(n) : n \in \mathbb{N}\}$ where $f \in \mathcal{F}$. Then $\text{Acc}_\alpha$ is decidable.

**THEOREM 4.11 (COMPOSITION).** Let $f_1, \dots, f_d \in \mathcal{F}$. Define functions $g_1, \dots, g_d: \mathbb{N} \to \mathbb{N}$ such that $g_i = f_1 \circ \dots \circ f_i$. Let $\Sigma = \{0, 1\}^d$, $P_i = \{g_i(n) : n \in \mathbb{N}\}$ for $1 \le i \le d$, and $\alpha \in \Sigma^\omega$ be the characteristic word of $(P_1, \dots, P_d)$. Then $\text{Acc}_\alpha$ is decidable.

**PROOF.** We will prove the theorem by repeatedly applying Cor. 4.8. Let $g_0$ be the identity function, $P_0 = \mathbb{N}$, and note that $g_i = g_{i-1} \circ f_i$. Observe that $P_{i+1} = \{g_i(f_{i+1}(n)) : n \in \mathbb{N}\}$ and $P_i = \{g_i(n) : n \in \mathbb{N}\}$.

Therefore, $P_1 \supset \dots \supset P_d$. Let $\alpha^{(0)} = \alpha$, and denote by $\alpha^{(i)}$ the restriction of $\alpha$ to the positions where $P_i$ holds. Let $b_i \in \Sigma$ be the letter whose first $i$ components are 1 and the remaining $d-i$ components are all 0. It is clear that $\alpha^{(i)} \in \{b_i, \dots, b_d\}^\omega$.

Since all functions are strictly increasing, so are their compositions, and we deduce that

$$ \alpha^{(i)} = b_i^{k_0} \alpha^{(i+1)}(0) b_i^{k_1} \alpha^{(i+1)}(1) \cdots b_i^{k_n} \alpha^{(i+1)}(n) \cdots $$

where $\alpha^{(i+1)} \in \{b_{i+1}, \dots, b_d\}^\omega \subset \Sigma^\omega$, $k_0 = f_{i+1}(0)$, and $k_n = f_{i+1}(n) - f_{i+1}(n-1) - 1$. Since $f_{i+1} \in \mathcal{F}$, by Definition 4.9, the sequence $\langle b_i^{k_n} \rangle_{n \in \mathbb{N}}$ is effectively profinitely ultimately periodic. Hence the hypothesis of Cor. 4.8 is satisfied, and $\text{Acc}_{\alpha^{(i)}}$ reduces to $\text{Acc}_{\alpha^{(i+1)}}$. However, $\alpha^{(d)} = b_d^\omega$ and therefore $\text{Acc}_{\alpha^{(d)}}$ is clearly decidable. We conclude that $\text{Acc}_\alpha$ is decidable. $\square$

**PROOF OF COR. 1.3.** Recall, by [14, Thm. 5.2], $N_d$, $\text{Pow}_b \in \mathcal{F}$. On applying the previous theorem with $f_1(n) = n^d$, $f_2(n) = b^n$ we get $g_1(n) = n^d$, $g_2(n) = b^{nd}$. Thus, $\text{Acc}_\alpha$ is decidable for the characteristic word $\alpha$ of the predicates $(P_1, P_2)$, where $P_1 = \{g_1(n) : n \in \mathbb{N}\}$ and $P_2 = \{g_2(n) : n \in \mathbb{N}\}$. Equivalently, the MSO theory of $\langle \mathbb{N}; <, N_d, \text{Pow}_{b_d} \rangle$ is decidable. $\square$

## 4.4 From Characteristic to Order Words

We will now use our reduction techniques to discuss when the acceptance problem for the characteristic word $\alpha$ is in fact equivalent to that for the order word $\alpha'$. Note that $\text{Acc}_{\alpha'}$ trivially reduces to $\text{Acc}_\alpha$ by Lem. 4.5; we therefore focus on the other direction.

**Definition 4.12 (Procyclic Predicates).** A strictly increasing function $f: \mathbb{N} \to \mathbb{N}$ is said to be *procyclic$^3$* if the sequence $f(n)$ is effectively ultimately periodic modulo any $m \in \mathbb{N}$, i.e. given any $m$, there exist computable $N$, $p$ such that for all $n \ge N$, $f(n+p) \equiv f(n)$ mod $m$. The corresponding $P = \{f(n) : n \in \mathbb{N}\}$ is called a *procyclic predicate*.

**Definition 4.13 (Effectively Sparse Predicates).** A strictly increasing function $f: \mathbb{N} \to \mathbb{N}$ is said to be effectively sparse if for any $K \in \mathbb{N}$, the inequality $f(n+1) - f(n) \le K$ has finitely many solutions in $n$ which can moreover be effectively enumerated. The corresponding $P = \{f(n) : n \in \mathbb{N}\}$ is said to be an effectively sparse predicate.

**Definition 4.14 (Pairwise Effectively Sparse Predicates).** Strictly increasing functions $f_1, f_2: \mathbb{N} \to \mathbb{N}$ are said to be *pairwise effectively sparse* if for any $K \in \mathbb{N}$, the inequality $|f_1(n) - f_2(m)| \le K$ has finitely many solutions in $n, m$ which can moreover be effectively enumerated. The corresponding $P_1 = \{f_1(n) : n \in \mathbb{N}\}$ and $P_2 = \{f_2(n) : n \in \mathbb{N}\}$ are said to be *pairwise effectively sparse predicates*.

<footnote>$^3$This definition is weaker than the notion of (effectively) profinitely ultimately periodic sequences defined by Carton and Thomas [14]. The function $f$ would be effectively profinitely ultimately periodic if, for any morphism $h$ from $\mathbb{N}$ into a finite monoid $M$, the sequence $\gamma(n) = h(f(n+1) - f(n))$ were effectively ultimately periodic. On the other hand, our definition of procyclic functions only considers morphisms into cyclic groups. It is often much easier to show that functions meet the criterion of being procyclic rather than being effectively profinitely ultimately periodic.</footnote>
We remark that similar notions of effective sparsity have been considered in literature as early as [34].

**THEOREM 4.15 (SPARSE PROCYCLIC PREDICATES).** Let $(P_1, \dots, P_d)$ be a tuple of predicates with characteristic word $\alpha$ and order word $\alpha'$. Suppose

(1) $P_1, \dots, P_d$ are each (a) procyclic and (b) effectively sparse;

(2) each distinct $(P_i, P_j)$ is pairwise effectively sparse.

Then, $\mathrm{Acc}_\alpha$ reduces to $\mathrm{Acc}_{\alpha'}$.

**PROOF.** Let $\mathbf{0} = (0, \dots, 0)$. We observe that

$$ \alpha = \mathbf{0}^{k_0} \alpha'(0) \mathbf{0}^{k_1} \alpha'(1) \cdots \mathbf{0}^{k_n} \alpha'(n) \cdots . $$

The above suggests using Cor. 4.7 to prove the theorem. In order to do so, we need to show that for any morphism $h$ into a finite monoid $M$, we can construct a transducer $\mathcal{B}$ such that $\mathcal{B}(\alpha') = \gamma \in M^\omega$, where $\gamma(n) = h(\mathbf{0}^{k_n} \alpha'(n)) = h(\mathbf{0}^{k_n})h(\alpha'(n))$. The transducer $\mathcal{B}$ outputs $\gamma(n)$ upon reading $\alpha(n)$: it gets the second factor directly from the input. We will show that we can compute the first factor with finite state.

First, note that via a simple pigeonhole argument that exploits the finiteness of monoid $M$, we can compute $K, m \ge 1$ such that $K$ is a multiple of $m$, and for all $j \ge K$, $h(\mathbf{0}^j) = h(\mathbf{0}^{j+m})$. In other words, if $k_n$ is sufficiently large, it suffices to only keep track of it modulo $m$. Now, consider conditions (1b) and (2) of the premise. By the very definition of sparsity, we can compute $N$ such that for all $n \ge N$, $k_n \ge K$. This means that we can compute when $k_n$ is guaranteed to be sufficiently large.

The prefix $\gamma(0) \cdots \gamma(N-1)$ of the output can be hardcoded for the prefix $\alpha'(0) \cdots \alpha'(N-1)$ of the input. It only remains to show how to track $k_n$ modulo $m$ for the infinite suffix. For this, we will use condition (1a) of the premise: that $P_1, \dots, P_d$ are each procyclic. This means that each of $f_1, \dots, f_d$ are effectively ultimately periodic modulo $m$, i.e. for each $i$, one only needs finitely many states to evaluate $f_i(n)$, and moreover the state for $f_i(n)$ uniquely determines that for $f_i(n+1)$. As an example, $3^n + 2^n$ modulo 8 follows the pattern 2, 5, 5, 3, 1, 3, 1, 3, 1, 3, ..., which can be represented by a typical lasso-shaped graph.

The transducer $\mathcal{B}$ thus keeps track of: (*) for each $i$, what the next occurrence of $P_i$ will be modulo $m$, and (**) what the occurrence of $P_j$ indicated by the last read letter of $\alpha'(n-1)$ was, modulo $m$.

Upon reading the next letter of $\alpha'(n)$, it can update its record, and appropriately compute $k_n$, the number of intervening 0's, modulo $m$. Let this remainder be $r_n < m$. Finally, to write its output, $\mathcal{B}$ simply uses the fact that

$$ \gamma(n) = h(\mathbf{0}^{k_n} \alpha'(n)) = h(\mathbf{0}^{k_n}) h(\alpha'(n)) = h(\mathbf{0}^{K+r_n}) h(\alpha'(n)) $$

and we are done. $\square$

## 4.5 Normal Words

Recall that a word $\alpha \in \Sigma^\omega$ is weakly normal if every $u \in \Sigma^*$ appears infinitely in $\alpha$.<fnref n="4" /> Normality is usually considered when $\Sigma = \{0, \dots, b-1\}$ is the alphabet of digits and $\alpha$ is the base-$b$ expansion of a real number $a$. Thus, when $a = \sqrt{2}$ and $b = 10$, $\alpha = 141421356 \dots$. We have the following result about such words.

**THEOREM 4.16.** If $\alpha$ is weakly normal, then $\mathrm{Acc}_\alpha$ is decidable.

Intuitively, the proof uses the abundance of each factor to guarantee that the set of states visited infinitely often is an entire bottom strongly connected component in the graph induced by the automaton. We defer its technical details to [8, App. A.4].

# 5 LINEAR RECURRENCE SEQUENCES WITH A SINGLE DOMINANT ROOT

In this section we prove the first main result of this paper, whose corollaries appeared in the abstract.

**THEOREM 5.1.** Consider LRS (over $\mathbb{Z}$) of the form

$$ u_n^{(i)} = c_i \rho_i^n + \sum_{j=1}^{k_i} p_{i,j}(n) \rho_{i,j}^n, $$

for $1 \le i \le d$, such that for all $i$ and $j$,

(1) $c_i, \rho_i, \rho_{i,j} \in \overline{\mathbb{Q}}$ and $\rho_{i,j} \in \overline{\mathbb{Q}}[x]$,

(2) $c_i > 0, \rho_i > 1$ and $|\rho_{i,j}| < |\rho_i|$, and

(3) there exist only finitely many pairs $(n, m) \in \mathbb{N}^2$ such that $c_i \rho_i^n = c_j \rho_j^m$.

Writing $P_i \subseteq \mathbb{N}$ for the value set of $\langle u_n^{(i)} \rangle_{n=0}^\infty$, the MSO theory of $\langle \mathbb{N}; <, P_1, \dots, P_d \rangle$ is decidable assuming Schanuel's conjecture. The decidability is unconditional in either of the following cases:

(a) If $1/\log(\rho_1), \dots, 1/\log(\rho_d)$ are linearly independent over $\mathbb{Q}$;

(b) If $\mathrm{rank}(G_M(\rho_1, \dots, \rho_d)) \ge d-2$, and $\rho_1, \dots, \rho_d$ are pairwise multiplicatively independent.

We remark that the condition $\mathrm{rank}(G_M(\rho_1, \dots, \rho_d)) \ge d-2$ is exactly the same as “each triple of distinct $\rho_i, \rho_j, \rho_k$ is multiplicatively dependent”, which appears in the statement of Thm. 1.1. Intuitively, these statements mean that over $\mathbb{Q}$, there are at most two linearly independent elements among $\log(\rho_1), \dots, \log(\rho_d)$. Moreover, (b) implies (a) by Lem. 2.11. Finally, condition (3) is equivalent to the following: For every $1 \le i, j \le d$, the equation $c_i \rho_i^n = c_j \rho_j^m$ has at most one solution $(n, m) \in \mathbb{N}^2$; The proof is elementary.

Thm. 5.1 implies Thm. 1.1 from the Introduction. For pairwise multiplicatively independent $\rho_1, \dots, \rho_d$ this is immediate. Suppose $\rho_1, \dots, \rho_d$ are not pairwise multiplicatively independent. Then $1/\log(\rho_1), \dots, 1/\log(\rho_d)$ are not linearly independent over $\mathbb{Q}$. We can compute pairwise multiplicatively independent $\lambda_1, \dots, \lambda_m \in \mathbb{N}$ such that for all $1 \le i \le d$, $\rho_i = \lambda_{\sigma(i)}^{\mu(i)}$ for some $\sigma(i), \mu(i) \in \mathbb{N}$. Consider $\langle \mathbb{N}; <, \mathrm{Pow}_{\lambda_1}, \dots, \mathrm{Pow}_{\lambda_m} \rangle$. The original characteristic word can be recovered by noting that precisely every $\mu(i)$-th occurrence of $\mathrm{Pow}_{\lambda_{\sigma(i)}}$ is an occurrence of $\mathrm{Pow}_{\rho_i}$. This can be implemented with a simple transduction; hence by Lem. 4.5, the MSO theory of $\langle \mathbb{N}; <, \mathrm{Pow}_{\rho_1}, \dots, \mathrm{Pow}_{\rho_d} \rangle$ reduces to that of $\langle \mathbb{N}; <, \mathrm{Pow}_{\lambda_1}, \dots, \mathrm{Pow}_{\lambda_m} \rangle$. It remains to observe that if every triple of $\rho_1, \dots, \rho_d$ is multiplicatively dependent, then so is every triple of $\lambda_1, \dots, \lambda_m$.

## 5.1 Reduction to the Order Word

To prove Thm. 5.1 we will use the framework described in Sec. 3. Let $\langle u_n^{(i)} \rangle_{n=0}^\infty$ and $P_i$ be as in the statement of Thm. 5.1. Denote by $\alpha$ the characteristic word of $(P_1, \dots, P_d)$, and by $\alpha'$ the order word

<footnote n="4">⁴In comparison, a normal word has the stronger property that each factor $u$ of length $n$ appears with asymptotic frequency $1/|\Sigma|^n$. A real number is normal if it is normal in every base $b$. Constants like $\sqrt{2}$, $e$, and $\pi$ are all conjectured to be normal [29].</footnote>
of $(P_1, \dots, P_d)$. We will need order words obtained from sequences that do not necessarily take exclusively integer values.

**Definition 5.2.** Let $\langle v_n^{(1)} \rangle_{n=0}^{\infty}, \dots, \langle v_n^{(d)} \rangle_{n=0}^{\infty}$ be a family of real-valued, strictly increasing sequences with pairwise disjoint ranges. Further let $Z = \cup_{i=1}^d \{v_n^{(i)} : n \in \mathbb{N}\}$. We define the word

$$ \gamma := \operatorname{Ord}(\langle v_n^{(1)} \rangle_{n=0}^{\infty}, \dots, \langle v_n^{(d)} \rangle_{n=0}^{\infty}) \in \{1, \dots, d\}^{\omega} $$

by

$$ \gamma(n) = i \iff \exists z \in \langle v_n^{(i)} \rangle_{n=0}^{\infty}: |\{y \in Z : y < z\}| = n. $$

We now prove the following.

**THEOREM 5.3.** Let $\alpha, \alpha'$ be as above. $\mathrm{Acc}_{\alpha}$ reduces to $\mathrm{Acc}_{\alpha'}$. Furthermore, we can construct positive real algebraic $r_1, \dots, r_d$ such that $\mathrm{Acc}_{\alpha'}$ reduces to $\mathrm{Acc}_{\xi}$, where $\xi = \mathrm{Ord}(\langle r_1 \rho_1^n \rangle_{n=0}^{\infty}, \dots, \langle r_d \rho_d^n \rangle_{n=0}^{\infty})$.

In Sec. 5.2 we will show that $\xi$ is effectively almost-periodic and therefore $\mathrm{Acc}_{\xi}$ is decidable. To prove Thm. 5.3, we will need the following lemma, whose main tool is Thm. 2.13.

**LEMMA 5.4.** Let $\langle u_n^{(1)} \rangle_{n=0}^{\infty}, \dots, \langle u_n^{(d)} \rangle_{n=0}^{\infty}$ be as above. We can compute $N, m_1, \dots, m_d \in \mathbb{N}$ with the following properties.

(a) For all $1 \le i \le d$, $\langle u_{m_i+n}^{(i)} \rangle_{n=0}^{\infty}$ is strictly increasing. Moreover, for every $K \in \mathbb{N}$ and $1 \le i \le d$, there exists effectively computable $L_i$ such that for all $n \ge L_i$, $u_{n+1}^{(i)} - u_n^{(i)} > K$.

(b) For all $1 \le i \le d$ and $n \in \mathbb{N}$,

$$ u_n^{(i)} \ge N \iff n \ge m_i. $$

(c) $u_{m_1}^{(1)} = N$.

(d) For all $1 \le i, j \le d$, $n_i \ge m_i$ and $n_j \ge m_j$, we have that $c_i \rho_i^{n_i} \ne c_j \rho_j^{n_j}$ and $u_{n_i}^{(i)} \ne u_{n_j}^{(j)}$.

(e) For $1 \le i, j \le d$, $n_i \ge m_i$ and $n_j \ge m_j$,

$$ c_i \rho_i^{n_i} > c_j \rho_j^{n_j} \Rightarrow u_{n_i}^{(i)} > u_{n_j}^{(j)}. $$

**PROOF.** Let $1 \le i, j \le d$ with $i \ne j$. We first tackle (d). By assumption, there are only finitely many pairs $(n_i, n_j) \in \mathbb{N}^2$ satisfying $c_i \rho_i^{n_i} = c_j \rho_j^{n_j}$, which is equivalent to $c_i/c_j = \rho_j^{n_j} - n_i$. Using Thm. 2.4, we can compute a basis for $G = G_M(c_i/c_j, \rho_i, \rho_j)$, and then we can compute all (of the finitely many) $(k_1, k_2, k_3) \in G$ such that $k_1 = 1$. Let $k_{i,j} = 1 + \max_{(1,k_2,k_3) \in G}(k_2, -k_3)$. We have that $c_i \rho_i^{n_i} \ne c_j \rho_j^{n_j}$ for every $n_i, n_j \ge k_{i,j}$.

Next, for all $1 \le i \le d$ apply Lem. 2.5 to compute $b_i, R_i > 0$ such that $|u_n^{(i)} - c_i \rho_i^{n_i}| < b_i R_i^n$ for all $n \ge 0$. Then,

$$ \begin{aligned} u_{n_i}^{(i)} - u_{n_j}^{(j)} = & c_i \rho_i^n - c_j \rho_j^n + u_{n_i}^{(i)} - c_i \rho_i^n - u_{n_j}^{(j)} + c_j \rho_j^n \\ & > c_i \rho_i^n - c_j \rho_j^n - b_i R_i^n - b_j R_j^n. \end{aligned} $$

Using Thm. 2.13, for each pair $1 \le i < j \le d$ we compute $k'_{i,j}$ such that for all $n_i, n_j \ge k'_{i,j}$, $|c_i \rho_i^n - c_j \rho_j^n| > b_i R_i^n + b_j R_j^n$ and $u_{n_i}^{(i)} - u_{n_j}^{(j)}$, $c_i \rho_i^n - c_j \rho_j^n$ have the same sign.

Now suppose $n_i, n_j \ge k'_{i,j}$, $k'_{i,j}$. By the arguments above, $c_i \rho_i^{n_i} \ne c_j \rho_j^{n_j}$ and hence $u_{n_i}^{(i)} \ne u_{n_j}^{(j)}$.

We next examine (a). Let $1 \le i \le d$. Then

$$ \begin{aligned} & u_{n+1}^{(i)} - u_n^{(i)} < c_i \rho_i^{n+1} - c_i \rho_i^{n+1} - b_i R_i^{n+1} - b_i R_i^n \\ & = c_i(\rho_i - 1)\rho_i^n - b_i(R_i + 1)R_i^n. \end{aligned} $$

As $\rho_i > R_i$, one can compute $k_i \in \mathbb{N}$ such that $c_i(\rho_i - 1)\rho_i^n > b_i(R_i + 1)R_i^n$ for all $n \ge k_i$.

Thus when $m_i \ge k_i, k_{i,j}, k'_{i,j}$ for all $i, j$, items (a), (d) and (e) are satisfied. Let $m'_i$ for $1 \le i \le d$ be such that $\ge k_i, k_{i,j}, k'_{i,j}$ for all $i, j$. Choose $N' \ge 0$ such that $N' \ge u_{m'_i}^{(i)}$ for all $1 \le i \le d$. Let $m_1$ be the smallest number such that $u_{m_1}^{(1)} \ge N'$ and $N = u_{m_1}^{(1)}$. Finally, for $1 \le i \le d$, let $m_i$ be the smallest number such that $u_{m_i}^{(i)} \ge N$. Then (b) and (c) are also satisfied. $\square$

**PROOF OF THM. 5.3.** By Lem. 5.4 (d), each letter of $\alpha[N, \infty)$ is a tuple from $\{0, 1\}^d$ containing at most a single 1. Let $r_i = c_i \rho^{m_i}$ for $1 \le i \le d$, and $\xi = \mathrm{Ord}(\langle r_1 \rho_1^n \rangle_{n=0}^{\infty}, \dots, \langle r_d \rho_d^n \rangle_{n=0}^{\infty}) \in \{1, \dots, d\}^{\omega}$. By (c-e), the word $\xi$, up to a renaming of variables, is equal to a suffix of $\alpha'$ that can be effectively determined. We can now finalise the proof.

(1) Each $P_i$ is procyclic. To see this, let $f(n)$ be the nth largest element of $P_i$. We have to show that $\langle f(n) \mod m \rangle_{n=0}^{\infty}$ is effectively eventually periodic for every $m \in \mathbb{N}$. By Lem. 5.4 (a), the sequences $\langle u_n^{(i)} \rangle_{n=0}^{\infty}$ and $\langle f(n) \rangle_{n=0}^{\infty}$ agree on a suffix that can be effectively determined. It remains to invoke Lem. 2.6.

(2) By Lem. 5.4 (a), each $P_i$ is effectively sparse.

(3) Finally, we prove that $P_1, \dots, P_d$ are pairwise effectively sparse. Let $1 \le i < j \le d$ and $K \ge 0$. Using Lem. 2.5, compute $R_i, R_j, b_i, b_j > 0$ such that $R_i < \rho_i, R_j < \rho_j$, and for all $n \ge 0$, $b_i R_i^n > |u_n^{(i)} - c_i \rho_i^n|$ and $b_j R_j^n > |u_n^{(j)} - c_j \rho_j^n| + K$. Then, the triangle inequality and Thm. 2.13 yield $N' \ge 0$ such that for all $n \ge N'$,

$$ |u_n^{(i)} - u_n^{(j)}| > |c_i \rho_i^n - c_j \rho_j^n| - b_i R_i^n - b_j R_j^n + K \ge K. $$

By Thm. 4.15, $\mathrm{Acc}_{\alpha'}$ reduces to $\mathrm{Acc}_{\alpha'}$. Recall that $\alpha'$ can be obtained from $\xi$ through finite modifications, which can be realised by a transducer. Similarly, $\xi$ can be obtained from $\alpha'$ via a transduction. It remains to invoke Lem. 4.5. $\square$

## 5.2 Effective Almost Periodicity of the Order Word

In this section, let $r_i, \rho_i \in \mathbb{R} \cap \mathbb{Q}$ with $r_i > 0$ and $\rho_i > 1$ for $1 \le i \le d$. Suppose for all $1 \le i < j \le d$ and $n, m \in \mathbb{N}$, $r_i \rho_i^n \ne r_j \rho_j^n$. Let $\xi = \mathrm{Ord}(\langle r_1 \rho_1^n \rangle_{n=0}^{\infty}, \dots, \langle r_d \rho_d^n \rangle_{n=0}^{\infty}) \in \{1, \dots, d\}^{\omega}$ as in Def. 5.2. We will prove the following.

**THEOREM 5.5.**

(a) The word $\xi$ is almost-periodic.

(b) Assuming Schanuel's conjecture, $\xi$ is effectively almost-periodic.

(c) If $1/\log(\rho_1), \dots, 1/\log(\rho_d)$ are linearly independent over $\mathbb{Q}$, then $\xi$ is unconditionally effectively almost-periodic.

(d) If rank($G_M(\rho_1, \dots, \rho_d)$) $\ge$ $d-2$, and $\rho_1, \dots, \rho_d$ are pairwise multiplicatively independent, then $\xi$ is unconditionally effectively almost-periodic.

This result, together with Thm. 5.3, will prove Thm. 5.1. By scaling and reordering the $d$ sequences, **we can without loss of generality assume that $1 < \rho_1 \le \rho_2 \le \dots \le \rho_d$ and $r_1 = 1$. Let**

$$ V = \{\log(r_i \rho_i^n) : 1 \le i \le d, n \in \mathbb{N}\} $$
<figure><img src="image_5.png" /><figcaption>Figure 1: Generating $\xi$.</figcaption></figure>

<figure><img src="image_6.png" /><figcaption>Figure 2: The suffix $\xi[3, \infty)$ as a cutting sequence.</figcaption></figure>

and $\langle v_n \rangle_{n=0}^{\infty}$ be the ordering of $V$ with $v_0 < v_1 < \dots$. Observe that
$$ \xi = \operatorname{Ord}(\langle \log(r_1 \rho_1^n) \rangle_{n=0}^{\infty}, \dots, \langle \log(r_d \rho_d^n) \rangle_{n=0}^{\infty}). $$

Our strategy to prove Thm. 5.5 will be to show that $\xi$ has a suffix that belongs to the class $\mathcal{T}_O$ of toric words; recall from Sec. 2.7 that words in $\mathcal{T}_O$ are uniformly recurrent and hence almost-periodic. To prove effective almost-periodicity, we will deploy number theory either through Baker's theorem or Schanuel's conjecture.

**Example 5.6.** Suppose $r_1 = 1$, $\rho_1 = 2$, $r_2 = 9$, $\rho_2 = 3$. Then
$$ 2^0 < 2^1 < 2^2 < 2^3 < 9 \cdot 3^0 < 2^4 < 9 \cdot 3^1 < 2^5 < \dots $$

and hence $\xi = 11112121121 \dots$. We have $v_0 = 0$, $v_1 = \log(2)$, $v_2 = 2\log(2)$, $v_3 = 3\log(2)$, $v_4 = \log(9)$, and so on. Let $a_n = n \log(r_1 \rho_1^n) = n \log(2)$ and $b_n = \log(r_2 \rho_2^n) = \log(9) + n \log(3)$. Figure 1 illustrates a way to generate $\xi$. We start at the point $(0,0)$ and follow the line $y=x$. Every time a vertical line $x=a_n$ for some $n$ is hit, we write a 1. When we hit a horizontal line $y=b_n$ for some $n$, we write 2. If we discard the first three characters of $\xi$, we obtain a cutting sequence (equivalently, a billiard word), illustrated in Fig. 2. (See [19, Chap. 4.1.2] and [3, 4] for more on billiard words.) Figure 2 is obtained from Fig. 1 by a translation and a scaling. In Fig. 2, we start at the point $(0, y)$, where $0 < y < 1$, and follow the dashed line which has slope $\log(2)/\log(3)$. When we hit a line $x=n$ for $n \in \mathbb{N}$, we write 1; When we hit $y=n$, we write 2.

We will not directly use the fact that a suffix of $\xi$ is a cutting sequence, but combinatorial properties of such sequences can be used to prove a weaker version of Thm. 5.5 (c); see Sec. 5.2.1. We note that cutting sequences generated by a line on the plane with irrational slope (as in Fig. 2) are exactly the Sturmian words [24].

We continue our proof of Thm. 5.5. Define $z_n = \frac{v_n}{\log(\rho_1)}$, and observe that $\langle z_n \rangle_{n=0}^{\infty}$ is strictly increasing. Let $\sigma: \{z_n : n \in \mathbb{N}\} \to \{1, \dots, d\}$ be such that $\xi(n) = \sigma(z_n)$. Observe that for every $n$, there

exists $m \in \mathbb{N}$ such that $z_m = n$ and $\sigma(z_m) = 1$. For this value of $m$, $v_m = \log(r_1 \rho_1^n) = n \log(\rho_1)$. In Ex. 5.6, $z_0 = 0$, $z_1 = 1$, $z_2 = 2$, $z_3 = 3$, $z_4 = \log(9)/\log(2) \approx 3.17$, $z_5 = 4$, $z_6 = \log(9 \cdot 3)/\log(2) \approx 4.75$, $z_7 = 5$, $z_8 = 6$, and so on.

We will next factorise $\xi = w_-w_0w_1\dots$. Intuitively, for $n \in \mathbb{N}$, the finite word $w_n$ contains the labels of all terms of $\langle z_n \rangle_{n=0}^{\infty}$ (obtained by applying $\sigma$) that lie in the interval $[n, n+1)$. Formally, let $\langle k_n \rangle_{n=0}^{\infty}$ be the sequence over $\mathbb{N}$ such that for all $n, m \in \mathbb{N}$, $n \le v_m < n+1$ if and only if $k_n \le m < k_{n+1}$. Then $w_- = \xi[0, k_0)$ and $w_n = \xi[k_n, k_{n+1})$ for all $n \in \mathbb{N}$. Consider $n \in \mathbb{N}$. As argued earlier, there exists $m \in \mathbb{N}$ such that $z_m = n$ and $\sigma(z_m) = 1$. That is, the first letter of $w_n$ for every $n$ is 1. Moreover, in each such $w_n$ the letter 1 occurs exactly once. In Ex. 5.6, $w_-$ is empty, $w_0 = w_1 = w_2 = 1$, $w_3 = 12$, $w_4 = 12$, $w_5 = 1$, and so on.

Let $N$ be the smallest integer $n$ such that every letter of $\{1, \dots, d\}$ appears in $w_0 \cdots w_n \in \{1, \dots, d\}^*$. In Ex. 5.6, $N=3$. Further let $\Sigma = \{w_0, w_1, w_2, \dots\}$ be the set of all finite patterns over $\{1, \dots, d\}$ that start with the letter 1 and contain at most one instance of $i$ for all $i \in \{1, \dots, d\}$. Define $\beta \in \Sigma^\omega$ by $\beta(n) = w_{N+n}$. In our example, $\beta = (12)(12)(1)\cdots$. Observe that the suffix $w_N w_{N+1} \cdots$ of $\xi$ is the image of $\beta$ under the application of the morphism $\mu: \Sigma^* \to \{1, \dots, d\}^*$ defined by $\mu(w) = w(0)\cdots w(|w|-1)$ for $w \in \Sigma^*$. Since effectively almost-periodic words are closed under applications of morphisms (provided that the image word is also infinite) and finite modifications [28], the word $\beta$ is effectively almost-periodic if and only if $\xi$ is. We will next show that $\beta$ is toric with $\beta \in \mathcal{T}_O$. Recall that $\{x \mid x \text{ denotes the fractional part of } x\} = x - \lfloor x \rfloor$.

**THEOREM 5.7.** For $2 \le i \le d$, let $\delta_i = \frac{\log(\rho_1)}{\log(\rho_i)} \in \mathbb{T}$ and

$$ s_i = \left\{ \frac{(N+1) \log(\rho_1) - \log(r_i)}{\log(\rho_i)} \right\} \in \mathbb{T}. $$

Then $\beta$ is the toric word generated by $\mathbf{\delta} = (\delta_2, \dots, \delta_d) \in \mathbb{T}^{d-1}$ and $\mathbf{s} = (s_2, \dots, s_d) \in \mathbb{T}^{d-1}$, as well as a collection of open subsets of $\mathbb{T}^{d-1}$ defined by linear inequalities (in variables $x_2, \dots, x_d$) of the form $x_i/\delta_i < x_j/\delta_j$ or $x_i/\delta_i \sim 1$, where $\sim = \{>, <\}$ and $2 \le i, j \le d$.

**PROOF.** For $2 \le i \le d$ and $n \in \mathbb{N}$, let

$$ L(n, i) = \left\{ \frac{\log(r_i \rho_i^k)}{\log(\rho_1)} : k \in \mathbb{N} \right\} \cap (-\infty, N+n+1] $$

and $\Delta(n, i)$ be the smallest distance from $N+n+1$ to an element of $L(n, i)$. Intuitively, $L(n, i)$ is the “downward distance” from $N+n+1$ to the lattice $\{\log(r_i \rho_i^k)/\log(\rho_1) : k \in \mathbb{N}\}$. By construction of $N$, the value of $\Delta(n, i)$ is well-defined and finite for every $n$ and $i$.

Let $b = b_0 b_1 \cdots b_m \in \Sigma$, where $b_i \in \{1, \dots, d\}$ for all $i$ and $b_0 = 1$. By definition, $\beta(n) = b$ if and only if $w_{N+n} = b$, which is the case if and only if the following hold.

(*) There exist $k_1, \dots, k_m \in \mathbb{N}$ such that

$$ N + n \le \frac{\log (r_{b_1} \rho_{b_1}^{k_1})}{\log(\rho_1)} < \dots < \frac{\log (r_{b_m} \rho_{b_m}^{k_m})}{\log(\rho_1)} < N + n + 1. $$

(**) For every $k \in \mathbb{N}$ and $i \in \{2, \dots, d\}$ not appearing in $b$,

$$ \frac{\log(r_i \rho_i^k)}{\log(\rho_1)} \notin [N+n, N+n+1). $$
<figure><img src="image_7.png" /><figcaption>Figure 3: The torus for $\rho_1 = 2$, $\rho_2 = 3$, and $\rho_3 = 5$.</figcaption></figure>

As discussed earlier, for every $t \in \mathbb{N}$ there exist $l \in \mathbb{N}$ such that

$$z_l = t = \log(r_1 \rho_l^k) / \log(\rho_1).$$

Since no two distinct terms of $\langle z_n \rangle_{n=0}^\infty$ are equal, for every $i \neq 1$ and $k \in \mathbb{N}$, $\log(r_i \rho_i^k) / \log(\rho_1) \notin \mathbb{N}$. Thus in (*) and (**) we can replace non-strict inequalities with strict ones, and vice versa.

Next, observe that (*) is equivalent to

$$\Delta(n, b_m) < \dots < \Delta(n, b_1) < 1. \qquad (7)$$

Similarly, (**) holds if and only if for every $i \in \{2, \dots, d\}$ not appearing in $b$,

$$\Delta(n, i) > 1. \qquad (8)$$

Since for all $i$ and $k \in \mathbb{N}$,

$$\frac{\log(r_i \rho_i^k)}{\log(\rho_1)} = \frac{\log(r_i)}{\log(\rho_1)} + k \frac{\log(\rho_i)}{\log(\rho_1)},$$

we have that

$$\Delta(n, i) = \frac{\log(\rho_i)}{\log(\rho_1)} \cdot \left\{ \frac{N + n + 1 - \log(r_i) / \log(\rho_1)}{\log(\rho_i) / \log(\rho_1)} \right\} = \frac{1}{\delta_i} \{s_i + n\delta_i\}.$$

Consider the dynamical system on $\mathbb{T}^{d-1}$ given by $(g, s)$, where $g(y_2, \dots, y_d) = (\{y_2 + \delta_2\}, \dots, \{y_d + \delta_d\})$. Recall from Sec. 2.7 that for $n \in \mathbb{N}$, $g^{(n)}(s) = (\{s_2 + n\delta_2\}, \dots, \{s_d + n\delta_d\})$. Considering (7) and (8), we are led to defining, for $b = b_0 b_1 \dots b_m \in \Sigma$, $S_b \subseteq \mathbb{T}^{d-1}$ as the (open) set of all $(x_2, \dots, x_d) \in \mathbb{T}^{d-1}$ such that

$$\frac{x_{b_m}}{\delta_{b_m}} < \dots < \frac{x_{b_1}}{\delta_{b_1}} < 1 \quad \wedge \quad \bigwedge_{\substack{1 \le j \le d \\ j \ne b_1, \dots, b_m}} \frac{x_j}{\delta_j} > 1. \qquad (9)$$

With this definition, for all $b \in \Sigma$ and $n \in \mathbb{N}$, $\beta(n) = b$ if and only if $g^{(n)}(s) \in S_b$. $\square$

In the remainder of this section, let $\mathbf{s} = (s_2, \dots, s_d) \in \mathbb{T}^{d-1}$ and $\mathbf{\delta} = (\delta_2, \dots, \delta_d) \in \mathbb{T}^{d-1}$, and $g: \mathbb{T}^{d-1} \to \mathbb{T}^{d-1}$ be defined as above. Figure 3 illustrates the target sets $\{S_b : b \in \Sigma\}$ constructed in Thm. 5.7 for the sequences $\langle 2^n \rangle_{n=1}^\infty$, $\langle 3^n \rangle_{n=1}^\infty$, and $\langle 5^n \rangle_{n=1}^\infty$. Figure 3 can also be viewed as follows. Consider a dynamical system on $\mathbb{N}$ that starts at 2 and at each step jumps to the next power of 2. At each step, a letter from $\{1, 12, 13, 123, 132\}$ is written depending on whether the point jumped over a power of 3 or a power of 5 in the last step (and in what order). The exact letter to be written is determined by keeping track of the fractional part of $\log_3(2^n)$ and $\log_5(2^n)$; this gives rise to the linear inequalities defining the open sets depicted in Fig. 3.

Since $\beta \in \mathcal{T}_O$, it is uniformly recurrent (Sec. 2.7). As mentioned earlier, the suffix $w_N w_{N+1} \cdots$ of $\xi$ is the image of $\beta$ under a mor- phism, and hence is almost-periodic by [28, Sec. 3]. It follows that $\xi$ is almost-periodic; **this proves Thm. 5.5 (a).**

We next analyse effective almost-periodicity of $\beta$, which implies effective almost-periodicity of $\xi$. We will need the following lemma.

**LEMMA 5.8.** Let $\alpha$ be a uniformly recurrent word for which $\alpha(n)$ can be effectively determined given $n$. Then the word $\alpha$ is effectively almost-periodic if and only if we can decide occurrence of a given finite word $w$ in $\alpha$.

**PROOF.** Recall that every finite factor of a uniformly recurrent word occurs infinitely often and with bounded gaps. Let $w$ be a finite pattern that occurs in $\alpha$. We will show how to compute $M \in \mathbb{N}$ such that $w$ occurs at least twice in every factor of $\alpha$ of length $M$. The value $M$ is then an upper bound on the gaps between consecutive occurrences of $w$ in $\alpha$. Note that such $M$ exists by the uniform recurrence assumption. Let $T_n$ be the set of all factors of $\alpha$ of length $n$, which can be computed by enumerating all words of length $n$ and checking whether each one occurs in $\alpha$. The value $M$ can be found by computing $T_n$ for increasing values of $n$. $\square$

We next study how to decide whether given $w \in \Sigma^*$ occurs in $\beta$.

**LEMMA 5.9.** Let $w \in \Sigma^*$. There exists an open subset $S_w \subseteq \mathbb{T}^{d-1}$ with the following property. For all $n \in \mathbb{N}$, the pattern $w$ occurs in $\beta$ at the position $n$ if and only if $g^{(n)}(s) \in S_w$. Furthermore, we can compute a representation of $S_w$ as a Boolean combination of inequalities of the form

$$h(x_2/\delta_2, \dots, x_d/\delta_d, 1/\delta_2, \dots, 1/\delta_d) \sim 0, \qquad (10)$$

where $h$ is a $\mathbb{Q}$-affine form and $\sim$ is an inequality symbol.

**PROOF.** See [8, App. A.5]. $\square$

We next prove Thm. 5.5 (c). Suppose $1/\log(\rho_1), \dots, 1/\log(\rho_d)$ are linearly independent over $\mathbb{Q}$. Then for all $c_2, \dots, c_d, k \in \mathbb{Q}$,

$$\sum_{i=2}^{d} c_i \delta_i = k \iff \frac{c_2}{\log(\rho_2)} + \dots + \frac{c_d}{\log(\rho_d)} = \frac{k}{\log(\rho_1)} \\ \Rightarrow k, c_2, \dots, c_d = 0.$$

Hence $G_A(\mathbf{\delta})$ is the trivial group, $\mathbb{T}\mathbf{\delta} = \mathbb{T}^{d-1}$, and by Kronecker's theorem (Thm. 2.14), $\langle g^{(n)}(s) \rangle_{n=0}^\infty$ is dense in $\mathbb{T}^{d-1}$. Therefore, a pattern $w \in \Sigma^*$ occurs in $\beta$ if and only if $S_w \neq \emptyset$. As shown in Lem. 5.9, to decide whether $S_w \neq \emptyset$ we have to decide the truth of $\Psi := \exists x_2, \dots, x_d : \Phi(x_2, \dots, x_d)$ where $\Phi$ is a formula of the form

$$\bigvee_{j \in J} \bigwedge_{m \in M} h_{j,k}(x_2/\delta_2, \dots, x_d/\delta_d, 1/\delta_2, \dots, 1/\delta_d) \sim_{j,k} 0.$$

Recall that each $h_{j,k}$ is a $\mathbb{Q}$-affine form. Hence $\Psi$ is equivalent to $\exists \tilde{x}_2, \dots, \tilde{x}_d : \Phi(\tilde{x}_2, \dots, \tilde{x}_d)$. Applying Fourier-Motzkin Elimination, we can compute finitely many $\mathbb{Q}$-affine forms $h_{l,m}$ and an inequality symbols $\sim_{l,m}$ such that $\Psi$ is true if and only if

$$\bigvee_{l \in L} \bigwedge_{m \in M} h_{l,m} (1/\delta_2, \dots, 1/\delta_d) \sim_{l,m} 0.$$

Recall that $\frac{1}{\delta_i} = \frac{\log(\rho_i)}{\log(\rho_1)}$. For $h(x_2, \dots, x_d) = c_1 + c_2 x_2 + \dots + c_d x_d$, $h(1/\delta_2, \dots, 1/\delta_d) = \frac{1}{\log(\rho_1)}(c_1 \log(\rho_1) + \dots + c_d \log(\rho_d))$.

Hence for all $l, m$, whether $h_{l,m}(1/\delta_2, \dots, 1/\delta_d) \sim_{l,m} 0$ can be decided using Baker's theorem (Lem. 2.12). Thus, under the assumption that $1/\log(\rho_1), \dots, 1/\log(\rho_d)$ are linearly independent over $\mathbb{Q}$,
we can decide whether a given pattern $w \in \Sigma^*$ occurs in $\beta$. We conclude that $\beta$ and hence $\xi$ are effectively almost-periodic. This proves Thm. 5.5 (c). To prove Thm. 5.5 (d), recall Lem. 2.11 and invoke Thm. 5.5 (c).

It remains to prove Thm. 5.5 (b). Assuming Schanuel's conjecture, we can compute a basis of $G_A(1/\log(\rho_1), \dots, 1/\log(\rho_d))$ (Lem. 2.9). Hence we can compute an $\mathbb{R}_{\exp}$ formula defining the compact $\mathbb{T}_{\delta,s} \subseteq \mathbb{T}^{d-1}$ in which in $\langle f^{(n)}(s) \rangle_{n=0}^{\infty}$ is dense (Sec. 2.7). Recall from Sec. 2.7 that a pattern $w$ occurs in $\beta$ if and only if $S_w \cap \mathbb{T}_{\delta,s} \neq \emptyset$, which can be effectively verified using a decision procedure for the first-order theory of $\mathbb{R}_{\exp}$. Hence $\beta$ and $\xi$ are effectively almost-periodic assuming Schanuel's conjecture. This proves Thm. 5.5 (b).

### 5.2.1 Applying the Theory of Cutting Sequences. Let

$$ \xi = \text{Ord}(\langle r_1 \rho_1^n \rangle_{n=0}^{\infty}, \dots, \langle r_d \rho_d^n \rangle_{n=0}^{\infty}) $$

be as above. As mentioned earlier, it can directly be shown that $\xi$ has a suffix that is the cutting sequence generated by the line $\{(s_1 + t/\log(\rho_1), \dots, s_d + t/\log(\rho_d)): t \ge 0\}$, where $s_i \in [0, 1)$ for all $i$. As in Sec. 4.5, write $p(n)$ for the number of distinct factors of $\xi$ of length $n$; the function $p$ is the factor complexity of $\xi$. The factor complexity of cutting sequences has been extensively studied, and in many cases, an exact formula for $p(n)$ is known. We give an overview of results in this direction.

(i) If $d=2$ and $\log(\rho_1)/\log(\rho_2)$ is irrational, then $\xi$ is a Sturmian word and therefore $p(n) = n+1$. See, e.g. [2, Chap. 10.5].

(ii) By [3], if $d=3$, and $1/\log(\rho_1)$, $1/\log(\rho_2)$, $1/\log(\rho_3)$ as well as $\log(\rho_1)$, $\log(\rho_2)$, $\log(\rho_3)$ are linearly independent over $\mathbb{Q}$, then $p(n) = n^2 + n + 1$.

(iii) For arbitrary $d > 0$, Bedaride [6] gives an exact formula for $p(n)$ assuming $1/\log(\rho_1), \dots, 1/\log(\rho_d)$ as well as every triple $\log(\rho_i), \log(\rho_j), \log(\rho_k)$ for pairwise distinct $i, j, k$ are linearly independent over $\mathbb{Q}$. This generalises the well-known result [4] of Baryshnikov.

Going back to our word $\xi$, let $w$ be a finite pattern of length $n$, and suppose we know the value of $p(n)$. Then we can decide whether $w$ occurs (as required by Lem. 5.8) in $\xi$ by just reading prefixes of $\xi$ until we have seen $p(n)$ distinct factors of length $n$. Using this approach, we can prove that the word $\xi$ is effectively almost-periodic under the assumption of (iii). Note, however, that this result is strictly weaker than Thm. 5.5 (b). Consider, for example, $\rho_1 = 2$, $\rho_2 = 3$ and $\rho_3 = 6$. By Lem. 2.11, $1/\log(\rho_1), \dots, 1/\log(\rho_3)$ are linearly independent over $\mathbb{Q}$, but $\log(\rho_1), \dots, \log(\rho_3)$ are not.

## 5.3 Proof of Theorem 5.1

We can now combine everything we have shown so far to prove Thm. 5.1. For $1 \le i \le d$, let $\langle u_n^{(i)} \rangle_{n=0}^{\infty}$ for $1 \le i \le d$ be as in the statement of Thm. 5.1 with the value set $P_i \subseteq \mathbb{N}$. Further let $\alpha$ be the characteristic word of $(P_1, \dots, P_d)$, and recall that the MSO theory of $\langle \mathbb{N}; <, P_1, \dots, P_d \rangle$ is decidable if and only if $\text{Acc}_\alpha$ is decidable. Applying Thm. 5.3, we can construct $r_1, \dots, r_d$ such that $\text{Acc}_\alpha$ reduces to $\text{Acc}_\xi$, where $\xi = \text{Ord}(\langle r_1 \rho_1^n \rangle_{n=0}^{\infty}, \dots, \langle r_d \rho_d^n \rangle_{n=0}^{\infty})$. Applying Thm. 5.5, we obtain conditions under which $\xi$ is effectively almost-periodic. It remains to recall from Thm. 4.2 that $\text{Acc}_\xi$ is decidable if $\xi$ is effectively almost-periodic.

# 6 MSO DECIDABILITY VIA EXPANSIONS IN INTEGER BASES

In this section, we discuss a second class of LRS that give rise to interesting MSO theories; we will show that these are intimately connected to base-$b$ expansions of certain algebraic numbers. That is, we will show that the base-$b$ expansion of $\sqrt[d]{p/q}$ is intrinsic to the pair of predicates $\{qn^d: n \in \mathbb{N}\}$ and $\{pb^{nd}: n \in \mathbb{N}\}$. For example, the binary expansion of $\sqrt[3]{1/27} = 1/3$ underlies the pair of predicates $\{27n^3: n \in \mathbb{N}\}$ and $\{8^n: n \in \mathbb{N}\}$, while the binary expansion of $\sqrt[5]{5}$ underlies the pair $\{n^3: n \in \mathbb{N}\}$ and $\{5 \cdot 8^n: n \in \mathbb{N}\}$. We can use these connections to give decidability results for various MSO theories assuming that certain numbers are normal. The dynamical systems at play in this section differ from the ones we considered previously: they are defined by numeration systems [24, Chap. 7] as opposed to translations on a torus (Sec. 5.2 and 2.7).

## 6.1 Normal numbers

A number is (weakly) normal in base $b$ if its base-$b$ expansion $\alpha$ is a (weakly) normal word: that is, $\alpha$ contains infinitely many occurrences of each finite word over $\Sigma = \{0, \dots, b-1\}$. Recall from Thm. 4.16 that for such $\alpha$, $\text{Acc}_\alpha$ is decidable. For a detailed discussion of normal numbers, see surveys [21, 29] and the book [12]. In particular, [21] states the following conjecture.

**CONJECTURE 6.1.** An irrational algebraic number $\alpha$ is weakly normal in any integer base $b \ge 2$.

The strongest result towards this conjecture is due to Adamczewski and Bugeaud [1]. Let $p(n)$ be the number of distinct factors of $\alpha$ of length $n$. The function $p$ is called the factor complexity of $\alpha$.

**THEOREM 6.2.** If $b \ge 2$ and $\alpha$ is the base-$b$ expansion of an irrational algebraic number, then

$$ \liminf_{n \to \infty} \frac{p(n)}{n} = +\infty. $$

## 6.2 Reductions and decidability

We begin by considering the case where $\sqrt[d]{p/q}$ is rational, which implies that its base-$b$ expansion is ultimately periodic for any $b \ge 2$. The following is a generalisation of Cor. 1.3; see [8, App. A.6] for the proof, which is a simple application of Thm. 4.11.

**THEOREM 6.3.** Let $b, d \ge 2$ and $p, q \ge 1$ be integers such that $\sqrt[d]{p/q}$ is rational. Let $\alpha \in (\{0, 1\}^2)^\omega$ be the characteristic word of $(P_1, P_2)$, where $P_1 = \{qn^d: n \in \mathbb{N}\}$ and $P_2 = \{pb^{nd}: n \in \mathbb{N}\}$. Then the problem $\text{Acc}_\alpha$ is decidable.

The case where $\sqrt[d]{p/q}$ is irrational is more involved.

**THEOREM 6.4.** Let $b, d, p, q$ be positive integers such that $\sqrt[d]{p/q}$ is irrational. Furthermore, let

(1) $\alpha \in (\{0, 1\}^2)^\omega$ be the characteristic word of $(P_1, P_2)$, where $P_1 = \{qn^d: n \in \mathbb{N}\}$ and $P_2 = \{pb^{nd}: n \in \mathbb{N}\}$;

(2) $\beta \in \{0, 1, \dots, b-1\}^\omega$ be the infinite string of digits in the base-$b$ expansion of $\eta = \sqrt[d]{p/q}$ and

(3) $\gamma$ be the order word corresponding to $\alpha$, i.e. the word obtained by deleting all occurrences of $(0, 0)$ from $\alpha$.

Then the problems $\text{Acc}_\alpha$, $\text{Acc}_\beta$, and $\text{Acc}_\gamma$ are Turing-equivalent.
PROOF. We will prove the theorem by showing:

(1) $Acc_β$ reduces to $Acc_α$.

(2) $Acc_α$ reduces to $Acc_γ$.

(3) $Acc_γ$ reduces to $Acc_β$.

**Part (1):** $Acc_β$ reduces to $Acc_α$. By construction (except for an easily computable finite prefix), we have the invariant

$$ \beta(n) = \lfloor \eta b^n \rfloor \mod b, \quad \beta(n) \in \{0, \dots, b-1\}. $$

For example, if $p = 2$, $q = 1$, $b = 10$, and $d = 2$, then $\eta = \sqrt{2} = 1.4142\dots$ and $\beta(0) = 1$, $\beta(1) = 4$, $\beta(2) = 1$ etc. This observation accounts for one reduction of the Turing equivalence.

We will prove the claim by constructing a deterministic transducer $\mathcal{B}$ such that $\beta = \mathcal{B}(\alpha)$ and applying Lem. 4.5. The states of $\mathcal{B}$ are $R = \{0, \dots, b-1\}$ with initial state $b-1$. The transducer moves from state $q$ to state $q+1 \mod b$ if it reads $(1, 0)$ and does not move otherwise. The transducer outputs its current state $q$ on reading $(0, 1)$, and otherwise outputs the empty word. Thus, the letter $(0, 0)$ has no effect on the state or output of the transducer. By construction, the transducer keeps count of the number of occurrences of $P_1$ modulo $b$, and outputs this count on encountering an occurrence of $P_2$. Hence its $n$th output will be $b_n \mod b$, where $b_n := |\{m \in \mathbb{N} : qm^d < pb^{nd}\}| - 1$. It remains to observe that

$$ b_n = |\{m \in \mathbb{N} : m < b^n \cdot \sqrt[d]{p/q}\} - 1| = \lfloor \eta b^n \rfloor \pmod{b}. $$

**Part (2):** $Acc_α$ reduces to $Acc_γ$. This reduction requires a more refined understanding of the word $\alpha$. We readily observe that $(1, 1)$ does not occur in $\alpha$. If $qm^d = pb^{nd}$, then $m = \eta b^n$. As $\eta$ is irrational, $m$ and $b^n$ cannot both be integers. Thus, all letters of $\alpha$ are one of $(0, 0)$, $(0, 1)$ and $(1, 0)$.

Consider the order word $\gamma \in \{(1, 0), (0, 1)\}^\omega$ of $(P_1, P_2)$. Write

$$ \alpha = (0, 0)^{n_0} \gamma(0)(0, 0)^{n_1} \gamma(1) \dots. $$

We apply Thm. 4.15 to show that in the case of $(P_1, P_2)$, the acceptance problem of the characteristic word reduces to that of the order word. Condition (1) of the premise, i.e. that $P_1$ and $P_2$ are procyclic and effectively sparse, are easily seen to hold. We have also established that $P_1$ and $P_2$ can never hold simultaneously. To argue Condition (2), i.e. that $P_1, P_2$ are pairwise effectively sparse, we apply the following result of Schinzel and Tijdeman [33].

**LEMMA 6.5 (SCHINZEL AND TIJDEMAN).** For every $N \ge 1$, the equation $|qn^d - pb^{md}| = N$ has finitely many solutions $(n, m)$ that can be effectively enumerated.

Hence the claim follows from Thm. 4.15: $Acc_α$ of the characteristic word reduces to $Acc_γ$ of the order word.

**Part (3):** $Acc_γ$ reduces to $Acc_β$. Note that $\gamma$ itself can be written as $\gamma = (1, 0)^{m_0} (0, 1)(1, 0)^{m_1} (0, 1)\dots$. We now reduce $Acc_γ$ to $Acc_β$ using Cor. 4.7. We remark that despite the differing underlying arithmetic, the key automata-theoretic ideas are similar to the proof

of Thm. 4.15. We record the invariants:

$$ S_k = \sum_{i=0}^{k} m_i = \lfloor \eta b^k \rfloor $$

$$ \beta_k = \lfloor \eta b^k \rfloor \pmod{b} $$

$$ bS_k \le S_{k+1} < b(S_k + 1) $$

$$ S_{k+1} = bS_k + \beta_{k+1} = S_k + m_{k+1}. $$

Define

$$ \gamma' = \perp^{m_0} \beta(0) \perp^{m_1} \beta(1) \dots. $$

Applying Lem. 4.5, $Acc_γ$ reduces to $Acc_γ'$ via a straightforward transduction, which is in fact a homomorphism. It thus suffices to reduce $Acc_γ'$ to $Acc_β$.

We denote $S_k = \lfloor \eta b^k \rfloor$ and observe that $bS_k \le S_{k+1} < b(S_k + 1)$ (one can check the identity $b\lfloor x \rfloor \le \lfloor bx \rfloor < b(\lfloor x \rfloor + 1)$). Thus, $S_{k+1} = bS_k + \beta_{k+1} = S_k + m_{k+1}$. Given $\beta$ and $m_0$, we can use the above properties to track $S_k$, and hence $m_k$ modulo $t$ for any integer $t$. This is useful, because: (1) it is easy to observe that $\langle m_k \rangle_{k \in \mathbb{N}}$ is a strictly increasing sequence, and that we can effectively compute $j$ such that $m_k \ge N$ for all $k \ge j$; (2) for any morphism $h$ into a finite monoid $M$, there exist effective $N, t$ such that for all $n \ge N$, $h(\perp^n) = h(\perp^{n+t})$.

By the observations above, given any morphism $h$ into a finite monoid $M$ we can construct a transducer $\mathcal{B}$ with $\mathcal{B}(\beta) = \mu \in M^\omega$. Recall that we take the $j$th factor of $\gamma'$ to be $\perp^{m_j} \beta(j)$. On reading $\beta(j)$, $\mathcal{B}$ outputs $\mu_j$, with the property that $h(\perp^{m_j} \beta(j)) = \mu_j$ for all $j \in \mathbb{N}$. Invoking Cor. 4.7, $Acc_γ'$ reduces to $Acc_β$. $\square$

By Conj. 6.1, it is expected that $\sqrt[d]{p/q}$ is a weakly normal number in base-$b$ when it is irrational. Hence, if the conjecture holds, $Acc_β$ is decidable by Thm. 4.16. Applying Theorem 6.4, both $Acc_α$ and $Acc_γ$ are decidable assuming Conj. 6.1.

By mirroring the proof of Thm. 6.4 in the special case where $p = b, q = 1, d = 2$, we can show the following.

**THEOREM 6.6.** Let $b \ge 2$, $P_1 = N_2$, $P_2 = \text{Pow}_b$, and $\Sigma = \{0, 1\}^2$. Further let $\alpha \in \Sigma^\omega$ denote the characteristic word of $(P_1, P_2)$ and $\beta \in \{0, \dots, b-1\}^\omega$ be the base-$b$ expansion of $\sqrt{b}$. The problems $Acc_α$ and $Acc_β$ are Turing-equivalent.

See [8, App. A.7] for the proof. Applying this result with $b = 2$, the MSO theory of $\langle \mathbb{N} ; <, N_2, \text{Pow}_2 \rangle$ is Turing-equivalent to $Acc_β$, where $\beta$ is the binary expansion of $\sqrt{2}$, as stated in the abstract.

ACKNOWLEDGMENTS

Toghrul Karimov, Joël Ouaknine, and Mihir Vahanwala were supported by the DFG grant 389792660 as part of TRR 248 (see https://perspicuous-computing.science). Joël Ouaknine is also affiliated with Keble College, Oxford as emmy network Fellow. Valérie Berthé was supported by the Agence Nationale de la Recherche through the project "SymDynAr" (ANR-23-CE40-0024-01). James Worrell was supported by EPSRC Fellowship EP/X033813/1.

The Max Planck Institute for Software Systems is part of the Saarland Informatics Campus. This work partly arose through exchanges held at the workshop Algorithmic Aspects of Dynamical Systems, which took place in April and May 2023 at McGill University's Bellairs Research Institute in Barbados.
REFERENCES

[1] Boris Adamczewski and Yann Bugeaud. 2007. On the complexity of algebraic numbers I. Expansions in integer bases. *Annals of Mathematics* (2007), 547–565.

[2] Jean-Paul Allouche and Jeffrey Shallit. 2003. *Automatic sequences: theory, applications, generalizations*. Cambridge university press.

[3] Pierre Arnoux, Christian Mauduit, Iekata Shiokawa, and Jun-ichi Tamura. 1994. Complexity of sequences defined by billiard in the cube. *Bulletin de la Société Mathématique de France* 122, 1 (1994), 1–12.

[4] Yu. Baryshnikov. 1995. Complexity of trajectories in rectangular billiards. *Com- munications in mathematical physics* 174 (1995), 43–56.

[5] Paul T Bateman, Carl G Jockusch, and Alan R Woods. 1993. Decidability and undecidability of theories with a predicate for the primes. *The Journal of symbolic logic* 58, 2 (1993), 672–687.

[6] Nicolas Bedaride. 2009. Directional complexity of the hypercubic billiard. *Discrete mathematics* 309, 8 (2009), 2053–2066.

[7] Valérie Berthé, Toghrul Karimov, Joël Ouaknine, Mihir Vahanwala, and James Worrell. 2023. The Monadic Theory of Toric Words. *arXiv preprint arXiv:2311.04895* (2023).

[8] Valérie Berthé, Toghrul Karimov, Joris Nieuwveld, Joël Ouaknine, Mihir Vahanwala, and James Worrell. 2024. On the Decidability of Monadic Second-Order Logic with Arithmetic Predicates. *arXiv:2405.07953* [cs.LO].

[9] Achim Blumensath. 2023. Monadic Second-Order Model Theory. www.fi.muni.cz/~blumens/. [Online; accessed on 09 November 2023].

[10] J. R. Büchi. 1990. On a Decision Method in Restricted Second Order Arithmetic. In *The Collected Works of J. Richard Büchi*. Springer New York, 425–435.

[11] J. R. Büchi and L. H. Landweber. 1969. Definability in the Monadic Second-Order Theory of Successor. *The Journal of Symbolic Logic* 34, 2 (1969), 166–170. http://www.jstor.org/stable/2271090

[12] Yann Bugeaud. 2012. *Distribution modulo one and Diophantine approximation*. Cambridge Tracts in Mathematics, Vol. 193. Cambridge University Press, Cambridge. xvi+300 pages. https://doi.org/10.1017/CBO9781139017732

[13] Jin-yi Cai, Richard J. Lipton, and Yechezkel Zalcstein. 2000. The Complexity of the A B C Problem. *SIAM J. Comput.* 29, 6 (2000), 1878–1888. https://doi.org/10.1137/S0097539794276853

[14] Olivier Carton and Wolfgang Thomas. 2002. The Monadic Theory of Morphic Infinite Words and Generalizations. *Information and Computation* 176, 1 (2002), 51–65.

[15] Henri Cohen. 2013. *A course in computational algebraic number theory*. Vol. 138. Springer Science & Business Media.

[16] George B Dantzig, B Curtis Eaves, et al. 1973. Fourier-Motzkin elimination and its dual. *J. Comb. Theory, Ser. A* 14, 3 (1973), 288–297.

[17] Calvin C. Elgot and Michael O. Rabin. 1966. Decidability and Undecidability of Extensions of Second (first) Order Theory of (generalized) Successor. *The Journal of Symbolic Logic* 31, 02 (1966), 169–181.

[18] Graham Everest, Alf van der Poorten, Igor Shparlinski, and Thomas Ward. 2003. *Recurrence Sequences*. American Mathematical Society.

[19] N. Pytheas Fogg, Valéré Berthé, Sébastien Ferenczi, Christian Mauduit, and Anne Siegel. 2002. *Substitutions in dynamics, arithmetics and combinatorics*. Springer.

[20] Steven M. Gonek and Hugh L. Montgomery. 2016. Kronecker's Approximation Theorem. *Indagationes Mathematicae* 27, 2 (2016), 506–523. https://www.sciencedirect.com/science/article/pii/S0019357716000148 In Memoriam J.G. Van der Corput (1890–1975) Part 2.

[21] Glyn Harman. 2002. One hundred years of normal numbers. In *Surveys in Number Theory*. AK Peters/CRC Press, 57–74.

[22] Toghrul Karimov, Engel Lefaucheux, Joël Ouaknine, David Purser, Anton Varonka, Markus A. Whiteland, and James Worrell. 2022. What's decidable about linear loops? *Proc. ACM Program. Lang.* 6, POPL (2022), 1–25.

[23] Serge Lang. 1966. *Introduction to Transcendental Numbers*. Addison-Wesley.

[24] M. Lothaire. 2002. *Algebraic combinatorics on words*. Vol. 90. Cambridge university press.

[25] A. Macintyre and A. J. Wilkie. 1996. On the Decidability of the Real Exponential Field. In *Kreiseliana. About and Around Georg Kreisel*, Piergiorgio Odifreddi (Ed.). A K Peters, 441–467.

[26] David W Masser. 1988. Linear relations on algebraic groups. *New Advances in Transcendence Theory* (1988), 248–262.

[27] Eugene M Matveev. 2000. An explicit lower bound for a homogeneous rational linear form in the logarithms of algebraic numbers. *II. Izvestiya: Mathematics* 64, 6 (2000), 1217.

[28] An. Muchnik, A. Semenov, and M. Ushakov. 2003. Almost periodic sequences. *Theoretical Computer Science* 304, 1 (2003), 1–33.

[29] Martine Queffélec. 2006. Old and new results on normality. *Lecture Notes-Monograph Series* (2006), 225–236.

[30] Alexander Rabinovich. 2007. On decidability of monadic logic of order over the naturals extended by monadic predicates. *Information and Computation* 205, 6 (2007), 870–889.

[31] Alexander Rabinovich and Wolfgang Thomas. 2006. Decidable theories of the ordering of natural numbers with unary predicates. In *International Workshop on Computer Science Logic*. Springer, 562–574.

[32] Raphael M Robinson. 1958. Restricted set-theoretical definitions in arithmetic. *Proc. Amer. Math. Soc.* 9, 2 (1958), 238–242. https://doi.org/0.1090/S0002-9939-1958-0093479-4

[33] Andrzej Schinzel and Robert Tijdeman. 1976. On the equation $y^m = P(x)$. *Acta Arithmetica* 31 (1976), 199–204.

[34] A. L. Semenov. 1980. On certain extensions of the arithmetic of addition of natural numbers. *Mathematics of The USSR-Izvestiya* 15 (1980), 401–418. https://apisemanticscholar.org/CorpusID:123422158

[35] A. L. Semenov. 1984. Logical Theories of One-Place Functions on the Set of Natural Numbers. *Mathematics of the USSR-Izvestiya* 22, 3 (1984), 587–618.

[36] Wolfgang Thomas. 1997. Languages, automata, and logic. In *Handbook of Formal Languages: Volume 3 Beyond Words*. Springer, 389–455.

[37] Michel Waldschmidt. 2000. *Diophantine Approximation on Linear Algebraic Groups: Transcendence Properties of the Exponential Function in Several Variables*. Springer Berlin Heidelberg, Berlin, Heidelberg.