Frontiers of tractability for recursive queries

Niniejsza praca jest poświęcona językom zapytań z rekurencją, dla których klasyczne problemy decyzyjne są na granicy rozstrzygalności. Językami zapytań są programy datalogu i rozszerzenia fragmentów logiki pierwszego rzędu, w szczególności fragmentu z dwiema zmiennymi FO2. Analizowane struktury są skończone, zazwyczaj interpretowane jako skończone słowa lub skończone drzewa.Na ogólnych strukturach zajmujemy się FO2 rozszerzoną o operator deterministycznego domknięcia przechodniego. Problem spełnialności jest nierozstrzygalny, ale pokazujemy, że jeśli w sygnaturze jest tylko jedna relacja binarna to problem spełnialności staje się rozstrzygalny. Modele dla formuł w tej logice mają pewne cechy struktury drzewiastej, dlatego interesująca wydaje się logika FO2 na drzewach.Przeprowadzamy szczegółową analizę problemu spełnialności dla FO2 na drzewach.Następnie zajmujemy się problemami zawierania, równoważności i ograniczoności dla monadycznych programów datalogu na drzewach z etykietami wziętymi z nieskończonego alfabetu. Pokazujemy, że w ogólności wszystkie te problemy są nierozstrzygalne i analizujemy fragmenty programów monadycznego datalogu.Interesują nas programy bez potomka, programy liniowe i programy zniżkowe. Najważniejsze wyniki to: problem zawierania i ograniczoności są rozstrzygalne dla programów bez potomka na drzewach urangowanych; zawieranie jest rozstrzygalne dla programów zniżkowych na nieurangowanych drzewach; oraz zawieranie jest rozstrzygalne dla liniowych programów bez potomka na nieurangowanych drzewach.

This thesis is a study of query languages with recursion for which classical decision problems are on the border of tractability or decidability. The query languages are datalog programs and extensions of weak fragments of first order logic, in particular the two-variable fragment FO2. The analyzed structures are finite, usually interpreted as finite words or finite trees.On arbitrary structures we analyze FO2 extended with the deterministic transitive closure. The satisfiability problem was known to be undecidable, but we show that when the signature has only one binary relation then satisfiability becomes decidable. The models for formulas in this fragment have tree-like structures, which brings attention to FO2 on trees.We provide a detailed analysis of the satisfiability problem for FO2 on trees.Then we investigate containment, equivalence and boundedness problems for monadic datalog programs on trees with labels taken from an infinite alphabet. We show that all these problems are undecidable in general and analyze some fragments of monadic datalog programs. We are interested in child-only programs, linear programs and downward programs. The most important results are: containment and boundedness problems are decidable for child-only programs on ranked trees; containment is decidable for downward programs on unranked trees; and containment is decidable for linear child-only programs on unranked trees.