Unexplained behaviour wrt the well founded semantics - Part 1

Help!
1

Hi all,

I’m using: SWI-Prolog version 8.2.4

I have the following program :

:- table (p/1,q/1) as incremental. 
:- dynamic([p/1,q/1], [incremental(true)]).
q(1).
p(X) :- tnot(q(X)), tnot(p(X)).

I obtained 2 different results with the two following executions (whereas I expect to obtain the same results).

Execution 1: (the good results wrt well founded semantics)

?- p(1).
false.

?- retract(q(1)).
true.

?- q(1).
false.

?- p(1).
% WFS residual program
    p(1) :-
        tnot(p(1)).
p(1).

Execution 2 (obtained after ending the first prolog process and reconsulting):

?- p(1).
false.

?- retract(q(1)).
true.

?- p(1).
false.

Could you explain to me why checking q(1) after having retracted it is necessary to obtain the good result ?

Best regards

Christophe

2

This is a bug, though I’m not yet sure how to fix it. At the same time it is a bit impractical way to code this. q/1 is a simple dynamic fact (at least for now). While tnot/1 is typically used as negation in WFS tabled context and tnot/1 wants a tabled predicate, I guess you decided to make q/1 both tabled and dynamic. That doesn’t work as-is.

The practical way around is to make q/1 only dynamic and incremental and use \+/1 rather than tnot/1. That is safe as tnot/1 only differs from \+/1 if there is a loop through the negated argument. So the program becomes

:- table p/1 as incremental.
:- dynamic q/1 as incremental.

q(1).
p(X) :- \+ q(X), tnot(p(X)).

And all works (for me at least) as advertised. This is anyway the preferred way to code this if q/1 is a simple list of facts. Things may get more complicated if q/1 contains rules, and in particular if it contains rules that lead to cycles. Another way to “solve” this is to have a static tabled predicate as argument to the tnot/1 and make that call the dynamic predicate.

I have to think about the consequences of q/1 being both dynamic and tabled. Considering that the quite comprehensive test set ported from XSB doesn’t seem to include any tests for this suggests this is not common practice :slight_smile:

edit Pushed 5772c803985cb8f88b0f96052abf8c939f8b8c23 to address this.

2 Likes
3

Hi Jan,
many thanks for your quick answer.
Unfortunately, as you guessed it, the q predicate is apriori involved in cyclic rules… But I will first try your 2 solutions you propose because I am not sure about the need to table q.
About the second solution, I do not understand when you say “and make that call the dynamic predicate”. Could you give me more details ?

By the way, I was wondering if there is any scientific paper or book about the use of the well founded semantics, i.e. some documentation that explains not what is WFS, but how to concretely use it, whether there are programming idioms or even design patterns associated to WFS.

Many thanks again !

Best regards

Christophe

4

Instead of tnot(q(X)), call tnot(qs(X)), table qs/1 and give it the definition

qs(X) :- q(X).

If you picked up the edit, I pushed a fix that makes your original work just fine.

Good question. I’d poke around in the XSB world. That is where it comes from and where it is actually used for years. Well, maybe some people here have gathered concrete experience?

5

Thank you very much Jan. I try all this and get back to tell if I managed to solve my problem.

Oh, and I’m sorry but I’m new here and I do not know what to to with
“edit Pushed 5772c803985cb8f88b0f96052abf8c939f8b8c23 to address this.”
Sorry for this stupid question. I try to search the wiki to understand but without success. Sorry for bothering…

Christophe

6

These hashes are GIT commit hashes. If not specified otherwise they refer to the main (swipl-devel.git) repo. You can find the details of this commit, usually by running git show <hash> in your (up-to-date) checked out version of the source code.

People can use this information for backporting to older versions, finding references, check if they already have the patch, etc. If you want to keep it simple, wait for the next (development) release. If you are in a hurry, build from source or (for Windows) download the daily binaries the next day (they are build around 3am UTC).

7

Thanks a lot Jan !
I am impressed you can go so quickly deep into such a complex code, even if it’s yours :astonished:

8

I must say that Jan is one of the most talented software developers I have seen in my life.

1 Like
9

Hi Jan,

I found another case that does not behave as I expect. The first problem I had and that you solved was

:- table (p/1,q/1) as incremental.
:- dynamic([p/1,q/1], [incremental(true)]).
q(1).
p(X) :- tnot(q(X)), tnot(p(X)).

Now the new problem occurs when adding just one line as follows:

:- table (p/1,q/1) as incremental.
:- dynamic([p/1,q/1], [incremental(true)]).
q(1).
p(X) :- tnot(q(X)), tnot(p(X)).
p(X) :- q(X).

In this case, we have the following execution:

?- p(1).
true.

?- retract(q(1)).
true.

?- p(1).
false.

Here, it is ok that at first p(1) is true. But when retracting q(1), it seems as if p(1) was not recomputed, thus leading to tnot(p(1)) to false and then both rules giving p(1) are false so p(1) is false. Instead, I think that since q(1) is no longer true, then p(1) is no longer true, so when looking at rule

p(X) :- tnot(q(X)), tnot(p(X)).

it should infer p(1) undefined. Is there something I miss ?

I precise I am doing these tests having recompiled the source code of SWI (on linux).

Christophe

edit: I’ve just tested the same example with XSB 4.0, and it works as expected. The XSB code is:

:- table p/1 as incremental.
p(X) :- tnot(qs(X)), tnot(p(X)).
p(X) :- qs(X).

:- table qs/1 as incremental.
qs(X) :- q(X).

:- dynamic q/1 as incremental.
q(1).

and the execution is:

| ?- p(1).

yes
| ?- increval:incr_retract(q(1)).

yes
| ?- p(1).

undefined
10

Thanks :slight_smile: The problem was not that there was no reevaluation taking place. The problem was that tnot/1 still found the invalidated answer for p(1) and thus failed immediately. The second problem was that turning the answer into a conditional answer didn’t force the trie to be recompiled, so then we got simply true. Now we get what we expect :slight_smile: Pity that the XSB test set didn’t test this :frowning:

Pushed a couple of patches to address this.

1 Like
11

Cool !
Many thanks, Jan. I recompile and test as soon as possible.

12

Hi Jan,
sorry to bother you again, but I find other problems after recompiling. So the program is the last one :

:- table (p/1,q/1) as incremental.
:- dynamic([p/1,q/1],[incremental(true)]).
q(1).
p(X) :- tnot(q(X)),tnot(p(X)).
p(X) :- q(X).

Now the execution is :

?- p(1).
true.

?- retract(q(1)).
true.

?- p(1).
% WFS residual program
    p(1) :-
        tnot(p(1)).
p(1).

?- assert(q(1)).
true.

?- p(1).
% WFS residual program
    p(1).
p(1).

?- retract(q(1)).
true.

?- p(1).
false.

The three first queries are ok, and now work well thanks to your patches. But then reasserting q(1) should get back to p(1) true. And after that, retracting q(1) should get p(1) undefined. Do you agree ?

Cheers

edit : If that can help, I’ve found another example of the same kind:

Program:


:- table p/1 as incremental.
p(X) :- tnot(qs(X)), tnot(p(X)).
p(X) :- tnot(rs(X)), tnot(p(X)).

:- table qs/1 as incremental.
qs(X) :- q(X).
:- table rs/1 as incremental.
rs(X) :- q(X).

:- dynamic q/1 as incremental.
q(1).

and execution:


?- p(1).
false.

?- retract(q(1)).
true.

?- p(1).
% WFS residual program
    p(1) :-
        tnot(p(1)).
p(1).

?- assert(q(1)).
true.

?- p(1).
% WFS residual program
    p(1) :-
        tnot(p(1)).
p(1).

The last answer should be false I think.

1 Like
13

Thanks to Jan’s great works, there is no problem anymore.
Thank you !

14

Hi Jan,
Sorry to bother you again, but I found the following problem:

Program

:- table p/1 as incremental.
p(X) :- tnot(q(X)), r(X), tnot(p(X)).
p(X) :- r(X).

:- table q/1 as incremental.
q(X) :- tnot(r(X)).
:- table r/1 as incremental.
r(X) :- r1(X).

:- dynamic r1/1 as incremental.
r1(1).

Execution

?- p(1).
true.

?- retract(r1(1)).
true.

?- p(1).
ERROR: Type error: `worklist' expected, found `invalid' (an atom)
ERROR: In:
ERROR:   [38] '$tbl_wkl_negative'(invalid)
ERROR:   [37] negation_suspend(user:q(1),ret,invalid) at /usr/local/lib/swipl/boot/tabling.pl:892
ERROR:   [35] p(1) at /media/sf_WumpusWorld/test11.pl:3
ERROR:   [34] call(system:<closure>(p/1)(1)) at /usr/local/lib/swipl/boot/init.pl:484
ERROR:   [33] reset(system:call(...),_46230,_46232) at /usr/local/lib/swipl/boot/init.pl:572
ERROR:   [32] delim(ret,system:call(...),139959898508016,[]) at /usr/local/lib/swipl/boot/tabling.pl:606
ERROR:   [31] activate(ret,system:call(...),139959898508016) at /usr/local/lib/swipl/boot/tabling.pl:584
ERROR:   [30] run_leader(ret,system:call(...),fresh(139959902516752,139959898508016),_46350,_46352) at /usr/local/lib/swipl/boot/tabling.pl:570
ERROR:   [29] setup_call_catcher_cleanup('$tabling':'$idg_set_current'(_46408,<trie>(0x7f4af44bfe40)),'$tabling':run_leader(ret,...,...,_46426,_46428),_46396,'$tabling':finished_leader(_46438,_46440,...,...)) at /usr/local/lib/swipl/boot/init.pl:646
ERROR:   [28] create_table(<trie>(0x7f4af44bfe40),fresh(139959902516752,139959898508016),ret,user:p(1),system:call(...)) at /usr/local/lib/swipl/boot/tabling.pl:384
ERROR:   [27] catch('$tabling':create_table(<trie>(0x7f4af44bfe40),...,ret,...,...),deadlock,'$tabling':restart_tabling(<closure>(p/1),...,...)) at /usr/local/lib/swipl/boot/init.pl:546
ERROR:   [23] ignore(user:p(1)) at /usr/local/lib/swipl/boot/init.pl:529
ERROR:   [22] setup_call_catcher_cleanup('$tabling':nb_setval('$tbl_reeval',true),'$tabling':ignore(...),_46624,'$tabling':nb_delete('$tbl_reeval')) at /usr/local/lib/swipl/boot/init.pl:646
ERROR:   [20] reeval_node(<trie>(0x7f4af44bfe40)) at /usr/local/lib/swipl/boot/tabling.pl:1999
ERROR:   [19] reeval_heads([[<trie>(0x7f4af44bfe40)]],<trie>(0x7f4af44bfe40),_46710) at /usr/local/lib/swipl/boot/tabling.pl:1931
ERROR:   [16] reeval_paths([[<trie>(0x7f4af43b5f70)|...],...|...],<trie>(0x7f4af44bfe40)) at /usr/local/lib/swipl/boot/tabling.pl:1917
ERROR:   [15] try_reeval(<trie>(0x7f4af44bfe40),user:p(1),ret) at /usr/local/lib/swipl/boot/tabling.pl:1868
ERROR:   [14] catch('$tabling':try_reeval(<trie>(0x7f4af44bfe40),...,ret),deadlock,'$tabling':retry_reeval(<trie>(0x7f4af44bfe40),...)) at /usr/local/lib/swipl/boot/init.pl:546
ERROR:    [9] toplevel_call(user:user: ...) at /usr/local/lib/swipl/boot/toplevel.pl:1116
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.
   Exception: (35) p(1) ?
15

Thanks. That was a simple one solved by 1750b24d77505d3b1f35aa3d9865f94226c3a129. I’m a little surprised by the number of issues that remained. Good thing is that your examples can go almost unmodified into the test suite :slight_smile:

16

That’s great Jan ! Problems have been solved both in the examples and in my original code. Glad that the examples may be integrated to the test suite. I’ve made then from my original code which is a bit longer, trying to get the same situations but with the shortest program possible.
Thanks again !

2 Likes