Feature Request: Add Tabling to Prevent Infinite Loops

[blackwint3r]

Could we implement a tabling mechanism similar to SWI-Prolog's in N3, allowing predicates to be marked as tabled to prevent infinite recursion and enable memoization?
In Prolog, we use the table/1 directive to achieve this property. I'd like similar functionality in N3/eye reasoner for backward-chained predicates.

For example:

{?x :succ ?y} <= {?x :succ ?z. ?z :succ ?y}

Currently, for certain properties, even though there are intuitive ways to express them, I’m forced to use tricky workarounds to avoid loops. One such workaround involves renaming the property to create a dummy version:

{?x :_succ ?y} <= {?x :succ ?y}
{?x :_succ ?y} <= {?x :succ ?z. ?z :succ ?y}

Alternatively, I might convert some predicates to forward chaining.

However, for larger programs, circular references are not always this straightforward—they could involve complex loops, And the above workarounds are not always useful. Furthermore, when using terms defined via backward chaining, the interactions between terms often cause problems in unexpected places, making debugging especially difficult.

In addition, (while not as critical as the above) memoization is also incredibly useful for tasks like recursively calculating Fibonacci numbers.
Therefore, having a built-in mechanism, such as [] e:table :succ, to mark predicates as tabled, would be extremely helpful.

[josd]

Nice indeed and is now done in v11.8.0 using log:table.
There is also an example at https://github.com/eyereasoner/eye/tree/master/reasoning/path

[blackwint3r]

I didn’t expect it to be implemented so quickly, Thank you for your hard work!

But I found the test case below is not worked as expected, and gave me stack_overflow error in eye:

@prefix log: <http://www.w3.org/2000/10/swap/log#> .
@prefix : <#>.

[] log:table :has,  :has-instance.

{?x :has ?y} <= {?x :has-instance  ?y}.
{?x :has-instance ?y} <= {?x a :Class. ?x :has ?y}.

:A :has :b.
:A a :Class.
:A :has-instance  :c.

{:A :has ?y} => {:result :is  ?y}. # query

Nearly identical code in swi-prolog, using tabling, worked as expected:

:- table has/2.
:- table has_instance/2.
has(X, Y) :- has_instance(X, Y).
has_instance(X, Y) :- class(X), has(X, Y).

has(a, b).
class(a).
has_instance(a, c).

I also tried true <= {[] log:table :has} (hoping the statement would execute when loading the program) but to no avail. Can't figure out why...

[josd]

The point is that log:table is not a directive like in prolog but just an ordinary triple and it was not yet "active" when asserting :has and :has-instance triples for which eye checks if they are not yet in the deductive closure. It is now fixed in v11.8.2

[blackwint3r]

I’ve found a strange bug, the following test fails to pass:

@prefix log: <http://www.w3.org/2000/10/swap/log#> .
@prefix : <#> . 

[] log:table :q. #comment it out works fine
{?s :p :o1} <= {?s :q :o2.}.
:x :q :o2.

{:x :p :o1} => {:test :pass 1}.

[josd]

Very strange indeed and I couldn't understand it.
So I tried a few things and what now works in v11.9.4 is shifting the internal table/1 declarations from parsing time to just before reasoning time.

[blackwint3r]

I’ve run into a problem again. I have observed that log:table can run into issues when the tabled predicate appears in the conclusion of rule, both backward and forward.

1. When the tabled predicate appears in the conclusion of a backward rule, and during its evaluation it encounters built-ins such as log:forAllIn, log:collectAllIn, e:fail, e:call, e:findall, or e:closure whose truth values depend on the entire knowledge base (with the argument being a blank node denote the entire default graph), it will fail.
   This happens if the tabled predicate itself is one of these built-ins, or if these built-ins appear in the antecedents of its backward rules, or in the antecedents of predicates in its antecedents, and so on.
   Here is an example, all tests failed when the log:table statements were uncommented:

@prefix e: <http://eulersharp.sourceforge.net/2003/03swap/log-rules#> .
@prefix log: <http://www.w3.org/2000/10/swap/log#> .
@prefix : <#> .

# [] log:table :all-like.
# [] log:table log:forAllIn.
# [] log:table :had-implies.
# [] log:table :alone-like.
# [] log:table :both-like.
# [] log:table :feel.

:Alice :like :apple, :peach.
:Bob :like :apple.
{?x :like :apple} => {?x a :Healthy}.
# ------------------------------- e:findall / log:collectAllIn ------------------------------- #
{?answer :all-like :apple} <= {[] e:findall (?x {?x :like :apple} ?answer)  } .
#{?answer :all-like :apple} <= { (?x {?x :like :apple} ?answer) log:collectAllIn []  } .
{?answer :all-like :apple} => {:test :pass 1}.

# ------------------------------- log:forAllIn ------------------------------- #
{?g1 :had-implies ?g2 } <= { (?g1 ?g2) log:forAllIn []}.
{ {:Bob :like ?o} :had-implies {:Alice :like ?o}} => {:test :pass 2}.

# ------------------------------- e:fail ------------------------------- #
{:Alice :alone-like ?o} <= {:Alice :like ?o. [] e:fail {:Bob :like ?o}}.
{:Alice :alone-like :peach}  => {:test :pass 3}.

# ------------------------------- e:call ------------------------------- #
{:They :both-like ?o} <= {:Alice :like ?o. [] e:call {:Bob :like ?o}}.
{:They :both-like :apple}  => {:test :pass 4}.

# ------------------------------- e:closure ------------------------------- #
{?x :feel :happy} <= {[] e:closure ?g. ?g log:includes {?x a :Healthy}} .
{:Alice :feel :happy}  => {:test :pass 5}.

2. When the tabled predicate appears in the conclusion of a forward rule, reasoner will get stuck:

@prefix log: <http://www.w3.org/2000/10/swap/log#> .

[] log:table :pass.  
:Bob :like :apple.
{?x :like :apple} => {:test :pass 7}.

[josd]

With v11.9.7 and the uncommented log:table triples it should now pass

:Alice :like :apple.
:Alice :like :peach.
:Bob :like :apple.
:Alice a :Healthy.
:Bob a :Healthy.
:test :pass 1 .
:test :pass 2 .
:test :pass 3 .
:test :pass 4 .
:test :pass 5 .

[blackwint3r]

Appreciate!
Currently the second test case still got stuck, though.

@prefix log: <http://www.w3.org/2000/10/swap/log#> .

[] log:table :pass.  
:Bob :like :apple.
{?x :like :apple} => {:test :pass 7}.

[josd]

This is strange: we assert :test :pass 7 and when we call :test :pass 7 immediately after it fails, so it is asserting infinitely ...

[josd]

So 3 issues with tabling in 1 day:

1/ https://github.com/orgs/eyereasoner/discussions/139#discussioncomment-12310146 with a rather ugly work-around
2/ https://github.com/orgs/eyereasoner/discussions/139#discussioncomment-12315632 fundamental issue
3/ a crash with an internal case using log:table

ERROR: Received fatal signal 11 (segv)
Time: Tue Feb 25 22:34:43 2025
Inferences: 56755
Running GC: 1-th garbage collection]
Thread: 1 (main)
C-stack trace labeled "crash":
  [0] save_backtrace() at /home/jdroo/github.com/SWI-Prolog/swipl-devel/src/os/pl-cstack.c:337 [0x7f3ae0162515]
  [1] sigCrashHandler() at /home/jdroo/github.com/SWI-Prolog/swipl-devel/src/os/pl-cstack.c:937 [0x7f3ae01625fd]
  [2] __restore_rt() at libc_sigaction.c:? [0x7f3adfe33520]
  [3] early_reset_vars___LD() at /home/jdroo/github.com/SWI-Prolog/swipl-devel/src/pl-gc.c:1585 [0x7f3ae008520c]
  [4] mark_foreign_frame___LD() at /home/jdroo/github.com/SWI-Prolog/swipl-devel/src/pl-gc.c:1684 [0x7f3ae0089dac]
  [5] f_ensureStackSpace___LD() at /home/jdroo/github.com/SWI-Prolog/swipl-devel/src/pl-gc.c:4701 [0x7f3ae008b45f]
  [6] ensureStackSpace_ex___LD() at /home/jdroo/github.com/SWI-Prolog/swipl-devel/src/pl-gc.h:122 [0x7f3ae0120562]
  [7] INIT_SEQ_STRING___LD() at /home/jdroo/github.com/SWI-Prolog/swipl-devel/src/os/../pl-codelist.h:57 [0x7f3ae0156448]
  [8] PL_unify_text() at /home/jdroo/github.com/SWI-Prolog/swipl-devel/src/os/pl-text.c:715 [0x7f3ae0156bfd]
  [9] x_chars___LD() at /home/jdroo/github.com/SWI-Prolog/swipl-devel/src/pl-prims.c:4101 (discriminator 3) [0x7f3ae009933e]
  [10] pl_atom_codes2_va() at /home/jdroo/github.com/SWI-Prolog/swipl-devel/src/pl-prims.c:4227 [0x7f3ae0099787]
  [11] PL_next_solution___LD() at /home/jdroo/github.com/SWI-Prolog/swipl-devel/src/pl-vmi.c:4344 [0x7f3ae005a89d]
  [12] query_loop() at /home/jdroo/github.com/SWI-Prolog/swipl-devel/src/pl-pro.c:179 [0x7f3ae00a3512]
  [13] prologToplevel() at /home/jdroo/github.com/SWI-Prolog/swipl-devel/src/pl-pro.c:656 [0x7f3ae00a4091]
  [14] swipl(+0x10eb) [0x56005e2620eb]
  [15] __libc_start_call_main() at ./csu/../sysdeps/nptl/libc_start_call_main.h:58 [0x7f3adfe1ad90]
  [16] call_init() at ./csu/../csu/libc-start.c:128 [0x7f3adfe1ae40]
  [17] swipl(+0x1135) [0x56005e262135]


PROLOG STACK (without arguments):
  [23] system:atom_codes/2 <foreign>
  [22] wt0/1 [PC=46 in clause 11]
  [21] wt/1 [PC=16 in clause 2]
  [17] w3/0 [PC=213 in clause 2]
  [16] w4/0 [PC=16 in clause 1]
  [15] eam/1 [PC=971 in clause 1]
  [14] system:catch/3 [PC=2 in clause 1]
  [13] gre/1 [PC=1014 in clause 1]
  [12] system:catch/3 [PC=2 in clause 1]
  [11] run/0 [PC=533 in clause 1]
Running on_halt hooks with status 139
Killing 226005 with default signal handlers
Segmentation fault