Tools for Datalog boundedness

Abstract
A given Datalog program is bounded if its dependent of the input database) is interesting because depth of recursion is independent of the input database. Deciding boundedness is a basic task for the analysis of these database logic programs. We develop a number of new tools for proving (un)decidability of various kinds of boundedness for programs with: a small arity of the recursively defined predicates or a small number of rules. (1) We use the mortality problem of Turing machines to show that uniform boundedness is undecidable for arity 3 predicates and for arity 1 predicates when # is also allowed. (2) We use a single rule polymorphically to show that program (predicate) boundedness is undecid- able for two linear rules (one rule and a projection), one initialization rule and small arity predicates. (3) We use the theory of semi-linear sets to sharpen the conditions under which one can decide boundedness for one linear rule, any initialization rules and any arity predicates.

This publication has 14 references indexed in Scilit: