Optimally Rewriting Formulas and Database Queries: A Confluence of Term Rewriting, Structural Decomposition, and Complexity

Authors Hubie Chen, Stefan Mengel



PDF
Thumbnail PDF

File

LIPIcs.ICDT.2024.16.pdf
  • Filesize: 0.63 MB
  • 17 pages

Document Identifiers

Author Details

Hubie Chen
  • Department of Informatics, King’s College London, UK
Stefan Mengel
  • Univ. Artois, CNRS, Centre de Recherche en Informatique de Lens (CRIL), France

Acknowledgements

The authors thank Carsten Fuhs, Moritz Müller, and Riccardo Treglia for useful feedback and pointers.

Cite As Get BibTex

Hubie Chen and Stefan Mengel. Optimally Rewriting Formulas and Database Queries: A Confluence of Term Rewriting, Structural Decomposition, and Complexity. In 27th International Conference on Database Theory (ICDT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 290, pp. 16:1-16:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024) https://doi.org/10.4230/LIPIcs.ICDT.2024.16

Abstract

A central computational task in database theory, finite model theory, and computer science at large is the evaluation of a first-order sentence on a finite structure. In the context of this task, the width of a sentence, defined as the maximum number of free variables over all subformulas, has been established as a crucial measure, where minimizing width of a sentence (while retaining logical equivalence) is considered highly desirable. An undecidability result rules out the possibility of an algorithm that, given a first-order sentence, returns a logically equivalent sentence of minimum width; this result motivates the study of width minimization via syntactic rewriting rules, which is this article’s focus. For a number of common rewriting rules (which are known to preserve logical equivalence), including rules that allow for the movement of quantifiers, we present an algorithm that, given a positive first-order sentence ϕ, outputs the minimum-width sentence obtainable from ϕ via application of these rules. We thus obtain a complete algorithmic understanding of width minimization up to the studied rules; this result is the first one - of which we are aware - that establishes this type of understanding in such a general setting. Our result builds on the theory of term rewriting and establishes an interface among this theory, query evaluation, and structural decomposition theory.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic
  • Theory of computation → Database query processing and optimization (theory)
Keywords
  • width
  • query rewriting
  • structural decomposition
  • term rewriting

Metrics

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

References

  1. Serge Abiteboul, Richard Hull, and Victor Vianu. Foundations of Databases. Addison-Wesley, 1995. URL: http://webdam.inria.fr/Alice/.
  2. Isolde Adler and Mark Weyer. Tree-width for first order formulae. Log. Methods Comput. Sci., 8(1), 2012. URL: https://doi.org/10.2168/LMCS-8(1:32)2012.
  3. Franz Baader and Tobias Nipkow. Term rewriting and all that. Cambridge University Press, 1998. Google Scholar
  4. Christoph Berkholz and Hubie Chen. Compiling existential positive queries to bounded-variable fragments. In Dan Suciu, Sebastian Skritek, and Christoph Koch, editors, Proceedings of the 38th ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems, PODS 2019, Amsterdam, The Netherlands, June 30 - July 5, 2019, pages 353-364. ACM, 2019. URL: https://doi.org/10.1145/3294052.3319693.
  5. Hans L. Bodlaender. A linear-time algorithm for finding tree-decompositions of small treewidth. SIAM J. Comput., 25(6):1305-1317, 1996. URL: https://doi.org/10.1137/S0097539793251219.
  6. Hans L. Bodlaender, Pål Grønås Drange, Markus S. Dregi, Fedor V. Fomin, Daniel Lokshtanov, and Michal Pilipczuk. An o(c^k n) 5-approximation algorithm for treewidth. In 54th Annual IEEE Symposium on Foundations of Computer Science, FOCS 2013, 26-29 October, 2013, Berkeley, CA, USA, pages 499-508. IEEE Computer Society, 2013. URL: https://doi.org/10.1109/FOCS.2013.60.
  7. Simone Bova and Hubie Chen. The complexity of width minimization for existential positive queries. In Nicole Schweikardt, Vassilis Christophides, and Vincent Leroy, editors, Proc. 17th International Conference on Database Theory (ICDT), Athens, Greece, March 24-28, 2014, pages 235-244. OpenProceedings.org, 2014. URL: https://doi.org/10.5441/002/icdt.2014.25.
  8. Simone Bova and Hubie Chen. How many variables are needed to express an existential positive query? Theory Comput. Syst., 63(7):1573-1594, 2019. URL: https://doi.org/10.1007/s00224-018-9884-z.
  9. Ashok K. Chandra and Philip M. Merlin. Optimal implementation of conjunctive queries in relational data bases. In John E. Hopcroft, Emily P. Friedman, and Michael A. Harrison, editors, Proceedings of the 9th Annual ACM Symposium on Theory of Computing, May 4-6, 1977, Boulder, Colorado, USA, pages 77-90. ACM, 1977. URL: https://doi.org/10.1145/800105.803397.
  10. Hubie Chen. On the complexity of existential positive queries. ACM Trans. Comput. Log., 15(1):9:1-9:20, 2014. URL: https://doi.org/10.1145/2559946.
  11. Hubie Chen. The tractability frontier of graph-like first-order query sets. J. ACM, 64(4):26:1-26:29, 2017. URL: https://doi.org/10.1145/3073409.
  12. Hubie Chen and Víctor Dalmau. Decomposing quantified conjunctive (or disjunctive) formulas. SIAM J. Comput., 45(6):2066-2086, 2016. URL: https://doi.org/10.1137/140957378.
  13. Víctor Dalmau, Phokion G. Kolaitis, and Moshe Y. Vardi. Constraint satisfaction, bounded treewidth, and finite-variable logics. In Pascal Van Hentenryck, editor, Principles and Practice of Constraint Programming - CP 2002, 8th International Conference, CP 2002, Ithaca, NY, USA, September 9-13, 2002, Proceedings, volume 2470 of Lecture Notes in Computer Science, pages 310-326. Springer, 2002. URL: https://doi.org/10.1007/3-540-46135-3_21.
  14. Georg Gottlob, Nicola Leone, and Francesco Scarcello. Hypertree decompositions: A survey. In Jirí Sgall, Ales Pultr, and Petr Kolman, editors, Mathematical Foundations of Computer Science 2001, 26th International Symposium, MFCS 2001 Marianske Lazne, Czech Republic, August 27-31, 2001, Proceedings, volume 2136 of Lecture Notes in Computer Science, pages 37-57. Springer, 2001. URL: https://doi.org/10.1007/3-540-44683-4_5.
  15. Georg Gottlob, Nicola Leone, and Francesco Scarcello. Robbers, marshals, and guards: game theoretic and logical characterizations of hypertree width. Journal of Computer and System Sciences, 66(4):775-808, 2003. URL: https://doi.org/10.1016/S0022-0000(03)00030-8.
  16. Martin Grohe. The complexity of homomorphism and constraint satisfaction problems seen from the other side. J. ACM, 54(1):1:1-1:24, 2007. URL: https://doi.org/10.1145/1206035.1206036.
  17. Martin Grohe, Thomas Schwentick, and Luc Segoufin. When is the evaluation of conjunctive queries tractable? In Jeffrey Scott Vitter, Paul G. Spirakis, and Mihalis Yannakakis, editors, Proceedings on 33rd Annual ACM Symposium on Theory of Computing, July 6-8, 2001, Heraklion, Crete, Greece, pages 657-666. ACM, 2001. URL: https://doi.org/10.1145/380752.380867.
  18. Phokion G. Kolaitis and Moshe Y. Vardi. Conjunctive-query containment and constraint satisfaction. J. Comput. Syst. Sci., 61(2):302-332, 2000. URL: https://doi.org/10.1006/jcss.2000.1713.
  19. Maxwell Herman Alexander Newman. On theories with a combinatorial definition of "equivalence". Annals of mathematics, pages 223-243, 1942. Google Scholar
  20. Christos H. Papadimitriou. Computational complexity. Addison-Wesley, 1994. Google Scholar
  21. Ryan Williams. Faster decision of first-order graph properties. In Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, pages 80:1-80:6. ACM, 2014. URL: https://doi.org/10.1145/2603088.2603121.
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