[m-users.] Tabling a semidet predicate

[Zoltan Somogyi]

2021-06-09 02:25 GMT+10:00 "Volker Wysk" <post at volker-wysk.de>:
> Actually, I've tried to apply this workaround to my real project and get
> this:
> 
> 
> desktop ~/src/mtt $ ./mtt "a"
> ...
> *** Mercury runtime: caught segmentation violation ***
> cause: address not mapped to object
> PC at signal: 139993005971239 (7f52a9645727)
> address involved: (nil)
> This may have been caused by a stack overflow, due to unbounded recursion.
> exiting from signal handler

In the absence of details, there is nothing we can do with such a report.
This could have been caused by changes in gcc that break previous guarantees,
or it could be a bug in Mercury; we can't tell.

> I've searched for a textbook, which explains the theory behind tabling, but
> couldn't find any.

There is no "the theory behind tabling", because there are many different forms
of tabling, which work differently. One theory can't cover them all.

The theory behind Mercury's minimal model tabling is covered in the first
of the two references mentioned in section 19.2 in the reference manual,
Sagonas's PhD thesis. It is also covered in some of his papers on the topic.

> I need to know, to what classes of problems tabling can
> be applied to achieve termination, and how.

All forms of tabling target programs in which the set of recursive calls
(as identified by their input arguments) is finite; none can guarantee
the termination of programs in which this set is infinite. They differ in
*what they do* when they detect that a call depends on itself.

Zoltan.