Why tabling seems to need the base case clauses to end with a cut?

[jasagredo]

I have the following prolog file:

:- use_module(library(clpz)).
:- use_module(library(tabling)).
:- use_module(library(debug)).

:- dynamic(memo_/1).

memo(Goal) :-
        (   memo_(Goal)
        ->  true
        ;   once(Goal),
            assertz(memo_(Goal))
        ).

foo_memo(0, _, 1).
foo_memo(N, X, Y) :-
    N1 #= N - 1,
    memo(foo_memo(N1, X, Y)).

:- table foo/3.

foo(0, _, 1).
foo(N, X, Y) :-
    N1 #= N - 1,
    $ foo(N1, X, Y).

where the memo/1 definition was taken from https://www.metalevel.at/prolog/memoization (section "Doing it manually", btw Scryer uses :- dynamic(memo_/1). not :- dynamic memo_/1.).

Once the file is consulted, the query foo_memo/3 instantly returns as expected, and the memoized clauses are right:

?- foo_memo(2, 125, X).
   X = 1.
?- listing(memo_/1).
memo_(foo_memo(0,125,1)).
memo_(foo_memo(1,125,1)).
   true.

However the seemingly equivalent foo/3 query enters an infinite decreasing loop, which in Ctrl^C returns an answer (the correct one) and memoizes it for future queries:

?- foo(2, 125, X).
call:user:foo(1,125,A).
call:user:foo(0,125,A).
call:user:foo(-1,125,A).
call:user:foo(-2,125,A).
call:user:foo(-3,125,A).
call:user:foo(-4,125,A).
...
call:user:foo(-424,125,A).
exception:error('$interrupt_thrown',repl/0):user:foo(-424,125,A).
exit:user:foo(0,125,1).
exit:user:foo(1,125,1).
   X = 1
;  ... .
?- foo(2, 125, X).
   X = 1
;  ... .

If I alter the first clause a bit with a cut, the query becomes instant too:

:- table foo/3.

foo(0, _, 1) :- !.
foo(N, X, Y) :-
    N1 #= N - 1,
    $ foo(N1, X, Y).

then:

?- foo(2, 125, X).
call:user:foo(1,125,A).
call:user:foo(0,125,A).
exit:user:foo(0,125,1).
exit:user:foo(1,125,1).
   X = 1

Why is this the case? I would have expected the first clause to be successful, then the query to return, not to explore other branches without providing an answer first.

[jjtolton]

Is this true even if you remove the debug:$/1 ?

[jasagredo]

Yes, it happens still without the debug:$/1:

Screen.Recording.2024-12-11.181830.mp4

with the file:

:- use_module(library(tabling)).
:- use_module(library(clpz)).

:- table foo/3.

foo(0, _, 1).
foo(N, X, Y) :-
    N1 #= N - 1,
    foo(N1, X, Y).

[jasagredo]

This does seem to be the same on SWI-Prolog. With the file:

:- table foo/3.

foo(0, _, 1).
foo(N, X, Y) :-
    N1 is N - 1,
    foo(N1, X, Y).

I get the following trace:

1 ?- trace, foo(1, 125, X).
   Call: (13) foo(1, 125, _1650) ? creep
^  Call: (14) start_tabling(<closure>(foo/3), user:foo(1, 125, _1650), call(<closure>(foo/3)(1, 125, _1650))) ? creep
   Call: (24) foo(1, 125, _1650) ? creep
   Call: (25) _4864 is 1+ -1 ? creep
   Exit: (25) 0 is 1+ -1 ? creep
   Call: (25) foo(0, 125, _1650) ? creep
^  Call: (26) start_tabling(<closure>(foo/3), user:foo(0, 125, _1650), call(<closure>(foo/3)(0, 125, _1650))) ? creep
   Call: (36) foo(0, 125, _1650) ? creep
   Exit: (36) foo(0, 125, 1) ? creep
   Redo: (36) foo(0, 125, _1650) ? creep
   Call: (37) _10718 is 0+ -1 ? creep
   Exit: (37) -1 is 0+ -1 ? creep
   Call: (37) foo(-1, 125, _1650) ? creep
^  Call: (38) start_tabling(<closure>(foo/3), user:foo(-1, 125, _1650), call(<closure>(foo/3)(-1, 125, _1650))) ? creep
   Call: (48) foo(-1, 125, _1650) ? creep
   Call: (49) _14944 is -1+ -1 ? creep
   Exit: (49) -2 is -1+ -1 ? creep
   Call: (49) foo(-2, 125, _1650) ? creep
^  Call: (50) start_tabling(<closure>(foo/3), user:foo(-2, 125, _1650), call(<closure>(foo/3)(-2, 125, _1650))) ? creep
   Call: (60) foo(-2, 125, _1650) ? creep
   Call: (61) _19170 is -2+ -1 ? creep
   Exit: (61) -3 is -2+ -1 ? creep
   Call: (61) foo(-3, 125, _1650) ? creep
^  Call: (62) start_tabling(<closure>(foo/3), user:foo(-3, 125, _1650), call(<closure>(foo/3)(-3, 125, _1650))) ?
...

I see an Exit: (36) foo(0, 125, 1) so I'm unsure why it continues with a Redo: (36) foo(0, 125, _1650) 🧩

[jjtolton]

This is really fascinating.

?- foo(2, 125, X).
call:user:foo(1,125,A).
call:user:foo(0,125,A).
call:user:foo(-1,125,A).
call:user:foo(-2,125,A).
call:user:foo(-3,125,A).
call:user:foo(-4,125,A).

Your finding here shows that the SLG resolution of tabling does not meet our standard intuition for how SLD resolution works. It never seems to hit the "base case" on the first pass, but it is "tabled" for the second pass.

[jasagredo]

It does hit the base case. If you output something in the base case clause it will be printed the first time it is hit. But for some reason it redoes the base case query.

[jjtolton]

You are right. What I meant was, it does not stop at the base case.

[jasagredo]

And what is even more surprising, having a cut on the base case actually makes it stop!

[triska]

I think the second clause misses a constraint #N #> 0 ?

Without this constraint, the predicate does not terminate universally, whether or not we use tabling:

?- foo(2, 125, X), false.
   loops.

[jasagredo]

That is right. I actually found the issue while solving today's Advent of Code in a bit more intricate clause (just with more intermediate terms), and tabling was deadlocking forever.

There I think I made sure that the recursive predicate terminates universally by adding the negated predicate to later clauses as you suggest, and it deadlocks even with cuts.

While producing the minimal example I ended up with this.

However I think that even if you add N #> 0 it still doesn't terminate if tabling is enabled right?

[jasagredo]

Turned out that I was using:

  length(X, L),
  0 #= L mod 2,
  !,
  same_length(X1, X2),
  append(X1, X2, X),

But this will generate infinitely long X1 and X2 only to fail again on append. That is why my solution was looping even with cuts.

[jjtolton]

I think the second clause misses a constraint #N #> 0 ?

Without this constraint, the predicate does not terminate universally, whether or not we use tabling:

?- foo(2, 125, X), false.
loops.

🤦‍♂️ I can't believe I didn't see that. I have so much to learn.

[jasagredo]

I think I found the why for this phenomenon. The paper on which tabling is based mentions the following:

The leader, defined in Figure 4, takes responsibility for computing all the answers of its scheduling component...

With figure 4 being:

run_leader(Wrapper,Worker,Table) :-
  create_scheduling_component,
  activate(Wrapper,Worker,Table),
  completion,
  unset_scheduling_component.

And then:

Note that a failure driven loop is used to backtrack over all the alternatives of Worker.

as seen in figure 6:

activate(Wrapper,Worker,Table) :-
  table_set_status(Table,active),
  (
    delim(Wrapper,Worker,Table),
    fail
    ;
    true
  ).

So indeed it will run the predicate and for this to terminate it has to terminate universally, as @triska pointed out above.

If you agree with my conclusion, let's mark this as the solution to the discussion (although I found it thanks to Markus' suggestion!).