Subsumption-Based Tabled Evaluation

The second measure determines whether one term subsumes another. A term t₁ subsumes a term t₂ if t₂ is an instance of t₁. Furthermore, we say that t₁ properly subsumes t₂ if t₂ is not a variant of t₁. Under subsumption-based tabling, when a tabled call C is issued, a search is performed for a table entry containing a subsuming subgoal S. Notice that, if such an entry exists, then its answer set $\cal {A}$ logically contains all the solutions to satisfy C. The subset of answers $\cal {A}$^$\prime$ $\subseteq$ $\cal {A}$ which unify with C are said to be relevant to C. Likewise, upon the derivation of an answer A for a producing subgoal S, A is inserted into the answer set $\cal {A}$ of S if and only if A is not subsumed by some answer A' already present in $\cal {A}$.

Notice that subsumption-based tabling permits greater reuse of computed results, thus avoiding even more program resolution, and thereby can lead to time and space performances superior to variant-based tabling. However, there is a downside to this paradigm. First of all, subsumptively tabled predicates do not interact well with certain Prolog constructs with which variant-tabled predicates can (see Example 5.2.3 below). Further, in the current implementation of subsumption-based tabling, subsumptive predicates may not take part in negative computations which result in the delay of a literal containing a subsumptive subgoal (see Section 10.1). This requires subcomputations in which subsumptive predicates take part to be LRD-stratified.

Example 5.2.1   The terms t₁: p(f(Y),X,1) and t₂: p(f(Z),U,1) are variants as one can be made to look like the other by a renaming of the variables. Therefore, each subsumes the other.
The term t₃: p(f(Y),X,1) subsumes the term t₄: p(f(Z),Z,1). However, they are not variants. Hence t₃ properly subsumes t₄.$\Box$