Document Open Access Logo

Existential Definability over the Subword Ordering

Authors Pascal Baumann , Moses Ganardi , Ramanathan S. Thinniyam , Georg Zetzsche

PDF

File

Thumbnail PDF
PDF
LIPIcs.STACS.2022.7.pdf
  • Filesize: 0.72 MB
  • 15 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Complexity theory and logic
  • Theory of computation → Logic
Keywords
  • subword
  • subsequence
  • definability
  • expressiveness
  • first order logic
  • existential fragment
  • quantifier alternation

Metrics

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

Abstract

We study first-order logic (FO) over the structure consisting of finite words over some alphabet A, together with the (non-contiguous) subword ordering. In terms of decidability of quantifier alternation fragments, this logic is well-understood: If every word is available as a constant, then even the Σ₁ (i.e., existential) fragment is undecidable, already for binary alphabets A.
However, up to now, little is known about the expressiveness of the quantifier alternation fragments: For example, the undecidability proof for the existential fragment relies on Diophantine equations and only shows that recursively enumerable languages over a singleton alphabet (and some auxiliary predicates) are definable.
We show that if |A| ≥ 3, then a relation is definable in the existential fragment over A with constants if and only if it is recursively enumerable. This implies characterizations for all fragments Σ_i: If |A| ≥ 3, then a relation is definable in Σ_i if and only if it belongs to the i-th level of the arithmetical hierarchy. In addition, our result yields an analogous complete description of the Σ_i-fragments for i ≥ 2 of the pure logic, where the words of A^* are not available as constants.

Cite As Get BibTex

Pascal Baumann, Moses Ganardi, Ramanathan S. Thinniyam, and Georg Zetzsche. Existential Definability over the Subword Ordering. In 39th International Symposium on Theoretical Aspects of Computer Science (STACS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 219, pp. 7:1-7:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022) https://doi.org/10.4230/LIPIcs.STACS.2022.7

Author Details

Pascal Baumann
  • Max Planck Institute for Software Systems (MPI-SWS), Kaiserslautern, Germany
Moses Ganardi
  • Max Planck Institute for Software Systems (MPI-SWS), Kaiserslautern, Germany
Ramanathan S. Thinniyam
  • Max Planck Institute for Software Systems (MPI-SWS), Kaiserslautern, Germany
Georg Zetzsche
  • Max Planck Institute for Software Systems (MPI-SWS), Kaiserslautern, Germany

References

  1. Parosh Aziz Abdulla and Bengt Jonsson. Verifying programs with unreliable channels. information and computation, 127(2):91-101, 1996. Google Scholar
  2. Mohamed Faouzi Atig, Dmitry Chistikov, Piotr Hofman, K. Narayan Kumar, Prakash Saivasan, and Georg Zetzsche. The complexity of regular abstractions of one-counter languages. In Martin Grohe, Eric Koskinen, and Natarajan Shankar, editors, Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, New York, NY, USA, July 5-8, 2016, pages 207-216. ACM, 2016. URL: https://doi.org/10.1145/2933575.2934561.
  3. Mohamed Faouzi Atig, Roland Meyer, Sebastian Muskalla, and Prakash Saivasan. On the upward/downward closures of Petri nets. In Kim G. Larsen, Hans L. Bodlaender, and Jean-François Raskin, editors, 42nd International Symposium on Mathematical Foundations of Computer Science, MFCS 2017, August 21-25, 2017 - Aalborg, Denmark, volume 83 of LIPIcs, pages 49:1-49:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.MFCS.2017.49.
  4. Ricardo A. Baeza-Yates. Searching subsequences. Theoretical Computer Science, 78(2):363-376, 1991. Google Scholar
  5. Laura Barker, Pamela Fleischmann, Katharina Harwardt, Florin Manea, and Dirk Nowotka. Scattered factor-universality of words. In Developments in Language Theory - 24th International Conference, DLT 2020, Tampa, FL, USA, May 11-15, 2020, Proceedings, volume 12086 of Lecture Notes in Computer Science, pages 14-28. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-48516-0_2.
  6. David Barozzini, Lorenzo Clemente, Thomas Colcombet, and Pawel Parys. Cost automata, safe schemes, and downward closures. In Artur Czumaj, Anuj Dawar, and Emanuela Merelli, editors, 47th International Colloquium on Automata, Languages, and Programming, ICALP 2020, July 8-11, 2020, Saarbrücken, Germany (Virtual Conference), volume 168 of LIPIcs, pages 109:1-109:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.ICALP.2020.109.
  7. Jean Berstel. Transductions and Context-Free Languages. Teubner, 1979. Google Scholar
  8. Karl Bringmann and Marvin Künnemann. Quadratic conditional lower bounds for string problems and dynamic time warping. In IEEE 56th Annual Symposium on Foundations of Computer Science, FOCS 2015, Berkeley, CA, USA, 17-20 October, 2015, pages 79-97. IEEE Computer Society, 2015. URL: https://doi.org/10.1109/FOCS.2015.15.
  9. Karl Bringmann and Marvin Künnemann. Multivariate fine-grained complexity of longest common subsequence. In Proceedings of the Twenty-Ninth Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 2018, New Orleans, LA, USA, January 7-10, 2018, pages 1216-1235. SIAM, 2018. URL: https://doi.org/10.1137/1.9781611975031.79.
  10. Lorenzo Clemente, Pawel Parys, Sylvain Salvati, and Igor Walukiewicz. The diagonal problem for higher-order recursion schemes is decidable. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, New York, NY, USA, July 5-8, 2016, pages 96-105. ACM, 2016. URL: https://doi.org/10.1145/2933575.2934527.
  11. Joel D. Day, Pamela Fleischmann, Maria Kosche, Tore Koß, Florin Manea, and Stefan Siemer. The edit distance to k-subsequence universality. In 38th International Symposium on Theoretical Aspects of Computer Science, STACS 2021, March 16-19, 2021, Saarbrücken, Germany (Virtual Conference), volume 187 of LIPIcs, pages 25:1-25:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.STACS.2021.25.
  12. Cees Elzinga, Sven Rahmann, and Hui Wang. Algorithms for subsequence combinatorics. Theoretical Computer Science, 409(3):394-404, 2008. Google Scholar
  13. Lukas Fleischer and Manfred Kufleitner. Testing Simon’s congruence. In 43rd International Symposium on Mathematical Foundations of Computer Science, MFCS 2018, August 27-31, 2018, Liverpool, UK, volume 117 of LIPIcs, pages 62:1-62:13. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. URL: https://doi.org/10.4230/LIPIcs.MFCS.2018.62.
  14. Pawel Gawrychowski, Maria Kosche, Tore Koß, Florin Manea, and Stefan Siemer. Efficiently testing Simon’s congruence. In 38th International Symposium on Theoretical Aspects of Computer Science, STACS 2021, March 16-19, 2021, Saarbrücken, Germany (Virtual Conference), volume 187 of LIPIcs, pages 34:1-34:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.STACS.2021.34.
  15. Peter Habermehl, Roland Meyer, and Harro Wimmel. The downward-closure of petri net languages. In Samson Abramsky, Cyril Gavoille, Claude Kirchner, Friedhelm Meyer auf der Heide, and Paul G. Spirakis, editors, Automata, Languages and Programming, 37th International Colloquium, ICALP 2010, Bordeaux, France, July 6-10, 2010, Proceedings, Part II, volume 6199 of Lecture Notes in Computer Science, pages 466-477. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-14162-1_39.
  16. Matthew Hague, Jonathan Kochems, and C.-H. Luke Ong. Unboundedness and downward closures of higher-order pushdown automata. In Rastislav Bodík and Rupak Majumdar, editors, Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016, pages 151-163. ACM, 2016. URL: https://doi.org/10.1145/2837614.2837627.
  17. Simon Halfon, Philippe Schnoebelen, and Georg Zetzsche. Decidability, complexity, and expressiveness of first-order logic over the subword ordering. In Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, pages 1-12. IEEE Computer Society, 2017. URL: https://doi.org/10.1109/LICS.2017.8005141.
  18. Simon Halfon, Philippe Schnoebelen, and Georg Zetzsche. Decidability, complexity, and expressiveness of first-order logic over the subword ordering. CoRR, abs/1701.07470, 2017. URL: http://arxiv.org/abs/1701.07470.
  19. Juris Hartmanis and John E Hopcroft. What makes some language theory problems undecidable. Journal of Computer and System Sciences, 4(4):368-376, 1970. Google Scholar
  20. Prateek Karandikar, Manfred Kufleitner, and Philippe Schnoebelen. On the index of Simon’s congruence for piecewise testability. Inf. Process. Lett., 115(4):515-519, 2015. URL: https://doi.org/10.1016/j.ipl.2014.11.008.
  21. Prateek Karandikar and Philippe Schnoebelen. Decidability in the logic of subsequences and supersequences. In 35th IARCS Annual Conference on Foundation of Software Technology and Theoretical Computer Science, FSTTCS 2015, December 16-18, 2015, Bangalore, India, volume 45 of LIPIcs, pages 84-97. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2015.84.
  22. Prateek Karandikar and Philippe Schnoebelen. The height of piecewise-testable languages and the complexity of the logic of subwords. Log. Methods Comput. Sci., 15(2), 2019. URL: https://doi.org/10.23638/LMCS-15(2:6)2019.
  23. Dexter C. Kozen. Theory of computation. Springer Verlag London Limited, 2010. Google Scholar
  24. Oleg V. Kudinov, Victor L. Selivanov, and Lyudmila V. Yartseva. Definability in the subword order. In Conference on Computability in Europe, pages 246-255. Springer, 2010. Google Scholar
  25. Dietrich Kuske. Theories of orders on the set of words. RAIRO-Theoretical Informatics and Applications, 40(01):53-74, 2006. Google Scholar
  26. Dietrich Kuske and Christian Schwarz. Complexity of Counting First-Order Logic for the Subword Order. In Javier Esparza and Daniel Kráľ, editors, 45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020), volume 170 of Leibniz International Proceedings in Informatics (LIPIcs), pages 61:1-61:12, Dagstuhl, Germany, 2020. Schloss Dagstuhl-Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.MFCS.2020.61.
  27. Dietrich Kuske and Georg Zetzsche. Languages ordered by the subword order. In Foundations of Software Science and Computation Structures - 22nd International Conference, FOSSACS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, volume 11425 of Lecture Notes in Computer Science, pages 348-364. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-17127-8_20.
  28. David Maier. The complexity of some problems on subsequences and supersequences. Journal of the ACM (JACM), 25(2):322-336, 1978. Google Scholar
  29. Yuri Matiyasevich. Hilbert’s tenth problem. MIT press, 1993. Google Scholar
  30. Pierre Péladeau. Logically defined subsets of N^k. Theoretical computer science, 93(2):169-183, 1992. Google Scholar
  31. Jacques Sakarovitch and Imre Simon. Subwords. In M. Lothaire, editor, Combinatorics on Words, Cambridge Mathematical Library, chapter 6, pages 105-142. Cambridge University Press, 2nd edition, 1997. URL: https://doi.org/10.1017/CBO9780511566097.009.
  32. Georg Zetzsche. An approach to computing downward closures. In Automata, Languages, and Programming - 42nd International Colloquium, ICALP 2015, Kyoto, Japan, July 6-10, 2015, Proceedings, Part II, volume 9135 of Lecture Notes in Computer Science, pages 440-451. Springer, 2015. URL: https://doi.org/10.1007/978-3-662-47666-6_35.
  33. Georg Zetzsche. Computing downward closures for stacked counter automata. In Ernst W. Mayr and Nicolas Ollinger, editors, 32nd International Symposium on Theoretical Aspects of Computer Science, STACS 2015, March 4-7, 2015, Garching, Germany, volume 30 of LIPIcs, pages 743-756. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015. URL: https://doi.org/10.4230/LIPIcs.STACS.2015.743.
  34. Georg Zetzsche. The complexity of downward closure comparisons. In Ioannis Chatzigiannakis, Michael Mitzenmacher, Yuval Rabani, and Davide Sangiorgi, editors, Proc. of the 43rd International Colloquium on Automata, Languages and Programming (ICALP 2016), volume 55 of Leibniz International Proceedings in Informatics (LIPIcs), pages 123:1-123:14, Dagstuhl, Germany, 2016. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. Google Scholar
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact