Definite Programs

Definite programs, also called Horn Clause Programs, are those programs without negation. In XSB, this means without the \+/1, fail_if/1, not/1 or tnot/1 operators. Consider the Prolog program

path(X,Y) :- path(X,Z), edge(Z,Y).
path(X,Y) :- edge(X,Y).

together with the query ?- path(1,Y). This program has a simple, declarative meaning: there is a path from X to Y if there is a path from X to some node Z and there is an edge from Z to Y, or if there is an edge from X to Y. Prolog, however, enters into an infinite loop when computing an answer to this query. The inability of Prolog to answer such queries, which arise frequently, comprises one of its major limitations as an implementation of logic.

A number of approaches have been developed to address this problem by reusing partial answers to the query path(1,Y) [21,48,4,50,51]. The ideas behind these algorithms can be described in the following manner. Calls to tabled predicates, such as path(1,Y) in the above example, are stored in a searchable structure together with their proven instances. This collection of tabled subgoals paired with their answers, generally referred to as a table, is consulted whenever a new call, C, to a tabled predicate is issued. If C is sufficiently similar to a tabled subgoal S, then the answer set $\cal {A}$ associated with S may be used to satisfy C^5.1. In such instances, C is resolved against the answers in $\cal {A}$, and hence we refer to C as a consumer of $\cal {A}$ (or S). If there is no such S, then C is entered into the table and is resolved against program clauses as in Prolog -- i.e., using SLD resolution. As each answer is derived during this process, it is inserted into the table entry associated with C if it contains information not already in $\cal {A}$. We hence refer to C as a generator, or producer, as resolution of C in this manner produces the answers stored in its table entry. If the answer is in fact added to this set, then it is additionally scheduled to be returned to all consumers of C. If instead it is rejected as redundant, then the evaluation simply fails and backtracks to generate more answers.

Notice that since consuming subgoals resolve against unique answers rather than repeatedly against program clauses, tabling will terminate whenever

1. a finite number of subgoals are encountered during query evaluation, and
2. each of these subgoals has a finite number of answers.

Indeed, it can be proven that for any program with the bounded term depth property -- roughly, where all terms generated in a program have a maximum depth -- SLG computation will terminate. These programs include the important class of Datalog programs.