Tools for datalog boundedness

Abstract

A given Datalog program is bounded if its 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 undecidable 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.