Abstract
We show that the existential fragment of Büchi arithmetic is strictly less expressive than full Büchi arithmetic of any base, and moreover establish that its \(\varSigma _2\)-fragment is already expressively complete. Furthermore, we show that regular languages of polynomial growth are definable in the existential fragment of Büchi arithmetic.
Parts of this research were carried out while the first author was affiliated with the Department of Computer Science, University College London, UK.
Chapter PDF
Similar content being viewed by others
Keywords
References
Benedikt, M., Libkin, L., Schwentick, T., Segoufin, L.: Definable relations and first-order query languages over strings. J. ACM 50(5), 694–751 (2003). https://doi.org/10.1145/876638.876642
Bruyère, V.: Entiers et automates finis. Mémoire de fin d’études (1985)
Bruyère, V., Hansel, G., Michaux, C., Villemaire, R.: Logic and \(p\)-recognizable sets of integers. Bull. Belg. Math. Soc. Simon Stevin 1(2), 191–238 (1994). https://doi.org/10.36045/bbms/1103408547
Büchi, J.: Weak second-order arithmetic and finite automata. Math. Logic Quart. 6(1–6), 66–92 (1960). https://doi.org/10.1002/malq.19600060105
Chistikov, D., Haase, C.: The taming of the semi-linear set. In: Automata, Languages, and Programming, ICALP. LIPIcs, vol. 55, pp. 128:1–128:13. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2016). https://doi.org/10.4230/LIPIcs.ICALP.2016.128
Chrobak, M.: Finite automata and unary languages. Theor. Comput. Sci. 47(3), 149–158 (1986). https://doi.org/10.1016/0304-3975(86)90142-8
Ginsburg, S., Spanier, E.: Bounded ALGOL-like languages. T. Am. Math. Soc. pp. 333–368 (1964). https://doi.org/10.2307/1994067
Guépin, F., Haase, C., Worrell, J.: On the existential theories of Büchi arithmetic and linear p-adic fields. In: Logic in Computer Science, LICS. pp. 1–10. IEEE (2019). https://doi.org/10.1109/LICS.2019.8785681
Lohrey, M., Zetzsche, G.: Knapsack and the power word problem in solvable Baumslag-Solitar groups. In: Mathematical Foundations of Computer Science, MFCS. LIPIcs, vol. 170, pp. 67:1–67:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020). https://doi.org/10.4230/LIPIcs.MFCS.2020.67
Presburger, M.: Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. In: Comptes Rendus du I congres de Mathematiciens des Pays Slaves, pp. 92–101 (1929)
Szilard, A., Yu, S., Zhang, K., Shallit, J.: Characterizing regular languages with polynomial densities. In: Mathematical Foundations of Computer Science, MFCS. Lect. Notes Comp. Sci., vol. 629, pp. 494–503. Springer (1992). https://doi.org/10.1007/3-540-55808-X_48
To, A.: Unary finite automata vs. arithmetic progressions. Inf. Process. Lett. 109(17), 1010–1014 (2009). https://doi.org/10.1016/j.ipl.2009.06.005
Villemaire, R.: The theory of (\(\mathbb{{N}}, +, {V}_k, {V}_l\)) is undecidable. Theor. Comput. Sci. 106(2), 337–349 (1992). https://doi.org/10.1016/0304-3975(92)90256-F
Wolper, P., Boigelot, B.: On the construction of automata from linear arithmetic constraints. In: Tools and Algorithms for the Construction and Analysis of Systems, TACAS. Lect. Notes Comp. Sci., vol. 1785, pp. 1–19. Springer (2000). https://doi.org/10.1007/3-540-46419-0_1
Woods, K.: The unreasonable ubiquitousness of quasi-polynomials. Elect. J. Combin. 21(1), P1.44 (2014). https://doi.org/10.37236/3750
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
© 2021 The Author(s)
About this paper
Cite this paper
Haase, C., Różycki, J. (2021). On the Expressiveness of Büchi Arithmetic. In: Kiefer, S., Tasson, C. (eds) Foundations of Software Science and Computation Structures. FOSSACS 2021. Lecture Notes in Computer Science(), vol 12650. Springer, Cham. https://doi.org/10.1007/978-3-030-71995-1_16
Download citation
DOI: https://doi.org/10.1007/978-3-030-71995-1_16
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-71994-4
Online ISBN: 978-3-030-71995-1
eBook Packages: Computer ScienceComputer Science (R0)