Weird tabling question

General
1

I’m trying to do something odd. Basically, I’m trying to queue and delay the execution of certain clauses until later.

:- dynamic negation_queue/1 as incremental.
:- dynamic negation_commit/1 as incremental.

:- table negation_helper/1 as incremental.

negation_helper(G) :-
    var(G) -> throw(user_error(negation_helper)).

% We've already committed to G
negation_helper(G) :-
    negation_commit(G),
    format('Already committed ~w', G),
    !.

% G isn't true right now.
negation_helper(G) :-
    not(G), !, fail.

% Queue G and fail.
negation_helper(G) :-
    !,
    negation_queue(G)
    -> fail
    ; format('I am queueing negation ~w~n', G), assert(negation_queue(G)), format('done'), fail.

rule :-
    writeln('I am reasoning, but about to block'),
    
    negation_helper(true),
    
    writeln('I am done').

process_queue :-
    retract(negation_queue(G)),
    % XXX What happens if G is no longer true?
    G,
    assert(negation_commit(G)).

This results in:

- rule.
I am reasoning, but about to block
I am queueing negation true
ERROR: '$idg_changed'/1: No permission to update variant `user:negation_helper(true)'
ERROR: No permission to update variant `user:negation_helper(true)'
ERROR: In:
ERROR:   [23] assert(negation_queue(true))
ERROR:   [22] negation_helper(true) at /home/ed/Dropbox/temp/swi/new.pl:25
ERROR:   [21] call(user:<closure>(negation_helper/1)(true)) at /home/ed/Documents/swipl-devel/build/home/boot/init.pl:502
ERROR:   [20] reset(user:call(...),_372,_374) at /home/ed/Documents/swipl-devel/build/home/boot/init.pl:604
ERROR:   [19] delim(ret,user:call(...),94686524255520,[]) at /home/ed/Documents/swipl-devel/build/home/boot/tabling.pl:607
ERROR:   [18] activate(ret,user:call(...),94686524255520) at /home/ed/Documents/swipl-devel/build/home/boot/tabling.pl:587
ERROR:   [17] run_leader(ret,user:call(...),fresh(94686524300528,94686524255520),_492,_494) at /home/ed/Documents/swipl-devel/build/home/boot/tabling.pl:573
ERROR:   [16] setup_call_catcher_cleanup('$tabling':'$idg_set_current'(_550,<trie>(0x561deca55c20)),'$tabling':run_leader(ret,...,...,_568,_570),_538,'$tabling':finished_leader(_580,_582,...,...)) at /home/ed/Documents/swipl-devel/build/home/boot/init.pl:679
ERROR:   [15] create_table(<trie>(0x561deca55c20),fresh(94686524300528,94686524255520),ret,user:negation_helper(true),user:call(...)) at /home/ed/Documents/swipl-devel/build/home/boot/tabling.pl:388
ERROR:   [14] catch('$tabling':create_table(<trie>(0x561deca55c20),...,ret,...,...),deadlock,'$tabling':restart_tabling(<closure>(negation_helper/1),...,...)) at /home/ed/Documents/swipl-devel/build/home/boot/init.pl:565
ERROR:   [13] start_tabling_2(<closure>(negation_helper/1),user:negation_helper(true),user:call(...),<trie>(0x561deca55c20),fresh(94686524300528,94686524255520),ret) at /home/ed/Documents/swipl-devel/build/home/boot/tabling.pl:375
ERROR:   [11] '$wrap$negation_helper'(true)1-st clause of '$wrap$negation_helper'/1 <no source>
ERROR:   [10] rule at /home/ed/Dropbox/temp/swi/new.pl:30
ERROR:    [9] toplevel_call(user:user:rule) at /home/ed/Documents/swipl-devel/build/home/boot/toplevel.pl:1173
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.

I assume this error is because negation_helper/1 is invalidating its own incremental table. Is there any way to accomplish this?

negation_helper/1 does not need to be tabled, but rule does.

@jan you probably will guess by the name, but I’m experimenting with a new way of handling negation in OOAnalyzer. If this works, it might solve some of the issues we had with monotonic tabling…

2

Instead of not/1, shouldn’t you be using tnot/1 with tabling?

3

I think tnot/1 is only for Well Founded Semantics, which I’m not using. But maybe I should take another look at it, since it seems related to the negation problem I’m actually trying to solve.

4

tnot/1 does time its argument a little different from +/1, which simply calls. tnot/1 demands the argument to be tabled. But, for example, if there is one answer in the table it will not bother to call the goal as it knows it is false. If it suspends it will also consider the negation true as soon as there is a single answer.

5

@jan do you have any suggestions for my original question?

I was playing with tnot/1 some, and I did find a way to represent a simplistic OOAnalyzer-like example using it. But I ran into problems with forall/2 not behaving as I expected – it seemed to lose track of conditional negations. Is this expected? This is not a big deal, I am just curious. I can share the example.

For now, I’d much rather get my original idea working, because it would require few changes to try out.

6

I was celebrating the 50 year anniversary of Prolog in Paris :slight_smile: Hmm. What goes wrong is easy to see: as in XSB, it is not allowed for incremental table updates to modify the dynamic predicates on which the same table depends. I guess this could in theory be “fixed” by re-triggering the incremental resolution until we reach fixed point. No clue how hard that would be to implement, neither whether it would make much sense.

Can you give a bit more high level description of what you try to achieve?

As far as forall/2 is concerned, this is implemented as \+ (Gen, \+ Test). Tabling can in general not deal with \+/1 unless the argument can be completed locally, i.e. there is no recursive dependency through the \+/1.

Tabling extends the range of programs that are “pure”, but itself interacts poorly with non-pure code :frowning:

7

Celebrating Prolog in Paris sounds very nice! :slight_smile:

I am assuming that the reason for the restriction is a semantic one – what should the behavior be if an incremental tabled predicate updates a dynamic predicate that the table depends on? In particular, if we assert(d) and then call a tabled subgoal that depends on d, which is now invalidated, do we use existing tabled answers or recompute?

For my purposes, it does not really matter. In the worst case, I will end up asserting a few extra “queue” facts.

I think if SWI had true opaque tables that I could manually manage, I would be able to implement this.

There are a few ways I can describe it… hopefully one makes sense :wink:

At a high-level, I’m trying to create a predicate negation_helper(G) that will fail until some other code decides that it is OK for negation_helper(G) to succeed.

I want to use this to delay decisions about negations, similar to tnot/1. But because of OOAnalyzer’s reasoning loop, I need/want to have explicit control over when it is “safe” to conclude that the failure to prove a fact actually constitutes negation.

From an OOAnalyzer perspective, there are a bunch of rules. Some have negations and some do not. If there is a rule that has a negation not(incrementalFact), I want to delay the interpretation of that negation until all rules (at least those that don’t have negations) that might produce incrementalFact have had the opportunity to do so.

(A while back we had some discussions about OOAnalyzer’s implicit dependence on rule ordering. A lot of those ordering decisions are to address this problem – so that by the time a negation is evaluated, any rules that might have made that negation false have already executed. This change makes those dependencies automatic/explicit. These observations are new for me, but obviously not for logic reasoning… if I had known what I was doing, I probably would have designed OOAnalyzer to utilize WFS.)

8

At the (high) risk talking nonsense, what about the code below? The semantics of negation_helper/1 will be that of not (you may use tnot/1 for \+ G, depending on intended semantics) after asserting run_negation_queue/0. Before it is simply false. Asserting this fact shall reevaluate all tables for negation_helper/1 and propagate to its dependencies.

:- table negation_helper/1 as incremental.
:- dynamic run_negation_queue/0 as incremental.

negation_helper(G) :-
    run_negation_queue,
    \+ G.

process_queue :-
    assert(run_negation_queue).
9

I am not sure if this will work or not. The downside is that we don’t put the unified Goal in the queue, so we have less control over the order in which the queue is processed. I am honestly not sure at this point if the order of the queue matters. It’s worth a try!

10

Maybe you could store the queue in non-incremental dynamic predicate and make process_queue/0 re-evaluate the affected negation_helper/1 nodes in the order you please? The order in which the system does this is hard to predict. Letting the system do this does have the advantage that it will only evaluate the nodes it considers relevant.

11

Now I feel very silly. I didn’t realize that an incremental tabled predicate was allowed to access a non-incremental dynamic predicate. I feel like that was true in XSB, but maybe I am misremembering things.

Anyway, I think I can leverage this to accomplish what I wanted.

12

I think removing “as incremental” from the declaration of negation_queue/1 in my original question gives the behavior I wanted. :exploding_head: Sorry for wasting your time!

1 Like