Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Decidability for Sturmian words

Philipp Hieronymi, Dun Ma, Reed Oei, Luke Schaeffer, Christian Schulz, Jeffrey Shallit

TL;DR

It is proved that the first-order expansions of Presburger arithmetic by a single Sturmian word are uniformly ω-automatic, and the decidability of the theory of the class of such structures is deduced.

Abstract

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.

Decidability for Sturmian words

TL;DR

It is proved that the first-order expansions of Presburger arithmetic by a single Sturmian word are uniformly ω-automatic, and the decidability of the theory of the class of such structures is deduced.

Abstract

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.

Paper Structure

This paper contains 20 sections, 35 theorems, 91 equations, 1 figure, 2 tables.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Omega-regular structures
  4. Binary representations
  5. Ostrowski representations
  6. Hashtag-binary encoding
  7. Hashtag-binary coding of continued fractions
  8. Hashtag-Ostrowski-representations
  9. Recognizing addition in Ostrowski numeration systems
  10. The uniform omega-regularity of R-alpha
  11. Decidability results
  12. Automatically Proving Theorems about Sturmian Words
  13. Classical theorems
  14. Powers
  15. Antisquares and more
  16. ...and 5 more sections

Key Result

Lemma 3.3

Let $w \in R$. Then there is a unique irrational number $\alpha\in [0,1]$ such that $w$ is a $\#$-binary coding of the continued fraction of $\alpha$.

Figures (1)

  • Figure 1: The procedure of Lemma \ref{['lem:binary-coding-infinite-aut']}. (a) The original automaton, with transitions for "any even number," "any odd number," and "any number." (b) The finite automata recognizing these sets in binary encoding. (c) The combined automaton produced by Lemma \ref{['lem:binary-coding-infinite-aut']}.

Theorems & Definitions (78)

  • proof
  • Definition 3.2
  • Lemma 3.3
  • proof
  • Definition 3.4
  • Lemma 3.5
  • proof
  • Lemma 3.6
  • proof
  • Lemma 3.7
  • ...and 68 more