On the Number of Quantifiers as a Complexity Measure

Authors Ronald Fagin , Jonathan Lenchner , Nikhil Vyas , Ryan Williams



PDF
Thumbnail PDF

File

LIPIcs.MFCS.2022.48.pdf
  • Filesize: 0.77 MB
  • 14 pages

Document Identifiers

Author Details

Ronald Fagin
  • IBM Research, Almaden, CA, USA
Jonathan Lenchner
  • IBM T.J. Watson Research Center, Cambridge, MA, USA
Nikhil Vyas
  • MIT EECS, Cambridge, MA, USA
Ryan Williams
  • MIT CSAIL and EECS, Cambridge, MA, USA

Cite AsGet BibTex

Ronald Fagin, Jonathan Lenchner, Nikhil Vyas, and Ryan Williams. On the Number of Quantifiers as a Complexity Measure. In 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 241, pp. 48:1-48:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.MFCS.2022.48

Abstract

In 1981, Neil Immerman described a two-player game, which he called the "separability game" [Neil Immerman, 1981], that captures the number of quantifiers needed to describe a property in first-order logic. Immerman’s paper laid the groundwork for studying the number of quantifiers needed to express properties in first-order logic, but the game seemed to be too complicated to study, and the arguments of the paper almost exclusively used quantifier rank as a lower bound on the total number of quantifiers. However, last year Fagin, Lenchner, Regan and Vyas [Fagin et al., 2021] rediscovered the game, provided some tools for analyzing them, and showed how to utilize them to characterize the number of quantifiers needed to express linear orders of different sizes. In this paper, we push forward in the study of number of quantifiers as a bona fide complexity measure by establishing several new results. First we carefully distinguish minimum number of quantifiers from the more usual descriptive complexity measures, minimum quantifier rank and minimum number of variables. Then, for each positive integer k, we give an explicit example of a property of finite structures (in particular, of finite graphs) that can be expressed with a sentence of quantifier rank k, but where the same property needs 2^Ω(k²) quantifiers to be expressed. We next give the precise number of quantifiers needed to distinguish two rooted trees of different depths. Finally, we give a new upper bound on the number of quantifiers needed to express s-t connectivity, improving the previous known bound by a constant factor.

Subject Classification

ACM Subject Classification
  • Theory of computation → Finite Model Theory
Keywords
  • number of quantifiers
  • multi-structural games
  • complexity measure
  • s-t connectivity
  • trees
  • rooted trees

Metrics

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

References

  1. Miklós Ajtai and Ronald Fagin. Reachability is harder for directed than for undirected finite graphs. J. Symbolic Logic, 55(1):113-150, March 1990. Google Scholar
  2. Greg Barnes, Jonathan F. Buss, Walter L. Ruzzo, and Baruch Schieber. A sublinear space, polynomial time algorithm for directed s-t connectivity. SIAM J. Comput., 27(5):1273-1282, 1998. URL: https://doi.org/10.1137/S0097539793283151.
  3. David A. Mix Barrington, Neil Immerman, and Howard Straubing. On uniformity within NC^1. In Proceedings: Third Annual Structure in Complexity Theory Conference, Georgetown University, Washington, D. C., USA, June 14-17, 1988, pages 47-59. IEEE Computer Society, 1988. URL: https://doi.org/10.1109/SCT.1988.5262.
  4. Paul Beame, Russell Impagliazzo, and Toniann Pitassi. Improved depth lower bounds for small distance connectivity. Comput. Complex., 7(4):325-345, 1998. URL: https://doi.org/10.1007/s000370050014.
  5. Xi Chen, Igor Carboni Oliveira, Rocco A. Servedio, and Li-Yang Tan. Near-optimal small-depth lower bounds for small distance connectivity. In Proceedings of the 48th Annual ACM SIGACT Symposium on Theory of Computing, STOC 2016, Cambridge, MA, USA, June 18-21, 2016, pages 612-625. ACM, 2016. URL: https://doi.org/10.1145/2897518.2897534.
  6. Edmund M. Clarke and E. Allen Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic. In Workshop on the Logic of Programs, Lecture Notes in Computer Science, volume 131, pages 52-71, 1981. Google Scholar
  7. Hubert Comon, Max Dauchet, Rémi Gilleroz, Florent Jacquemard, Denis Luguiez, Sophie Tison, and Marc Tommasi. Tree automata techniques and applications, 1999. URL: http://www.eecs.harvard.edu/~shieber/Projects/Transducers/Papers/comon-tata.pdf.
  8. A. Dawar, M. Grohe, S. Kreutzer, and N. Schweikardt. Model theory makes formulas large. In L. Arge, C. Cachin, T. Jurdziński, and A. Tarlecki, editors, ICALP07, volume 4596, pages 913-924. Springer, 2007. Google Scholar
  9. Andrzej Ehrenfeucht. An application of games to the completeness problem for formalized theories. Fundamenta Mathematicae, 49:129-141, 1961. Google Scholar
  10. Ronald Fagin, Jonathan Lenchner, Kenneth W. Regan, and Nikhil Vyas. Multi-structural games and number of quantifiers. In 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1-13, 2021. Google Scholar
  11. Ronald Fagin, Jonathan Lenchner, Nikhil Vyas, and Ryan Williams. On the number of quantifiers as a complexity measure, 2022. URL: http://arxiv.org/abs/2207.00104.
  12. Roland Fraïssé. Sur quelques classifications des systèmes de relations. Université d’Alger, Publications Scientifiques, Série A, 1:35-182, 1954. Google Scholar
  13. Parikshit Gopalan, Richard J. Lipton, and Aranyak Mehta. Randomized time-space tradeoffs for directed graph connectivity. In FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science, 23rd Conference, Mumbai, India, December 15-17, 2003, Proceedings, volume 2914 of Lecture Notes in Computer Science, pages 208-216. Springer, 2003. URL: https://doi.org/10.1007/978-3-540-24597-1_18.
  14. Frank Harary. Note on Carnap’s relational asymptotic relative frequencies. J. Symb. Log., 23(3):257-260, 1958. Google Scholar
  15. Neil Immerman. Number of quantifiers is better than number of tape cells. J. Comput. Syst. Sci., 22(3):384-406, 1981. Google Scholar
  16. Neil Immerman. Descriptive complexity. Graduate Texts in Computer Science. Springer, 1999. URL: https://doi.org/10.1007/978-1-4612-0539-5.
  17. Deepanshu Kush and Benjamin Rossman. Tree-depth and the formula complexity of subgraph isomorphism. In 61st IEEE Annual Symposium on Foundations of Computer Science, FOCS 2020, Durham, NC, USA, November 16-19, 2020, pages 31-42. IEEE, 2020. URL: https://doi.org/10.1109/FOCS46700.2020.00012.
  18. Leonid Libkin. Elements of Finite Model Theory. Texts in Theoretical Computer Science. Springer, 2012. URL: https://www.springer.com/gp/book/9783540212027.
  19. Christos Papdimitriou. Computational Complexity. Addison-Wesley Publishing Company, Reading, MA USA, 1995. Google Scholar
  20. Omer Reingold. Undirected st-connectivity in log-space. Proceedings of the 37th annual ACM symposium on the theory of computing, pages 376-385, 2005. Google Scholar
  21. Benjamin Rossman. Formulas vs. circuits for small distance connectivity. In Symposium on Theory of Computing, STOC 2014, New York, NY, USA, May 31 - June 03, 2014, pages 203-212. ACM, 2014. URL: https://doi.org/10.1145/2591796.2591828.
  22. Walter J. Savitch. Relationships between nondeterministic and deterministic tape complexities. J. Comput. Syst. Sci., 4(2):177-192, 1970. URL: https://doi.org/10.1016/S0022-0000(70)80006-X.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail