Beatty sequences for a quadratic irrational: Decidability and applications

Let α and β be real numbers belonging to the same quadratic field. We show that the inhomogeneous Beatty sequence ( ⌊ n α + β ⌋ ) n ≥ 1 is synchronized, in the sense that there is a finite automaton that takes as input the Ostrowski representations of n and y in parallel, and accepts if and only if y = ⌊ n α + β ⌋ . Since it is already known that the addition relation is computable for Ostrowski representations based on a quadratic irrational, a consequence is a new and rather simple proof that the first-order logical theory of these sequences with addition is decidable. The decision procedure is easily implemented in the free software Walnut . As an application, we show that for each r ≥ 1 it is decidable whether the set { ⌊ n α + β ⌋ : n ≥ 1 } forms an additive basis (or asymptotic additive basis) of order r . Using our techniques, we also solve some open problems of Reble and Kimberling, and give an explicit characterization of a sequence of Hildebrand et al.