arXiv++ Combinatorics

We show that the first-order theory of Sturmian words over Presburger arithmetic is decidable. Using a general adder recognizing addition in Ostrowski numeration systems by Baranwal, Schaeffer and Shallit, we prove that the first-order expansions of Presburger arithmetic by a single Sturmian word are uniformly $ω$-automatic, and then deduce the decidability of the theory of the class of such structures. Using an implementation of this decision algorithm called Pecan, we automatically reprove classical theorems about Sturmian words in seconds, and are able to obtain new results about antisquares and antipalindromes in characteristic Sturmian words.

We consider Presburger arithmetic (PA) extended by scalar multiplication by an algebraic irrational number $α$, and call this extension $α$-Presburger arithmetic ($α$-PA). We show that the complexity of deciding sentences in $α$-PA is substantially harder than in PA. Indeed, when $α$ is quadratic and $r\geq 4$, deciding $α$-PA sentences with $r$ alternating quantifier blocks and at most $c\ r$ variables and inequalities requires space at least $K 2^{\cdot^{\cdot^{\cdot^{2^{C\ell(S)}}}}}$ (tower of height $r-3$), where the constants $c, K, C>0$ only depend on $α$, and $\ell(S)$ is the length of the given $α$-PA sentence $S$. Furthermore deciding $\exists^{6}\forall^{4}\exists^{11}$ $α$-PA sentences with at most $k$ inequalities is PSPACE-hard, where $k$ is another constant depending only on~$α$. When $α$ is non-quadratic, already four alternating quantifier blocks suffice for undecidability of $α$-PA sentences.