Eliminating Recursion from Monadic Datalog Programs on Trees

TL;DR

This paper explores the decidability of eliminating recursion in monadic datalog programs on labeled trees, showing undecidability in general but decidability under certain restrictions, and analyzing related equivalence problems.

Contribution

It demonstrates the undecidability of boundedness in general and identifies conditions under which this problem becomes decidable, advancing understanding of datalog program optimization.

Findings

Boundedness problem is undecidable for monadic datalog on trees.

Decidability is regained when descendant relation is disallowed.

Equivalence to a given nonrecursive program is decidable under certain restrictions.

Abstract

We study the problem of eliminating recursion from monadic datalog programs on trees with an infinite set of labels. We show that the boundedness problem, i.e., determining whether a datalog program is equivalent to some nonrecursive one is undecidable but the decidability is regained if the descendant relation is disallowed. Under similar restrictions we obtain decidability of the problem of equivalence to a given nonrecursive program. We investigate the connection between these two problems in more detail.