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].
Introduction
.
1.1.

Introduction

. The query relation R, that answers, for a given directed
graph (database), if that is possible, for given two nodes, to reach one of them from
the other in an odd number of steps, is not a first order one. That is because of lack
of recursion in the first order logic. This observation led to the study of DATALOG
(DATAbase LOGic) programs which combine existential positive first order logic with
recursion. For example the relation R can be defined by an "odd-distance" DATALOG
program:
(i) R(X;Y ):- E(X;Y
where E is the edge relation of the graph. E is so called extensional predicate
we treat it as an input and are not able to prove new facts about it. R is the
output, or intensional predicate (IDB). The program proves facts about it. The first
rule is an initialization rule: it has only the extensional predicate in the body. But
the second rule contains the intensional predicate among its premises, so it can be
used recursively and deep proofs can be constructed. It is clear that if in some graph
there is a path from an element A to B of an odd length n then to prove R(A; B) for
Supported by the KBN grant 8T11C02913
y jma@tcs.uni.wroc.pl, Institute of Computer Science, Wroc/law University, ul Przesmyckiego 20,
J. MARCINKOWSKI
such elements a proof of a depth about log n may be needed. So in huge databases
arbitrarily deep proofs are necessary to evaluate the program.
On the other hand, consider a program which computes the "has 3-tail" query:
(iii) 1TAIL(Z):- E(Z; X).
(v) 3TAIL(Z):- 2TAIL(Y ); E(Z; Y ).
If 3TAIL(A) is provable for some A then there exists a proof of the fact which
is not deeper than 3, regardless of the number of elements in the database. 1TAIL,
2TAIL and 3TAIL are IDB predicates and the second and third rules are recursive.
But in fact, the recursion can be eliminated at all from the last program. It is possible
to write an equivalent one where only proofs of deep 1 will be necessary:
The recursion can be eliminated from a given program, and the program is equivalent
to a first order query if and only if there is an a priori upper bound on the
depth of the proofs needed to evaluate queries, and so every fact that can be derived
by the program, can be derived in constant time (in parallel, with polynomially many
processors) independent of the size of the database (this equivalence was proved in
[3], the "if" direction is nontrivial). Such programs are called bounded.
1.2. Previous works and our contribution. The problem of distinction
whether a given DATALOG program is bounded or not, is important for DATALOG
queries optimization, but is, in general, undecidable. Sufficient conditions for boundedness
were given in [17], [10], [18] and [19]. The decidability-undecidability border,
for cases of different syntactical restrictions and semantical assumptions has been
studied in [20], [5], [2], [6], [8], [9], [24], [23].
The syntactical restrictions considered were: number of rules or of recursive rules
in the program, maximal arity of the IDB symbols and linearity of rules.
The semantical assumptions concern the status of the IDB relations before the
execution of the program. If they are empty, then we deal with weak (program)
boundedness. While arbitrary relations must be considered as possible IDB inputs
then strong (uniform) boundedness is studied.
Undecidability of uniform boundedness implies undecidability of program boundedness
for fixed syntactical restrictions (with possibly some additional initialization
rules, see Section 1.7 for a discussion). The survey of previously known results ((i)-(v)
below) illustrates the difference in the level of difficulty of undecidability proofs, for
uniform and program boundedness.
Decidability has been proved for monadic programs program boundedness,
(so also for the uniform) [6], [5] and for typed single rule programs [20]. It is also
known that the program (and uniform) boundedness is decidable for programs with
single linear recursive rule if the IDB predicate is binary [24]. Moreover, program
boundedness is decidable for binary programs if each IDB predicate is defined by only
one recursive rule [23].
Undecidability has been proved for
(i) program boundedness of linear binary programs [9].
ACHILLES, TURTLE, AND SMALL DATALOG PROGRAMS 3
(ii) program boundedness of programs with one recursive rule and two initializations
[2],
(iii) Program boundedness of programs consisting of two linear recursive rules
and one initialization [9],
(iv) uniform boundedness of ternary programs [9],
(v) uniform boundedness of arity 5 linear programs [8]
Decidability of the uniform boundedness for programs consisting of only one rule
was stated as an open problem in [11], where NP-hardness of the problem was proved
and then in [2] and [12]. No undecidability results for uniform boundedness of programs
with small number of rules have been proved since then.
In this paper we give strong improvements of the results (ii)-(v) showing that:
(vi) uniform boundedness is undecidable for ternary linear programs (Section 3.1).
This improves the results (iv) and (v).
(vii) uniform boundedness is undecidable for single recursive rule ternary programs
(Section 3.3). This improves (iv).
The additional improvement is, that our program is syntactically simpler: the
recursive rule is quasi-linear, which means that, generally speaking, it has a form:
where I and J are intensional predicates. Since it is the only recursive rule, the
proof from the program is a tree with only one (possibly) long branch.
Notice that in (vi) and (vii) we still allow a number of initializations so the results
hold also for program boundedness.
(viii) uniform and program boundedness are undecidable for programs consisting
of one linear recursive rule and one initialization (Section 4.3).
Since program boundedness is clearly decidable for programs consisting of one
rule the result (viii) closes the number/linearity of rules classification for program
boundedness. It is a strong improvement of (ii) and (iii).
Finally, in Section 4.5 we solve the problem of Kanellakis showing that:
(ix) uniform boundedness of single rule programs is undecidable.
1.3. The Method. While different techniques were used in the proofs of the
results (i)-(v) (reduction to the halting and mortality problems of a Turing Machine,
reduction from the halting problem of a two counters machine, syntactical reduction
of an arbitrary DATALOG program to a single recursive rule program), we develop
for all our results a universal method, based on an encoding of Conway functions. We
have learned about Conway functions from the paper of Philippe Devienne, Patrick
Leb'egue and Jean-Christophe Routier [7] , who used them to prove undecidability of
the, so called, "cycle unification". We feel that our paper would not have been written
without their previous work. Our encoding is nevertheless quite different from the
one in [7]: the first difference is that a language with functions was used there.
We construct, as we call it, Achilles-Turtle machine, a variant of Turing machine.
Next, we use a version of the Conway theorem to prove that what we constructed is
really a universal machine. Then we encode the Achilles-Turtle machine with DATALOG
programs. Due to particular simplicity of Achilles-Turtle machine (one is really
tempted to claim that it is the simplest known universal machine) it is possible to
encode it with syntactically very small DATALOG programs. We believe that this is
not the last time that Achilles-Turtle machine is used in undecidability proofs.
4 J. MARCINKOWSKI
We combine the Conway functions method with the technique of using a binary
EDB relation as an order: if there is a chain long enough in the relation then we can
think that it represents a tape of the machine. If there is no such chain then proofs
are not too long. This method goes back to [9] and [8].
1.4. Open Problems. While the classification is finished for program boundedness
the following syntactical restrictions still give interesting open problems concerning
decidability of uniform boundedness:
(i) binary programs,
(ii) linear binary programs,
(iii) programs consisting of a single linear rule.
We do not know any example of syntactical restrictions for which uniform boundedness
would be decidable and program boundedness not. It seems that the most
likely candidate for the example is the class of linear binary programs. Program
boundedness is known to be undecidable for the class.
1.5. Preliminaries. A DATALOG program is a finite set of Horn clauses (called
rules) in the language of first order logic without equality and without functions.
The predicates, used in the program, but only in the bodies of the rules, are called
extensional predicates or EDB. A predicate which occurs in a head of some rule is
called intensional or IDB. A rule is called recursive if an IDB predicate occurs in its
body. A rule which is not recursive is an initialization rule. A recursive rule is linear
if it has only one occurrence of IDB in the body. A program is linear if each of its
recursive clauses is linear. Arity of a DATALOG program is the highest arity of the
IDB predicates used.
So, for example, in the two programs of Section 1.1 the predicate E is extensional,
and all the other predicates are intensional. The rules (i) and (iii) are initializations.
Rules (ii), (iv) and (v) are recursive. Rules (iv) and (v) are linear and so the "has
3 tail" program is linear. It is also monadic, while the "odd-distance" program is
binary.
A database is a finite set of ground atomic formulas. A derivation (or a proof) of
a ground atomic formula A, from the program P and the database D, is a finite tree
such that: (i) each of its nodes is labeled with a ground atomic formula, (ii) each leaf
is labeled with an atom from D, (iii) for each non-leaf node there exists a rule R in
the program P and a substitution oe, such that oe of the head of R is the label of the
node and the substitutions of the body of R are the labels of its children, (iv) A is
the label of the root of the tree. The depth of the proof is the depth of the derivation
tree.
Instead of writing proof from the program P in the database D we use the expression
simply proof if the context is clear.
Notice that if P is a linear program then a P-proof is a sequence of ground atomic
formulas. In such case we use the word length for the depth of the proof.
In general, a program P is bounded if for every database D, if an atom can be
proved from P and D then it has a proof not deeper than a fixed constant c.
Different conventions concerning the input and output of a DATALOG program
correspond to different definitions of boundedness: predicate, program and uniform
boundedness are studied. A program is predicate bounded , with respect to a fixed
predicate PRE, if there is a constant c such that for every database D, such that there
are no facts about IDB predicates in D, and for every ground atom
if the atom has a proof from P and D then it has a proof not deeper than c. This
definition reflects the situation when the EDB predicates are the input and only one
ACHILLES, TURTLE, AND SMALL DATALOG PROGRAMS 5
predicate is the output of the program. A program P is program bounded if it is
predicate bounded for all IDB predicates.
A program is uniformly bounded if there is a constant c such that for every
database D, (here we do not suppose that the IDB predicates do not occur in D)
and for every ground atom A if the atom has a proof from P and D then it has a
proof not deeper then c. Here all the predicates are viewed as the input and as the
output of a program.
1.6. Example: Program Boundedness vs. Uniform Boundedness. To
make the difference between program boundedness and uniform boundedness clear
for the reader we give an example of a program which is bounded but not uniformly
bounded
The signature of the program consists of one extensional predicate E and one
intensional predicate I . Both the predicates are binary.
The rules are:
It is convenient to think that E is a graph, and I is a kind of a pebble game:
by the initialization rule (i) we can start the game by placing both the pebbles in
any node which has a tail of length at least 2. By the rule (iii) we do not need to
distinguish between the pebbles. By rules (iv) and (v) we can always move one of the
pebbles to a neighbouring node, and finally, if the two pebbles meet in node that is
the end of a tail of length at least two then we can by the rule (ii), move the pebbles
to any two nodes.
We prove that the program is program bounded but not uniformly bounded:
Lemma 1.1. For a database D such that the input predicate I is empty, either
there are no proofs in D or for each pair D;E of elements of D the fact I(D; E) can
be proved in no more than 7 derivation steps
Proof. We consider two cases:
case 1: There are elements in D such that E(A; B) and E(B;C) hold.
Then, in the first step, we use the rule (i) to prove I(A; A). Then, using twice the
rule (v) we get I(C; A). Then use the rule (iii) to get I(A; C) and twice the rule (v)
to get I(C; C). Finally, the rule (ii) can be used to derive I(D; E).
case 2: There are no such elements in the database D. Then, since I is
given as empty, no proofs at all are possible.
The structure of the proof of the Lemma 1.1 above, as well as the structure of the
program itself, is a good illustration of one of the ideas of the proofs in Sections 3 and
4. The program contains some initialization rule (rules) which allows to start a kind
of game, or computation, if only there exists a substructure of required form in the
database. Then, if there is enough of facts in the database we can proceed with the
computation and, when it terminates, use an analogon of the rule (ii) to "flood" the
6 J. MARCINKOWSKI
database. Otherwise, if there is no enough of facts then only short proofs are possible
(or no proofs at all, as in the example).
Lemma 1.2. For each constant c there exist a database D with nonempty input
predicate I, and elements of D such that I(A; B) is P-provable, but the shortest
proof of the fact requires more than c steps.
Proof. The database contains the elements: C and the following
facts: E(C
We will show that the fact I(C 2c ; C 1 ) is provable, and the shortest proof
has exactly steps. First we show that such a proof exists: in the k'th step use
the already proved fact derive I(C The rule used in the k'th
derivation step is (v) if k is odd and (iv) if k is even.
To show that shorter proofs are not possible notice that only the bodies of the
rules (iii)-(v) can be satisfied in D, and so only those rules can be used.
Define the distance between nodes of D as follows: the distance between A and A
is 0, and the distance between A and B is less or equal k if and only if there exists a
node C such that either E(B;C) or E(C; B) and the distance between A and B is at
most 1. The distance between a pair of nodes A; B in D and a pair of nodes C; D
in D is defined as a sum of distances from A to C and from B to D. Now, notice that
if a fact of the form I(A; B) is derived in k steps from the fact I(C; D), and if only the
rules (iii)-(v) were used in the proof then the distance between A; B and C; D is not
greater than k. Finally, observe that the distance in D between C
1.7. Program Boundedness vs. Uniform Boundedness. Discussion.
The notions of uniform and program boundedness formalize, on the technical level,
the informal notion of boundedness. Uniform boundedness is what we need when the
program under consideration is a subprogram of a bigger one. Then, it can happen,
that the predicates that are supposed to be the output of the program are also a part
of the input. Program boundedness, on the other hand, corresponds to the view of an
entire DATALOG program as a definition of, possibly many, output predicates. This
is similar to the distinction between program and uniform equivalence of DATALOG
programs (see [21]), where again the first notion applies to entire programs, while
the second one to subprograms equivalence. It is known that program equivalence is
undecidable, while uniform equivalence is decidable [5],[21],[22]]. We can observe that
also for the case of boundedness, the uniform version, for given syntactical restrictions
is a priori "more decidable": Suppose that program boundedness is decidable
for some syntactical restrictions, and that the restrictions allow arbitrary number of
initializations. Then uniform boundedness is also decidable for the restrictions. To
see that consider a program P over a signature with IDB symbols I i , where 1
Let Q be the program P with its signature enriched with new EDB symbols
and for each i the arity of E i is equal to the arity of I i , and with k new
rules:
I
It is easy to see that Q is program bounded if and only if P is uniformly bounded.
So we reduced the decision problem of the uniform boundedness of P to the problem
of program boundedness of the program Q.
The survey of results gives an evidence that it is more difficult to prove undecidability
of uniform boundedness than undecidability of program boundedness, the
argument above shows that there are reasons for that. But on the other hand we
do not know any example of syntactical restrictions for which uniform boundedness
ACHILLES, TURTLE, AND SMALL DATALOG PROGRAMS 7
would be decidable and program boundedness not. The most likely candidate for the
example is the class of linear binary programs. Program boundedness is undecidable
for the class and decidability of uniform boundedness is open.
2. Achilles-Turtle machine.
2.1. The tool: Conway functions.
Definition 2.0. A Conway function is a function g with natural arguments
defined by a system of equations:
a
a
a
where a i ,q i are natural numbers, q i ji (that means, that i=q i is a natural number),
and q i jp for each i and (a i for each i.
For a Conway function g and given natural number N let C(g; N) be a statement
asserting that there exists a natural number i such that g i
See Section 2.3 to find a nice example giving an idea of what a Conway function.
is. Proof of the following theorem can be found in [4], in [14] or in [7].
Theorem 2.1. (Conway)
The problem:
given a Conway function g, and a natural number N . Does C(g; N) hold ?
is undecidable.
Our main tool is the following refined version of Theorem 2.1 :
Theorem 2.2.
1. There exists a computable sequence fgn g of Conway functions such
2)g is not recursive (is r.e. complete).
(ii) For each g n , if a i and q i are coefficients from the definition of the function
2.
(iii) For each g n , if there are such
2. There exists a universal Conway function g, such that
(i) the set fN : C(g; 2 N )g is not recursive (is r.e. complete).
(ii) if a i and q i are coefficients from the definition of the function g then
(a 2.
(iii) For each N , if there are such
Proof.
1. It is known that the problem: given a finite automaton with 2 counters, does
the computation starting from fixed beginning state, and from empty counters
reach some fixed final state is undecidable, even if we require that the final
state can be reached only if the both counters are empty (read the remark in
the end of this section to see what precisely we mean by a finite automaton
with 2 counters).
For a given automaton A of this kind we will construct a Conway function g A
which satisfies conditions (ii) and (iii) of the theorem and such that C(gA ; 2)
holds if and only if the computation of A reaches the final state. First we
8 J. MARCINKOWSKI
need to modify A a little bit: we construct an automaton B which terminates
if and only if A terminates and which satisfies the following conditions:
(iv) the second counter of B can be increased only if the first counter is
decreased in the same computation step,
(v) the states of B are numbered. If any of the counters is increased in the
computation step when the state s i is being changed into s j then
The details of the construction of B are left as an easy exercise. The hint is
that all what must be done is adding a couple of new states. For example if
there is an instruction of A which increases the second counter and keeps the
first unchanged, it must be substituted by two instructions: first of them only
increases the first counter and changes the state into a new one, the second
increases the second counter and decreases the first.
Now, suppose that the states of the automaton B are s
is the beginning state. Let be an increasing sequence of primes
such that (such a sequence can be found for each k, since
the density of primes around n is c= log n). We encode the configuration of
B:
state is s i , the first counter contains the number n and the second counter
contains m
as the natural number 2 It is easy to notice that, if x and y are codes
of two subsequent configurations of B then y=x depends only of the remainder
x (mod p) where and that y=x - 2. So we can define the
required Conway function. To define the first step properly we put a
and which is the code of the beginning configuration.
We put also a p f
reach 1 in the iteration of the function
next to the one when the code of the final configuration is reached.
2. We use the well known fact that there exists a particular finite automaton with
counters for which the problem does the computation starting from a fixed
beginning state s b , given first counter, and empty second counter, reach the
configuration of some fixed final state s f and empty counters is undecidable.
Then the proof is similar as of (i). To start the computation properly we
put a all such even i that p j ji does not hold for any
for each N it holds that g(2 N . The last is the code
of the beginning configuration.
Remark: Automata with counters. Our notion of a finite automaton with
two counters is similar to the one in Kozen's book [13], with the difference that
we assume that the automaton has no input tape. Since two counter automata (with
read-only input tape) are as powerful as Turing machines the problem whether a given
automaton of this kind will terminate for given input is undecidable. But, for each
input separately, we can hide the input in the finite control of the automaton (in fact
the input tape is a finite object for each input). So also the problem whether a given
automaton without input tape will terminate, when started from a fixed beginning
state and from empty counters is undecidable. Now we show, as it is needed in
the proof of the second claim of Theorem 2.2, that there exists a particular finite
automaton with 2 counters for which the problem does the computation starting from
a fixed beginning state s b , given first counter, and empty second counter, reach the
configuration of some fixed final state s f and empty counters is undecidable. First
observe that there exists an automaton as required but with 3 counters: it is universal
ACHILLES, TURTLE, AND SMALL DATALOG PROGRAMS 9
Turing machine with the contents of the part of the tape left of the head remembered
on one counter, right on the head on the second counter, and with auxiliary third
counter needed for operating the first two. Then use the standard techniques to
encode the three counters as two. See [13] for details.
Convention 2.3. Since now we consider only Conway functions g n where
existence was proved in Theorem 2.2.i. In particular we assume that the
claims (ii) and (iii) from Theorem 2.2.i. hold.
2.2. Achilles-Turtle machine. For a given Conway function g and given input
N we will construct an Achilles-Turtle machine, which will compute the subsequent
iterations of g(N ).
It is a variant of a multi-head Turing Machine, with read-only tape. Each cell
of the tape is coloured with one of the colours K 0 , K (where p is as in
the definition of the function g). If the cell X is coloured with the colour K i (we
denote the fact as K i (X)) and the cell S(X) (S is a successor function on the tape)
is coloured with K j then p). The colour K 0 will be called white and
called red.
There are 3 heads. The first of them symbolizes Achilles. The second is the
Turtle. The third is called Guide. The transition rules will be designed in such a way,
that the heads will never go left. Achilles and Guide will move right in each step of
the computation. Achilles will try to catch the Turtle.
The configuration of the machine is described by the positions of the heads. In the
beginning of the computation Achilles is in some arbitrary white cell X on the tape.
The Turtle and Guide are both is in the cell S N (X). So the beginning configuration is:
CON(X;S N (X); S N (X)).
Where again S is the successor function on the tape.
The idea is, that the computation can reach a configuration of a form
or Achilles can be exactly k cells behind the Turtle, if g i
In each computation step the heads of the machine move according to one of the
following transition rules
(R
since a i =q
Rules (R i ) are run rules and rules (J i ) are jump rules. Configurations of the form
are called special.
See Section 2.3 for a nice example of Achilles-Turtle machine. The following easy
lemma gives an intuition of how the computation of the machine proceeds:
Lemma 2.4.
(i) If, in some configuration of the machine, the Turtle is in the cell X and the
Guide is in Y then
(ii) If, in some configuration of the machine, the Turtle is in the cell X and
Achilles is in some S k (X) where none of the jump rules will be used later
J. MARCINKOWSKI
in the computation.
(iii) Suppose that in some configuration of the machine Achilles is in some cell
X, Turtle is in some S t (X) and the Guide is in S r (X). If one of the jump rules can
be used later, then
(iv) A special configuration can only be a result of a transition done according to
one of the jump rules.
(v) Achilles is always in a white cell.
(vi) If in some configuration of the machine the Guide is in the cell X then in
the next configuration he will be in S r (X) for some
Proof. (i) The claim is true for the beginning configuration and for every configuration
being a result of a use of a jump rule. The run rules move the Guide right
and keep the Turtle in his cell.
(ii) If Achilles is right of the Turtle then the jump rule can not be used. But the
run rules only move Achilles right.
(iii) follows from (i) and (ii)
(iv) By (i) the Guide can never be left of the Turtle. The run rules move him
right, so after the execution of a run rule he is right of the Turtle.
(v) He starts in a white cell and moves p cells right in each step.
(vi) That is since hold for every i (see
Convention 2.3).
Now we will formulate and prove some lemmas about the equivalence between the
behaviour of the Conway function and the result of the computation of the Achilles-
Turtle machine. Our goal is:
Lemma 2.5. The following conditions are equivalent:
(i) C(g; N) holds.
(ii) The Achilles-Turtle machine can reach a configuration of a form
(iii) The Achilles-Turtle machine can reach a configuration of a form
CON(A;S(A);S(A)).
(iv) The Achilles-Turtle machine can reach a configuration of a form
Lemma 2.6. Suppose in some special configuration of the machine Achilles is in
some cell A, and Turtle and Guide are in some
(i) after k steps the configuration will be CON(S \Gammai (T ); T
(ii) there are exactly two configurations that can be reached after k
and
Proof. (i) Each of the k steps will be done according to the rule R i . So, after k
steps Achilles will be in the cell S kp will be in S kp(a i =q i
the Turtle in T .
(ii) By (i), CON(S \Gammai (T reached after k steps. Then the rule
R i may be used once again, what leads to CON(S p\Gammai (T
the rule J i may be used. That leads to
Lemma 2.7. Suppose in some special configuration of the machine Achilles is
in the cell A, and Turtle and Guide are in some
p. Then the following two conditions are equivalent:
ACHILLES, TURTLE, AND SMALL DATALOG PROGRAMS 11
(i) it is possible to reach a special configuration CON(X;S l (X); S l (X)) as the
next special configuration.
Proof. By Lemma 2.6 (ii) the configuration after k steps will be either
or
In the first case Achilles will be already right of the Turtle and, by Lemma 2.4
(ii),(iv), a special configuration will not be reached any more.
To prove the equivalence we show that the configuration reached in the second
case is just of the form
CON(X;S g(m) (X); S g(m) (X)).
In fact:
CON(X;S g(m) (X); S g(m) (X)).
Lemma 2.8. The following two conditions are equivalent:
(i) The Achilles-Turtle machine can reach a configuration of the form
CON(X;S l (X); S l (X)).
(ii) There exists a natural number j such that g j
Proof. The (i))(ii) implication is proved by induction on the number of special
configurations reached during the computation.
The (ii))(i) implication is proved by induction on j.
In both cases Lemma 2.7 is used for the induction step.
Proof. Of Lemma 2.5:
(i), (ii) and (iii) are equivalent by Lemma 2.8 and Convention 2.3 (claim (iii) of
Theorem 2.2.i). Clearly, (ii) implies (iv). Also (iv) implies (ii): If a configuration
reached after some number of steps, and K 1 (T ) holds, then consider
the configuration after the last step of the computation which was done according
to a jump rule (the last step when the Turtle was moved). This configuration is
2.3. Achilles-Turtle Machine. An Example. In order to give the reader an
idea of how the machine works we are going to provide a nice example of a Conway
function (or rather Conway-like function) and of the Achilles-Turtle machine built
for this function. The function g that we start from will be the well-known Collatz
J. MARCINKOWSKI
function: take a natural number, if it is even then divide it by two, if it is odd then
multiply it by three and add one. The problem if the iterations of the procedure give
finally the result 1, regardless of the natural number that we start from, is open. More
formally, in the spirit of Definition 2.0 we can define function g as;
ae
And the open problem is then whether
We do not only multiply the number, but also add 1, so this is not really a Conway
function in the sense of Definition 2.0 but we anyway find this example to be inter-
esting, and we can, and will, construct our Achilles-Turtle machine for this function:
The rules of the Example Achilles-Turtle machine
initial configuration: CON(X;S N (X); S N
transition rules:
run rules:
jump rules:
final configuration: CON(X;S(X);S(X)):
The coefficients in run rules and in the white jump rule are here calculated according
to the definitions of (R i ) and (J i ) from the beginning of Section 2.2. The left
hand side of the red jump rule is not CON(S 2 (A); S 4 (G); S 4 (G)), as it would follow
from the definition: this is the place where we add 1 form the 3n + 1.
Now suppose, for concreteness of the example, that N is 5. Then the subsequent
iterations of g are: 5, 16, 8, 4, 2, 1. The beginning configuration of the machine will
be then CON(A;S 5 (A); S 5 (A)) for some white cell A and the computation sequence
of the machine is:
CON(S 4 (X); S 5 (X); S 17 (X)) (RR?) CON(S 26 (X); S
CON(S 6 (X); S 22 (X); S 22 (X)) (RJ?) CON(S 28 (X); S
CON(S 8 (X); S 22 (X); S 23 (X)) (WR?) CON(S
CON(S 12 (X); S 22 (X); S 25 (X)) (WR) CON(S 34 (X); S 38 (X); S 38 (X)) (WJ)
CON(S 14 (X); S 22 (X); S 26 (X)) (WR) CON(S 36 (X); S 38 (X); S 39 (X)) (WR)
ACHILLES, TURTLE, AND SMALL DATALOG PROGRAMS 13
CON(S
CON(S
CON(S 20 (X); S 22 (X); S 29 (X)) (WR) CON(S 42 (X); S 42 (X); S 43 (X)) (WR)
CON(S 22 (X); S 22 (X); S
where RR means that red run rule was used to obtain the configuration, WR is
white run rule, RJ red jump rule, and WJ is white jump rule. The configurations
marked with ? are depicted below (Fig. 1).
3. Ternary programs.
3.1. The ternary linear program P.
Theorem 3.1. For each Conway function g n from Theorem 2.2.i there exists,
and can be efficiently constructed, an arity 3 linear DATALOG program P with one
IDB predicate which is uniformly bounded if and only if C(gn ; 2) holds.
The signature of the program contains one binary EDB symbol S, which is going
to serve as a kind of order for us, p monadic EDB symbols which will play as the
colours and a ternary IDB symbol CON . The program P consists of :
Transition rules (for each
Flooding rule: CON(X;Y;Z):-CON(S;T ; R); K 1 (T
where Km is understood as K i if m j i (mod p). Since S is no longer a true successor
we must explain the meaning of the S l symbols in the rules:
Notational Convention: (for example) a rule:
should be understood as:
CON(X2;Y 4; X1):-
CON(X;X1;Y
Let us explain the meaning of the rules: The transition rules are the same as in
the Achilles-Turtle machine, with the exception, that they check if the cells (nodes)
that Achilles runs over are painted properly. The flooding rule proves everything in
one step if Turtle is in a red node. The initialization allows to start the computation
in each (white) node, if there is a properly coloured piece of tape near the node.
Lemma 3.2. If C(gn ; 2) does not hold, then for each c there exists a database D
and a tuple A; of elements of D such that CON(A;T ; G) can be proved in D with
P and the proof of CON(A;T ; G) requires more than c steps.
14 J. MARCINKOWSKI
A
A
A
A
A
A
A
A
A
A
A
A
G
G
G
G
Fig. 2.1. Subsequent configurations of the example Achilles-Turtle machine
Proof. D is just a long enough S-chain (see Definition 3.4 below) with empty IDB
relation. First we prove that the flooding rule can not be used in such a database,
provided that C(gn ; 2) does not hold. Suppose it can be used. That means that
can be proved for some red T . If we follow the proof of CON(A;T ; G)
in D we will notice, that it gives a legal computation of the Achilles-Turtle machine
and that the first fact in the proof is the beginning configuration of the machine.
ACHILLES, TURTLE, AND SMALL DATALOG PROGRAMS 15
That is a contradiction by Lemma 2.5. Now, take the first element Z of the order.
By initialization we have CON(Z;S 2 (Z); S 2 (Z)). Using 2c times the run rule 2 we
get the shortest proof of the fact
CON(S 2pc
Now we are going to prove:
Lemma 3.3. If C(gn ; 2) holds then there exists c such that, in any database D,
for every tuple A; B; C of elements of D if CON(A;B;C) can be proved in D with
the program P then there exists a proof of CON(A;B;C) shorter than c steps.
Proof. Suppose holds. That means that, if we start the computation
of the Achilles-Turtle machine in a configuration CON(X;S 2 (X); S 2 (X)) then it is
possible to reach a final configuration CON(A;S(A);S(A)).
Notice, that during the computation, none of the heads will move left of X or
right of S(A). Let K be the distance between X and S(A) and let K' be the number of
steps of the computation necessary to reach the final configuration. Clearly pK'+1=
K. We are going to prove, that c=K'+2 is the proper constant.
We will need some definitions:
Definition 3.4. An S-chain of elements of a database D, is a set X
such that S(Xm ; Xm+1 ) and Km (Xm decreasing S-chain
of elements of the database D, is a set X
and Km (Xm (where Km should be understood as K
(mod p)). In both cases we say that the chain begins in X 0 .
Definition 3.5. Let k be a natural number. We say that a node W of a database
D is not k-founded if there exists a decreasing S-chain which begins in W and consists
of more than k elements. W is k-founded if such a chain does not exist.
Definition 3.6. Let k be a natural number. We say that a database D is not
k-founded if there exists an S-chain consisting of more than k elements.
Obviously, D is k-founded if such a chain does not exist.
Now we consider 2 cases:
Lemma 3.7. If D is not K-founded then for each tuple A; B; C of elements of
D the fact CON(A;B;C) can be proved and the proof requires no more then K'+2
steps.
Proof. Take X such that there exists an S-chain of length K beginning in X .
Thanks to the initialization rule CON(X;S 2 (X); S 2 (X)) is provable in D and has a
proof of length 1. Now we can pretend that the chain from X to S K (X) is a tape and
start a computation of the Achilles-Turtle machine. Since the transition rules of the
machine are rules of program P , each step of the computation can be encoded by one
step of proof. So there exists an element T of the chain such that S(T ) is red, and
can be proved after K'+1 steps. One more step (using flooding)
is needed to prove CON of every tuple after that.
Lemma 3.8. Let D be a K-founded database.
i=0 is a P-proof in D. If the flooding rule is not
used in the proof then m -K'.
i=0 be a P-proof in D, and suppose it is the shortest
possible proof of CON(Am ; Bm ; Cm ). Then the flooding rule is used at most once, for
the last step of the proof.
(iii) If CON(A;B;C) can be P-proved in D for some tuple A; B; C, the proof
requires no more than K
Proof. (i) The set A i , m) is a subsequence of an S-chain of length pm.
J. MARCINKOWSKI
(ii) Suppose that the step from
done according to the flooding rule. Then
is a shorter proof of CON(Am
(iii) It follows from (i) and (ii).
This ends the proof of Lemma 3.3 and of Theorem 3.1.
Theorem 3.9. Uniform boundedness of ternary linear DATALOG programs is
undecidable.
Proof. This follows from Theorems 2.2 and 3.1.
3.2. The arity 5 single recursive rule program R.
Theorem 3.10. For each Conway function g n from Theorem 2.2 i. there exists,
and can be efficiently constructed, an arity 5 DATALOG program R consisting of one
quasi-linear recursive rule and of some initializations, which is uniformly bounded iff
holds.
As in the previous subsection the signature of the program contains one binary
EDB symbol S, which is going to serve as a kind of order for us, p monadic EDB
symbols which will play as the colours and a ternary IDB symbol CON . There is also
additional IDB symbol STEER of arity 5. The program R consists of:
The recursive rule:
G;
Initialization "transition" rules (for each
G;
G; S d i (G); S d i (G)):-K i (S i (A)):
The initialization "flooding" rule: STEER(X;T ; Y; R; S):-K 1 (T
The initialization: CON(A;S 2 (A); S 2 (A)):-K 0 (A); K 1
Let us explain what is going on here: The triples (Achilles, Turtle, Guide) are
nodes of a graph defined on D 3 by means of order and colouring. Each proof, either
from program P or from R is a path in the graph. The graph is not given by the EDB
relations but can be defined from them by a DATALOG program without recursion.
If we want to define the vertices beginning in a node A; T ; G "on-line", when the
computation reaches the node (as in P), then we must use more than only one rule,
but the rules are linear: they read nothing more than just the information about
the EDB situation around. If we define the graph in advance (by initializations),
then one recursive rule is enough: we have a "graph accessibility" program in this
case. But the rule is only "quasi-linear ": it makes use of the additional IDB (but
not recursive) predicate STEER. If I were the reader I would ask a question here:
why the STEER predicate is not of arity 6 ? Why do not we want to hide the
rule for Achilles in the initializations and have a simpler recursive clause ? In fact,
some additional problems arise here, since we do not have a flooding rule for Achilles.
We were forced to design the recursive rule in this way because of the uniformity
ACHILLES, TURTLE, AND SMALL DATALOG PROGRAMS 17
reasons. It is crucial, that Achilles goes down the chains. Thanks to that we can say:
no long chains, no long proofs (Lemmas 3.8 and 3.12, case 1). We could write the
initializations of the hypothetical 6-ary STEER in such a way, that Achilles would
move only down the chains, while running according to the STEER facts proved by
the initializations. But we would have no control of what is given as the STEER at
the beginning.
Lemma 3.11. If C(gn ; 2) does not hold, then for each c there exists a database
D and a tuple A; B; C of elements of D such that CON(A;B;C) can be proved in D
with a program R and the proof of C(A; B; C) requires more than c steps.
Proof. As Lemma 3.2.
Lemma 3.12. If C(gn ; 2) holds then there exists a c such that, in every database
D, for every tuple A; B; C of elements of D if CON(A;B;C) can be proved in D with
R then there exists a proof of CON(A;B;C) shorter than of c steps.
Definition 3.13. If A; B; C is a tuple of elements of the database D then we
say that CON(A;B;C) is a fact about A.
Proof. of Lemma 3.12: Suppose C(gn ; 2) holds. Then there is a computation of
the Achilles-Turtle machine starting in some configuration CON(X;S 2 (X); S 2 (X))
and reaching CON(Y;S(Y ); S(Y )). The computation requires space kp (that is the
distance from X to Y is kp), for some natural k. We will consider 2 cases:
Case 1: A is 1)p-founded. Then every proof of a fact about A is no longer than
1. That is because of the Achilles' part in the recursive rule. This is analogous to
Lemma 3.8 (i).
Case 2: C is not
take V such that A = S (k+1)p (V ) and there is a chain of length (k + 1)p from
V to A. Because of the initialization rule CON(V;S 2 (V provable in D and
has a proof of length 1. Now we can pretend that the chain from V to S kp+1 (V ) is a
tape and let Achilles and Turtle play their game there. Among other rules possibly
given by the predicate STEER they have also the "standard" Achilles-Turtle machine
rules. So, after k moves the configuration CON(S kp (V
will be reached and we will be allowed to use the flooding. Every fact of the form
CON(A;B;C) will be proved in one step. So no new facts about A can be proved
later. Of course nothing new about the IDB predicate STEER can be proved after
the first step.
This ends the proof of Lemma 3.12 and of Theorem 3.10.
3.3. The ternary single recursive rule program Q.
Theorem 3.14. For each Conway function g n from Theorem 2.2.i. there exists,
and can be efficiently constructed, an arity 3 DATALOG program Q consisting of one
quasi-linear recursive rule and of some initializations, which is uniformly bounded iff
holds.
Similarly as in the previous subsection the signature of the program contains one
binary EDB symbol S, which is going to serve as a kind of order for us, p monadic
EDB symbols which will play as colours and a ternary IDB symbol CON . The graph
which was defined by a arity 5 relation in the previous section will be defined here
as an intersection of four graphs defined by ternary constraints. So, we will have
four additional ternary IDB symbols in the
language of the program. The rules of the program Q are:
The recursive rule:
J. MARCINKOWSKI
G; G 0
The initialization "constraints" rules:
(G;
For each i (0 there is a rule
(G;
For each i (0 there is a rule
For each i (0 there is a rule G; S d i (G)):
For each i (0 there is a rule
G; S p(a i
G; G 0 ):-K 1 (T
The initialization:
To prove the correctness of the construction we shall argue that the ternary relations
really define the same graph as the relation STEER of the last section. It is easy
to notice that if STEER(A;T ; G; T can be proved by one of the initializations of
G; G 0 ) and
can also be proved. For the opposite inclusion, suppose that T is not red. We first
consider the relation E G;T;T 0 . Since the Guide "does not see" how far from each other
Achilles and Guide are, the constraint allows the Turtle to stay in the same place or to
jump according to the proper jump rule. It is the relation E A;T;T 0 that decides if the
Turtle will be allowed to jump. If Achilles is far away, then the Turtle can only wait.
If Achilles is about to catch the Turtle, then the Turtle is allowed to jump (see [1])
anywhere. But, because of the relation E G;T;T 0 this "anywhere" can be only S d i (G),
for the proper i. In this way already the first two relations force the Turtle to behave
as he should.
The relation forces the Guide to move ahead. It allows the Guide to
execute his jump rule but only if the Turtle jumps together with him (this prevents
ACHILLES, TURTLE, AND SMALL DATALOG PROGRAMS 19
the danger that Guide jumps while the Turtle runs). Whatever the Turtle is doing,
the Guide is allowed to use his proper run rule. There is a danger here that Turtle
will jump, and the Guide will only run, what is not allowed by the Achilles-Turtle
machine rules. That is prevented by the relation E T;T 0 remains in the
same place then the Guide is allowed to go anywhere. But if he moves, then the Guide
must join him.
If T is red then the constraints allow the Guide and Turtle to go anywhere.
Theorem 3.15.
Uniform boundedness of single recursive rule ternary DATALOG programs is undecidable

Proof. It follows from Theorems 2.2.i and 3.14.
Remark: We could use Theorem 2.2.ii. instead of i. and get more "universal"
DATALOG programs. For example Theorem 3.1 would then have the form:
There exists an arity 3 linear DATALOG program P with one IDB predicate and
a computable sequence fp(N)g of initialization rules, such that the program P [ p(N)
is uniformly bounded if and only if C(g; n) holds, where g is the universal Conway
function from Theorem 2.2. ii.
In fact this is the form from [15]. It can not however be done in Section 4, so
we decided not to present the results in the most general versions but to preserve the
notational uniformity instead.
4. Single rule programs.
4.1. Constants: notational proviso. In Sections 4.2 - 4.5 we are going to
encode the computation of Achilles-Turtle machine into a very small number of rules
(one or two). We can not afford having a separate predicate for each colour any more.
Instead, we are going to have one binary predicate COL, and understand COL(C,A)
as "the colour of A is C". So, instead of predicates we need to have constants to name
colours.
There are no constants in DATALOG. But in fact, if we want to use some (say,
constants we can simply increase the arity of all the IDB symbols with k and write
a sequence C of variables as the k last arguments in each occurrence of
each IDB predicate in the program. This is one of the reasons why the programs in
the following sections are of high arity.
Example: The program
with constants a; b can be written as:
means "P (X; Y ) if the constants are understood as A; B".
Thanks to that we can suppose that there are constants in the language. We
will use the following constants: jump, run, joker, constants for colours: colour i ,
will be also called white, colour 1 will be red, and
colour 2 will be pink).
J. MARCINKOWSKI
4.2. The Achilles-Turtle game . In this section we will modify the description
of the Achilles-Turtle machine and define its equivalent version with only one transition
rule. To make our notation compatible with the database notation we are going
to forget about the tape, and use a kind of infinite graph instead. To distinguish, the
version of the machine will be called the Achilles-Turtle game.
The transition rules of the Achilles - Turtle Machine are indexed with three pa-
rameters: first of them is either jump or run, the remaining two are colours of the
Turtle's cell and the Guide's cell before the transition. The idea of what is going on
bellow is to treat the parameters as arguments occurring in the goals of the body of
the single rule. While solving the first four goals of the body we will substitute proper
parameters for the variables COND, TCOLOR and GCOLOR. Then the parameters
will be used to compute the positions of Achilles, Turtle and Guide after the execution
of the rule.
The following definition introduces the predicates that will be used in the construction
of the single rule. We do not hope that the reader will understand the
definition until he reads the proof of Lemma 4.2.
Definition 4.1. For a given Conway function g, as in Theorem 2.2 i. the
Achilles-Turtle graph is the relational structure G with exactly the nodes and the relations
listed below:
the nodes of G are: colour joker and an infinite
sequence of nodes c
holds for each node c i .
for each i if
COL(red; joker) holds.
(iv)
holds for each i.
holds for each i j 0 (mod p) and for each 0 -
(v)
holds for each i.
holds for each i.
holds.
(vi)
holds for all
ACHILLES, TURTLE, AND SMALL DATALOG PROGRAMS 21
holds for all
(vii)
holds
but
holds for all k.
holds for all k.
(viii)
holds
holds
(ix)
holds for each i and for each colour.
holds for each i.
holds for each i and for each colour.
TRULE(run; red; joker; joker) holds.
holds for each i.
holds for each i.
holds.
The set of the nodes c i , of the graph can be in a natural way understood
as a tape of Achilles-Turtle machine. Notice that all the facts from the definition
are "local" in the sense that if some elements c i and c j are directly connected by a
fact then and there is no white node between c i and c j .
Now we are going to use the relations of the Achilles-Turtle graph to encode all
the rules of the machine in only one transition rule:
CONF
where BODY is the conjunction of the following facts:
22 J. MARCINKOWSKI
COL(TCOLOR;T
G;
Lemma 4.2. Suppose T is not red. Then can be computed from
in a single computation step of the Achilles-Turtle machine if and
only if CONF can be reached from CONF (A; T ; G) in a single step of the
Achilles-Turtle graph game.
Proof. It is clear that the move of Achilles is performed in the same way by the
machine and the game (he simply moves p cells ahead). We should check that this is
also the case with the Turtle and the Guide.
The "only if" direction is easier: if the transition of the machine has been done
according to the run rule then substitute run for the variable COND. Else substitute
jump. For the variable TCOLOR substitute the colour of the Turtle's cell. For the
variable GCOLOR substitute the colour of the Guide's cell. Now, if there is no
white node between G and G 0 then substitute . If there is exactly one
such white node then substitute the node for X 1 and . If there are two such
nodes then substitute the first of them for X 1 and the second for X 2 (notice that by
condition (ii) from Theorem 2.2. i. there are at most two white nodes between G
and G 0 ). The "GRULE" goals in the lines (v)-(vii) of the BODY are satisfied in this
way. If COND is run then substitute T for X 3 (notice that in this case
COND is jump then substitute joker for X 3 . The two "TRULE" goals of the BODY
are satisfied in this way. To satisfy the last two goals substitute joker for X 4 if the
COND is run and if the COND is jump then substitute G 0 for X 4 .
For the "if" direction first notice that if the conjunction of
can be satisfied, then really the distance between Achilles and the Turtle, before
the transition, is smaller than p, and so jump is allowed according to the Achilles-
Turtle machine rules. The rules for the Guide (defined by claims (vi), (vii) and (viii)
of Definition 4.1) assure that if only COND, TCOLOR and GCOLOR are chosen in
a fair way then the Guide of the game moves in the same way as the one from the
machine. The Turtle now: if the COND is run then he should not move, and in fact
the conjunction
can be satisfied only if
If the COND is jump then the Turtle should go to the same node where Guide
does. The conjunction
can be satisfied for every choice of joker is substituted for X 3 , but
the conjunction:
ACHILLES, TURTLE, AND SMALL DATALOG PROGRAMS 23
is satisfied only if X
The following lemma is much easier to prove than Lemma 4.2. and is left as an
exercise for the reader.
Lemma 4.3. If c t is red then each configuration of the form CONF
can be reached from CONF in a single step of the graph game.
Hint: Put COND equal to run and TCOLOR equal to red.
4.3. Single linear rule program with initialization. In this section we will
use the Achilles-Turtle game to construct a DATALOG program with one linear recursive
rule and one initialization, which is uniformly bounded if and only if C(g; 2)
holds.
The EDB predicates of the program will be the same as the used in the Definition
4.1.
It will be one ternary IDB predicate CONFIG. The variables A; T ; G in a fact of
the form
should be, as usually, understood as Achilles, Turtle and Guide,
Consider a database D. We suppose that colour
run and joker occur in D. A Motorway will be a sequence of elements of the database
which can be used for playing the Achilles - Turtle game:
Definition 4.4. Suppose are elements of D. We say that the
sequence is a Motorway if
is a subgraph of
where ordered sets of elements are considered. G is the database from Definition 4.1.
So, for example, we require that S(X 3 hold in D, if
is a Motorway.
Now we are ready to write
the linear recursive rule of program
CONF
Where is the conjunction of facts needed for the sequence
to be a Motorway. Notice that the last lines the rule are exactly
the literals of BODY in which T 0 or G 0 occurs, with run substituted for COND and
red substituted for TCOLOR.
And
J. MARCINKOWSKI
the initialization of program
CONF
Thanks to the last lines of the recursive rule we can be sure that if the fact
CONF can be proved in one step from CONF IG(A; T ; G) then it can
also be proved in one step from each fact of the form CONF
is red (see the proof of Lemma 4.8 case 1).
Our next goal is to show that if a long proof using the recursive rule is possible
in some database D then there is a long Motorway in D.
Lemma 4.5. Consider a sequence:
of elements of a database. If, for each 0 - k - x \Gamma 1 the subsequence
is a Motorway then also the whole sequence is a Motorway.
Proof. The conditions (i)-(x) of Definition 4.1 are "local": if some elements
and c j occur in a condition then and there is no white node between c i
and c j .
Lemma 4.6. Suppose that
CONF
CONF
CONF
CONF
is a sequence of facts, such that if 0 -
CONF
can be derived from:
CONF
by a single use of the recursive rule.
Then there exists a sequence
of elements of the database which is a Motorway.
Proof. That follows from Lemma 4.5 and from the construction of the recursive
rule.
Definition 4.7. If A; T ; G is a tuple of nodes of the database D then we say that
is a fact about A.
Now we are ready to prove that If C(g; 2) holds then the program T is uniformly
bounded.
Lemma 4.8. If C(g; 2) holds then there exists a constant C such that in every
database D if the program T proves some fact, then the fact can be proved in no more
than C derivation steps.
ACHILLES, TURTLE, AND SMALL DATALOG PROGRAMS 25
Proof. If C(g; 2) holds then the Achilles-Turtle game can reach the configuration
CONF (X; S(X); S(X)) for some white X . S(X) is red then. Suppose the K moves
are needed to reach this configuration. and the nodes
of the machine graph left of Y or right of S(X) are not visited during the computation.
We are going to prove that K+2 is a good candidate to be C.
Consider an element A of D. There are 2 possibilities:
case 1:
There is a Motorway of length (K + 1)p in the database, such that A is its last node.
Suppose
is the Motorway. By the initialization rule
CONF
can be proved in one derivation step. During the next K derivation steps one can
simulate K steps of Achilles-Turtle game, and so after K+1 steps we derive
CONF
Since A \Gammap+1 is red one can argue like in the proof of Lemma 4.3 to see that in
the next derivation step we can prove
for each T 0 and each G 0 such
And, because of the last lines of the recursive rule, no other facts can be
proved about A.
case 2:
No such Motorway.
Then, by Lemma 4.6 every proof has less than K+3 steps.
We still need to show that if C(g; 2) does not hold then the program is unbounded.
Lemma 4.9. If C(g; 2) does not hold then for each constant C there exist a
database D, with empty input IDB relation, and a fact
which can be proved in the database but the proof requires more than C steps.
26 J. MARCINKOWSKI
Proof. It's enough to show that arbitrarily long proofs are needed in the Achilles-
Turtle game graph (we suppose that there are no IDB input facts). So start with
(that can be done by initialization) and use 2C times the run rule for Turtle in
a pink-coloured cell. Notice that the position of the Turtle will remain unchanged
during the computation and the final configuration will be
The shortest proof of the fact really requires 2C+1 steps (including initialization).
To summarize:
Theorem 4.10. Uniform boundedness and program boundedness are undecidable
for programs consisting of one linear rule and one initialization.
Proof. The problem: for given Conway function g, does C(g; 2) hold is undecid-
able, even for functions satisfying conditions (ii) and (iii) of Theorem 2.2.i. For each
such function we can construct a DATALOG program, with one linear rule and one
initialization which is not program bounded if C(g; 2) does not hold (Lemma 4.9) and
which is uniformly bounded if C(g; 2) holds (Lemma 4.8).
4.4. Single rule program: how one can not construct it. Now we would
like to modify the construction of the previous section and get a single rule program.
The only problem is how to initialize the predicate CONF IG. The simplest solution
would be not to initialize it at all, but just check, in the same way as we use the
"Motorway" goal in the body of the rule to check that the needed EDB facts hold.
So the rule should look like this:
CONF
CONF
In this way, one could think, we secure that it is possible to start the computation
of the Achilles-Turtle machine in each place, where any derivation step is made. But it
is not enough to go in the footsteps of the proof of Lemma 4.8. We require there, that
the initial configuration is not only provable, what is really secured by the would-be
rule above, but that it is provable in a bounded number of steps (in fact, just one
step, in the previous section). We are to think of a new trick to assure that.
4.5. Single rule program: how to construct it.
The single recursive rule S is:
ACHILLES, TURTLE, AND SMALL DATALOG PROGRAMS 27
CONF IG(run; Z; A
CONF IG(W; run; A; T ; G), main
premise
CONF IG(jump; run; A; A 2 ; A 2 ); initialization
premise
jump=run
premise
Where the constant joker occurs p times in the "predicate" Motorway. We have
added two additional arguments to the recursive predicate here. The rule asserts that
if something can be derived then its first argument is run. So, if only the constants
run and jump are not interpreted in the same way in the database, then the fact
can not be proved by the program, and if it is provable then it is provable in 0
steps (is given as a part of the input).
Also the fact
does not require a deep proof: if any proof at all is possible then the fact is given
in the input.
The "jump=run premise" is normally useless as the main or as the initialization
premise of a derivation step: it has "jump" as the second argument. But if run
and jump are equal in the database, then we use it to show that if anything can be
proved about A then everything can be proved about it in one step. That is why
must hold and why joker is red.
We use the methods of Section 4.3 to prove that the constructed single rule
program is uniformly bounded if and only if C(g; 2) holds:
Lemma 4.11. If C(g; 2) holds then there exists a constant C such that in every
database D if some fact can be proved with the rule S, then it has a proof no deeper
than C.
Proof. Let K be like in the proof of Lemma 4.8. We need to consider two cases:
case 1:
jump and run are different elements of the database.
28 J. MARCINKOWSKI
Suppose that for some A there is a fact about it which has a proof of length at
least K+2. Then, we follow the proof of Lemma 4.8: we use the fact that the needed
initialization has been given in the input, so it has a short (0-step) proof, and show
that everything can be proved about A in no more than K+2 derivation steps.
case 2:
jump and run are interpreted as the same element of the database.
Suppose that anything can be proved about some A p . Then
CONF IG(jump; jump; joker; joker; joker)
holds in the database. Since holds and since
joker is red, every fact of the form
CONF IG(run; Z; A
can be proved in one derivation step, if only
Lemma 4.12. If C(g; 2) does not hold then for each constant C there exist a
database D, and a fact
CONF IG(run; run; A
which can be proved, with the rule S, in the database D, but the proof requires
more than C steps.
Proof. We proceed in a similar way as in the proof of Lemma 4.9, with the
following differences:
(i) we no longer assume that the IDB input is empty. Instead, we require that
there are the following CONF IG facts in the input:
and, for each x - C:
CONF
(ii) we require that for each x - C
holds.
This ends the proof of
Theorem 4.13. Uniform boundedness of single rule DATALOG programs is
undecidable.
ACHILLES, TURTLE, AND SMALL DATALOG PROGRAMS 29



--R


Boundedness is Undecidable for Datalog Programs with a Single Recursive Rule
DATALOG versus First Order Logic

Parallel evaluation of recursive rule queries
Decidable Optimization Problems for Database Logic Programs
Halting Problem of One Binary Recursive Horn Clause is Undecidable
Undecidable Optimization Problems for Database Logic Programs
Undecidable Boundedness Problems for Datalog Programs
A Time Bound on the Materialization of Some Recursively Defined Views
Logic Programming and Parallel Complexity
Elements of Relational Database Theory in Handbook of Theoretical Computer Science


The 3 Frenchmen Method Proves Undecidability of the Uniform Boundedness for Single Recursive Rule Ternary DATALOG Programs
Undecidability of Uniform Boundedness for Single Rule Datalog Programs
On Recursive Axioms in Relational Databases
Data Independent Recursion in Deductive Databases
A Decidable Class of Bounded Recursions
On Computing Restricted Projections of Representative Instances


Some Positive Results for Boundedness of Multiple Recursive Rules
Decidability and undecidability results for boundedness of linear recursive queries
--TR

--CTR
Foto Afrati , Stavros Cosmadakis , Eugnie Foustoucos, Datalog programs and their persistency numbers, ACM Transactions on Computational Logic (TOCL), v.6 n.3, p.481-518, July 2005
Evgeny Dantsin , Thomas Eiter , Georg Gottlob , Andrei Voronkov, Complexity and expressive power of logic programming, ACM Computing Surveys (CSUR), v.33 n.3, p.374-425, September 2001
query optimization;decidability;DATALOG