Achilles, turtle, and undecidable boundedness problems for small DATALOG programs

DATALOG is the language of logic programs without function symbols. It is considered to be the paradigmatic database query language. If it is possible to eliminate recursion from a DATALOG program then it is bounded. Since bounded programs can be executed in parallel constant time, the possibility of automatized boundedness detecting is believed to be an important issue and has been studied in many papers. Boundedness was proved to be undecidable for different kinds of semantical assumptions and syntactical restrictions. Many different proof techniques were used. In this paper we propose a uniform proof method based on the discovery of, as we call it, the Achilles-Turtle machine, and make strong improvements on most of the known undecidability results. In particular we solve the famous open problem of Kanellakis showing that uniform boundedness is undecidable for single rule programs (called also sirups). This paper is the full version of [J. Marcinkowski, Proc. 13th STACS, Lecture Notes in Computer Science 1046, pp. 427-438], and [J. Marcinkowski, 11th IEEE Symposium on Logic in Computer Science, pp. 13-24].