Decidability for Sturmian words
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , , , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2021
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866913466047004672 |
|---|---|
| author | Hieronymi, Philipp Ma, Dun Oei, Reed Schaeffer, Luke Schulz, Christian Shallit, Jeffrey |
| author_facet | Hieronymi, Philipp Ma, Dun Oei, Reed Schaeffer, Luke Schulz, Christian Shallit, Jeffrey |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2102_08207 |
| institution | arXiv |
| publishDate | 2021 |
| record_format | arxiv |
| spellingShingle | Decidability for Sturmian words Hieronymi, Philipp Ma, Dun Oei, Reed Schaeffer, Luke Schulz, Christian Shallit, Jeffrey Logic in Computer Science Combinatorics Logic 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. |
| title | Decidability for Sturmian words |
| topic | Logic in Computer Science Combinatorics Logic |
| url | https://arxiv.org/abs/2102.08207 |