#214 Incremental tabling returns incorrect answer

Wish List
open
nobody
None
5
2013-12-14
2013-12-08
Michael Kifer
No

%% The following simple program shows that incremental tabling does not always
%% update all tables correctly.

/ Please see explanations inline /

:- dynamic p/1, neg_p/1 as incremental.
:- table q/1, defeated/1 as incremental.
:- import incr_assert/1 from increval.

bb(x).
cc(a).
q(X) :- bb(X).
q(X) :- p(X).

defeated(p(X)) :- cc(X), clause(neg_p(),).

/
Only q(X) :- bb(X) can fire, so Attempt 1 prints only
q = x -- correct
/
?- writeln('Attempt 1:'), (q(X), writeln(q=X), fail ; true).

/
Now q(X) :- p(X) :- cc(X), X=a can fire.
Also, defeated(p(X)) is false, since clause(neg_p(
),) is false.
So, Attempt 2 will print
q = a -- correct
q = x -- correct/
?- incr_assert((p(X):-cc(X),tnot(defeated(p(X))))).
?- writeln('Attempt 2:'), (q(X), writeln(q=X), fail ; true).

/*
Now neg_p(X) becomes a head of a clause. So, defeated(p(a)) is true.
Therefore, p(a) now becomes false, so q(a) should be false.
Attempt 3 should be printing
q = x
but instead prints both
q = a -- wrong!!!
q = x -- correct

** This is an incremental tabling problem. Indeed, the next
abolish_all_tables and subsequent Attempt 4 should that when tables
are cleared out then it would print only q = x.
/
?- incr_assert(neg_p(a)).
?- writeln('Attempt 3:'), (q(X), writeln(q=X), fail ; true).

/ Only after abolishing we are getting a correct result. /
?- abolish_all_tables.
?- writeln('Attempt 4:'), (q(X), writeln(q=X), fail ; true).

Discussion

  • Terrance Swift
    Terrance Swift
    2013-12-13

    I don't consider this a bug for now, because ...

    If you make the change:

    %defeated(p(X)) :- cc(X), clause(neg_p(),).
    defeated(p(X)) :- cc(X), neg_p(Y).

    Things work fine -- at least in the SVN version. The problem is that the clause/2 isn't really considered a call in terms of creating the call dependency graph. In fact, I think it should be, unless there is some compelling case that I'm missing. So I'll close it out.

     
  • Terrance Swift
    Terrance Swift
    2013-12-13

    • status: open --> closed
     
  • Terrance Swift
    Terrance Swift
    2013-12-13

    Problem was with the use of clause/2. Closing for now.

     
  • Michael Kifer
    Michael Kifer
    2013-12-14

    the problem is that for defeasible reasoning one needs to do metaprogramming.
    I am not sure this is relevant at present, but maybe it should be reclassified as a wish list?

     
  • Michael Kifer
    Michael Kifer
    2013-12-14

    • status: closed --> open
    • Group: Performance problem --> Wish List