Is there a way to momentarily deactivate memoization?

Hi Jan, hi everyone,

I am using tabled resolution, and I would like to detect loops, i.e. variants of a predicate call calling themselves. Tabled resolution detects such loops, then suspends the variants, and returns false (if I understand well). I thought this detection could be embedded within a test so that actions can be done when false is returned. However, thanks to memoization, this creates an answer for the recursive call, which then reactivates the suspended call producing an answer that I don’t want.
Here is an example:

:- table test/1.

test(X) :-
		X = "ok"
		X = "other"

which returns

?- test(X).
X = "other" ;
X = "ok".

while I would like to return only

?- test(X).
X = "other".

Is it possible to do that ?

Kind regards

This is an invalid program. SWI-Prolog does not yet check this. Using XSB you get

Illegal cut over incomplete tabled subgoal: test(_v0), from within a call to _$call/1Removing incomplete tables...

In general you can use cuts with tabling, but only if the predicate being cut can be completed before the cut is doing its work.

More or less. If a variant is detected it (for SWI-Prolog) captures the continuation and then fails. When answers come in through other paths in the proof tree it calls the continuation with these answers.

Could you explain in logical/declarative terms what you try to do? The tabled control flow is rather hard to follow and (thus) one should typically not think about tabled execution in a procedural way.

Thanks for your answer Jan.

I am trying to compare 2 tree structures defined by rules, with some rules that may be recursive. Thus I have defined a recursive predicate to browse the two trees in parallel. I used tabled resolution for this predicate in order to :

  • speed up the process since some calls may be needed many times,
  • prevent from loops : in this case I would like to execute an ad-hoc action. Hence my question.

I’ve just tried this program:

:- table test/1.

test(X) :-
	X = "other"
test(X) :-
	X = "ok".

which gives:

?- test(X).
X = "other".

This program is still not valid however since XSB displays the same error as before. Anyway I will try it on my tree comparison program.

I’m afraid I don’t get what you are after. Some code may help. As for test(X) :- \+ test(X), this is indeed invalid as we have a loop through something that is cut. You can write test(X) :- tnot(test(X)), which is quickly identified by the Well Formed Semantics as undefined. After all, logically this is a contradiction.

Thanks for your answer Jan. I will try to find a smaller example of my problem.
Thanks again.