Interesting behaviour in bagof call

First of all the behaviour happens with assoc and dict. So it is either a bagof issue or normal because the same behaviour I have also on scryer prolog. But when it is normal then I would like it to have an explanation.

I have the following code:

:- use_module(library( assoc)).
:- use_module(library( lists)).

rule1( _{v1:[A]}, (A=1)).
rule1( _{v2:A}, (A=2)).

rule2( _{v1:A}, (A=1)).
rule2( _{v2:A}, (A=2)).

solve1( RULE, DICT_OUT, L_OUT) :- true
, DICT_OUT = _{v1:_, v2:_}
, bagof( S, ( D, RULE, C)^( C=..[RULE, D, S], C, D >:< DICT_OUT), L_OUT)
.


When I call it then I get the following results:

?- solve1( rule1, D, L).
D = _{v1:_, v2:_A},
L = [_A=2] ;
D = _{v1:[_A], v2:_},
L = [_A=1].

?- solve1( rule2, D, L).
D = _{v1:_A, v2:_B},
L = [_A=1, _B=2].

I don’t understand where the difference comes from. What I want is the second, so I used as a solution this:

solve1_2( RULE, DICT_OUT, L_OUT) :- true
, DICT_OUT = _{v1:_, v2:_}
, bagof( EL, ( D, RULE, C,S)^( C=..[RULE, D, S], C, EL = ( D >:< DICT_OUT, S)), L_OUT0)
, maplist( [(C,S),S]>>(C), L_OUT0, L_OUT)
.

The output I want to have is:

(ins)?- solve1_2( rule1, D, L).
D = _{v1:[_A], v2:_B},
L = [_A=1, _B=2].

The assoc version looks like this:

rule3( AS, (A=1)) :- list_to_assoc([v1-[A]], AS).
rule3( AS, (A=2)) :- list_to_assoc([v2-A], AS).

rule4( AS, (A=1)) :- list_to_assoc([v1-A], AS).
rule4( AS, (A=2)) :- list_to_assoc([v2-A], AS).

assoc_unify( A1, A2) :- true
, bagof(V1=V2, K^( gen_assoc( K, A1, V1), gen_assoc( K, A2, V2)), L)
, maplist(call, L)
.

solve2( RULE, DICT_OUT, L_OUT) :- true
, list_to_assoc( [v1-_, v2-_], DICT_OUT)
, bagof( S, ( D, RULE, C)^( C=..[RULE, D, S], C, assoc_unify( D , DICT_OUT) ), L_OUT)
.

And the output is:


?- solve2( rule3, DICT_OUT, L_OUT).
DICT_OUT = t(v2, _A, <, t(v1, _, -, t, t), t),
L_OUT = [_A=2] ;
DICT_OUT = t(v2, _, <, t(v1, [_A], -, t, t), t),
L_OUT = [_A=1].

?- solve2( rule4, DICT_OUT, L_OUT).
DICT_OUT = t(v2, _A, <, t(v1, _B, -, t, t), t),
L_OUT = [_B=1, _A=2].

In the second variation DICT_OUT changes 2 times and bagof does not backtrack. I have no idea which of both outputs are actually considered wrong. When I take the bagof docs word by word then the backtracking version should be ok.

Is this a bug?

And is there an easier was to say bagof that DICT_OUT should be modified inplace?

Thanks in Advance,
Frank Schwidom

Not an answer, but whenever I have trouble with a bagof/3, I first rewrite without the ^, as a separate predicate, e.g.:

solve1( RULE, DICT_OUT, L_OUT) :- true
, DICT_OUT = _{v1:_, v2:_}
, bagof( S, solve1a(S, DICT_OUT), L_OUT)
.
solve1a(S, DICT_OUT) :-
    C=..[RULE, D, S], 
    C, 
    D >:< DICT_OUT.

BTW, I think you can do the call like this:

    call(RULE, D, S)

so it becomes:

solve1a(S, DICT_OUT) :-
    call(RULE, D, S), 
    D >:< DICT_OUT.

Thanks for your idea, I reformulated it (RULE was missing):

solve1_3( RULE, DICT_OUT, L_OUT) :- true
, DICT_OUT = _{v1:_, v2:_}
, bagof( S, solve1_3a( RULE, S, DICT_OUT), L_OUT)
.

solve1_3a( RULE, S, DICT_OUT) :- true
, call(RULE, D, S)
, D >:< DICT_OUT
.

And the behaviour keeps the same:

?- solve1_3( rule1, D, L).
D = _{v1:_, v2:_A},
L = [_A=2] ;
D = _{v1:[_A], v2:_},
L = [_A=1].

?- solve1_3( rule2, D, L).
D = _{v1:_A, v2:_B},
L = [_A=1, _B=2].

I found a variation without dictionaries:


rule5( 0, [A], (A=1)).
rule5( 1, A, (A=2)).

rule6( 0, A, (A=1)).
rule6( 1, A, (A=2)).

solve3( RULE, L, L_OUT) :- true
, L = [_,_]
, bagof( S, ( RULE, I, D)^( call( RULE, I, D, S), nth0(I, L, D)), L_OUT)
.

/*

% same problem here

(ins)?- solve3( rule5, L, L_OUT).
L = [_, _A],
L_OUT = [_A=2] ;
L = [[_A], _],
L_OUT = [_A=1].

(ins)?- solve3( rule6, L, L_OUT).
L = [_A, _B],
L_OUT = [_A=1, _B=2].

*/

Regards, 
Frank.

And btw. I get the same output for this example in gprolog and scryer prolog.

When this operation produces 1 output :


?- L0 = [(0, A, (A=1)), (1, B, (B=1))], L = [_,_], bagof( S, ( L0, I, D)^( member( (I,D,S), L0) , nth0(I, L, D) ), L_OUT).
L0 = [(0, A, A=1), (1, B, B=1)],
L = [_A, _B],
L_OUT = [_A=1, _B=1].

why then this produces 2 outputs?


?- A=[_,_], B=[_,_] , bagof( I, E^(nth0( I, A, E), nth0( I, B, E)), L).
A = [_A, _],
B = [_A, _],
L = [0] ;
A = [_, _A],
B = [_, _A],
L = [1].

Regards.

You do not use existential qualification for the list L. This list introduces 2 variables that get different values with rule5 ([A] vs A) and twice the same value for rule6.

Getting bagof/3 wrong is really easy. I think group_by/4, which was introduced as part of library(solution_sequences) to provide more SQL-like primitives might be better primitive. This is like bagof/3, but you specifify the variables on which you want to group rather than those on which you do not want to group.

group_by doesn’t really solve my problem:


rule5( 0, [A], (A=1)).
rule5( 1, A, (A=2)).

rule6( 0, A, (A=1)).
rule6( 1, A, (A=2)).

solve3( RULE, L, L_OUT) :- true
, L = [_,_]
, bagof( S, ( RULE, I, D)^( call( RULE, I, D, S), nth0(I, L, D)), L_OUT)
.

solve3_2( RULE, L, L_OUT) :- true
, L = [_,_]
, group_by( L, S, ( call( RULE, I, D, S), nth0(I, L, D)), L_OUT)
.

/*

?- solve3( rule5, L, L_OUT).
L = [_, _A],
L_OUT = [_A=2] ;
L = [[_A], _],
L_OUT = [_A=1].

?- solve3( rule6, L, L_OUT).
L = [_A, _B],
L_OUT = [_A=1, _B=2].

?- solve3_2( rule5, L, L_OUT).
L = [_, _A],
L_OUT = [_A=2] ;
L = [[_A], _],
L_OUT = [_A=1].

?- solve3_2( rule6, L, L_OUT).
L = [_A, _B],
L_OUT = [_A=1, _B=2].

*/

In the end it does the same like bagof but with the inverted quantification :


(ins)?- listing(group_by).
:- meta_predicate solution_sequences:group_by(?,?,0,-).

solution_sequences:group_by(By, Template, Goal, Bag) :-
    ordered_term_variables(Goal, GVars),
    ordered_term_variables(By+Template, UVars),
    ord_subtract(GVars, UVars, ExVars),
    bagof(Template, ExVars^Goal, Bag).

true.

There should be one parameter more for bagof / group_by where I can explicitly say: It is a free variable but it does not get grouped but unified again. That would solve it. Then I could avoid the intermediate list processing.

It is not clear to me what you are trying to solve. I only notice that the reason you get one answer for one and two for the other is because you get the same list in one case and two different lists in the other.

I assume this is an artificial version of some real problem. The clean way out might be at a higher level.