PREDICATE BOUNDEDNESS OF LINEAR MONADIC DATALOG IS IN PSPACE

Datalog programs, are a special case of logic programs without function symbols. Detection of boundedness permits Datalog programs to be optimized by the elimination of recursion. To determine whether a predicate is bounded in a Datalog program is known to be undecidable. However, previous work (Cosmadakis et al., 20th ACM Symposium on the Theory of Computing, 1988) has show that for monadic Datalog, this problem is decidable, with upper and lower bounds of EXPSPACE and PSPACE respectively for linear monadic programs. We establish that predicate boundedness for linear monadic programs is in fact in PSPACE, yielding a tight bound for this problem.^a