Regular Path Queries and Modal Constraints: Decidability of Query Containment under a Graph Database Schema

Niniejsza rozprawa rozwiązuje problem zawierania zapytań w obecności więzów, dla zapytań UCRPQ (ang. unions of conjunctive regular path queries) i więzów wyrażonych przy użyciu rozszerzenia logiki deskrypcyjnej ALC, która może być postrzegana jako wariant notacyjny logiki (multi)modalnej; główny wynik pracy dotyczy logiki ALCOreg, rozszerzającej ALC o stałe i wyrażenia regularne.

Przedstawione badania teoretyczne leżą na pograniczu teorii baz danych – w szczególności grafowych baz danych – oraz reprezentacji wiedzy i wnioskowania. Problem jest rozważany w standardowej semantyce zbiorowej, z naturalnym – i bardziej wymagającym – założeniem, że rozważane bazy danych są skończone. Uzyskany wynik znacząco zawęża lukę pomiędzy rozstrzygalnością a nierozstrzygalnością dla tego problemu: jest to, jak się zdaje, pierwszy pozytywny wynik obejmujący pełną klasę zapytań CRPQ w tym kontekście, a istnieje znany wynik nierozstrzygalności (Rudolph 2016) dotyczący tego samego języka zapytań i innego rozszerzenia logiki ALC, znanego jako ALCOIF.

Kluczowe idee dowodu bazują na moich publikacjach; używane techniki zostały gruntownie przeprojektowane, ujednolicone i uogólnione na potrzeby tej rozprawy. W najbardziej technicznych częściach rozprawy pracuję z grafami skierowanymi, używając typów bisymilarności drzew (częściowych rozwinięć grafu) do reprezentacji więzów modalnych, oraz typów homomorfizmu grafów do rozumowania o zapytaniach. Jest to niestandardowe: rozważany problem jest zwykle badany albo w kontekście baz danych (w teorii baz danych), albo w kontekście interpretacji (w reprezentacji wiedzy i wnioskowaniu); szczegółowo opisuję redukcję problemu do rozważanego wariantu.

Jedna z głównych konstrukcji w dowodzie opiera się na metodzie stworzonej do rozwiązania problemu wynikania zapytań w modelach skończonych w obecności przechodnich relacji (Gogacz, Ibañez-García, and Murlak 2018). Metoda ta może być postrzegana jako konstrukcja automatu na drzewach, rozpoznającego dekompozycje grafów na silnie spójne składowe; głównym wyzwaniem jest reprezentacja tych składowych w abstrakcyjny sposób, tak żeby alfabet automatu był skończony, ale umożliwiał rozłożenie informacji o więzach i zapytaniach pomiędzy składowymi. Wprowadzam też kilka innych konstrukcji podobnych do technik występujących w literaturze; w szczególności, do mało znanej konstrukcji na automatach skończonych (Hesse 2003; Bojańczyk 2009), i do procedury finite chase (Rosati 2006).

Moim priorytetem było przedstawienie opracowanych metod w przystępny sposób. Rozwiązanie problemu opisuję jako łańcuch redukcji do coraz prostszych problemów. Kluczową częścią wyniku są grafy z rangami: ich definicja, uogólnienie używanych konstrukcji w celu uwzględnienia rang, i redukcja głównego problemu do kontekstu grafów z rangami. Definiuję je jednak dopiero w rozdziale 8; niemal połowę rozprawy poświęcam wprowadzeniu głównych technik w prostszych kontekstach, żeby ułatwić ich zrozumienie. Przy przechodzeniu do trudniejszych kontekstów, wyjaśniam dlaczego wcześniejsze podejścia zawodzą, i jakie intuicje stoją za bardziej zaawansowanymi wariantami używanych technik.

Staram się przedstawiać pełne, formalne dowody. Zaletą tego podejścia jest to, że wymusza definiowanie pojęć odpowiednich nie tylko do wysokopoziomowego opisu rozwiązania, ale także do niskopoziomowych dowodów. Istotną wadą jest duża liczba nowych definicji, co jest potęgowane przez pracę w kontekście grafów, niestandardowym dla tego problemu. Aby temu zaradzić, włożyłem dużo wysiłku w opracowanie jak najprostszych definicji; uważam, że wprowadzone przeze mnie pojęcia są w zdecydowanej większości naturalne i dobrze dopasowane do rozważanych problemów.

This dissertation solves the problem of query containment under constraints for unions of conjunctive regular path queries (UCRPQs) and constraints expressed using an extension of the description logic ALC. The logic ALC can be seen as a notational variant of (multi-)modal logic; we consider the logic ALCOreg, extending ALC with constants and regular expressions.

This theoretical research lies on the border of database theory – graph databases in particular – and the field of knowledge representation and reasoning. We study the problem under the standard set semantics, in the natural – and more challenging – setting of only finite databases. The obtained result significantly narrows the decidability gap for this problem, as it appears to be the first decidability result for the full class of conjunctive regular path queries in this context, and there is a known undecidability result by Rudolph (2016) concerning the same query language and another extension of the description logic ALC, known as ALCOIF.

The core idea of the proof of the main result is based on several papers published by the author; the techniques have been heavily reworked, unified, and generalized for this dissertation. In the most technical parts of the thesis we work in the setting of directed graphs, using bisimilarity types of trees (partial unravellings) to represent modal constraints, and using homomorphism types of graphs to reason about queries. This is non-standard, as the problem is usually studied either in the setting of databases (in database theory) or in the setting of interpretations (in knowledge representation and reasoning); we describe in detail how to reduce the problem from the latter setting to ours.

One of the main constructions in the proof is based on a technique for solving the finite query entailment problem in the presence of transitivity by Gogacz, Ibañez-García, and Murlak (2018), which can be seen as constructing a tree automaton recognizing decompositions of graphs into strongly connected components; the main challenge is to represent the components abstractly, to keep the alphabet of the automaton finite, while being able to distribute information about constraints and queries over these components. Some other constructions presented in this thesis bear strong similarities to several other techniques existing in the literature; most notably, a little-known construction on deterministic finite automata (Hesse 2003; Bojańczyk 2009), and the finite chase procedure by Rosati (2006).

The focus of the dissertation is describing the developed techniques in an accessible way. The solution is organized as a chain of reductions to simpler problems. A crucial part of the result is describing the setting of ranked graphs, showing that the main problem can be reduced to reasoning in this setting, and generalizing the techniques to this setting. However, this is done only in Chapter 8; nearly half of this dissertation is devoted to introducing the core techniques in simpler settings, to make them easier to understand. When moving to increasingly difficult settings, we make an effort to discuss why simpler approaches fail, and what the intuitions behind their more advanced variants are.

We strive to provide full, formal proofs. The advantage of this approach is that it forces us to develop notions that are suitable not just for high-level descriptions, but also for low-level arguments. A notable downside is a large number of new definitions, which is amplified by the fact that we work in the setting of graphs, non-standard for this problem. To circumvent this, a lot of effort has been put into keeping the definitions as simple as possible; the author believes that the introduced concepts are, in the vast majority, natural and well-suited to the considered problems.