20.2 Tabled evaluation

(Note: “Tabled evaluation” has no relation to the “fact tables” described above.)

Ordinarily, the results of each procedure call are not recorded; if the same procedure is called with the same arguments, then the answer(s) must be recomputed again. For some procedures, this recomputation can be very wasteful.

With tabled evaluation, the implementation keeps a table containing the previously computed results of the specified procedure; this table is sometimes called the memo table (since it “remembers” previous answers). At each procedure call, the implementation will search the memo table to check whether the answer(s) have already been computed, and if so, the answers will be returned directly from the memo table rather than being recomputed. This can result in much faster execution, at the cost of additional space to record answers in the table.

The implementation can also check at runtime for the situation where a procedure calls itself recursively with the same arguments, which would normally result in an infinite loop; if this situation is encountered, it can (at the programmer’s option) either throw an exception, or avoid the infinite loop by computing solutions using a “minimal model” semantics. (Specifically, the minimal model computed by our implementation is the perfect model.)

When targeting the generation of C code, the current Mercury implementation supports three different pragmas for tabling, to cover these three cases: ‘loop_check’, ‘memo’, and ‘minimal_model’. (None of these are supported when targeting the generation of C# or Java code.)

• The ‘loop_check’ pragma asks only for loop checking. With this pragma, the memo table will map each distinct set of input arguments only to a single boolean saying whether a call with those arguments is currently active or not; the pragma’s only effect is to cause the predicate to throw an exception if this boolean says that the current call has the same arguments as one of its ancestors, which indicates an infinite recursive loop.

  Note that loop checking for nondet and multi predicates assumes that calls to these predicates generate all their solutions and then fail. If a caller asks them only for some solutions and then cuts away all later solutions (e.g. via a quantification that only asks whether a solution satisfying a particular test exists), then the cut-away call never gets a chance to record the fact that it is not longer active. The next call to that predicate with the same arguments will therefore think that the previous call is still active, and will consider this call to be an infinite loop.

• The ‘memo’ pragma asks for both loop checking and memoization. With this pragma, the memo table will map each distinct set of input arguments either to the set of results computed previously for those arguments, or to an indication that the call is still active and thus those results are still being computed. This predicate will thus look for infinite recursive loops (and throw an exception if and when it finds one) but it will also record all its solutions in the memo table, and will avoid recomputing solutions that are already available in the memo table.
• The ‘minimal_model’ pragma asks for the computation of a “minimal model” semantics. These differ from the ‘memo’ pragma in that the detection of what appears to be an infinite recursive loop is not fatal. The implementation will consider the apparently infinitely recursive calls to fail if the call concerned has no way of computing any solutions it has not already computed and recorded, and if it does have such a way, then it switches the execution to explore those ways before coming back to the apparently infinitely recursive call.

  Minimal model evaluation is applicable only to procedures that can succeed more than once, and only in grades that explicitly support it.

The syntax for each of these declarations is

:- pragma memo(Name/Arity).
:- pragma memo(Name/Arity, [list of tabling attributes]).
:- pragma loop_check(Name/Arity).
:- pragma loop_check(Name/Arity, [list of tabling attributes]).
:- pragma minimal_model(Name/Arity).
:- pragma minimal_model(Name/Arity, [list of tabling attributes]).

where Name/Arity specifies the predicate or function to which the declaration applies. The declaration applies to all modes of the predicate and/or function named. At most one of these declarations may be specified for any given predicate or function.

Programmers can also request the application of tabling only to one particular mode of a predicate or function, via declarations such as these:

:- pragma memo(Name(in, in, out)).
:- pragma memo(Name(in, in, out), [list of tabling attributes]).
:- pragma loop_check(Name(in, out)).
:- pragma loop_check(Name(in, out), [list of tabling attributes]).
:- pragma minimal_model(Name(in, in, out, out)).
:- pragma minimal_model(Name(in, in, out, out), [list of tabling attributes]).

Because all variants of tabling record the values of input arguments, and all except ‘loop_check’ also record the values of output arguments, you cannot apply any of these pragmas to procedures whose arguments’ modes include any unique component.

Tabled evaluation of a predicate or function that has an argument whose type is a foreign type will result in a run-time error unless the foreign type is one for which the ‘can_pass_as_mercury_type’ and ‘stable’ assertions have been made (see Using foreign types from Mercury).

The optional list of attributes allows programmers to control some aspects of the management of the memo table(s) of the procedure(s) affected by the pragma.

The ‘allow_reset’ attribute asks the compiler to define a predicate that, when called, resets the memo table. The name of this predicate will be “table_reset_for”, followed by the name of the tabled predicate, followed by its arity, and (if the predicate has more than one mode) by the mode number (the first declared mode is mode 0, the second is mode 1, and so on). These three or four components are separated by underscores. The reset predicate takes a di/uo pair of I/O states as arguments. The presence of these I/O state arguments in the reset predicate, and the fact that tabled predicates cannot have unique arguments together imply that a memo table cannot be reset while a call using that memo table is active.

The ‘statistics’ attribute asks the compiler to define a predicate that, when called, returns statistics about the memo table. The name of this predicate will be “table_statistics_for”, followed by the name of the tabled predicate, followed by its arity, and (if the predicate has more than one mode) by the mode number (the first declared mode is mode 0, the second is mode 1, and so on). These three or four components are separated by underscores. The statistics predicate takes three arguments. The second and third are a di/uo pair of I/O states, while the first is an output argument that contains information about accesses to and modifications of the procedure’s memo table, both since the creation of the table, and since the last call to this predicate. The type of this argument is defined in the file table_builtin.m in the Mercury standard library. That module also contains a predicate for printing out this information in a programmer-friendly format.

As mentioned above, the Mercury compiler implements tabling only when targeting the generation of C code. In other grades, the compiler normally generates a warning for each tabling pragma that it is forced to ignore. The ‘disable_warning_if_ignored’ attribute tells the compiler not to generate such a warning for the pragma it is attached to. Since the ‘loopcheck’ and ‘minimal_model’ pragmas affect the semantics of the program, and such changes should not be made silently, this attribute may not be specified for them. But this attribute may be specified for ‘memo’ pragmas, since these affect only the program’s performance, not its semantics.

The remaining two attributes, ‘fast_loose’ and ‘specified’, control how arguments are looked up in the memo table. The default implementation looks up the value of each input argument, and thus requires time proportional to the number of function symbols in the input arguments. This is the only implementation allowed for minimal model tabling, but for predicates tabled with the ‘loop_check’ and ‘memo’ pragmas, programmers can also choose some other tabling methods.

The ‘fast_loose’ attribute asks the compiler to generate code that looks up only the address of each input argument in the memo table, which means that the time required is linear only in the number of input arguments, not their size. The tradeoff is that ‘fast_loose’ does not recognize calls as duplicates if they involve input arguments that are logically equal but are stored at different locations in memory. The following declaration calls for this variant of tabling.

:- pragma memo(Name(in, in, in, out),
        [allow_reset, statistics, fast_loose]).

The ‘specified’ attribute allows programmers to choose individually, for each input argument, whether that argument should be looked up in the memo table by value or by address, or whether it should be looked up at all:

:- pragma memo(Name(in, in, in, out), [allow_reset, statistics,
        specified([value, addr, promise_implied, output])]).

The ‘specified’ attribute should have an argument which is a list, and this list should contain one element for each argument of the predicate or function concerned (if a function, the last element is for the return value). For output arguments, the list element should be ‘output’. For input arguments, the list element may be ‘value’, ‘addr’ or ‘promise_implied’. The first calls for tabling the argument by value, the second calls for tabling the argument by address, and the third calls for not tabling the argument at all. This last course of action promises that any two calls that agree on the values of the value-tabled input arguments and on the addresses of the address-tabled input arguments will behave the same regardless of the values of the untabled input arguments. In most cases, this will mean that the values of the untabled arguments are implied by the values of the value-tabled arguments and the addresses of the address-tabled arguments, though the promise can also be fulfilled if the table predicate or function does not actually use the untabled argument for computing any of its output. (It is ok for it to use the untabled argument to decide what exception to throw.)

If the tabled predicate or function has only one mode, then this declaration can also be specified without giving the argument modes:

:- pragma memo(Name/Arity, [allow_reset, statistics,
        specified([value, addr, promise_implied, output])]).

Note that a ‘pragma minimal_model’ declaration changes the declarative semantics of the specified predicate or function: instead of using the completion of the clauses as the basis for the semantics, as is normally the case in Mercury, the declarative semantics that is used is a “minimal model” semantics, specifically, the perfect model semantics. Anything which is true or false in the completion semantics is also true or false (respectively) in the perfect model semantics, but there are goals for which the perfect model specifies that the result is true or false, whereas the completion semantics leaves the result unspecified. For these goals, the usual Mercury semantics requires the implementation to either loop or report an error message, but the perfect model semantics requires a particular answer to be returned. In particular, the perfect model semantics says that any call that is not true in all models is false.

Programmers should therefore use a ‘pragma minimal_model’ declaration only in cases where their intended interpretation for a procedure coincides with the perfect model for that procedure. Fortunately, however, this is usually what programmers intend.

For more information on tabling, see K. Sagonas’s PhD thesis The SLG-WAM: A Search-Efficient Engine for Well-Founded Evaluation of Normal Logic Programs. See [4]. The operational semantics of procedures with a ‘pragma minimal_model’ declaration corresponds to what Sagonas calls “SLGd resolution”.

In the general case, the execution mechanism required by minimal model tabling is quite complicated, requiring the ability to delay goals and then wake them up again. The Mercury implementation uses a technique based on copying relevant parts of the stack to the heap when delaying goals. It is described in Tabling in Mercury: design and implementation by Z. Somogyi and K. Sagonas, Proceedings of the Eight International Symposium on Practical Aspects of Declarative Languages.