Spooky metapredicate binding behavior with reif

[jjtolton]

I've been trying to work out why in some applications I have a buildup of dif:dif(...) attributed vars. I realize that depending on how you use reif predicates, the way the attributed vars stack up is very different.

Let's start with the most basic examples, it's unclear to me why the behavior in these is different:

:- use_module(library(reif)).

taskn(A, _/B/_/_, T) :-
        =(A,B,T).

?- A=1, taskn(1, _/A/_/_, T).
   A = 1, T = true.


?- A=1, =(_/1/_/_, _/A/_/_, T).
   A = 1, T = true
;  A = 1, T = false, dif:dif(_A/1/_B/_C,_D/1/_E/_F).
% why is there a choice point here? A seems to be fully qualified


?- A=1, Task=_/B/_/_, =(A,B,T).
   A = 1, Task = _A/1/_B/_C, B = 1, T = true
;  A = 1, Task = _A/B/_B/_C, T = false, dif:dif(1,B).
% A and B seem to be fully qualified, I'm surprised again that there is a choice point here.  Is this because T is not fully qualified?

This behavior seems to add to additional complications when using tfilter/3:

%% `Schedule` is bound to the same list in all examples %%

?- Res+\(Schedule=[t1/1/2/4,t2/1/0/2,t3/2/0/2,t4/1/6/20,t5/2/6/20,t6/3/2/11,t7/3/13/11],
         tfilter(taskn(1), Schedule, Res)
        ).
   Res = [t1/1/2/4,t2/1/0/2,t4/1/6/20]. % expected
   

?- Res+\(Schedule=[t1/1/2/4,t2/1/0/2,t3/2/0/2,t4/1/6/20,t5/2/6/20,t6/3/2/11,t7/3/13/11],
         tfilter(\Goal^T^(taskn(1,Goal,T)), Schedule , Res)
        ).
   Res = [t1/1/2/4,t2/1/0/2,t4/1/6/20]. % expected, so the behavior is not caused by lambda


?- Res+\(Schedule=[t1/1/2/4,t2/1/0/2,t3/2/0/2,t4/1/6/20,t5/2/6/20,t6/3/2/11,t7/3/13/11],
         tfilter(=(_/1/_/_),Schedule,Res)
        ).
   Res = [t1/1/2/4]
;  Res = [t2/1/0/2]
;  Res = [t4/1/6/20]
;  Res = [], dif:dif(_A/1/_B/_C,t1/1/2/4), dif:dif(_A/1/_B/_C,t2/1/0/2), dif:dif(_A/1/_B/_C,t4/1/6/20). 
% why is this different than taskn/3?


?- Res+\(Schedule=[t1/1/2/4,t2/1/0/2,t3/2/0/2,t4/1/6/20,t5/2/6/20,t6/3/2/11,t7/3/13/11],
         tfilter(\Goal^T^(=(1,N,T),=(Goal,_/N/_/_,T)), Schedule,Res)
        ).
   Res = [t1/1/2/4,t2/1/0/2,t4/1/6/20], dif:dif(1,_A), dif:dif(t3/2/0/2,_B/_A/_C/_D), dif:dif(1,_E), dif:dif(t5/2/6/20,_F/_E/_G/_H), dif:dif(1,_I), dif:dif(t6/3/2/11,_J/_I/_K/_L), dif:dif(1,_M), dif:dif(t7/3/13/11,_N/_M/_O/_P)
;  Res = [t1/1/2/4,t2/1/0/2], dif:dif(1,_A), dif:dif(t3/2/0/2,_B/_A/_C/_D), dif:dif(1,_E), dif:dif(1,_F), dif:dif(t5/2/6/20,_G/_F/_H/_I), dif:dif(1,_J), dif:dif(t6/3/2/11,_K/_J/_L/_M), dif:dif(1,_N), dif:dif(t7/3/13/11,_O/_N/_P/_Q)
;  Res = [t1/1/2/4,t4/1/6/20], dif:dif(1,_A), dif:dif(1,_B), dif:dif(t3/2/0/2,_C/_B/_D/_E), dif:dif(1,_F), dif:dif(t5/2/6/20,_G/_F/_H/_I), dif:dif(1,_J), dif:dif(t6/3/2/11,_K/_J/_L/_M), dif:dif(1,_N), dif:dif(t7/3/13/11,_O/_N/_P/_Q)
;  Res = [t1/1/2/4], dif:dif(1,_A), dif:dif(1,_B), dif:dif(t3/2/0/2,_C/_B/_D/_E), dif:dif(1,_F), dif:dif(1,_G), dif:dif(t5/2/6/20,_H/_G/_I/_J), dif:dif(1,_K), dif:dif(t6/3/2/11,_L/_K/_M/_N), dif:dif(1,_O), dif:dif(t7/3/13/11,_P/_O/_Q/_R)
;  Res = [t2/1/0/2,t4/1/6/20], dif:dif(1,_A), dif:dif(1,_B), dif:dif(t3/2/0/2,_C/_B/_D/_E), dif:dif(1,_F), dif:dif(t5/2/6/20,_G/_F/_H/_I), dif:dif(1,_J), dif:dif(t6/3/2/11,_K/_J/_L/_M), dif:dif(1,_N), dif:dif(t7/3/13/11,_O/_N/_P/_Q)
;  Res = [t2/1/0/2], dif:dif(1,_A), dif:dif(1,_B), dif:dif(t3/2/0/2,_C/_B/_D/_E), dif:dif(1,_F), dif:dif(1,_G), dif:dif(t5/2/6/20,_H/_G/_I/_J), dif:dif(1,_K), dif:dif(t6/3/2/11,_L/_K/_M/_N), dif:dif(1,_O), dif:dif(t7/3/13/11,_P/_O/_Q/_R)
;  Res = [t4/1/6/20], dif:dif(1,_A), dif:dif(1,_B), dif:dif(1,_C), dif:dif(t3/2/0/2,_D/_C/_E/_F), dif:dif(1,_G), dif:dif(t5/2/6/20,_H/_G/_I/_J), dif:dif(1,_K), dif:dif(t6/3/2/11,_L/_K/_M/_N), dif:dif(1,_O), dif:dif(t7/3/13/11,_P/_O/_Q/_R)
;  Res = [], dif:dif(1,_A), dif:dif(1,_B), dif:dif(1,_C), dif:dif(t3/2/0/2,_D/_C/_E/_F), dif:dif(1,_G), dif:dif(1,_H), dif:dif(t5/2/6/20,_I/_H/_J/_K), dif:dif(1,_L), dif:dif(t6/3/2/11,_M/_L/_N/_O), dif:dif(1,_P), dif:dif(t7/3/13/11,_Q/_P/_R/_S).

% ???

As far as I can tell, all of these higher order predicates that are arg0 to tfilter/3 are logically consistent:

?- A=1,
   taskn(A, _/A/_/_, T),
   =(_/1/_/_,_/A/_/_,T),
   call(\Goal^T^(taskn(1,Goal,T)), _/1/_/_, T),
   call(\Goal^T^(=(1,N,T),=(Goal,_/N/_/_,T)), _/1/_/_, T).
   A = 1, T = true
;  false. % but this choice point surprises me!

The choice point does not seem to go away even if you qualify T:

?- A=1, T=true,
   taskn(A, _/A/_/_, T),
   =(_/1/_/_,_/A/_/_,T),
   call(\Goal^T^(taskn(1,Goal,T)), _/1/_/_, T),
   call(\Goal^T^(=(1,N,T),=(Goal,_/N/_/_,T)), _/1/_/_, T).
   A = 1, T = true
;  false.

If the answer is, "just used named predicates with reif" that's an acceptable answer. But I have a feeling there's some deeper intuition to be found about Prolog here that I would love to learn!

[jjtolton]

Ok, I think I might see what is going on here. dif/2 and dif/3 are a lot smarter than I'm giving them credit for, I think.

?- =(_/1/_/_, _/1/_/_, T).
   T = true
;  T = false, dif:dif(_A/1/_B/_C,_D/1/_E/_F).
% this caught me by surprise

This caught me by surprise, until I realized that this is actually quite precise -- arg0 and arg1 are the same unless they are not(!!!), depending on the values of the anonymous vars.

?- =(A/1/B/C, A/1/B/C, T).
   T = true.

Mystery solved, it would seem.

[jjtolton]

Okay, it is a bit convoluted, but I was able to achieve the same behavior as using a named predicate in the following manner:

?- Res+\(Schedule=[t1/1/2/4,t2/1/0/2,t3/2/0/2,t4/1/6/20,t5/2/6/20,t6/3/2/11,t7/3/13/11],
         N=1,
         TaskN=(\A^Goal^T^(Goal=_/B/_/_,=(A,B,T))),
         Tn=(\Goal^T^(call(TaskN, N, Goal, T))),
         tfilter(Tn,Schedule,Res)
        ).
%@   Res = [t1/1/2/4,t2/1/0/2,t4/1/6/20].


?- Res+\(Schedule=[t1/1/2/4,t2/1/0/2,t3/2/0/2,t4/1/6/20,t5/2/6/20,t6/3/2/11,t7/3/13/11],
         N=1,
         tfilter(taskn(N),Schedule,Res)
        ).
%@   Res = [t1/1/2/4,t2/1/0/2,t4/1/6/20].

The world makes sense again! The advantage of using a named predicate is that there is a difference between an anonymous variable and a "really don't care what the value is" variable, and a named predicate such as

taskn(A, _/B/_/_, T) :- =(A,B,T).

allows reif predicates to "not care" about the anonymous variables, while with

=(_/1/_/_, _/1/_/_, T)

(=)/3 DOES have to care about the anonymous variables. But you can use lambda to force a "don't care" by hiding the anonymous variables:

?- Same2nd=(\A^B^T^(A=_/X/_/_,B=_/Y/_/_,=(X,Y,T))), call(Same2nd,_/1/_/_,_/1/_/_, T).
%@   Same2nd = \A^B^true^(A=_A/X/_B/_C,B=_D/Y/_E/_F,=(X,Y,true)), T = true.

😮‍💨

I think I just like to make my life harder than it needs to be.

[triska]

Good analysis and solution!

Thank you for posting this, also for future reference that we can point to in case such questions arise again.