LIPIcs.CSL.2022.24.pdf
- Filesize: 0.88 MB
- 23 pages
Document
Decidability for Sturmian Words
Authors
-
Part of:
Volume:
30th EACSL Annual Conference on Computer Science Logic (CSL 2022)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Computer Science Logic (CSL) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2022-01-27
File
Document Identifiers
Acknowledgements
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 As Get 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)
https://doi.org/10.4230/LIPIcs.CSL.2022.24
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.
Subject Classification
ACM Subject Classification
- Theory of computation → Logic and verification
Keywords
- Decidability
- Sturmian words
- Ostrowski numeration systems
- Automated theorem proving
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
- Jean-Paul Allouche and Jeffrey Shallit. Automatic Sequences: Theory, Applications, Generalizations. Cambridge University Press, 2003. URL: https://doi.org/10.1017/CBO9780511546563.
-
Aseem Baranwal, Luke Schaeffer, and Jeffrey Shallit. Ostrowski-automatic sequences: Theory and applications. Theor. Comput. Sci., 858:122-142, 2021.
- 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: https://doi.org/10.1007/978-3-030-28796-2.
- 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: http://projecteuclid.org.proxy2.library.illinois.edu/euclid.bbms/1103408547.
-
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.
- 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: https://doi.org/10.1142/S0129054113400182.
- Philipp Hieronymi. Expansions of the ordered additive group of real numbers by two discrete subgroups. J. Symb. Log., 81(3):1007-1027, 2016. URL: https://doi.org/10.1017/jsl.2015.34.
- Philipp Hieronymi, Danny Nguyen, and Igor Pak. Presburger arithmetic with algebraic scalar multiplications. arXiv:1805.03624, 2018. URL: http://arxiv.org/abs/1805.03624.
- Philipp Hieronymi and Alonza Terry Jr. Ostrowski numeration systems, addition, and finite automata. Notre Dame J. Form. Log., 59:215-232, July 2014. URL: https://doi.org/10.1215/00294527-2017-0027.
-
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.
-
Bakhadyr Khoussainov and Anil Nerode. Automata Theory and Its Applications. Birkhauser Boston, Inc., Secaucus, NJ, USA, 2001.
-
M. Lothaire. Algebraic combinatorics on words., volume 90. Cambridge: Cambridge University Press, 2002.
- Hamoon Mousavi. Automatic Theorem Proving in Walnut. CoRR, abs/1603.06017, 2016. URL: http://arxiv.org/abs/1603.06017.
- 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: https://doi.org/10.1051/ita/2016010.
- Reed Oei, Eric Ma, Christian Schulz, and Philipp Hieronymi. Pecan. available at https://github.com/ReedOei/Pecan, 2020.
- Reed Oei, Eric Ma, Christian Schulz, and Philipp Hieronymi. Pecan: An Automated Theorem Prover for Automatic Sequences using Büchi automata. arXiv, 2021. URL: http://arxiv.org/abs/2102.01727.
- 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: https://doi.org/10.1007/BF02940581.
- Andrew M. Rockett and Peter Szüsz. Continued fractions. World Scientific Publishing Co., Inc., River Edge, NJ, 1992. URL: https://doi.org/10.1142/1725.
-
Thoralf Skolem. Über einige Satzfunktionen in der Arithmetik. Skr. Norske Vidensk. Akad., Oslo, Math.-naturwiss. Kl., 7:1-28, 1931.
- 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: https://doi.org/10.4230/LIPIcs.CSL.2017.35.