Non-monotonic incremental updates and negation

I just read that the semi-naive incremental update of tabled
predicates is subject to the following restrictions:

  • Only monotonic updates, i.e. assertz/1 and no retract/1,
    if retract/1 the system falls back to simply invalidate tabled predicates,
    and cannot incrementally promote changes.

  • Only programs without negation, i.e. assertz/1 is only
    incrementally promoted if the program has no negation.
    The documentation here says “In particular it does not deal
    with negation”

Is this the state of the art. What would be needed to allow
either non-monotonic updates or to allow negation or to
allow both?

My naive question might not be related to your professional question. I have heard that the table functionality is based on well-founded sematics, which means rational trees (cyclic terms) are not allowed for the table because they are not well-founded. Although I havn’t check this question myself, but I am interested in theory about how to control these so called mixed fixpoint semantics. Also I am interested in the table from my zdd library point of view, though, which uses not so elegant hash tables as the prolog table.

I don’t know whether rational trees are allowed or not allowed
in a particular tabling system u based on a theory x, or in
another tabling system v based on a theory y, so:

Lets put rational trees and/or recursion aside
to make it simple and practical.

Incremental updates are sometimes solved with semi-naive
evaluation strategies. You can easily play with it, when a) the
update is monotonic and b) the program has no negation.

If the program has no negation you can query it via
a vanilla interpreter:

solve(true) :- !.
solve((A,B)) :- !, solve(A), solve(B).
solve(H) :- past(H, B), solve(B).

if the update is monotonic, you can query the delta with:

delta(true) :- !, fail.
delta((A,B)) :- solve(A), delta(B).
delta((A,B)) :- !, delta(A), call(B).
delta(H) :- past(H, B), delta(B).
delta(H) :- insert(H, B), call(B).

Try it! In the above past/2 is the counterpart to clause/2
that gives the old state, and insert/2 is what gives the
delta from old program state to new program state.

What if a) the update is non-monotonic, and/or what if b)
the program has also negation? Any suggestions?

Also Datalog theory and logic programming theory is
rich in alternative fixpoint ideas, you hear iterated
fixpoint, 3-valued fixpoint, etc… etc…

There is the Alice book, which seems to be a modern
source for Datalog etc… It seems they link back
“fixpoints” to “while” in some of their chapters:

Foundations of Databases
Chapter 17 - First Order, Fixpoint and While

Back in the times, such a nice book didn’t exist. The update
problems and thus some transaction dynamics are only
covered in the last chapter. :frowning: