[m-users.] Tabling a semidet predicate

[Zoltan Somogyi]

2021-06-08 22:47 GMT+10:00 "Volker Wysk" <post at volker-wysk.de>:
> Hi!
> 
> I have a semidet predicate, and want to achieve termination with tabling.
> Like this:
> 
> 
> :- pred test(int::in) is semidet.
> :- pragma minimal_model(test/1).
> 
> test(X) :- test(X).
> test(1).
> test(2).

The way to achieve termination in this case is not to enable tabling,
but to simply delete the first clause.

> I'm not sure if I understand this fully. Is this the way to go?

No. You have not told us anything about the *actual* program
you are working on, but probably what you want is pragma memo,
not pragma minimal_model.

> Why the
> restriction on the determinism category of the tabled predicate?

The point of minimal model tabling is to implement either one
recursive predicate or a set of mutually recursive predicates
that generate a set of solutions, where some recursive calls
may indirectly call themselves. If e.g. p(1, ...) calls p(2, ...) calls
... p(42, ...), which then calls p(1, ...), then instead of an infinite loop,
tabling recognizes that p(1, ...) indirectly called itself. In that case,
it suspends execution, and arranges for every solution computed
for p(1, ...) *that were computed on execution paths that do not
involve this recursive call* to be returned from the otherwise-
infinitely-recursive p(1, ...) call site. It continues doing so until
there are no computations paths left that can generate more
solutions. The set of solutions computed during this process
is the minimal model.

This whole process requires there to be at least two alternative
execution paths to generate solutions: one that goes through
a recursive call, and one that does not. If that is not true,
then *there is no point* in enabling minimal model tabling.
For any predicate that has at most one solution, you either
get a solution, or you don't, but both are guaranteed to be
the minimal model solution *without* enabling tabling.

Zoltan.