How to individually transact choicepoints for a generator predicate

Help!
1

I am struggling to find a way to use transactions to throw away side effect data from the failed choicepoints in a generator predicate. Here’s an example:

Let’s say I have multiple alternatives for a predicate called noun/3. I want to backtrack over these until I find the right one. Unfortunately, each instance of noun/3 asserts a term. I only want to keep the asserts for proofs that succeed and throw away the others. Below is an example.

The problem is that, since I am calling the noun/3 generator inside the transaction/1 predicate, Prolog only does a “redo” on the generator term, and so the transaction doesn’t rollback, it just keeps collecting changes from the (failed) backtracking.

I think I’m looking for a way to transact each choicepoint generated by the predicate passed to transaction/1 independently, rolling back all data done by a choice point on redo (as opposed to the current transaction/1 predicate that puts them all in a single transaction).

…or some other way of doing this. Unfortunately changing the noun predicates to not side effect is a large rewrite…

findDogInstance(ID) :-
    transaction((
        noun(dog, ID, Kind),
        Kind \== concept
    )).

noun(dog, ID, concept) :-
    gensym(dog, ID),
    assert(test(ID, is, dog, concept)).

noun(dog, ID, instance) :-
    gensym(dog, ID),
    assert(test(ID, is, dog, instance)).

?- findDogInstance(X).
X = dog2.

?- test(X, Y, Z, A).
% I don't want this one since it wasn't in the successful proof...
X = dog1,
Y = (is),
Z = dog,
A = concept ;

% I do want this one
X = dog2,
Y = (is),
Z = dog,
A = instance.
~~
2

Another alternative is if there is a way in Prolog to insert a predicate that runs before a redo of another predicate. Something like a redo_with_criteria(Goal, RedoGoal) predicate that backtracks over Goal and, before doing a redo on Goal, calls RedoGoal.

With that, I think I could use the transaction_updates/1 predicate to “undo” all the changes that got done.

3

Well, I found one alternative by using (possibly abusing) b_getval/2 since it undoes changes on backtracking. I wrote a transaction2/1 predicate that has the behavior I want. It does require using a special backtrack_assert/1 predicate, though. I’m not sure how efficient this is since the data could get large, but it at least shows the direction of what I’m looking for.

findDogInstance(ID) :-
    transaction2((
        noun(dog, ID, Kind),
        Kind \== concept
    )).

noun(dog, ID, concept) :-
    gensym(dog, ID),
    backtrack_assert(test(ID, is, dog, concept)).

noun(dog, ID, instance) :-
    gensym(dog, ID),
    backtrack_assert(test(ID, is, dog, instance)).

transaction2(Goal) :-
    b_setval(data, []),
    Goal,
    b_getval(data, FinalData),
    member(Item, FinalData),
    assert(Item).

backtrack_assert(Term) :-
    b_getval(data, Current),
    append([Term], Current, New),
    b_setval(data, New).

?- findDogInstance(X).
X = dog2.

?- test(X, Y, Z, A).
X = dog2,
Y = (is),
Z = dog,
A = instance.

?-
5

I guess the idea would be to have a generator before the transaction and then do the asserts and check inside, as in

noun(dog, concept).
noun(dog, instance).

     ...
     noun(dog, Class),
     transaction(( gensym(dog, ID),
                   assert(test(ID, is, dog, Class),
                   test(...))).
6

The problem I hit with that approach is that I want the noun/3 predicates to hide the fact that they just created this term and just pretend like it was there all along. Similar to my (poor) understanding of how abduction works. My example didn’t motivate this very well since I was trying to keep it simple.

Let me expand here: My goal is to be able to have predicates that “become true” for whatever you ask them by asserting terms…but then revert those terms if their truth didn’t actually help prove whatever is being proven. I originally thought transactions might be what I needed but I’m beginning to think it is a different problem and I just confused myself going that way.

The work done by @pmoura on logtalk assumptions is tantalizing close to what I think I need. Below I’ve copied the code for his assumei/1 predicate and the example works almost exactly like I want. In the example below, all of the failed choicepoints delete their side effects, just like I wanted. The only difference from my original design is that a choicepoint that succeeds, and is used to prove the whole query, disappears on final backtracking (i.e. after you push ; in this example). So, when the query is done, the data disappears.

This behavior might be OK for my scenario, I’ll have to work it through a bit. I think I can have assume/1 mark the data so I know it is “new” and then I can just reassert it afterwards…somehow.

findDogInstance(ID) :-
    noun(dog, ID, Kind),
    Kind \== concept,
    % Show what facts are currently asserted
    test(A, B, C, D),
    writeln(test(A, B, C, D)).

noun(dog, ID, concept) :-
    gensym(dog, ID),
    assume(test(ID, is, dog, concept)).

noun(dog, ID, instance) :-
    gensym(dog, ID),
    assume(test(ID, is, dog, instance)).

assume(Fact) :-
    assertz(Fact).

% TODO: Don't retract the fact if it was part of the solution
assume(Fact) :-
    retract(Fact),
    !,
    fail.


?- findDogInstance(X).
test(dog14,is,dog,instance)
X = dog14 ;
false.

% This is the only part that isn't right for my scenario.  
% I want the data for a proven solution to stick around...
?- test(A, B, C, D).
false.
7

FWIW, this solution did end up working for my scenario. The way I solved fishing out the “new” data and asserting afterwards so it sticks around was by maintaining a non-backtrackable global so that I know which asserts in the database were assumptions (and will disappear) and could reassert them so they stick around.

The only issue I’ve found so far is the fact that using \+ (and some other predicates potentially, I think) cuts the choice point that “undoes” the assumption and so they stick around in the database. So far, this hasn’t been a problem, I just have to code carefully. We’ll see if it is a problem later…

replaceAssumptions(Assumptions) :-
    must_be(list, Assumptions),
    nb_setval(assumptions, Assumptions).

capturedAssumptions(Assumptions, Clear) :-
    nb_current(assumptions, Assumptions),
    must_be(list, Assumptions),
    !,
    (
        Clear == clear
        ->
        (
            nb_delete(assumptions)
        )
        ;
        (
            true
        )
    ).

capturedAssumptions([], _).

releaseAssumption(data(Subject, Rel, Object, Graph)) :-
    nb_current(assumptions, Current),
    !,
    findall(data(SubjectIn, RelIn, ObjectIn, GraphIn),
        (
            member(data(SubjectIn, RelIn, ObjectIn, GraphIn), Current),
            \+ (SubjectIn = Subject, RelIn = Rel, ObjectIn = Object, GraphIn = Graph)
        ),
        New),
    replaceAssumptions(New).

% in case nb_getval(assumptions) has been deleted
releaseAssumption(_).

captureAssumption(Assumption) :-
    nb_current(assumptions, Current),
    !,
    append(Current, [Assumption], New),
    replaceAssumptions(New).

captureAssumption(Assumption) :-
    replaceAssumptions([Assumption]).

% Note that these *do not* undo assumptions if called with \+
assume(Subject, Relationship, Object, Graph) :-
    store_assert(Subject, Relationship, Object, Graph),
    captureAssumption(data(Subject, Relationship, Object, Graph)).

assume(Subject, Relationship, Object, Graph) :-
    store_retractall(Subject, Relationship, Object, Graph),
    releaseAssumption(data(Subject, Relationship, Object, Graph)),
    !,
    fail.