The simplest way to use tabling is to include the directive
:- auto_table.
anywhere in the source file. auto_table declares predicates tabled so that the program will terminate.
To understand precisely how auto_table does this, it is necessary to mention a few properties of SLG. For programs which have no function symbols, or where function symbols always have a limited depth, SLG resolution ensures that any query will terminate after it has found all correct answers. In the rest of this section, we restrict consideration to such programs.
Obviously, not all predicates will need to be tabled for a program to terminate. The auto_table compiler directive tables only those predicates of a module which appear to static analysis to contain an infinite loop, or which are called directly through tnot/1. It is perhaps more illuminating to demonstrate these conditions through an example rather than explaining them. For instance, in the program.
:- auto_table. p(a) :- s(f(a)). s(X) :- p(f(a)). r(X) :- q(X,W),r(Y). m(X) :- tnot(f(X)). :- mode ap1(-,-,+). ap1([H|T],L,[H|L1]) :- ap1(T,L,L1). :- mode ap(+,+,-). ap([],F,F). ap([H|T],L,[H|L1]) :- ap(T,L,L1). mem(H,[H|T]). mem(H,[_|T]) :- mem(H,T).
The compiler prints out the messages
% Compiling predicate s/1 as a tabled predicate % Compiling predicate r/1 as a tabled predicate % Compiling predicate m/1 as a tabled predicate % Compiling predicate mem/2 as a tabled predicate
Terminating conditions were detected for ap1/3 and ap/3, but not for any of the other predicates.
auto_table gives an approximation of tabled programs which we hope will be useful for most programs. The minimal set of tabled predicates needed to insure termination for a given program is undecidable. It should be noted that the presence of meta-predicates such as call/1 makes any static analysis useless, so that the auto_table directive should not be used in such cases.
Predicates can be explicitly declared as tabled as well, through the table/1. When table/1 is used, the directive takes the form
:- table(F/A).
where F is the functor of the predicate to be tabled, and A its arity.
Another use of tabling is to filter out redundant solutions for efficiency rather than termination. In this case, suppose that the directive edb/1 were used to indicate that certain predicates were likely to have a large number of clauses. Then the action of the declaration :- suppl_table in the program:
:- edb(r1/2). :- edb(r2/2). :- edb(r3/2). :- suppl_table. join(X,Z):- r1(X,X1),r2(X1,X2),r3(X2,Z).would be to table join/2. The suppl_table directive is the XSB analogue to the deductive database optimization, supplementary magic templates [5]. suppl_table/0 is shorthand for suppl_table(2) which tables all predicates containing clauses with two or more edb facts or tabled predicates. By specifying suppl_table(3) for instance, only predicates containing clauses with three or more edb facts or tabled predicates would be tabled. This flexibility can prove useful for certain data-intensive applications.