- Reference manual
- Tabled execution (SLG resolution)
- Example 1: using tabling for memoizing
- Example 2: avoiding non-termination
- Answer subsumption or mode directed tabling
- Tabling for impure programs
- Variant and subsumptive tabling
- Well Founded Semantics
- Incremental tabling
- Monotonic tabling
- Shared tabling
- Tabling restraints: bounded rationality and tripwires
- Tabling predicate reference
- About the tabling implementation
- Tabled execution (SLG resolution)
- Reference manual
Tabling avoids non-termination due to self-recursion. As Prolog allows for infinitely nested compound terms (function symbols in logic) and arbitrary numbers, the set of possible answers is not finite and thus there is no guaranteed termination.
This section describes restraints Grosof & Swift, 2013 that can be enforced to specific or all tabled predicates. Currently there are three defined restraints, limiting (1) the size of (the arguments to) goals, (2) the size of the answer substitution added to a table and (3) the number of answers allowed in any table. If any of these events occurs we can specify the action taken. We distinguish two classes of actions. First, these events can trap a tripwire which can be handled using a hook or a predefined action such as raising an exception, printing a warning or enter a break level. This can be used for limiting resources, be notified of suspicious events (debugging) or dynamically adjust the (tabling) strategy of the program. Second, they may continue the computation that results in a partial answer (bounded rationality). Unlike just not exploring part of the space though, we use the third truth value of well founded semantics to keep track of answers that have not been affected by the restraints and those that have been affected.
The tripwire actions apply for all restraints. If a tripwire action is triggered, the system takes the steps below.
- Call the prolog:tripwire/2 hook.
- If prolog:tripwire/2
fails, take one of the predefined actions:
- Print a message indicating the trapped tripwire and continue execution as normal, i.e., the final answer is the same as if no restraint was active.
- Throw an exception
- Print a message and start a break level (see break/0).
- [multifile]prolog:tripwire(Wire, Context)
- Called when tripwire Wire is trapped. Context
provides additional context for interpreting the tripwire. The hook can
take one of three actions:
- Succeed. In this case the tripwire is considered handled and execution proceeds as if there was no tripwire. Note that tripwires only trigger at the exact value, which implies that a wire on a count will be triggered only once. The hook can install a new tripwire at a higher count.
- Fail. In this case the default action is taken.
- Throw an exception. Exceptions are propagated normally.
Radial restraints limit the sizes of subgoals or answers. Abstraction of a term according to the size limit is implemented by size_abstract_term/3.
- [det]size_abstract_term(+Size, +Term, -Abstract)
- The size of a term is defined as the number of compound subterms (function
symbols) that appear in term. Abstract is an abstract
copy of Term where each argument is abstracted by copying
only the first Size function symbols and constants. Excess
function symbols are replaced by fresh variables.
This predicate is a helper for tabling where Term is the
ret/Nanswer skeleton that is added to the answer table. Examples:
Size Term Abstract 0 ret(f(x), a) ret(_, a) 1 ret(f(x), a) ret(f(x), a) 1 ret(f(A), a) ret(f(A), a) 1 ret(f(x), x(y(Z))) ret(f(x), x(_))
- This predicate is undefined in the sense of well founded semantics (see section 7.6 and undefined/0). Any answer that depends on this condition is undefined because either the restraint on the subgoal size or answer size was violated.
subgoal_abstract(Size) attribute, a tabled
subgoal that that is too large is abstracted by replacing
compound subterms of the goal with variables. In a nutshell, a goal
p(s(s(s(s(s(0)))))) is converted into the semantically
equivalent subgoal if the subgoal size is limited to 3.
..., p(s(s(s(X)))), X = s(s(0)), ...,
As a result of this, terms stored in the variant trie that
maps goal variants into answer tables is limited. Note that
does not limit the number of answer tables as atomic values are never
abstracted and there are, for example, an infinite number of integers.
Note that restraining the subgoal size does not affect the semantics,
provided more general queries on the predicate include all answers that
more specific queries do. See also call substitution as
described in section
7.5. In addition to the tripwire actions, the max_table_subgoal_size_action
can be set to the value
- Abstract the goal as described above and provide correctness by adding the required unification instructions after the goal.
answer_abstract(Size) attribute, a tabled
subgoal that produces answer substitutions (instances of the variables
in the goal) whose size exceed Size are trapped. In addition
to the tripwire actions, answer abstraction defines two additional modes
for dealing with too large answers as defines by the Prolog flag
- Ignore the too large answer. Note that this is semantically incorrect.
- In this mode, the large answer is abstracted in the same way as subgoals are abstracted (see section 7.10.1). This is semantically incorrect, but our third truth value undefined is used to remedy this problem. In other words, the abstracted value is added to the table as undefined and all conclusions that depend on usage of this abstracted value are thus undefined unless they can also be proved some other way.
Finally, using “as
the Prolog flag
the number of answers in a table is restrained. In addition to the
tripwire actions this restraint supports the action
complete_soundly is supported as a synonym for XSB
compatibility. If the restraint is reached in the bounded
rationality mode the system takes the following actions:
- Ignore the answer that triggered the restraint.
- Prune the choice points of the tabled goal to avoid more answers.
- Add an new answer to the table that does not bind any variables, i.e., an empty answer substitution. This answer is conditional on answer_count_restraint/0.
- This predicate is undefined in the sense of well founded
semantics (see section 7.6
Any answer that depends on this condition is undefined because the
max_answersrestraint on some table was violated.
The program and subsequent query below illustrate the behavior.
:- table p/2 as max_answers(3). p(M,N) :- between(1,M,N).
?- p(1 000 000, X). X = 3 ; X = 2 ; X = 1 ; % WFS residual program p(1000000, X) :- answer_count_restraint. p(1000000, X).