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

Valérie Berthé<EMAIL_ADDRESS>Université Paris Cité, IRIF,
CNRSParisFrance75013 0000-0001-5561-7882 ,  Toghrul Karimov<EMAIL_ADDRESS>0000-0002-9405-2332 ,  Joris Nieuwveld<EMAIL_ADDRESS>0009-0002-0339-1230 ,  Joël Ouaknine<EMAIL_ADDRESS>0000-0003-0031-9356 ,
Mihir Vahanwala<EMAIL_ADDRESS>0009-0008-5709-899X Max Planck Institute
for
Software SystemsSaarland Informatics CampusSaarbrückenGermany66123 and  James
Worrell<EMAIL_ADDRESS>0000-0001-8151-2443 University of Oxford, Department
of Computer ScienceOxfordUnited KingdomOX1 3QD

(2024)

###### Abstract.

We investigate the decidability of the monadic second-order (MSO) theory of
the structure $\langle\mathbb{N};<,P_{1},\ldots,P_{k}\rangle$, for various
unary predicates $P_{1},\ldots,P_{k}\subseteq\mathbb{N}$. We focus in
particular on ‘arithmetic’ predicates arising in the study of linear
recurrence sequences, such as fixed-base powers
$\mathsf{Pow}_{k}=\\{k^{n}:n\in\mathbb{N}\\}$, $k$-th powers
$\mathsf{N}_{k}=\\{n^{k}:n\in\mathbb{N}\\}$, and the set of terms of the
Fibonacci sequence $\mathsf{Fib}=\\{0,1,2,3,5,8,13,\ldots\\}$ (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 $\langle\mathbb{N};<,\mathsf{Pow}_{2},\mathsf{Fib}\rangle$
is decidable;

  * •

The MSO theory of
$\langle\mathbb{N};<,\mathsf{Pow}_{2},\mathsf{Pow}_{3},\mathsf{Pow}_{6}\rangle$
is decidable;

  * •

The MSO theory of
$\langle\mathbb{N};<,\mathsf{Pow}_{2},\mathsf{Pow}_{3},\mathsf{Pow}_{5}\rangle$
is decidable assuming Schanuel’s conjecture;

  * •

The MSO theory of $\langle\mathbb{N};<,\mathsf{Pow}_{4},\mathsf{N}_{2}\rangle$
is decidable;

  * •

The MSO theory of $\langle\mathbb{N};<,\mathsf{Pow}_{2},\mathsf{N}_{2}\rangle$
is Turing-equivalent to the MSO theory of $\langle\mathbb{N};<,S\rangle$,
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.

This is the full version of the paper (Berthé et al., 2024).

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

††journalyear: 2024††copyright: rightsretained††conference: 39th Annual
ACM/IEEE Symposium on Logic in Computer Science; July 8–11, 2024; Tallinn,
Estonia††booktitle: 39th Annual ACM/IEEE Symposium on Logic in Computer
Science (LICS ’24), July 8–11, 2024, Tallinn, Estonia††doi:
10.1145/3661814.3662119††isbn: 979-8-4007-0660-8/24/07††ccs: Theory of
computation Logic and verification

##  1\. Introduction

Büchi’s seminal 1962 paper (Büchi, 1990) established the decidability of the
monadic second-order (MSO) theory of the structure
$\langle\mathbb{N};<\rangle$, 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 $\langle\mathbb{N};<\rangle$ retain MSO decidability. In other
words, for which unary predicates $P_{1},\ldots,P_{k}$ is the MSO theory of
$\langle\mathbb{N};<,P_{1},\ldots,P_{k}\rangle$ decidable?111The restricted
focus on _unary_ (or _monadic_) predicates is justified by the fact that most
natural non-unary predicates immediately lead to undecidability (Robinson,
1958). Here by unary predicate we mean a fixed set of non-negative integers
$P\subseteq\mathbb{N}$. Taking, for example, $P$ to be the set of prime
numbers, Büchi and Landweber (Büchi and Landweber, 1969) observed in 1969 that
a proof of decidability of the MSO theory of $\langle\mathbb{N};<,P\rangle$
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 (Bateman et al., 1993).)

The set of prime numbers is, of course, highly intricate. In 1966, Elgot and
Rabin (Elgot and Rabin, 1966) considered a large class of simpler predicates
of ‘arithmetic’ origin, such as, for any fixed $k$, the set
$\mathsf{Pow}_{k}=\\{k^{n}~{}:~{}n\in\mathbb{N}\\}$ of powers of $k$, and the
set $\mathsf{N}_{k}=\\{n^{k}:n~{}\in~{}\mathbb{N}\\}$ of $k$-th powers. For
any such predicate $P$, they systematically established decidability of the
MSO theory of $\langle\mathbb{N};<,P\rangle$ 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 (Carton and Thomas, 2002), Rabinovich
(Rabinovich, 2007), and Rabinovich and Thomas (Rabinovich and Thomas, 2006),
among others. A related key concept is that of _effective almost periodicity_
, introduced in the 1980s by Semënov (Semenov, 1984), and recently brought to
bear in the MSO model checking of linear dynamical systems (Karimov et al.,
2022).

It is notable that whilst Elgot and Rabin establish separately the
decidability of the MSO theories, for example, of
$\langle\mathbb{N};<,\mathsf{Pow}_{2}\rangle$ and
$\langle\mathbb{N};<,\mathsf{Pow}_{3}\rangle$, they remain resolutely silent
on the obvious joint expansion
$\langle\mathbb{N};<,\mathsf{Pow}_{2},\mathsf{Pow}_{3}\rangle$. 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
$\langle\mathbb{N};<,\mathsf{Pow}_{2},\mathsf{Pow}_{3}\rangle$ is indeed
decidable. Although this is new, we should mention that decidability of the
_first-order_ theory of
$\langle\mathbb{N};<,\mathsf{Pow}_{2},\mathsf{Pow}_{3}\rangle$ has been known
for over forty years, an important result of Semënov (Semenov, 1980).

Looking over the last several decades’ worth of research work on monadic
second-order expansions of the structure $\langle\mathbb{N};<\rangle$, 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 $\langle\mathbb{N};<\rangle$
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_ (Berthé et al., 2023). 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
$\langle\mathbb{N};<,\mathsf{Pow}_{2},\mathsf{Pow}_{3}\rangle$, we are only
able to show decidability of the MSO theory of
$\langle\mathbb{N};<,\mathsf{Pow}_{2},\mathsf{Pow}_{3},\mathsf{Pow}_{5}\rangle$
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. (1)

The MSO theory of
$\langle\mathbb{N};<,\mathsf{Pow}_{\rho_{1}},\ldots,\mathsf{Pow}_{\rho_{d}}\rangle$
is decidable assuming Schanuel’s conjecture.

  2. (2)

If $1/\log(\rho_{1}),\ldots,1/\log(\rho_{d})$ are linearly independent over
$\mathbb{Q}$, then the decidability is unconditional.

  3. (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\mathbb{N};<,\mathsf{Pow}_{2},\mathsf{Pow}_{3},\mathsf{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}\colon n\in\mathbb{N}\\}$, and $P_{2}=\\{pb^{nd}\colon
n~{}\in~{}\mathbb{N}\\}$. The decidability of the MSO theory of
$\langle\mathbb{N};<,P_{1},P_{2}\rangle$ is Turing-equivalent to that of the
MSO theory of the base-$b$ expansion of $\eta$.222The 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_ we mean the MSO theory of the structure
$\langle\mathbb{N};<,P_{0},\ldots,P_{b-1}\rangle$, where each $P_{i}$ is the
unary predicate $\\{n\in\mathbb{N}\colon\alpha(n)=i\\}$.

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\mathbb{N};<,\mathsf{Pow}_{b^{d}},\mathsf{N}_{d}\rangle$ is decidable.

For example, we recover from the above the decidability of the MSO theory of
$\langle\mathbb{N};<,\mathsf{Pow}_{4},\mathsf{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\mathbb{N}$, we write $\alpha(n)$ for the
$n$th letter of $\alpha$. Thus $\alpha=\alpha(0)\alpha(1)\cdots$. We define
$\alpha[n,m)\coloneqq\alpha(n)\cdots\alpha(m-1)$, and assuming $\alpha$ is
infinite, $\alpha[n,\infty)\coloneqq\alpha(n)\alpha(n+1)\cdots$. 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_{0}u_{1}\cdots$, where $u_{i}\in\Sigma^{*}$ for all
$i\in\mathbb{N}$. Such a factorisation is uniquely determined by an increasing
sequence $\langle k_{n}\rangle_{n=0}^{\infty}$ over $\mathbb{N}$ such that
$u_{i}=\alpha[k_{i},k_{i+1})$ for all $i$. Finally, consider
$\alpha_{i}\in\Sigma_{i}^{\omega}$ for $1\leq i\leq d$. The _product word_
$\alpha\coloneqq\alpha_{1}\times\cdots\times\alpha_{d}$ is defined by
$\alpha(n)=(\alpha_{1}(n),\ldots,\alpha_{d}(n))\in\Sigma_{1}\times\cdots\times\Sigma_{d}$
for all $n$.

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

  * (a)

_effective_ if for any $n\in\mathbb{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\mathbb{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\mathbb{N}$, $w$
occurs in $\alpha[N,N+R(w))$.

Prominent examples of uniformly recurrent words include the Thue-Morse word
(Allouche and Shallit, 2003, Chap. 1) and all Sturmian words (Lothaire, 2002,
Chap. 2).

A _deterministic finite Muller automaton_ $\mathcal{A}$ over an alphabet
$\Sigma$ is given by a tuple $(Q,q_{\operatorname{init}},\delta,\mathcal{F})$,
where $Q$ is the (finite) set of states, $q_{\operatorname{init}}$ is the
initial state, $\delta\colon Q\times\Sigma\rightarrow 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_{\operatorname{init}},\sigma)$, where $R$ is the (finite) set of states,
$r_{\operatorname{init}}$ is the initial state, and $\sigma\colon
R\times\Sigma\rightarrow R\times\Gamma^{*}$ is the transition function. At
every step, $\mathcal{B}$ reads a letter from the input alphabet $\Sigma$,
transitions to the next state, and outputs a finite word over the output
alphabet $\Gamma$. We define $\sigma_{R}\colon R\times\Sigma\to R$ to be the
function that returns the next state, and $\sigma_{\Gamma^{*}}\colon
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\coloneqq Q\times Q\times 2^{Q}$. A path
$q_{0}q_{1}q_{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_{1}q_{2}\cdots q_{n}$. If $n\geq 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 $\mathsf{jour}(w,q)$, is the journey
made by $q_{0}\cdots q_{|w|}$ where $q_{i+1}=\delta(q_{i},w(i))$ for $1\leq
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
$\mathsf{jour}$ to take inputs from $M\times Q$: For equivalence class $m=[w]$
and state $q$, we define $\mathsf{jour}(m,q)=\mathsf{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_{0}u_{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_{\operatorname{init}}$,
$\mathsf{jour}(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};<\rangle$. For a
general perspective on MSO, see (Blumensath, 2023).

Let $\mathbb{S}\coloneqq\langle\mathbb{N};<,P_{1},\ldots,P_{m}\rangle$ be a
structure where each $P_{i}\subseteq\mathbb{N}$ is a unary predicate. We
associate a language $\mathcal{L}_{\mathbb{S}}$ of terms and formulas with
$\mathbb{S}$ as follows. The terms of $\mathcal{L}_{\mathbb{S}}$ are the
countably many constant symbols $\\{0,1,2,\ldots\\}$, 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}_{\mathbb{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 $\mathbb{S}$ is the set of all sentences belonging
to $\mathcal{L}_{\mathbb{S}}$ that are true in $\mathbb{S}$. The MSO theory of
$\mathbb{S}$ is _decidable_ if there exists an algorithm that, given a
sentence $\varphi\in\mathcal{L}_{\mathbb{S}}$, decides if $\varphi$ belongs to
the MSO theory of $\mathbb{S}$.

As an example, consider $\mathbb{S}=\langle\mathbb{N};<,P\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\>\>\>\land\>\>\>\forall z.\,x<z\Rightarrow y\leq z.$

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

$\displaystyle\varphi(X)$ $\displaystyle\coloneqq 1\in X\>\land\>0,2\notin
X\>\land\>\forall x.\>x\in X\Leftrightarrow s(s(s(x)))\in X,$
$\displaystyle\psi$ $\displaystyle\coloneqq\exists
X\colon\varphi(X)\>\land\>\forall y.\,\exists z>y\colon z\in X\>\land\>P(z).$

The formula $\varphi$ defines the subset ${\\{n\colon 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 $\mathbb{S}$ above is decidable.

The _Acceptance Problem_ for an infinite word $\alpha$, denoted
$\mathsf{Acc}_{\alpha}$, is to determine, given a deterministic Muller
automaton $\mathcal{A}$, whether $\mathcal{A}$ accepts $\alpha$. Let
$P_{1},\ldots,P_{d}\subset\mathbb{N}$ be predicates and
$\Sigma=\\{0,1\\}^{d}$.

###### Definition 2.2.

The _characteristic word_ of $(P_{1},\ldots,P_{d})$, written
$\alpha\coloneqq\operatorname{Char}(P_{1},\ldots,P_{d})\in\Sigma^{\omega}$, is
defined by $\alpha(n)=(b_{n,1},\ldots,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};<\rangle$.

###### Theorem 2.3 ((Thomas, 1997, Thms. 5.4 and 5.9)).

The decision problem of the MSO theory of the structure
$\langle\mathbb{N};<,P_{1},\ldots,P_{d}\rangle$ is Turing-equivalent to
$\mathsf{Acc}_{\alpha}$, where $\alpha$ is the characteristic word of
$(P_{1},\ldots,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 (Cohen, 2013, Sec. 4.2).

By a _multiplicative relation_ of
$(\lambda_{1},\ldots,\lambda_{d})\in\mathbb{C}^{d}$ we mean
$\mathbf{k}=(k_{1},\ldots,k_{d})\in\mathbb{Z}^{d}$ such that
$\lambda_{1}^{k_{1}}\cdots\lambda_{d}^{k_{d}}=1$. We write

$G\coloneqq G_{M}(\lambda_{1},\ldots,\lambda_{d})$

for the set of all multiplicative relations of
$(\lambda_{1},\ldots,\lambda_{d})$, which is a free abelian group under
addition. If $G=\\{(0,\ldots,0)\\}$, we say that
$X\coloneqq\\{\lambda_{1},\ldots,\lambda_{d}\\}$ is _multiplicatively
independent_. The _rank_ of $G$ is the cardinality of a largest
multiplicatively independent subset of $X$. If $\operatorname{rank}(G)=m$,
then $G$ has a _basis_
$B=\\{\mathbf{v}_{1},\ldots,\mathbf{v}_{m}\\}\subseteq\mathbb{Z}^{d}$ that is
linearly independent over $\mathbb{Q}$ with the property that every
$\mathbf{z}\in G$ can be written as an integer linear combination of
$\mathbf{v}_{1},\ldots,\mathbf{v}_{m}$. If $\lambda_{1},\ldots,\lambda_{d}$
are algebraic, we can compute a basis of $G$ using a deep result of Masser
(Masser, 1988).

###### Theorem 2.4 ((Cai et al., 2000)).

Given $\lambda_{1},\dots,\lambda_{d}\in\overline{\mathbb{Q}}$, one can compute
a basis for $G_{M}(\lambda_{1},\ldots,\lambda_{d})$.

Finally, for $\lambda_{1},\ldots,\lambda_{d}$ as above, we define the _group
of additive relations_ as

$G_{A}(\lambda_{1},\ldots,\lambda_{d})\coloneqq\\{(k_{1},\ldots,k_{d})\in\mathbb{Z}^{d}\colon
k_{1}\lambda_{1}+\cdots+k_{d}\lambda_{d}\in\mathbb{Z}\\}.$

Observe that
$G_{A}(\lambda_{1},\ldots,\lambda_{d})=G_{M}(e^{i2\pi\lambda_{1}},\ldots,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

(1) $u_{n+d}=c_{1}u_{n+d-1}+\cdots+c_{d}u_{n}$

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},\ldots,q_{m}\in\overline{\mathbb{Q}}[x]$ such that

(2) $u_{n}=q_{1}(n)\lambda_{1}^{n}+\cdots+q_{m}(n)\lambda_{m}^{n}$

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}|\geq|\lambda_{j}|$ for
all $1\leq j\leq m$. We refer the reader to the book (Everest et al., 2003)
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}|\leq rR^{n}$ for all $n\geq 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\geq 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},\ldots,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 (Lang, 1966).

###### 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}\coloneqq\langle{\mathbb{R};<,+,-,\cdot,\exp(\cdot),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 (Macintyre and Wilkie, 1996), 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},\ldots,\lambda_{d}\in\mathbb{R}_{>1}\cap\overline{\mathbb{Q}}$.
Assuming Schanuel’s conjecture, a basis for
$G_{A}(1/\log(\lambda_{1}),\ldots,1/\log(\lambda_{d}))$ can be computed.

The proof is in App. A.1.

###  2.6. Baker’s Theorem

By a _$\mathbb{Q}$ -affine form_ we mean
$h(x_{1},\ldots,x_{d})=a_{0}+\sum_{i=1}^{d}a_{i}x_{i}$, where
$a_{i}\in\mathbb{Q}$ for all $0\leq i\leq d$. We recall Baker’s celebrated
theorem on $\mathbb{Q}$-affine forms in logarithms.

###### Theorem 2.10 (Thm. 1.6 in (Waldschmidt, 2000)).

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\geq 2$,
$\lambda_{1},\dots,\lambda_{d}\in\mathbb{R}_{>1}\cap\overline{\mathbb{Q}}$ be
pairwise multiplicatively independent, and suppose

$\operatorname{rank}(G_{M}(\lambda_{1},\ldots,\lambda_{d}))\geq 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 App. A.2.

###### Lemma 2.12.

Given $\lambda_{1},\ldots,\lambda_{d}\in\overline{\mathbb{Q}}$ and
$a_{0},\ldots,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}^{e}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. ∎

Multiple effective versions of Baker’s theorem exist, which give a lower bound
on the magnitude of $\Lambda\coloneqq h(\log(\rho_{1}),\ldots,\log(\rho_{d}))$
for a $\mathbb{Q}$-affine form $h$, assuming $\Lambda\neq 0$. We use Matveev’s
version (Matveev, 2000) to prove the following in 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}\geq N$,

(3) $|c_{1}\rho_{1}^{n_{1}}-c_{2}\rho_{2}^{n_{2}}|\leq
b_{1}R_{1}^{n_{1}}+b_{2}R_{2}^{n_{2}}$

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\\}\coloneqq x-\lfloor
x\rfloor$ be the fractional part of $x$. A word $\alpha\in\Sigma^{\omega}$ is
_toric_ if there exist $d>0$,
$\mathbf{s}=(s_{1},\ldots,s_{d})\in\mathbb{T}^{d}$, a translation
$g\colon\mathbb{T}^{d}\to\mathbb{T}^{d}$ given by

(4)
$(x_{1},\ldots,x_{d})\to(\\{x_{1}+\delta_{1}\\},\ldots,\\{x_{d}+\delta_{d}\\})$

for $\delta_{1},\ldots,\delta_{d}\in\mathbb{T}$, and a collection
$\mathcal{S}=\\{S_{b}\colon b\in\Sigma\\}$ of subsets of $\mathbb{T}^{d}$ such
that for all $n\in\mathbb{N}$ and $b\in\Sigma$,

(5) $\alpha(n)=b\Leftrightarrow g^{(n)}(\mathbf{s})\in S_{b}.$

Here $g^{(n)}(\mathbf{s})$ denotes the result of iteratively applying $g$ to
$\mathbf{s}$ a total of $n$ times. That is, $\alpha$ is the _coding_ (with
respect to $\mathcal{S}$) of the trajectory of the discrete-time dynamical
system on $\mathbb{T}^{d}$ defined by $(g,\mathbf{s})$. Observe that
$g^{(n)}(\mathbf{s})=(\\{s_{1}+n\delta_{1}\\},\ldots,\\{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},\ldots,s_{d},\delta_{d}\in\mathbb{T}$
as above and a collection $\\{S_{b}\colon b\in\Sigma\\}$ of _open_ subsets of
$\mathbb{T}^{d}$ such that (5) holds for all $n\in\mathbb{N}$ and
$b\in\Sigma$. See (Berthé et al., 2023) for a discussion of various subclasses
of toric words.

Let $\mathbf{s},\bm{\delta}\in\mathbb{T}^{d}$, $G=G_{A}({\bm{\delta}})$, and
$g\colon\mathbb{T}^{d}\to\mathbb{T}^{d}$ be as in (4). Define
$\mathbb{T}_{\bm{\delta}}\coloneqq\\{\mathbf{z}\in\mathbb{T}^{d}\colon
G_{A}(\mathbf{z})\subseteq G_{A}({\bm{\delta}})\\}\subseteq\mathbb{T}^{d}$.
The following is a rephrasing of Kronecker’s theorem in Diophantine
approximation (Gonek and Montgomery, 2016). In the language of dynamical
systems, it states that the dynamical system (on $\mathbb{T}_{\bm{\delta}}$)
obtained by restricting $g$ to $\mathbb{T}_{\bm{\delta}}$ is _minimal_.

###### Theorem 2.14.

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

Let $\mathbf{v}_{1},\ldots,\mathbf{v}_{m}\in\mathbb{Z}^{d}$ be a basis of
$G_{A}({\bm{\delta}})$, where $m<d$. Write
$\mathbf{v}_{i}=(v_{i,1},\ldots,v_{i,d})$ for $1\leq i\leq m$ and let
$C=\max_{i}{\|\mathbf{v}_{i}\|}_{\infty}$, noting that
$|\mathbf{v}_{i}\cdot\mathbf{z}|\leq Cd$ for all
$\mathbf{z}\in\mathbb{T}^{d}$. We have that $z\in\mathbb{T}_{\bm{\delta}}$ if
and only if $\mathbf{v}_{i}\cdot\mathbf{z}\in\mathbb{Z}$ for all $i$, which is
equivalent to

$\bigwedge_{i=1}^{d}\>\bigvee_{|k|\leq Cd}\mathbf{v}_{i}\cdot\mathbf{z}=k.$

That is, $\mathbb{T}_{\bm{\delta}}$, viewed as a subset of $\mathbb{R}^{d}$,
is an intersection of $\mathbb{T}^{d}$ with a union of affine subspaces of
$\mathbb{R}^{d}$ with integer parameters. We can now define
$\mathbb{T}_{{\bm{\delta}},\mathbf{s}}\coloneqq\\{(\\{s_{1}+z_{1}\\},\ldots,\\{s_{d}+z_{d}\\})\mid(z_{1},\ldots,z_{d})\in\mathbb{T}_{\bm{\delta}}\\}$.
Applying Thm. 2.14, we obtain the following.

###### Theorem 2.15.

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

To prove the first main result of this paper, we will need to show that
$\mathsf{Acc}_{\alpha}$ is decidable for certain $\alpha\in\mathcal{T}_{O}$.
The following well-known fact will play an important role in this; See (Berthé
et al., 2023) for a proof.

###### Theorem 2.16.

Every $\alpha\in\mathcal{T}_{O}$ is uniformly recurrent.

###  2.8. Fourier-Motzkin Elimination

Let $\Phi(x_{1},\ldots,x_{m})$ be a Boolean combination of atomic formulas of
the form $h(x_{1},\ldots,x_{m})\sim 0$, where $h$ is a $\mathbb{Q}$-affine
form and $\sim$ is a (strict or non-strict) inequality symbol. Let $1\leq
l\leq m$, and consider the formula $\exists
x_{1},\ldots,x_{l}\in\mathbb{R}\colon\Phi(x_{1},\ldots,x_{m})$. Using the
Fourier-Motzkin Elimination (Dantzig et al., 1973), we can compute a formula
$\Psi(x_{l+1},\ldots,x_{m})=\bigvee_{j\in J}\bigwedge_{k\in
K}h_{j,k}(x_{l+1},\ldots,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},\ldots,z_{m}\in\mathbb{R}$, the sentence

$\exists
x_{1},\ldots,x_{l}\in\mathbb{R}\colon\Phi(x_{1},\ldots,x_{l},z_{l+1},\ldots,z_{m})$

holds if and only if $\Psi(x_{l+1},\ldots,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.
$\mathsf{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=\operatorname{Char}({P_{1},\dots,P_{d}})\in\big{(}\\{0,1\\}^{d}\big{)}^{\omega}$.

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

> For $\alpha=\operatorname{Char}({P_{1},\dots,P_{d}})$, establish the
> decidability of the automaton acceptance problem $\mathsf{Acc}_{\alpha}$.

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

(6)
$\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$

where each letter between the blocks of $\mathbf{0}$’s is not $\mathbf{0}$.
Characteristic words defined by a single predicate (e.g. $\mathsf{Pow}_{2}$,
the powers of $2$) are much better studied than those defined by multiple
predicates (e.g. $\mathsf{Pow}_{2},\mathsf{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=\operatorname{Char}({P_{1},\dots,P_{d}})\in\big{(}\\{0,1\\}^{d}\big{)}^{\omega}$,
their order word

$\alpha^{\prime}=\operatorname{Ord}({P_{1},\dots,P_{d}})\in\big{(}\\{0,1\\}^{d}\big{)}^{\omega}$

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

In compressing the characteristic word $\alpha$ to the order word
$\alpha^{\prime}$, one only retains partial information, i.e. a particular
aspect of the interaction between predicates. Not surprisingly (by Lem. 4.5),
$\mathsf{Acc}_{\alpha^{\prime}}$ always reduces to $\mathsf{Acc}_{\alpha}$.
Remarkably however, under certain circumstances, the interaction captured by
order words is the essence of the decision problem $\mathsf{Acc}_{\alpha}$:
For certain well-behaved tuples of predicates, given an automaton
$\mathcal{A}$, one can use the order word $\alpha^{\prime}$ to recover
sufficient information about the interspersed $\mathbf{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^{\prime}(0)\cdots\mathbf{0}^{k_{n}}\alpha^{\prime}(n)\cdots.$

An automaton $\mathcal{A}$ is crucially finite, and consequently one can
compute $K,p>0$ such that for all $n\geq 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^{\prime}$ using a transducer, then
$\mathsf{Acc}_{\alpha}$ reduces to $\mathsf{Acc}_{\alpha^{\prime}}$.

In Sec. 4, we develop the automata-theoretic machinery required to prove that
$\mathsf{Acc}_{\alpha}$ (the acceptance problem of the characteristic word)
reduces to $\mathsf{Acc}_{\alpha^{\prime}}$ (the acceptance problem of 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 $\mathsf{Acc}_{\alpha^{\prime}}$
for the order word $\alpha^{\prime}$ defined by tuples of LRS with one simple
dominant root. We do so by showing that $\alpha^{\prime}$ 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 $\mathsf{Acc}_{\beta}$ is decidable (Thm. 4.2). Through number-
theoretic arguments, we establish when the order word $\alpha^{\prime}$ is
indeed effectively almost-periodic.

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

  1. (1)

Identify sufficient conditions to reduce $\mathsf{Acc}_{\alpha}$ (the
acceptance problem of the characteristic word) to
$\mathsf{Acc}_{\alpha^{\prime}}$ (the acceptance problem of of the order
word). (Sec. 4)

  2. (2)

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

  3. (3)

Generate $\alpha^{\prime}$ as the trace of a toric dynamical system, and
exploit the underlying model to decide $\mathsf{Acc}_{\alpha^{\prime}}$. (Sec.
5.2)

In Sec. 6, we follow a similar approach to analyze
$\operatorname{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_ (Lothaire, 2002, 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 $\alpha$ is effective if its letters
can be effectively computed. Semënov considered the class of (effectively)
almost-periodic words in (Semenov, 1984).

###### Definition 4.1.

A word $\alpha\in\Sigma^{\omega}$ 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 $\alpha[R(u),\infty)$, or

  * (b)

occurs in every factor of $\alpha$ of length $R(u)$.

If, moreover, $\alpha$ is effective and a _return time_ $R(u)$ as above is
computable given $u$, then $\alpha$ is said to be _effectively almost-
periodic_.

###### Theorem 4.2 (Theorem 3 in (Muchnik et al., 2003)).

If $\alpha\in\Sigma^{\omega}$ is effectively almost-periodic, then
$\mathsf{Acc}_{\alpha}$ is decidable.

Carton and Thomas (Carton and Thomas, 2002) introduced the class of
profinitely ultimately periodic words as a framework to generalise the
thematic _contraction methods_ of Elgot and Rabin (Elgot and Rabin, 1966).

###### Definition 4.3.

Let $\Sigma$ 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
$\Sigma^{*}$ into a finite monoid $M$, we can compute $N$ and $p$ such that
for all $n\geq N$, $h(u_{n})=h(u_{n+p})$.

  * (b)

An infinite word $\alpha$ is called _effectively profinitely ultimately
periodic_ if it can be effectively factorised as an infinite concatenation
$u_{0}u_{1}\cdots$ of finite non-empty words forming an effectively
profinitely ultimately periodic sequence.

###### Theorem 4.4.

Let $\alpha\in\Sigma^{*}$. The problem $\mathsf{Acc}_{\alpha}$ is decidable if
and only if $\alpha$ is effectively profinitely ultimately periodic.

The if direction is due to Carton and Thomas (Carton and Thomas, 2002), and
the converse is due to Rabinovich (Rabinovich, 2007). 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
($\alpha\in\\{0,1\\}^{\omega}$) are effectively profinitely ultimately
periodic is identified by (Carton and Thomas, 2002, Thm. 5.2). This class
includes fixed base powers $\mathsf{Pow}_{k}=\\{k^{n}:n\in\mathbb{N}\\}$ as
well as $k$-th powers $\mathsf{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 $\alpha\in\Sigma^{\omega}$, $\mathcal{B}$ be a deterministic finite
transducer with input alphabet $\Sigma$ and output alphabet $\Gamma$, and
$\beta=\mathcal{B}(\alpha)\in\Gamma^{\omega}$. The problem
$\mathsf{Acc}_{\beta}$ reduces to $\mathsf{Acc}_{\alpha}$.

###### Proof.

Given an instance $\mathcal{A}=(Q,q_{\operatorname{init}},\delta,\mathcal{F})$
of $\mathsf{Acc}_{\beta}$, we shall construct $\mathcal{A}^{\prime}$ whose run
on $\alpha$ simulates the run of $\mathcal{A}$ on $\beta$. Write
$\mathcal{B}=(R,r_{\operatorname{init}},\sigma)$. The automaton
$\mathcal{A}^{\prime}$ must simulate what $\mathcal{B}$ would do upon reading
$\alpha$, and furthermore, what $\mathcal{A}$ would do upon reading each
output block of $\mathcal{B}(\alpha)$.

In order to do so, we express $\beta=u_{0}u_{1}\cdots$ such that $\mathcal{B}$
outputs $u_{n}$ upon reading the $n$th letter of $\alpha$ and correspondingly
decompose the run of $\mathcal{A}$ on $\beta$ as the concatenation of journeys
$(q_{\operatorname{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 $\mathcal{A}^{\prime}$ as

$\displaystyle Q^{\prime}$ $\displaystyle=Q\times 2^{Q}\times R;$
$\displaystyle q_{\operatorname{init}}^{\prime}$
$\displaystyle=(q_{\operatorname{init}},\emptyset,r_{\operatorname{init}});$
$\displaystyle\delta^{\prime}((q_{\mathsf{now}},V_{\mathsf{last}},r),a)$
$\displaystyle=(q_{\mathsf{next}},V,\sigma_{R}(r,a))$

such that the invariant
$\mathsf{jour}(\sigma_{\Gamma^{*}}(r,a),q_{\mathsf{now}})=(q_{\mathsf{now}},q_{\mathsf{next}},V)$
holds. By construction, the run
$(q_{\operatorname{init}},\emptyset,r_{\operatorname{init}})(q_{1},V_{0},r_{1})(q_{2},V_{1},r_{2})\cdots$
of $\mathcal{A}^{\prime}$ on $\alpha$ corresponds to the above concatenation
of journeys.

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

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

and the reduction is hence complete. ∎

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

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

###### Theorem 4.6.

Let $\alpha\in\Sigma^{\omega}$ and $\beta\in\Gamma^{\omega}$ be such that for
any morphism $h$ from $\Gamma^{*}$ into a finite monoid $M$, we can construct
a deterministic finite transducer $\mathcal{B}$ (with input alphabet $\Sigma$
and output alphabet $M$) and compute a factorisation $u_{0}u_{1}\cdots$ of
$\beta$ such that $\gamma=\mathcal{B}(\alpha)=\gamma(0)\gamma(1)\cdots\in
M^{\omega}$ satisfies $h(u_{n})=\gamma(n)$ for all $n\in\mathbb{N}$. Then
$\mathsf{Acc}_{\beta}$ reduces to $\mathsf{Acc}_{\alpha}$.

###### Proof.

Given a deterministic finite automaton $\mathcal{A}$ as an instance of
$\mathsf{Acc}_{\beta}$, we will use the natural morphism $h$ into the finite
quotient monoid $M=\Gamma^{*}/\sim_{\mathcal{A}}$ to reduce it to an instance
of $\mathsf{Acc}_{\alpha}$.

For $h,M$ chosen thus, consider the transducer $\mathcal{B}$, factorisation
$u_{0}u_{1}\cdots$ of $\beta$, and word $\gamma=\mathcal{B}(\alpha)\in
M^{\omega}$ 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$,
$\mathsf{jour}(u_{n},q)=\mathsf{jour}(\gamma(n),q)\in J$.

It is straightforward to construct a transducer $\mathcal{B}^{\prime}$ such
that $\mathcal{B}^{\prime}(\gamma)=\zeta=j_{0}j_{1}\cdots\in J^{\omega}$ has
the following properties:

  1. (1)

$j_{0}=\mathsf{jour}(\gamma(0),q_{\operatorname{init}})=\mathsf{jour}(u_{0},q_{\operatorname{init}})=(q_{\operatorname{init}},q_{1},V_{0})$;

  2. (2)

$j_{n}=\mathsf{jour}(\gamma(n),q_{n})=\mathsf{jour}(u_{n},q_{n})=(q_{n},q_{n+1},V_{n})$
for $n~{}\geq~{}1$.

We will now show how to decide $\mathsf{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
$\mathsf{Acc}_{\zeta}$. By Lem. 4.5, $\mathsf{Acc}_{\zeta}$ reduces to
$\mathsf{Acc}_{\gamma}$, which itself reduces to $\mathsf{Acc}_{\alpha}$. ∎

###### 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\colon\Sigma_{0}^{*}\to M$, we can construct a
transducer $\mathcal{B}$ with the following property. Its output
$\gamma\coloneqq\mathcal{B}(\alpha)\in M^{\omega}$ upon reading $\alpha$
satisfies $h(0^{k_{n}}\alpha(n))=\gamma(n)$ for all $n$. Then
$\mathsf{Acc}_{\beta}$ reduces to $\mathsf{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
$\mathsf{Acc}_{\beta}$ reduces to $\mathsf{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\coloneqq\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\geq 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$. ∎

###  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^{\prime}$ 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}\rightarrow\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
$\mathsf{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}\rightarrow\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\leq i\leq d$, and
$\alpha\in\Sigma^{\omega}$ be the characteristic word of
$(P_{1},\dots,P_{d})$. Then $\mathsf{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}\supseteq\dots\supseteq 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
$\mathsf{Acc}_{\alpha^{(i)}}$ reduces to $\mathsf{Acc}_{\alpha^{(i+1)}}$.
However, $\alpha^{(d)}=b_{d}^{\omega}$ and therefore
$\mathsf{Acc}_{\alpha^{(d)}}$ is clearly decidable. We conclude that
$\mathsf{Acc}_{\alpha}$ is decidable. ∎

###### Proof of Cor. 1.3.

Recall, by (Carton and Thomas, 2002, Thm. 5.2),
$\mathsf{N}_{d},\mathsf{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, $\mathsf{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};<,\mathsf{N}_{d},\mathsf{Pow}_{b^{d}}}\rangle$ is
decidable. ∎

###  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^{\prime}$. Note that
$\mathsf{Acc}_{\alpha^{\prime}}$ trivially reduces to $\mathsf{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}\rightarrow\mathbb{N}$ is said to
be _procyclic_ 333This definition is weaker than the notion of (effectively)
profinitely ultimately periodic sequences defined by Carton and Thomas (Carton
and Thomas, 2002). 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. 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\geq 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}\rightarrow\mathbb{N}$ is said to
be _effectively sparse_ if for any $K\in\mathbb{N}$, the inequality
$f(n+1)-f(n)\leq 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}\rightarrow\mathbb{N}$
are said to be _pairwise effectively sparse_ if for any $K\in\mathbb{N}$, the
inequality $|f_{1}(n)-f_{2}(m)|\leq 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_.

We remark that similar notions of effective sparsity have been considered in
literature as early as (Semenov, 1980).

###### 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^{\prime}$. Suppose

  1. (1)

$P_{1},\dots,P_{d}$ are each (a) procyclic and (b) effectively sparse;

  2. (2)

each distinct $(P_{i},P_{j})$ is pairwise effectively sparse.

Then, $\mathsf{Acc}_{\alpha}$ reduces to $\mathsf{Acc}_{\alpha^{\prime}}$.

###### Proof.

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

$\alpha=\mathbf{0}^{k_{0}}\alpha^{\prime}(0)\mathbf{0}^{k_{1}}\alpha^{\prime}(1)\cdots\mathbf{0}^{k_{n}}\alpha^{\prime}(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^{\prime})=\gamma\in M^{\omega}$, where
$\gamma(n)=h(\mathbf{0}^{k_{n}}\alpha^{\prime}(n))=h(\mathbf{0}^{k_{n}})h(\alpha^{\prime}(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\geq 1$ such that $K$ is a multiple of $m$,
and for all $j\geq 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\geq N$,
$k_{n}\geq 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^{\prime}(0)\cdots\alpha^{\prime}(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,\dots$, 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^{\prime}(n-1)$ was,
modulo $m$.

Upon reading the next letter of $\alpha^{\prime}(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\big{(}\mathbf{0}^{k_{n}}\alpha^{\prime}(n)\big{)}=h\big{(}\mathbf{0}^{k_{n}}\big{)}h(\alpha^{\prime}(n))=h\big{(}\mathbf{0}^{K+r_{n}}\big{)}h(\alpha^{\prime}(n))$

and we are done. ∎

###  4.5. Normal Words

Recall that a word $\alpha\in\Sigma^{\omega}$ is _weakly normal_ if every
$u\in~{}\Sigma^{*}$ appears infinitely in $\alpha$.444In 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 (Queffélec, 2006).  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\cdots$. We have the following result about such words.

###### Theorem 4.16.

If $\alpha$ is weakly normal, then $\mathsf{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 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^{(i)}_{n}=c_{i}\rho_{i}^{n}+\sum_{j=1}^{k_{i}}p_{i,j}(n)\rho_{i,j}^{n},$

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

  * (1)

$c_{i},\rho_{i},\rho_{i,j}\in\overline{\mathbb{Q}}$ and
$p_{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^{(i)}_{n}\rangle_{n=0}^{\infty}$, the MSO theory of
$\langle{\mathbb{N};<,P_{1},\ldots,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}),\ldots,1/\log(\rho_{d})$ are linearly independent over
$\mathbb{Q}$;

  * (b)

If $\operatorname{rank}(G_{M}(\rho_{1},\ldots,\rho_{d}))\geq d-2$, and
$\rho_{1},\ldots,\rho_{d}$ are pairwise multiplicatively independent.

We remark that the condition
$\operatorname{rank}(G_{M}(\rho_{1},\ldots,\rho_{d}))\geq 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}),\ldots,\log(\rho_{d})$. Moreover, (b) implies (a) by Lem.
2.11. Finally, condition (3) is equivalent to the following: For every $1\leq
i,j\leq 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},\ldots,\rho_{d}$ are not pairwise multiplicatively independent. Then
$1/\log(\rho_{1}),\ldots,1/\log(\rho_{d})$ are not linearly independent over
$\mathbb{Q}$. We can compute pairwise multiplicatively independent
$\lambda_{1},\ldots,\lambda_{m}\in\mathbb{N}$ such that for all $1\leq i\leq
d$, $\rho_{i}=\lambda_{\sigma(i)}^{\mu(i)}$ for some
$\sigma(i),\mu(i)\in\mathbb{N}$. Consider
$\langle\mathbb{N};<,\mathsf{Pow}_{\lambda_{1}},\ldots,\mathsf{Pow}_{\lambda_{m}}\rangle$.
The original characteristic word can be recovered by noting that precisely
every $\mu(i)$-th occurrence of $\mathsf{Pow}_{\lambda_{\sigma(i)}}$ is an
occurrence of $\mathsf{Pow}_{\rho_{i}}$. This can be implemented with a simple
transduction; hence by Lem. 4.5, the MSO theory of
$\langle\mathbb{N};<,\mathsf{Pow}_{\rho_{1}},\dots,\mathsf{Pow}_{\rho_{d}}\rangle$
reduces to that of
$\langle\mathbb{N};<,\mathsf{Pow}_{\lambda_{1}},\ldots,\mathsf{Pow}_{\lambda_{m}}\rangle$.
It remains to observe that if every triple of $\rho_{1},\ldots,\rho_{d}$ is
multiplicatively dependent, then so is every triple of
$\lambda_{1},\ldots,\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^{(i)}_{n}\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},\ldots,P_{d})$, and
by $\alpha^{\prime}$ the order word of $(P_{1},\ldots,P_{d})$. We will need
order words obtained from sequences that do not necessarily take exclusively
integer values.

###### Definition 5.2.

Let $\langle v^{(1)}_{n}\rangle_{n=0}^{\infty},\ldots,\langle
v^{(d)}_{n}\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^{(i)}_{n}\colon n\in\mathbb{N}\\}$. We define the word

$\gamma\coloneqq\operatorname{Ord}(\langle
v^{(1)}_{n}\rangle_{n=0}^{\infty},\ldots,\langle
v^{(d)}_{n}\rangle_{n=0}^{\infty})\in\\{1,\ldots,d\\}^{\omega}$

by

$\gamma(n)=i\Leftrightarrow\exists z\in\langle
v^{(i)}_{n}\rangle_{n=0}^{\infty}\colon\,|\\{y\in Z:y<z\\}|=n.$

We now prove the following.

###### Theorem 5.3.

Let $\alpha,\alpha^{\prime}$ be as above. $\mathsf{Acc}_{\alpha}$ reduces to
$\mathsf{Acc}_{\alpha^{\prime}}$. Furthermore, we can construct positive real
algebraic $r_{1},\ldots,r_{d}$ such that $\mathsf{Acc}_{\alpha^{\prime}}$
reduces to $\mathsf{Acc}_{\xi}$, where $\xi=\operatorname{Ord}(\langle
r_{1}\rho_{1}^{n}\rangle_{n=0}^{\infty},\ldots,\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 $\mathsf{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^{(1)}_{n}\rangle_{n=0}^{\infty},\ldots,\langle
u^{(d)}_{n}\rangle_{n=0}^{\infty}$ be as above. We can compute
$N,m_{1},\ldots,m_{d}\in\mathbb{N}$ with the following properties.

  1. (a)

For all $1\leq i\leq d$, $\langle u^{(i)}_{m_{i}+n}\rangle_{n=0}^{\infty}$ is
strictly increasing. Moreover, for every $K\in\mathbb{N}$ and $1\leq i\leq d$,
there exists effectively computable $L_{i}$ such that for all $n\geq L_{i}$,
$u^{(i)}_{n+1}-u^{(i)}_{n}>K$.

  2. (b)

For all $1\leq i\leq d$ and $n\in\mathbb{N}$,

$u^{(i)}_{n}\geq N\Leftrightarrow n\geq m_{i}.$

  3. (c)

$u^{(1)}_{m_{1}}=N$.

  4. (d)

For all $1\leq i,j\leq d$, $n_{i}\geq m_{i}$ and $n_{j}\geq m_{j}$, we have
that $c_{i}\rho_{i}^{n_{i}}\neq c_{j}\rho_{j}^{n_{j}}$ and
$u^{(i)}_{n_{i}}\neq u^{(j)}_{n_{j}}$.

  5. (e)

For $1\leq i,j\leq d$, $n_{i}\geq m_{i}$ and $n_{j}\geq m_{j}$,

$c_{i}\rho_{i}^{n_{i}}>c_{j}\rho_{j}^{n_{j}}\Rightarrow
u^{(i)}_{n_{i}}>u^{(j)}_{n_{j}}.$

###### Proof.

Let $1\leq i,j\leq d$ with $i\neq 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}}\rho_{i}^{-n_{i}}$. Using Thm. 2.4, we can
compute a basis for $G\coloneqq 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}}\neq c_{j}\rho_{j}^{n_{j}}$ for every
$n_{i},n_{j}\geq k_{i,j}$.

Next, for all $1\leq i\leq d$ apply Lem. 2.5 to compute $b_{i}$, $R_{i}>0$
such that $|u^{(i)}_{n}-c_{i}\rho_{i}^{n}|<b_{i}R_{i}^{n}$ for all $n\geq 0$.
Then,

$\displaystyle u^{(i)}_{n_{i}}-u^{(j)}_{n_{j}}$
$\displaystyle=c_{i}\rho_{i}^{n}-c_{j}\rho_{j}^{n}+u^{(i)}_{n_{i}}-c_{i}\rho_{i}^{n}-u^{(j)}_{n_{j}}+c_{j}\rho_{j}^{n}$
$\displaystyle>c_{i}\rho_{i}^{n}-c_{j}\rho_{j}^{n}-b_{i}R_{i}^{n}-b_{j}R_{j}^{n}.$

Using Thm. 2.13, for each pair $1\leq i<j\leq d$ we compute $k^{\prime}_{i,j}$
such that for all $n_{i},n_{j}\geq k^{\prime}_{i,j}$,
$|c_{i}\rho_{i}^{n}-c_{j}\rho_{j}^{n}|>b_{i}R_{i}^{n}+b_{j}R_{j}^{n}$ and
$u^{(i)}_{n_{i}}-u^{(j)}_{n_{j}}$, $c_{i}\rho_{i}^{n}-c_{j}\rho_{j}^{n}$ have
the same sign.

Now suppose $n_{i},n_{j}\geq k_{i,j},k_{i,j}^{\prime}$. By the arguments
above, $c_{i}\rho_{i}^{n_{i}}\neq c_{j}\rho_{j}^{n_{j}}$ and hence
$u^{(i)}_{n_{i}}\neq u^{(j)}_{n_{j}}$.

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

$\displaystyle u^{(i)}_{n+1}-u^{(i)}_{n}$
$\displaystyle<c_{i}\rho_{i}^{n+1}-c_{i}\rho_{i}^{n+1}-b_{i}R_{i}^{n+1}-b_{i}R_{i}^{n}$
$\displaystyle=c_{i}(\rho_{i}-1)\rho_{i}^{n}-b_{i}(R_{i}+1)R_{i}^{n}.$

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\geq k_{i}$.

Thus when $m_{i}\geq k_{i},k_{i,j},k_{i,j}^{\prime}$ for all $i,j$, items (a),
(d) and (e) are satisfied. Let $m_{i}^{\prime}$ for $1\leq i\leq d$ be such
that $\geq k_{i},k_{i,j},k_{i,j}^{\prime}$ for all $i,j$. Choose
$N^{\prime}\geq 0$ such that $N^{\prime}\geq u^{(i)}_{m^{\prime}_{i}}$ for all
$1\leq i\leq d$. Let $m_{1}$ be the smallest number such that
$u^{(1)}_{m_{1}}\geq N^{\prime}$ and $N=u^{(1)}_{m_{1}}$. Finally, for $1\leq
i\leq d$, let $m_{i}$ be the smallest number such that $u^{(i)}_{m_{i}}\geq
N$. Then (b) and (c) are also satisfied. ∎

###### 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\leq i\leq d$, and $\xi=\operatorname{Ord}(\langle
r_{1}\rho_{1}^{n}\rangle_{n=0}^{\infty},\ldots,\langle
r_{d}\rho_{d}^{n}\rangle_{n=0}^{\infty})\in\\{1,\ldots,d\\}^{\omega}$. By
(c-e), the word $\xi$, up to a renaming of variables, is equal to a suffix of
$\alpha^{\prime}$ that can be effectively determined. We can now finalise the
proof.

  1. (1)

Each $P_{i}$ is procyclic. To see this, let $f(n)$ be the $n$th largest
element of $P_{i}$. We have to show that $\langle f(n)\bmod
m\rangle_{n=0}^{\infty}$ is effectively eventually periodic for every
$m\in\mathbb{N}$. By Lem. 5.4 (a), the sequences $\langle
u^{(i)}_{n}\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. (2)

By Lem. 5.4 (a), each $P_{i}$ is effectively sparse.

  3. (3)

Finally, we prove that $P_{1},\ldots,P_{d}$ are pairwise effectively sparse.
Let $1\leq i<j\leq d$ and $K\geq 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\geq 0$, $b_{i}R_{i}^{n}>|u^{(i)}_{n}-c_{i}\rho_{i}^{n}|$ and
$b_{j}R_{j}^{n}>|u^{(j)}_{n}-c_{j}\rho_{j}^{n}+K|$. Then, the triangle
inequality and Thm. 2.13 yield $N^{\prime}\geq 0$ such that for all $n\geq
N^{\prime}$,

$|u^{(i)}_{n}-u^{(j)}_{n}|>|c_{i}\rho_{i}^{n}-c_{j}\rho_{j}^{n}|-b_{i}R_{i}^{n}-b_{j}R_{j}^{n}+K\geq
K.$

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

###  5.2. Effective Almost Periodicity of the Order Word

In this section, let $r_{i},\rho_{i}\in\mathbb{R}\cap\overline{\mathbb{Q}}$
with $r_{i}>0$ and $\rho_{i}>1$ for $1\leq i\leq d$. Suppose for all $1\leq
i<j\leq d$ and $n,m\in~{}\mathbb{N}$,
$r_{i}\rho_{i}^{n}~{}\neq~{}r_{j}\rho_{j}^{m}$. Let
$\xi\coloneqq\operatorname{Ord}(\langle
r_{1}\rho_{1}^{n}\rangle_{n=0}^{\infty},\ldots,\langle
r_{d}\rho_{d}^{n}\rangle_{n=0}^{\infty})\in\\{1,\ldots,d\\}^{\omega}$ as in
Def. 5.2. We will prove the following.

###### Theorem 5.5.

  1. (a)

The word $\xi$ is almost-periodic.

  2. (b)

Assuming Schanuel’s conjecture, $\xi$ is effectively almost-periodic.

  3. (c)

If $1/\log(\rho_{1}),\ldots,1/\log(\rho_{d})$ are linearly independent over
$\mathbb{Q}$, then $\xi$ is unconditionally effectively almost-periodic.

  4. (d)

If $\operatorname{rank}(G_{M}(\rho_{1},\ldots,\rho_{d}))\geq d-2$, and
$\rho_{1},\ldots,\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}\leq\rho_{2}\leq\cdots\leq\rho_{d}$ and $r_{1}=1$. Let

$V=\left\\{\log\big{(}r_{i}\rho_{i}^{n}\big{)}\colon 1\leq i\leq
d,\>n\in\mathbb{N}\right\\}$

and $\langle v_{n}\rangle_{n=0}^{\infty}$ be the ordering of $V$ with
$v_{0}<v_{1}<\cdots$. Observe that

$\xi=\operatorname{Ord}(\,\langle\log\big{(}r_{1}\rho_{1}^{n}\big{)}\rangle_{n=0}^{\infty},\ldots,\langle\log\big{(}r_{d}\rho_{d}^{n}\big{)}\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.

$a_{0}$$a_{1}$$a_{2}$$a_{3}$$a_{4}$$a_{5}$$a_{6}$$a_{7}$$b_{0}$$b_{1}$$b_{2}$
Figure 1. Generating $\xi$.

###### 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}<\cdots$

and hence
$\xi={\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}1}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}1}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}1}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}1}{\color[rgb]{0,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,1}\pgfsys@color@cmyk@stroke{1}{0}{0}{0}\pgfsys@color@cmyk@fill{1}{0}{0}{0}2}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}1}{\color[rgb]{0,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,1}\pgfsys@color@cmyk@stroke{1}{0}{0}{0}\pgfsys@color@cmyk@fill{1}{0}{0}{0}2}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}1}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}1}{\color[rgb]{0,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,1}\pgfsys@color@cmyk@stroke{1}{0}{0}{0}\pgfsys@color@cmyk@fill{1}{0}{0}{0}2}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}1}\cdots$.
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 (Fogg et al.,
2002, Chap. 4.1.2) and (Arnoux et al., 1994; Baryshnikov, 1995) 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
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}1}$; When
we hit $y=n$, we write
${\color[rgb]{0,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,1}\pgfsys@color@cmyk@stroke{1}{0}{0}{0}\pgfsys@color@cmyk@fill{1}{0}{0}{0}2}$.

$1$$2$$3$$4$$1$$2$$3$$(0,0)$ Figure 2. The suffix $\xi[3,\infty)$ as a cutting
sequence.

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 (Lothaire, 2002).

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\colon\\{z_{n}\colon n\in\mathbb{N}\\}\to\\{1,\ldots,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,
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}z_{0}}=0$,
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}z_{1}}=1$,
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}z_{2}}=2$,
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}z_{3}}=3$,
${\color[rgb]{0,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,1}\pgfsys@color@cmyk@stroke{1}{0}{0}{0}\pgfsys@color@cmyk@fill{1}{0}{0}{0}z_{4}}=\log(9)/\log(2)\approx
3.17$,
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}z_{5}}=4$,
${\color[rgb]{0,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,1}\pgfsys@color@cmyk@stroke{1}{0}{0}{0}\pgfsys@color@cmyk@fill{1}{0}{0}{0}z_{6}}=\log(9\cdot
3)/\log(2)\approx 4.75$,
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}z_{7}}=5$,
${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}z_{8}}=6$,
and so on.

We will next factorise $\xi=w_{-}w_{0}w_{1}\cdots$. 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\leq
v_{m}<n+1$ if and only if $k_{n}\leq 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}={\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}1}$,
$w_{3}={\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}1}{\color[rgb]{0,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,1}\pgfsys@color@cmyk@stroke{1}{0}{0}{0}\pgfsys@color@cmyk@fill{1}{0}{0}{0}2}$,
$w_{4}={\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}1}{\color[rgb]{0,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,1}\pgfsys@color@cmyk@stroke{1}{0}{0}{0}\pgfsys@color@cmyk@fill{1}{0}{0}{0}2}$,
$w_{5}={\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}1}$,
and so on.

Let $N$ be the smallest integer $n$ such that every letter of
$\\{1,\ldots,d\\}$ appears in $w_{0}\cdots w_{n}\in\\{1,\ldots,d\\}^{*}$. In
Ex. 5.6, $N=3$. Further let $\Sigma$ be the set of all finite patterns over
$\\{1,\ldots,d\\}$ that start with the letter 1 and contain at most one
instance of $i$ for all $i\in\\{1,\ldots,d\\}$. Define
$\beta\in\Sigma^{\omega}$ by $\beta(n)=w_{N+n}$. In our example,
$\beta=({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}1}{\color[rgb]{0,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,1}\pgfsys@color@cmyk@stroke{1}{0}{0}{0}\pgfsys@color@cmyk@fill{1}{0}{0}{0}2})({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}1}{\color[rgb]{0,1,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,1}\pgfsys@color@cmyk@stroke{1}{0}{0}{0}\pgfsys@color@cmyk@fill{1}{0}{0}{0}2})({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}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\colon\Sigma^{*}\to\\{1,\ldots,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 (Muchnik et al., 2003), 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\\}\coloneqq
x-\lfloor x\rfloor$ denotes the fractional part of $x$.

###### Theorem 5.7.

For $2\leq i\leq 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
$\bm{\delta}=(\delta_{2},\ldots,\delta_{d})\in\mathbb{T}^{d-1}$ and
$\mathbf{s}=(s_{2},\ldots,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},\ldots,x_{d}$) of the form
$x_{i}/\delta_{i}<x_{j}/\delta_{j}$ or $x_{i}/\delta_{i}\sim 1$, where
${\sim}\in\\{>,<\\}$ and $2\leq i,j\leq d$.

###### Proof.

For $2\leq i\leq d$ and $n\in\mathbb{N}$, let

$L(n,i)=\left\\{\frac{\log\big{(}r_{i}\rho_{i}^{k}\big{)}}{\log(\rho_{1})}\,\colon
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\big{(}r_{i}\rho_{i}^{k}\big{)}/\log(\rho_{1})\colon
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,\ldots,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.

  * ($\ast$)

There exist $k_{1},\ldots,k_{m}\in\mathbb{N}$ such that

$N+n\leq\frac{\log\big{(}r_{b_{1}}\rho_{b_{1}}^{k_{1}}\big{)}}{\log(\rho_{1})}<\cdots<\frac{\log\big{(}r_{b_{m}}\rho_{b_{m}}^{k_{m}}\big{)}}{\log(\rho_{1})}<N+n+1.$

  * ($\ast\ast$)

For every $k\in\mathbb{N}$ and $i\in\\{2,\ldots,d\\}$ not appearing in $b$,

$\frac{\log\big{(}r_{i}\rho_{i}^{k}\big{)}}{\log(\rho_{1})}\notin[N+n,N+n+1).$

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

$z_{l}=t=\log\big{(}r_{1}\rho_{1}^{t}\big{)}/\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\big{(}r_{i}\rho_{i}^{k}\big{)}/\log(\rho_{1})\notin\mathbb{N}$. Thus in
$(\ast)$ and $(\ast\ast)$ we can replace non-strict inequalities with strict
ones, and vice versa.

Next, observe that $(\ast)$ is equivalent to

(7) $\Delta(n,b_{m})<\cdots<\Delta(n,b_{1})<1.$

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

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

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

$\frac{\log\big{(}r_{i}\rho_{i}^{k}\big{)}}{\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,\mathbf{s})$,
where
$g(y_{2},\ldots,y_{d})=(\\{y_{2}+\delta_{2}\\},\ldots,\\{y_{d}+\delta_{d}\\})$.
Recall from Sec. 2.7 that for $n\in\mathbb{N}$,
$g^{(n)}(\mathbf{s})=(\\{s_{2}+n\delta_{2}\\},\ldots,\\{s_{d}+n\delta_{d}\\})$.
Considering (7) and (8), we are led to defining, for $b=b_{0}b_{1}\cdots
b_{m}\in\Sigma$, $S_{b}\subseteq\mathbb{T}^{d-1}$ as the (open) set of all
$(x_{2},\ldots,x_{d})\in\mathbb{T}^{d-1}$ such that

(9)
$\frac{x_{b_{m}}}{\delta_{b_{m}}}<\cdots<\frac{x_{b_{1}}}{\delta_{b_{1}}}<1\>\>\>\quad\land\bigwedge_{\begin{subarray}{c}1\leq
j\leq d\\\ j\neq b_{1},\ldots,b_{m}\end{subarray}}\frac{x_{j}}{\delta_{j}}>1.$

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

In the remainder of this section, let
$\mathbf{s}=(s_{2},\ldots,s_{d})\in\mathbb{T}^{d-1}$ and
$\bm{\delta}\coloneqq(\delta_{2},\ldots,\delta_{d})\in\mathbb{T}^{d-1}$, and
$g\colon\mathbb{T}^{d-1}\to\mathbb{T}^{d-1}$ be defined as above. Figure 3
illustrates the target sets $\\{S_{b}\colon 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}$.

11213132123 Figure 3. The torus for $\rho_{1}=2$, $\rho_{2}=3$, and
$\rho_{3}=5$.

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 morphism, and hence is almost-periodic by (Muchnik et al.,
2003, 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$. ∎

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)}(\mathbf{s})\in S_{w}$. Furthermore, we can compute a
representation of $S_{w}$ as a Boolean combination of inequalities of the form

(10)
$h(x_{2}/\delta_{2},\ldots,x_{d}/\delta_{d},1/\delta_{2},\ldots,1/\delta_{d})\sim
0,$

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

###### Proof.

See App. A.5. ∎

We next prove Thm. 5.5 (c). Suppose $1/\log(\rho_{1}),\ldots,1/\log(\rho_{d})$
are linearly independent over $\mathbb{Q}$. Then for all
$c_{2},\ldots,c_{d},k\in\mathbb{Q}$,

$\displaystyle\sum_{i=2}^{d}c_{i}\delta_{i}=k$
$\displaystyle\Leftrightarrow\frac{c_{2}}{\log(\rho_{2})}+\cdots+\frac{c_{d}}{\log(\rho_{d})}=\frac{k}{\log(\rho_{1})}$
$\displaystyle\Rightarrow k,c_{2},\ldots,c_{d}=0.$

Hence $G_{A}(\bm{\delta})$ is the trivial group,
$\mathbb{T}_{\bm{\delta}}=\mathbb{T}^{d-1}$, and by Kronecker’s theorem (Thm.
2.14), $\langle g^{(n)}(\mathbf{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\coloneqq\exists
x_{2},\ldots,x_{d}\colon\Phi(x_{2},\ldots,x_{d})$ where $\Phi$ is a formula of
the form

$\bigvee_{j\in J}\bigwedge_{k\in
K}h_{j,k}(x_{2}/\delta_{2},\ldots,x_{d}/\delta_{d},1/\delta_{2},\ldots,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\widetilde{x}_{2},\ldots,\widetilde{x}_{d}\colon\Phi(\widetilde{x}_{2},\ldots,\widetilde{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},\ldots,1/\delta_{d})\sim_{l,m}0.$

Recall that $\frac{1}{\delta_{i}}=\frac{\log(\rho_{i})}{\log(\rho_{1})}$. For
$h(x_{2},\ldots,x_{d})\coloneqq c_{1}+c_{2}x_{2}+\cdots+c_{d}x_{d}$,

$h(1/\delta_{2},\ldots,1/\delta_{d})=\frac{1}{\log(\rho_{1})}(c_{1}\log(\rho_{1})+\cdots+c_{d}\log(\rho_{d})).$

Hence for all $l,m$, whether
$h_{l,m}(1/\delta_{2},\ldots,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}),\ldots,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}),\ldots,1/\log(\rho_{d}))$ (Lem.
2.9). Hence we can compute an $\mathbb{R}_{\exp}$ formula defining the compact
$\mathbb{T}_{\bm{\delta},\mathbf{s}}\subseteq\mathbb{T}^{d-1}$ in which in
$\langle f^{(n)}(\mathbf{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}_{\bm{\delta},\mathbf{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=\operatorname{Ord}(\langle
r_{1}\rho_{1}^{n}\rangle_{n=0}^{\infty},\ldots,\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}),\ldots,s_{d}+t/\log(\rho_{d}))\colon t\geq 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. (Allouche and Shallit, 2003,
Chap. 10.5).

  * (ii)

By (Arnoux et al., 1994), 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 (Bedaride, 2009) gives an exact formula for
$p(n)$ assuming $1/\log(\rho_{1}),\ldots,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 (Baryshnikov, 1995) 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}),\ldots,1/\log(\rho_{3})$ are linearly independent over
$\mathbb{Q}$, but $\log(\rho_{1}),\ldots,\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\leq i\leq d$, let $\langle u^{(i)}_{n}\rangle_{n=0}^{\infty}$ for $1\leq
i\leq 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},\ldots,P_{d})$, and recall that the MSO theory of
$\langle{\mathbb{N};<,P_{1},\ldots,P_{d}}\rangle$ is decidable if and only if
$\mathsf{Acc}_{\alpha}$ is decidable. Applying Thm. 5.3, we can construct
$r_{1},\ldots,r_{d}$ such that $\mathsf{Acc}_{\alpha}$ reduces to
$\mathsf{Acc}_{\xi}$, where $\xi=\operatorname{Ord}(\langle
r_{1}\rho_{1}^{n}\rangle_{n=0}^{\infty},\ldots,\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 $\mathsf{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[3]{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_ (Lothaire, 2002, 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,\ldots,b-1\\}$. Recall from
Thm. 4.16 that for such $\alpha$, $\mathsf{Acc}_{\alpha}$ is decidable. For a
detailed discussion of normal numbers, see surveys (Harman, 2002; Queffélec,
2006) and the book (Bugeaud, 2012). In particular, (Harman, 2002) states the
following conjecture.

###### Conjecture 6.1.

An irrational algebraic number $\alpha$ is weakly normal in any integer base
$b\geq 2$.

The strongest result towards this conjecture is due to Adamczewski and Bugeaud
(Adamczewski and Bugeaud, 2007). 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\geq 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\geq 2$.
The following is a generalisation of Cor. 1.3; see App. A.6 for the proof,
which is a simple application of Thm. 4.11.

###### Theorem 6.3.

Let $b,d\geq 2$ and $p,q\geq 1$ be integers such that $\sqrt[d]{p/q}$ is
rational. Let $\alpha\in\left(\\{0,1\\}^{2}\right)^{\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 $\mathsf{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. (1)

$\alpha\in\left(\\{0,1\\}^{2}\right)^{\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. (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. (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 $\mathsf{Acc}_{\alpha}$, $\mathsf{Acc}_{\beta}$, and
$\mathsf{Acc}_{\gamma}$ are Turing-equivalent.

###### Proof.

We will prove the theorem by showing:

  1. (1)

$\mathsf{Acc}_{\beta}$ reduces to $\mathsf{Acc}_{\alpha}$.

  2. (2)

$\mathsf{Acc}_{\alpha}$ reduces to $\mathsf{Acc}_{\gamma}$.

  3. (3)

$\mathsf{Acc}_{\gamma}$ reduces to $\mathsf{Acc}_{\beta}$.

Part (1): $\mathsf{Acc}_{\beta}$ reduces to $\mathsf{Acc}_{\alpha}$. By
construction (except for an easily computable finite prefix), we have the
invariant

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

For example, if $p=2$, $q=1$, $b=10$, and $d=2$, then
$\eta=\sqrt{2}=1.4142\cdots$ 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\bmod 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}\bmod b$, where
$b_{n}\coloneqq|\\{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|\equiv\lfloor{\eta
b^{n}}\rfloor\pmod{b}.$

Part (2): $\mathsf{Acc}_{\alpha}$ reduces to $\mathsf{Acc}_{\gamma}$. 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)\cdots.$

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 (Schinzel and Tijdeman, 1976).

###### Lemma 6.5 (Schinzel and Tijdeman).

For every $N\geq 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: $\mathsf{Acc}_{\alpha}$ of the
characteristic word reduces to $\mathsf{Acc}_{\gamma}$ of the order word.

Part (3): $\mathsf{Acc}_{\gamma}$ reduces to $\mathsf{Acc}_{\beta}$. Note that
$\gamma$ itself can be written as
$\gamma=(1,0)^{m_{0}}(0,1)(1,0)^{m_{1}}(0,1)\cdots$. We now reduce
$\mathsf{Acc}_{\gamma}$ to $\mathsf{Acc}_{\beta}$ 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:

$\displaystyle S_{k}$ $\displaystyle=\sum_{i=0}^{k}m_{i}=\lfloor{\eta
b^{k}}\rfloor$ $\displaystyle\beta_{k}$ $\displaystyle\equiv\lfloor{\eta
b^{k}}\rfloor\pmod{b}$ $\displaystyle bS_{k}$ $\displaystyle\leq
S_{k+1}<b(S_{k}+1)$ $\displaystyle S_{k+1}$
$\displaystyle=bS_{k}+\beta_{k+1}=S_{k}+m_{k+1}.$

Define

$\gamma^{\prime}=\bot^{m_{0}}\beta(0)\bot^{m_{1}}\beta(1)\cdots.$

Applying Lem. 4.5, $\mathsf{Acc}_{\gamma}$ reduces to
$\mathsf{Acc}_{\gamma^{\prime}}$ via a straightforward transduction, which is
in fact a homomorphism. It thus suffices to reduce
$\mathsf{Acc}_{\gamma^{\prime}}$ to $\mathsf{Acc}_{\beta}$.

We denote $S_{k}=\lfloor{\eta b^{k}}\rfloor$ and observe that $bS_{k}\leq
S_{k+1}<b(S_{k}+1)$ (one can check the identity
$b\lfloor{x}\rfloor\leq\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}\geq N$ for all $k\geq
j$; (2) for any morphism $h$ into a finite monoid $M$, there exist effective
$N,t$ such that for all $n\geq N$, $h(\bot^{n})=h(\bot^{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^{\text{th}}$ factor of
$\gamma^{\prime}$ to be $\bot^{m_{j}}\beta(j)$. On reading $\beta(j)$,
$\mathcal{B}$ outputs $\mu_{j}$, with the property that
$h(\bot^{m_{j}}\beta(j))=\mu_{j}$ for all $j\in\mathbb{N}$. Invoking Cor. 4.7,
$\mathsf{Acc}_{\gamma^{\prime}}$ reduces to $\mathsf{Acc}_{\beta}$. ∎

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,
$\mathsf{Acc}_{\beta}$ is decidable by Thm. 4.16. Applying Theorem 6.4, both
$\mathsf{Acc}_{\alpha}$ and $\mathsf{Acc}_{\gamma}$ 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\geq 2$, $P_{1}=\mathsf{N}_{2}$, $P_{2}=\mathsf{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 $\mathsf{Acc}_{\alpha}$ and $\mathsf{Acc}_{\beta}$ are Turing-
equivalent.

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

###### Acknowledgements.

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)
  * Adamczewski and Bugeaud (2007) Boris Adamczewski and Yann Bugeaud. 2007.  On the complexity of algebraic numbers I. Expansions in integer bases.  _Annals of Mathematics_ (2007), 547–565.
  * Allouche and Shallit (2003) Jean-Paul Allouche and Jeffrey Shallit. 2003.  _Automatic sequences: theory, applications, generalizations_.  Cambridge university press.
  * Arnoux et al. (1994) 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.
  * Baryshnikov (1995) Yu. Baryshnikov. 1995\.  Complexity of trajectories in rectangular billiards.  _Communications in mathematical physics_ 174 (1995), 43–56.
  * Bateman et al. (1993) 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.
  * Bedaride (2009) Nicolas Bedaride. 2009\.  Directional complexity of the hypercubic billiard.  _Discrete mathematics_ 309, 8 (2009), 2053–2066.
  * Berthé et al. (2024) 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 _2024 39th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)_.  https://doi.org/10.1145/3661814.3662119
  * Berthé et al. (2023) 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).
  * Blumensath (2023) Achim Blumensath. 2023\.  Monadic Second-Order Model Theory.  www.fi.muni.cz/~blumens/.  [Online; accessed on 09 November 2023].
  * Büchi (1990) 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.
  * Büchi and Landweber (1969) 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
  * Bugeaud (2012) 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
  * Cai et al. (2000) 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
  * Carton and Thomas (2002) Olivier Carton and Wolfgang Thomas. 2002.  The Monadic Theory of Morphic Infinite Words and Generalizations.  _Information and Computation_ 176, 1 (2002), 51–65.
  * Cohen (2013) Henri Cohen. 2013\.  _A course in computational algebraic number theory_. Vol. 138.  Springer Science & Business Media.
  * Dantzig et al. (1973) 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.
  * Elgot and Rabin (1966) 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.
  * Everest et al. (2003) Graham Everest, Alf van der Poorten, Igor Shparlinski, and Thomas Ward. 2003.  _Recurrence Sequences_.  American Mathematical Society.
  * Fogg et al. (2002) N. Pytheas Fogg, Valéré Berthé, Sébastien Ferenczi, Christian Mauduit, and Anne Siegel. 2002.  _Substitutions in dynamics, arithmetics and combinatorics_.  Springer.
  * Gonek and Montgomery (2016) 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.
  * Harman (2002) Glyn Harman. 2002\.  One hundred years of normal numbers.  In _Surveys in Number Theory_. AK Peters/CRC Press, 57–74.
  * Karimov et al. (2022) 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.
  * Lang (1966) Serge Lang. 1966\.  _Introduction to Transcendental Numbers_.  Addison-Wesley.
  * Lothaire (2002) M. Lothaire. 2002\.  _Algebraic combinatorics on words_. Vol. 90.  Cambridge university press.
  * Macintyre and Wilkie (1996) 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.
  * Masser (1988) David W Masser. 1988\.  Linear relations on algebraic groups.  _New Advances in Transcendence Theory_ (1988), 248–262.
  * Matveev (2000) 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\.
  * Muchnik et al. (2003) An. Muchnik, A. Semenov, and M. Ushakov. 2003.  Almost periodic sequences.  _Theoretical Computer Science_ 304, 1 (2003), 1–33.
  * Queffélec (2006) Martine Queffélec. 2006\.  Old and new results on normality.  _Lecture Notes-Monograph Series_ (2006), 225–236.
  * Rabinovich (2007) 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.
  * Rabinovich and Thomas (2006) 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.
  * Robinson (1958) 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
  * Schinzel and Tijdeman (1976) Andrzej Schinzel and Robert Tijdeman. 1976.  On the equation $y^{m}=P(x)$.  _Acta Arithmetica_ 31 (1976), 199–204.
  * Semenov (1980) 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://api.semanticscholar.org/CorpusID:123422158
  * Semenov (1984) 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.
  * Thomas (1997) Wolfgang Thomas. 1997\.  Languages, automata, and logic.  In _Handbook of Formal Languages: Volume 3 Beyond Words_. Springer, 389–455.
  * Waldschmidt (2000) Michel Waldschmidt. 2000\.  _Diophantine Approximation on Linear Algebraic Groups: Transcendence Properties of the Exponential Function in Several Variables_.  Springer Berlin Heidelberg, Berlin, Heidelberg.

##  Appendix A Omitted proofs

###  A.1. Proof of Lemma 2.9

We will use the following lemmas to prove Lem. 2.9.

###### Lemma A.1.

Assume that $d,e\geq 1$ and that

$f(x_{1},\dots,x_{e})=\frac{c_{1}}{\sum_{i=1}^{e}b_{i,1}x_{i}}+\cdots+\frac{c_{d}}{\sum_{i=1}^{e}b_{i,d}x_{i}}$

for some $c_{j},b_{i,j}\in\mathbb{Q}$ such that for $1\leq j<j^{\prime}\leq
d$, $\sum_{i=1}^{e}b_{i,j}x_{i}\neq s\sum_{i=1}^{e}b_{i,j^{\prime}}x_{i}$ does
not hold for any $s\in\mathbb{R}$. If $f(x_{1},\dots,x_{d})=0$, then
$c_{1},\dots,c_{d}=0$.

###### Proof.

For $1\leq j\leq d$, Let $V_{j}$ be the $e-1$-dimensional subspace of
$\mathbb{R}^{e}$ where $\sum_{i=1}^{e}b_{i,j}x_{i}=0$ holds for all
$(x_{1},\dots,x_{e})\in\mathbb{R}^{e}$. Assume that for $1\leq j\leq d$,
$c_{j}\neq 0$.

If $\langle{\mathbf{x}_{n}}\rangle_{n=0}^{\infty}$ is a
$\mathbb{R}^{e}$-valued sequence converging to $\mathbf{x}\in V_{j}$, then
$\lim_{n\to\infty}|f(\mathbf{x}_{n})|=+\infty$. Hence, as
$f(x_{1},\dots,x_{e})=0$, $\mathbf{x}\in V_{j^{\prime}}$ for some $1\leq
j^{\prime}\leq d$ unequal to $j$. Then $V_{j}\cap V_{j^{\prime}}$ is again a
linear subspace of $\mathbb{R}^{e}$ of dimension at most $e-1$.

If $V_{j}\cap V_{j^{\prime}}$ has dimension less than $e-1$ for all $1\leq
j^{\prime}\leq d$ unequal to $j$, then

$V_{j}\subsetneq\cup_{\begin{subarray}{c}1\leq j^{\prime}\leq d\\\
j^{\prime}\neq j\end{subarray}}(V_{j}\cap V_{j^{\prime}})$

giving a contradiction that each $\textbf{x}\in V_{j}$ is in some
$V_{j^{\prime}}$ with $j^{\prime}\neq j$.

Thus, $V_{j}=V_{j^{\prime}}$ for some $j^{\prime}\neq j$, and so
$\sum_{i=1}^{e}b_{i,j}x_{i}=0$ if and only if
$\sum_{i=1}^{e}b_{i,j^{\prime}}x_{i}=0$. Hence, there is some
$s\in\mathbb{R}_{\neq 0}$ such that $b_{i,j}=sb_{i,j^{\prime}}$ for all $1\leq
i\leq e$. This gives a contradiction, and so $c_{j}=0$. As this holds for all
$1\leq j\leq d$, the lemma follows. ∎

###### Lemma A.2.

Assume that
$\lambda_{1},\dots,\lambda_{d}\in\mathbb{R}_{>1}\cap\overline{\mathbb{Q}}$ are
pairwise multiplicatively independent. Then
$1/\log(\lambda_{1}),\dots,1/\log(\lambda_{d})$ are linearly independent over
$\mathbb{Q}$ assuming Schanuel’s conjecture.

###### Proof.

First, using Thm. 2.4, compute a basis for
$G_{M}(\lambda_{1},\dots,\lambda_{d})$ and select a maximum multiplicative
independent subset $\\{\lambda_{1},\dots,\lambda_{e}\\}$, possibly needing to
renumber the $\lambda_{i}$. Then, for all $1\leq j\leq d$, one can compute
$b_{i,j}$ for $1\leq i\leq e$ such that
$\log(\lambda_{j})=\sum_{i=1}^{e}b_{i,j}\log(\lambda_{i})$ using the known
multiplicative relationships. Then we have to show that when
$c_{1},\dots,c_{d}\in\mathbb{Q}$ and

(11)
$\frac{c_{1}}{\sum_{i=1}^{e}b_{i,1}\log(\lambda_{i})}+\cdots+\frac{c_{d}}{\sum_{i=1}^{e}b_{i,d}\log(\lambda_{i})}=0$

Schanuel’s conjecture implies that all $c_{i}$ are zero. By multiplying (11)
by $\prod_{j=1}\sum_{i=1}^{e}b_{i,j}\log(\lambda_{i})$, we obtain a polynomial
expression in $\log(\lambda_{1}),\dots,\log(\lambda_{e})$ that equals zero.

We apply Schanuel’s conjecture (Conj. 2.7) with $\alpha_{i}=\log(\lambda_{i})$
for $1\leq i\leq e$. As $\lambda_{1},\dots,\lambda_{e}$ are multiplicatively
independent, $\log(\lambda_{1}),\dots,\log(\lambda_{e})$ are linearly
independent over $\mathbb{Q}$ by Baker’s theorem (Thm. 2.10). Then
$\\{\log(\lambda_{1}),\dots,\log(\lambda_{e}),\lambda_{1},\dots,\lambda_{e}\\}$
has transcendence degree at least $d$ by Schanuel’s conjecture while also
being equal to the transcendence degree of
$\\{\log(\lambda_{1}),\dots,\log(\lambda_{e})\\}$ as all $\lambda_{i}$ are
algebraic. Hence, $\log(\lambda_{1}),\dots,\log(\lambda_{e})$ are
algebraically independent.

This implies that the polynomial expression obtained from (11), has to
evaluate trivially to zero. That is, the rational function

$f(x_{1},\dots,x_{e})=\frac{c_{1}}{\sum_{i=1}^{e}b_{i,1}x_{i}}+\cdots+\frac{c_{d}}{\sum_{i=1}^{e}b_{i,d}x_{i}}$

is exactly zero. Assume that $1\leq j<j^{\prime}<d$ and
$\sum_{i=1}^{e}b_{i,j}x_{i}\neq s\sum_{i=1}^{e}b_{i,j^{\prime}}x_{i}$ holds
for a real number $s$. As $\lambda_{j^{\prime}}\neq 0$, some
$b_{i,j^{\prime}}$ is non-zero. Then $s=b_{i,j}/b_{i,j}\in\mathbb{Q}$. Hence,

$\log(\lambda_{j})=\sum_{i=1}^{e}b_{i,j}\log(\lambda_{i})=\sum_{i=1}^{e}sb_{i,j^{\prime}}\log(\lambda_{i})=s\log(\lambda_{j^{\prime}}),$

contradicting that $\lambda_{j}$ and $\lambda_{j^{\prime}}$ are
multiplicatively independent. Thus, the hypothesis of Lem. A.1 is satisfied
and all $c_{j}$ are 0. We conclude the statement. ∎

Now Lem. 2.9 easily follows.

###### Proof of Lem. 2.9.

If $\lambda_{i}$ and $\lambda_{j}$ are multiplicatively dependent, say
$\lambda_{i}^{a}=\lambda_{j}^{b}$ for some non-zero integers $a$ and $b$, then
$a\log(\lambda_{i})=b\log(\lambda_{j})$. Hence,
$a/\log(\lambda_{j})=b/\log(\lambda_{i})$, giving a non-trivial element in
$G_{A}(1/\log(\lambda_{1}),\dots,1/\log(\lambda_{d}))$.

Meanwhile, by Lem. A.2, for any pairwise multiplicative independent subset of
$\\{\lambda_{1},\dots,\lambda_{d}\\}$, the reciprocals of their logs are
linearly independent.

Together, this implies that any $\mathbb{Q}$-linear relationship among
$1/\log(\lambda_{1}),\dots,1/\log(\lambda_{d})$ can be reduced to a
relationship generated by pairwise multiplicative relationships. One can
easily find a basis among these by computing for each pair
$(\lambda_{i},\lambda_{j})$ whether they multiplicatively dependent using Thm.
2.4. ∎

###  A.2. Proof of Lemma 2.11

###### Proof of Lem. 2.11.

By the two assumptions, for any $1\leq i<j<k\leq d$ there exist
$b_{i},b_{j},b_{k}\in\mathbb{Z}_{\neq 0}$ such that
$\lambda_{i}^{b_{i}}\lambda_{j}^{b_{j}}\lambda_{k}^{b_{k}}=1$. Equivalently,
$b_{i}\log(\lambda_{i})+b_{j}\log(\lambda_{j})+b_{k}\log(\lambda_{k})=0$.
Hence, for $1\leq j\leq d$, let $b_{1,j},b_{2,j}\in\mathbb{Q}$ be such that
$\log(\lambda_{j})=b_{1,j}\log(\lambda_{1})+b_{2,j}\log(\lambda_{2})$. Then
$b_{1,1}=b_{2,2}=0$ and all other $b_{i,j}$ are non-zero.

For a contradiction, let $c_{1},\dots,c_{d}\in\mathbb{Q}$ be rational numbers
such that $\sum_{j=1}^{d}c_{j}/\log(\lambda_{j})=0$. Multiplying by
$\prod_{j=1}^{d}\log(\lambda_{j})$ gives

$\sum_{j=1}^{d}c_{j}\prod_{i=1,i\neq
j}^{d}\left(b_{1,j}\log(\lambda_{1})+b_{2,j}\log(\lambda_{2})\right)=0,$

which simplifies to

(12) $\sum_{i=0}^{d-1}e_{i}\log(\lambda_{1})^{i}\log(\lambda_{2})^{d-i}=0$

for some $e_{i}\in\mathbb{Q}$. Assume not all $e_{i}$ are zero. Then dividing
by $\log(\lambda_{2})^{d-1}$ shows that $\log(\lambda_{1})/\log(\lambda_{2})$
is the root of the non-zero polynomial
$\sum_{i=0}^{d-1}e_{i}x^{i}\in\mathbb{Q}[x]$. That is,
$\log(\lambda_{1})/\log(\lambda_{2})$ is an algebraic number, say $\alpha$ and
so $\log(\lambda_{1})-\alpha\log(\lambda_{2})=0$, contradicting Baker’s
theorem (Thm. 2.10). Hence, all $e_{i}$ have to be zero.

As (12) is obtained by multiplying
$\sum_{j=1}^{d}\frac{c_{j}}{\log(\lambda_{j})}$ with the non-zero number
$\prod_{j=1}^{d}\log(\lambda_{j})$,

(13) $\sum_{j=1}^{d}\frac{c_{i}}{b_{1,j}x_{1}+b_{2,j}x_{2}}=0.$

As in Lem. A.2, we deduce that as all $\lambda_{i}$ are pairwise
multiplicatively dependent and so (13) satisfies the hypothesis of Lem. A.1.
Thus, all $c_{i}$ are zero and the statement follows. ∎

###  A.3. Proof of Theorem 2.13

###### Proof of Thm. 2.13.

If $\rho_{1}$ and $\rho_{2}$ are multiplicatively dependent, say
$\rho_{1}^{m_{1}}=\rho_{2}^{m_{2}}$, let $\rho_{3}=\rho_{1}^{1/m_{2}}$,
$R_{3}=\max(R_{1}^{1/m_{2}},R_{2}^{1/m_{1}})$. Then $R_{3}<\rho_{3}$ and
solving

$|c_{1}\rho_{3}^{n_{1}^{\prime}}-c_{2}\rho_{3}^{n_{2}^{\prime}}|\leq(b_{1}+b_{2})R_{3}^{\max(n_{1}+n_{2})}$

when $c_{1}\rho_{3}^{n_{1}^{\prime}}\neq c_{2}\rho_{3}^{n_{2}^{\prime}}$ gives
all solutions to (3) by setting $n_{1}=m_{2}n_{1}^{\prime}$ and
$n_{2}=m_{1}n_{2}^{\prime}$. As the left-hand side can be bounded from below
by $C_{1}\rho_{3}^{\max(n_{1}^{\prime},n_{2}^{\prime})}$ for a computable
constant $C_{1}$ when it is non-zero, $\max(n_{1}^{\prime},n_{2}^{\prime})$
can be bounded from above and so $n_{1}$ and $n_{2}$ as well.

If $\rho_{1}$ and $\rho_{2}$ are multiplicatively independent, it is
sufficient to bound $n_{1},n_{2}$ that satisfy

(14) $|c_{1}\rho_{1}^{n_{1}}-c_{2}\rho_{2}^{n_{2}}|\geq
2b_{1}R_{1}^{n_{1}},2b_{2}R_{2}^{n_{2}}$

as adding the two cases gives the result. We can assume that
$\rho_{1}<\rho_{2}$. After dividing both sides by $c_{1}\rho_{1}^{n_{1}}$, we
apply Matveev’s result to
$\Lambda=c_{1}^{-1}c_{2}(\rho_{1}^{-1})^{n_{1}}\rho_{2}^{n_{2}}-1$ to find
that

$\log|\Lambda|\geq-C_{1}(1+\log(\max(1,n_{1},n_{2})))$

for some computable constant $C_{1}>0$. Thus, we want $n_{1}$ and $n_{2}$ to
satisfy

(15)
$\begin{split}\log|\Lambda|&\geq\log(2b_{1}/c_{1})+n_{1}\log(\rho_{1}/R_{1})\quad\text{and}\\\
\log|\Lambda|&\geq\log(2b_{2}/c_{1})+n_{2}\log(\rho_{2})-n_{1}\log(R_{1}).\end{split}$

If $n_{1}\geq n_{2}$ and the first of these equations is false, then

(16)
$C_{1}(1+\log(\max(1,n_{1})))\geq\log(c_{2}/(2b_{1}))+n_{1}\log(\rho_{1}/R_{1}).$

We can effectively bound $n_{1}$ (and thus $n_{2}$) as the right-hand side
grows logarithmically while the left-hand grows linearly in $n_{1}$.

If $n_{2}\geq n_{1}$ and the second equation of (15) is false,

$C_{1}(1+\log(\max(1,n_{2})))\leq\log(c_{2}/(2b_{1}))+n_{1}\log(\rho_{1}/R_{1}).$

Thus, we can compute constants $C_{3}$, $C_{4}$ such that $C_{4}>0$ and if the
second equation of (15) is false, then $n_{1}\geq C_{3}+C_{4}\log(n_{2})$.
Thus, we can assume that $n_{1}\leq C_{3}+C_{4}\log(n_{2})$. If the second
equation of (15) is false,

$C_{1}(1+\log(\max(1,n_{2})))\geq\log(c_{1}/2b_{2})+n_{2}\log(\rho_{2})-n_{1}\log(R_{1}).$

Using our bound on $n_{1}$, we obtain that when $n_{2}\geq 1$

$C_{1}(1+\log(n_{2}))\geq\log(c_{1}/2b_{2})+n_{2}\log(\rho_{2})-(C_{3}+C_{4}\log(n_{2}))\log(R_{1}).$

The left-hand side grows logarithmically in $n_{2}$ while the right-hand side
grows linearly. Hence, we can again bound $n_{2}$ (and thus $n_{1}$). The
result follows. ∎

###  A.4. Proof of Theorem 4.16

###### Proof of Thm. 4.16.

Consider a given deterministic Muller automaton $\mathcal{A}$ as a directed
graph allowing multiple edges. We partition the graph into its strongly
connected components (SCCs) and call an SCC without outgoing edges a bottom
SCC. We will show that the set of states visited infinitely often by the run
of $\mathcal{A}$ on $\alpha$ is precisely a bottom SCC. Hence, we decide
$\mathsf{Acc}_{\alpha}$ by simulating this run until a bottom SCC is
inevitably reached. Then $\alpha$ is accepted if and only if this bottom SCC
is in the Muller acceptance condition.

We need to show that (a) if an SCC is not a bottom SCC, then the run
eventually exits it; and (b) if the run enters a bottom SCC, it visits all its
states infinitely often.

For (a), let $S$ be a non-bottom SCC. There thus exist $q_{1}\in S,b\in\Sigma$
such that $\delta(q_{1},b)\notin S$, i.e. reading the letter $b$ in state
$q_{1}$ exits $S$. We will order the states of $S$ as $q_{1},\dots,q_{k}$,
construct words $u_{1}=b,\dots,u_{k}\in\Sigma^{+}$, and inductively prove that
for all $j\leq i$, $\delta(q_{j},u_{i})\notin S$. Since $\alpha$ is weakly
normal, $u_{k}$ will inevitably occur as a factor, and hence, the run will
exit $S$.

We have observed the base case to hold with $u_{1}=b$. For the induction step,
assume that for all $j\leq i$, $\delta(q_{j},u_{i})\notin S$. Now, if
$\delta(q_{i+1},u_{i})\notin S$, take $u_{i+1}=u_{i}$. Else, if
$\delta(q_{i+1},u_{i})=q\in S$, the strong connectivity of $S$ implies that
$\delta(q,v_{i})=q_{1}$ for some $v_{i}\in\Sigma^{*}$. Thus, take
$u_{i+1}=u_{i}v_{i}b$, and observe that for all $j\leq i+1$,
$\delta(q_{j},u_{i+1})\notin S$.

We prove (b) similarly. Fix an order of states $q_{1},\dots,q_{k}$ of $S$. By
definition, a run entering the bottom SCC $S$ will be confined in $S$. It thus
suffices to prove that for any $q\in S$, we can inductively construct a word
$u_{k}\in\Sigma^{+}$ such that for all $j\leq k$, the non-empty run of $u_{k}$
on $\mathcal{A}$ starting from $q_{j}$ visits $q$. The induction is similar to
the one above. Choose $q_{1}\in S,u_{1}\in\Sigma^{*}$ to be such that
$\delta(q_{1},u_{1})=q$. By the induction hypothesis, for every $j\leq i$, the
run on $u_{i}$ starting in $q_{j}$ visits $q$. If the run on $u_{i}$ starting
in $q_{i+1}$ visits $q$, take $u_{i+1}=u_{i}$. Else, use that $S$ is a bottom
SCC to identify $v_{i}\in\Sigma^{+}$ such that $\delta(q_{i+1},u_{i}v_{i})=q$,
and take $u_{i+1}=u_{i}v_{i}$. We have thus ensured that for all $j\leq i+1$,
the run on $u_{i}$ starting in $q_{j}$ visits $q$. Since $\alpha$ is weakly
normal, $u_{k}$ occurs as a factor infinitely often, and hence all $q\in S$
are visited infinitely often. ∎

###  A.5. Proof of Lemma 5.9

###### Proof of Lem. 5.9.

Consider $b=b_{0}b_{1}\cdots b_{m}\in\Sigma$, where $b_{i}\in\\{1,\ldots,d\\}$
for all $i$ and $b_{0}=1$. Let

$S_{b,k}=\\{\mathbf{x}\in\mathbb{T}^{d-1}\colon g^{(k)}(\mathbf{x})\in
S_{b}\\}.$

Since $g\colon\mathbb{T}^{d-1}\to\mathbb{T}^{d-1}$ is a homeomorphism,
$S_{b,k}$ is an open subset of $\mathbb{T}^{d-1}$. Since
$g^{(k)}(x_{2},\ldots,x_{d})=(\\{x_{2}+k\delta_{2}\\},\ldots,\\{x_{d}+k\delta_{d}\\})$,
from (9) it follows that $S_{b,k}$ is the set of all
$(x_{2},\ldots,x_{d})\in\mathbb{T}^{d-1}$ satisfying

$\frac{\\{x_{b_{m}}+k\delta_{b_{m}}\\}}{\delta_{b_{m}}}<\cdots<\frac{\\{x_{b_{1}}+k\delta_{b_{1}}\\}}{\delta_{b_{1}}}<1$

and

$\bigwedge_{\begin{subarray}{c}1\leq j\leq d\\\
j\,\neq\,b_{1},\ldots,b_{m}\end{subarray}}\frac{\\{x_{j}+k\delta_{j}\\}}{\delta_{j}}>1.$

For $2\leq i\leq d$, let $t_{i}=\lfloor k\delta_{i}\rfloor$. Observe that
$\\{x_{i}+k\delta_{i}\\}=x_{i}+k\delta_{i}-t_{i}$ if
$x_{i}+k\delta_{i}<t_{i}+1$ and
$\\{x_{i}+k\delta_{i}\\}=x_{i}+k\delta_{i}-(t_{i}+1)$ otherwise. Moreover,
$x_{i}+k\delta_{i}<t_{i}+1$ is equivalent to
$x_{i}/\delta_{i}+k<\frac{t_{i}+1}{\delta_{i}}$. Therefore,
$\frac{\\{x_{j}+k\delta_{j}\\}}{\delta_{j}}\bowtie 1$ (where $\bowtie$ is an
(in)equality symbol) is equivalent to

$\frac{x_{i}}{\delta_{i}}+k<\frac{t_{i}+1}{\delta_{i}}\Rightarrow\frac{x_{j}+k\delta_{j}-t_{j}}{\delta_{j}}\bowtie
1\qquad\land\\\
\frac{x_{i}}{\delta_{i}}+k\geq\frac{t_{i}+1}{\delta_{i}}\Rightarrow\frac{x_{j}+k\delta_{j}-(t_{j}+1)}{\delta_{j}}\bowtie
1.$

Rearranging, this formula can be written as a Boolean combination of
inequalities of the form (10) where $h$ is a $\mathbb{Q}$-affine form.
Similarly,
$\frac{\\{x_{i}+k\delta_{i}\\}}{\delta_{i}}<\frac{\\{x_{j}+k\delta_{j}\\}}{\delta_{j}}$
can be equivalently written as a Boolean combination of inequalities of the
form (10) by conditioning on whether $x_{i}/\delta_{i}+k<(t_{i}+1)/\delta_{i}$
and $x_{j}/\delta_{j}+k<(t_{j}+1)/\delta_{j}$. Finally, observe that $0\leq
x_{i}<1$ is equivalent to $0\leq x_{i}\delta_{i}<1/\delta_{i}$. We conclude
that $S_{b,k}$ can be defined by a Boolean combination of inequalities of the
form (10).

It remains to define $S_{w}=\bigcap_{k=0}^{|w|-1}S_{w(k),k}$. Since each
$S_{w(k),k}$ is open and defined by a Boolean combination of inequalities of
the form (10), we conclude the same for $S_{w}$. ∎

###  A.6. Proof of Theorem 6.3

###### Proof of Cor. 6.3.

By assumption, $p/q=A^{d}/B^{d}$ for some coprime integers $A,B\geq 1$. Thus,
$p=qA^{d}/B^{d}$ and $B^{d}$ divides $q$. Let $f_{1}(n)=(q/B^{d})n^{d}$ and
$f_{2}(n)=Ab^{n}$. Then $g_{1}(n)=f_{1}(n)=(q/B^{d})n^{d}$ and
$g_{2}(n)=g_{1}\circ f_{2}(n)=g_{1}(Ab^{n})=(q/B^{d})A^{d}b^{nd}=pb^{nd}$. Let
$\beta$ be the characteristic word of
$(\\{g_{1}(n):n\in\mathbb{N}\\},\\{g_{2}(n):n\in\mathbb{N}\\})$. Then the
problem $\mathsf{Acc}_{\beta}$ is decidable by Thm. 4.11 as by (Carton and
Thomas, 2002, Theorem 5.2), $f_{1},f_{2}\in\mathcal{F}$.

Then we construct a transducer $\mathcal{B}$ from $\beta$ to $\alpha$ as
follows. We keep track of the number of occurrences of $(1,0)$ and $(1,1)$ we
have encountered modulo $B^{d}$. When this counter is zero modulo $B^{d}$, we
output $\beta(n)$, otherwise we output $(0,j)$ instead of $(i,j)$. Thus, the
second predicate remains unchanged while for the first we only count every
$B^{d}$th term. Hence, $\alpha=\mathcal{B}(\beta)$ and so
$\mathsf{Acc}_{\alpha}$ is decidable using Lem. 4.5. ∎

###  A.7. Proof of Theorem 6.6

###### Proof of Thm. 6.6.

The proof mirrors that of Thm. 6.4 closely. To show that
$\mathsf{Acc}_{\beta}$ reduces to $\mathsf{Acc}_{\alpha}$, let
$\alpha^{\prime}$ be the word obtained from $n^{2}$ and $b\cdot b^{2n}$. Then
the transducer $\mathcal{B}$ that changes every $(1,1)$ into $(1,0)$ (and
leaves everything else unchanged) has the property that
$\mathcal{B}(\alpha)=\alpha^{\prime}$. This follows from the fact that a power
of $b$ is not a square if and only if it is of the form $b\cdot b^{2n}$. By
Lem. 4.5, $\mathsf{Acc}_{\alpha^{\prime}}$ reduces to $\mathsf{Acc}_{\alpha}$.
As $\mathsf{Acc}_{\alpha^{\prime}}$ and $\mathsf{Acc}_{\beta}$ are Turing-
equivalent, one direction follows.

To show the other direction, let $\gamma\in\\{(0,1),(1,0),(1,1)\\}^{\omega}$
be the word obtained by deleting all occurrences of $(0,0)$ from $\alpha$.
Denoting $\mathbf{0}=(0,0)$, we have:

$\alpha=\mathbf{0}^{k_{0}}\gamma(0)\cdots\mathbf{0}^{k_{n}}\gamma(n)\cdots.$

We invoke Lem. 6.5 to argue that for any $K$, we can compute $N$ such that for
all $n\geq N$, $k_{n}>K$. The number of intervening $\mathbf{0}$’s is
effectively eventually lower bounded, and thanks to the procyclic nature of
the predicates, can still be computed modulo any $m$. Thus, similar to the
proof of Thm. 4.15, one can use Cor. 4.7 to show that $\mathsf{Acc}_{\alpha}$
reduces to $\mathsf{Acc}_{\gamma}$. Our strategy to reduce
$\mathsf{Acc}_{\gamma}$ to $\mathsf{Acc}_{\beta}$ is to closely follow the
proof of Thm. 6.4 (3), and apply Cor. 4.7 in a similar way.

The terms $(1,0)$ signify the squares which are not powers of $b$, $(0,1)$,
the numbers $b\cdot b^{2n}$ and $(1,1)$ the numbers $b^{2n}$. We express
$\gamma$ as

$\gamma=(1,0)^{k_{0}}(1,1)(1,0)^{k_{1}}(0,1)\cdots(1,0)^{k_{2n}}(1,1)(1,0)^{k_{2n+1}}(0,1)\cdots.$

In order to apply Cor. 4.7, we are interested in computing $k_{n}$. Similarly
to the proof of Thm. 6.4 (3), we record:

$\displaystyle S_{2n}$ $\displaystyle=n+\sum_{i=0}^{2n}k_{i}=b^{n}$
$\displaystyle S_{2n+1}$