1 |
Static analysis of monadic datalog on finite labeled treesFrochaux, André 06 March 2017 (has links)
Die vorliegende Dissertation beinhaltet eine umfassende Untersuchung der Entscheidbarkeit und Komplexität der Probleme, die sich durch eine statische Analyse von monadischem Datalog auf endlichen gefärbten Bäumen stellen. Statische Analyse bedeutet hierbei Anfrageoptimierung ohne Blick auf konkrete Instanzen, aber mit Rücksicht auf deren zugrunde liegende Struktur. Im Kern beinhaltet dies die Lösung der drei folgenden Probleme: das Leerheitsproblem (die Frage, ob eine Anfrage auf jeder Instanz ein leeres Ergebnis liefert), das Äquivalenzproblem (die Frage, ob zwei Anfragen auf jeder Instanz das gleiche Ergebnis liefern) und das Query-Containment-Problem (die Frage, ob das Ergebnis der einen Anfrage auf jeder Datenbank im Ergebnis der anderen Anfrage enthalten ist). Von Interesse ist dabei, ob die Fragen für eine gegebene Anfragesprache entscheidbar sind und wenn ja, welche Komplexität ihnen innewohnt. Wir betrachten diese Probleme für monadisches Datalog auf unterschiedlichen Repräsentationen für endliche gefärbte Bäume. Hierbei unterscheiden wir zwischen ungeordneten und geordneten Bäumen, welche die Achsen child bzw. firstchild und nextsibling und deren Erweiterung um die descendant-Achse nutzen. Außerdem unterscheiden wir Alphabete mit und ohne Rang. Monadisches Datalog ist eine Anfragesprache, die in Abhängigkeit vom gewählten Schema die Ausdrucksstärke der monadischen Logik zweiter Stufe (MSO) erreicht und dennoch effizient ausgewertet werden kann. Wir zeigen, dass unter in der Datenbanktheorie üblichen Mengensemantik die drei genannten Probleme für alle Schemata ohne descendant-Achse EXPTIME-vollständig sind und lösbar in 2EXPTIME, falls die descendant-Achse involviert ist. Eine passende untere Schranke wird für fast alle Schemata gezeigt. Unter Multimengensemantik lassen sich die obigen Ergebnisse für das Leerheitsproblem übertragen, während das Query-Containment-Problem für alle betrachteten Schemata unentscheidbar ist. / This thesis provides a comprehensive investigation into the decidability and complexity of the fundamental problems entailed by static analysis of monadic datalog on finite labeled trees. Static analysis is used for optimizing queries without considering concrete database instances but exploiting information about the represented structure. Static analysis relies on three basic decision problems. First, the emptiness problem, whose task is to decide whether a query returns the empty result on every database. Second, the equivalence problem asking if the result of two given queries always coincides on every database. And finally, the query containment problem where it is to decide whether on every database a given query produces a subset of the results of a second given query. We are interested in finding out whether these problems are decidable and, if so, what their complexity is. We consider the aforementioned problems for monadic datalog on different representations of finite labeled trees. We distinguish unordered and ordered trees which use the axis child, as well as the axes firstchild and nextsibling, respectively. An extension of the schemas by the descendant-axis is also considered. Furthermore, we distinguish ranked and unranked labeling alphabets. Depending on the schema, the query language monadic datalog can reach the expressive power of monadic second order logic but remains efficiently evaluable. Under set semantics, we show EXPTIME-completness for all used schemas where the descendant-axis is omitted. If the descendant-axis is involved, we present an algorithm that solves the problem within 2-fold exponential time. A matching lower bound is proven for virtually all schemas. Finally, we prove that the complexity of the emptiness problem of monadic datalog on finite trees under bag semantics is the same as under set semantics. Furthermore, we show that the query containment problem of monadic datalog under bag semantics is undecidable in general.
|
Page generated in 0.0445 seconds