Decidability for Sturmian Words

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

Thumbnail PDF


  • Filesize: 0.88 MB
  • 23 pages

Document Identifiers

Author Details

Philipp Hieronymi
  • Department of Mathematics, University of Illinois at Urbana-Champaign, IL, USA
  • Mathematisches Institut, Universität Bonn, Germany
Dun Ma
  • Department of Mathematics, University of Illinois at Urbana-Champaign, IL, USA
Reed Oei
  • Department of Mathematics, University of Illinois at Urbana-Champaign, IL, USA
Luke Schaeffer
  • Institute for Quantum Computing, University of Waterloo, Canada
Christian Schulz
  • Department of Mathematics, University of Illinois at Urbana-Champaign, IL, USA
Jeffrey Shallit
  • School of Computer Science, University of Waterloo, Canada


Part of this work was done in the research project "Building a theorem-prover" at the Illinois Geometry Lab in Spring 2020. P.H. and C.S. were partially supported by NSF grant DMS-1654725. We thank Mary Angelica Gramcko-Tursi for carefully reading a draft of this paper.

Cite AsGet BibTex

Philipp Hieronymi, Dun Ma, Reed Oei, Luke Schaeffer, Christian Schulz, and Jeffrey Shallit. Decidability for Sturmian Words. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 24:1-24:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Decidability
  • Sturmian words
  • Ostrowski numeration systems
  • Automated theorem proving


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. Jean-Paul Allouche and Jeffrey Shallit. Automatic Sequences: Theory, Applications, Generalizations. Cambridge University Press, 2003. URL:
  2. Aseem Baranwal, Luke Schaeffer, and Jeffrey Shallit. Ostrowski-automatic sequences: Theory and applications. Theor. Comput. Sci., 858:122-142, 2021. Google Scholar
  3. Aseem R. Baranwal and Jeffrey Shallit. Critical exponent of infinite balanced words via the Pell number system. In Combinatorics on words, volume 11682 of Lecture Notes in Comput. Sci., pages 80-92. Springer, Cham, 2019. URL:
  4. Véronique Bruyère, Georges Hansel, Christian Michaux, and Roger Villemaire. Logic and p-recognizable sets of integers. Bull. Belg. Math. Soc. Simon Stevin, 1(2):191-238, 1994. Journées Montoises (Mons, 1992). URL:
  5. J. Richard Büchi. On a decision method in restricted second order arithmetic. In Logic, Methodology and Philosophy of Science (Proc. 1960 Internat. Congr.), pages 1-11. Stanford Univ. Press, Stanford, Calif., 1962. Google Scholar
  6. Daniel Goč, Dane Henshall, and Jeffrey Shallit. Automatic theorem-proving in combinatorics on words. Internat. J. Found. Comput. Sci., 24(6):781-798, 2013. URL:
  7. Philipp Hieronymi. Expansions of the ordered additive group of real numbers by two discrete subgroups. J. Symb. Log., 81(3):1007-1027, 2016. URL:
  8. Philipp Hieronymi, Danny Nguyen, and Igor Pak. Presburger arithmetic with algebraic scalar multiplications. arXiv:1805.03624, 2018. URL:
  9. Philipp Hieronymi and Alonza Terry Jr. Ostrowski numeration systems, addition, and finite automata. Notre Dame J. Form. Log., 59:215-232, July 2014. URL:
  10. Bakhadyr Khoussainov and Mia Minnes. Three lectures on automatic structures. In Logic Colloquium 2007, volume 35 of Lect. Notes Log., pages 132-176. Assoc. Symbol. Logic, La Jolla, CA, 2010. Google Scholar
  11. Bakhadyr Khoussainov and Anil Nerode. Automata Theory and Its Applications. Birkhauser Boston, Inc., Secaucus, NJ, USA, 2001. Google Scholar
  12. M. Lothaire. Algebraic combinatorics on words., volume 90. Cambridge: Cambridge University Press, 2002. Google Scholar
  13. Hamoon Mousavi. Automatic Theorem Proving in Walnut. CoRR, abs/1603.06017, 2016. URL:
  14. Hamoon Mousavi, Luke Schaeffer, and Jeffrey Shallit. Decision algorithms for Fibonacci-automatic words, I: Basic results. RAIRO Theor. Inform. Appl., 50(1):39-66, 2016. URL:
  15. Reed Oei, Eric Ma, Christian Schulz, and Philipp Hieronymi. Pecan. available at, 2020.
  16. Reed Oei, Eric Ma, Christian Schulz, and Philipp Hieronymi. Pecan: An Automated Theorem Prover for Automatic Sequences using Büchi automata. arXiv, 2021. URL:
  17. Alexander Ostrowski. Bemerkungen zur Theorie der Diophantischen Approximationen. Abh. Math. Semin. Univ. Hambg., 1(1):77-98, 250-251, Reprinted in Collected Mathematical Papers, Vol. 3, pp. 57-80., December 1922. URL:
  18. Andrew M. Rockett and Peter Szüsz. Continued fractions. World Scientific Publishing Co., Inc., River Edge, NJ, 1992. URL:
  19. Thoralf Skolem. Über einige Satzfunktionen in der Arithmetik. Skr. Norske Vidensk. Akad., Oslo, Math.-naturwiss. Kl., 7:1-28, 1931. Google Scholar
  20. Faried Abu Zaid, Erich Grädel, and Frederic Reinhardt. Advice Automatic Structures and Uniformly Automatic Classes. In Valentin Goranko and Mads Dam, editors, 26th EACSL Annual Conference on Computer Science Logic (CSL 2017), volume 82 of Leibniz International Proceedings in Informatics (LIPIcs), pages 35:1-35:20, Dagstuhl, Germany, 2017. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL:
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail