FINITE REPRESENTATION OF INFINITE QUERY ANSWERS

We define here a formal notion of finite representation of infinite query answers in logic programs. We apply this notion to Datalog(nS) (Datalog with n successors): an extension of Datalog capable of representing infinite phenomena like flow of time or plan construction. Predicates in Datalog(nS) can have arbitrary unary and limited n-ary function symbols in one fixed position. This class of logic programs is known to be decidable. However, least Herbrand models of Datalog(nS) programs may be infinite and consequently queries may have infinite answers. We present a method to finitely represent infinite least Herbrand models of Datalog(nS) programs as relational specifications. A relational specification consists of a finite set of facts and a finitely specified congruence relation. A relational specification has the following desirable properties: First, it is explicit in the sense that once it is computed, the original Datalog(nS) program (and its underlying computational engine) can be forgotten. Given a query to be evaluated, it is easy to obtain from the relational specification finitely many answer substitutions that represent infinitely many answer substitutions to the query. The method involved is a combination of a simple, unificationless, computational mechanism (graph traversal, congruence closure, or term rewriting) and standard relational query evaluation methods. Second, a relational specification is effectively computable and its computation is no harder, in the sense of the complexity class, than answering yes-no queries. Our method is applicable to every range-restricted Datalog(nS) program. We also show that for some very simple non-Datalog(nS) logic programs, finite representations of query answers do not exist.