Monadic datalog on trees

Among logics with fixpoint capabilities, one of the most prominent is datalog, obtained by adding fixpoint operator to unions of conjunctive queries (positive existential first order formulae). Datalog originated as a declarative programming language, but later found many applications in databases as a query language. Classical static analysis problems of containment, equivalence and boundedness have been widely studied on arbitrary structures. All these problems are undecidable. Since these problems are subtasks in important data management tasks, like query minimization, data integration, or data exchange, the negative results for full datalog fuel interest in restrictions. For example when restricting to monadic datalog programs the mentioned problems become decidable. It is also known that the containment problem is decidable for monadic datalog programs on trees. Recently datalog has been studied on tree databases that carry labels from an infinite alphabet that can be tested for equality. I will present some of our new results focusing on the containment problem for monadic datalog. This problem is in general undecidable but I will show some decidable fragments.