B-Prolog - Tabling

Tabling

Tabling has been found increasingly important for not only helping beginners write workable declarative programs but also developing real-world applications such as natural language processing, model checking, and machine learning applications. B-Prolog implements a tabling mechanism, called linear tabling, which is based on iterative computation of looping subgoals rather than suspension of them to compute the fixed points. The PRISM system, which heavily relies on tabling, has been the main driving force for the design and implementation of B-Prolog's tabling system.

The idea of tabling is to memorize the answers to tabled calls and use the answers to resolve subsequent variant calls. In B-Prolog, as in XSB, tabled predicates are declared explicitly by declarations in the following form:

:-table P1/N1,...,Pk/Nk.

For example, the following tabled predicate defines the transitive closure of a relation as given by edge/2.

:-table path/2. path(X,Y):-edge(X,Y). path(X,Y):-path(X,Z),edge(Z,Y).

With tabling, any query to the program is guaranteed to terminate as long as the term sizes are bounded.

By default, all the arguments of a tabled call are used in variant checking and all answers are tabled for a tabled predicate. B-Prolog supports table modes, which allow the system to use only input arguments in variant checking and table answers selectively. The table mode declaration

:-table p(M1,...,Mn):C.

instructs the system how to do tabling on p/n, where C, called a cardinality limit, is an integer which limits the number of answers to be tabled, and each Mi is a mode which can be min, max, + (input), or - (output). An argument with the mode min or max is assumed to be output. If the cardinality limit C is 1, it can be omitted with the preceding ':'.

Table modes are very useful for declarative description of dynamic programming problems. For example, the following program encodes the Dijkstra's algorithm for finding a path with the minimum weight between a pair of nodes.

:-table sp(+,+,-,min). sp(X,Y,,W) :- edge(X,Y,W). sp(X,Y,,W) :- edge(X,Z,W1), sp(Z,Y,Path,W2), W is W1+W2.

The table mode states that only one path with the minimum weight is tabled for each pair of nodes.