For a project I was hoping that monotonic shared tabling would be supported. As documented (SWI-Prolog -- Shared tabling), shared tabling doesn’t currently support incremental tabling of any kind though. From the notes in the documentation it doesn’t sound like it’s fundamentally impossible to have the more advanced tabling work with shared tables. It just hasn’t been implemented yet.
What is required to implement this? Is this about tries currently not being thread-safe? Or is there more to it?
I don’t know whether the docs are accurate. Its long ago that I worked on tabling. I would expect well founded semantics to work with shared tabling. I don’t think the thread-safety of tries is an issue. That is probably an issue if we would like to implement multi-threaded completion. Just for incremental and monotonic tabling, the story is probably the same as for normal tabling: make sure to claim ownership on incomplete/invalid or new tables and have other threads that want to use one of these table wait for its completion.
In other words, I would expect this to be fairly feasible. The tabling code could have had a little more design documentation though There was a plan to write this down as a proper article and compare it to the SLG WAM as we find it in XSB/YAP. It never happened
❯ swipl -q
?- [user].
|: :- dynamic foo/1 as monotonic.
|: :- table bar(sum) as (shared,monotonic).
|: bar(X) :- foo(X).
|: ^Dtrue.
?- bar(X).
false.
?- assert(foo(42)).
true.
?- bar(X).
ERROR: Type error: `trie' expected, found `<clause>(0x1821680)' (a clause_reference)
ERROR: In:
ERROR: [16] trie_gen(<clause>(0x1821680),ret)
ERROR: [15] moded_gen_answer(<clause>(0x1821680),ret,_24974) at /nix/store/dgf1rif85k1zxgz9zd92k8di7x738c53-swi-prolog-9.3.8-9362c70/lib/swipl/boot/tabling.pl:692
ERROR: [11] toplevel_call(user:user: ...) at /nix/store/dgf1rif85k1zxgz9zd92k8di7x738c53-swi-prolog-9.3.8-9362c70/lib/swipl/boot/toplevel.pl:1318
ERROR:
ERROR: Note: some frames are missing due to last-call optimization.
ERROR: Re-run your program in debug mode (:- debug.) to get more detail.
But it looks like this might actually be about the aggregation, and not about using a shared monotonic tabling.
This appears to work:
❯ swipl -q
?- [user].
|: :- dynamic foo/1 as monotonic.
|: :- table bar/2 as (shared,monotonic).
|: bar(X) :- foo(Y), X is Y + 1.
|: ^Dtrue.
?- bar(42).
false.
?- assert(foo(41)).
true.
?- bar(42).
true.
So is this just implemented except for a bug in aggregation?