Dif/2 call as implication premiss: is the implication's else part run? Should it be?

[dtonhofer]

I have tried to understand the behaviour of dif/2 (which leads to a state diagram) but have a this little phenomenon:

Here is some code which has a dif/2 call in place of an implication premiss (ok, not really an implication rather than a control construct):

magic_of_dif(A,B,W) :-
   A=f(_),
   B=f(y),
   % At this point, we cannot say for sure whether it will
   % turn out that A==B or not. It could go either way.
   (dif(A,B)
    -> 
    proceed_hoping_that_dif_will_turn_true(A,B,W)
    ;
    try_again(A,B)).
      
try_again(A,B) :-    
   format("Trying again after dif(A,B) collapsed to 'false'\n",[]);
   format("Post optimistic valus: A=~q, B=~q\n",[A,B]).
   
proceed_hoping_that_dif_will_turn_true(A,B,W) :- 
   format("Proceeding, hoping that dif/2 will turn true\n"), 
   format("Optimistic valus: A=~q, B=~q\n",[A,B]),
   ((W==make_equal) 
    -> 
    (A=f(y),format("Never get here\n",[]))           % dif(A,B) collapses to false
    ;
    (A=f(x),format("inequality confirmed\n",[]))).   % dif(A,B) confirmed to be true   

The “happy path” of execution would be to confirm dif(A,B) as true. “Optimistically continuing” when dif(A,B) was the right choice:

?- magic_of_dif(A,B,_).
Proceeding, hoping that dif/2 will turn true
Optimistic valus: A=f(_13388), B=f(y)
inequality confirmed
A = f(x),
B = f(y).

On the other hand, calling magic_of_dif/3 with the instruction to make A and B equal (the case where optimism is not rewarded) reveals that the else branch of ->/2 is not taken. Is this expected?

?- magic_of_dif(A,B,make_equal).
Proceeding, hoping that dif/2 will turn true
Optimistic valus: A=f(_12650), B=f(y)
false.

Maybe I have I have some wrong idea about the workings of dif/2?

[peter.ludemann]

In the code you’ve written, the call to dif/2 will behave as if it has succeeded, subject to further unification of the arguments. When the arguments are unified, then dif/2 will be re-awakened and can fail; however the if-then-else has already removed a choice point, so you won’t get the result you expect.

You can see this with a simpler query:

?- ( dif(X,Y) -> writeln(yes) ; writeln(no) ), X = 1, Y = 1.
yes
false.

compared to:

?- X = 1, Y = 1, ( dif(X,Y) -> writeln(yes) ; writeln(no) ).
no
X = Y, Y = 1.

You might want to look into library(reif) on this page: https://www.metalevel.at/prolog/metapredicates
(I’m in the process of turning this into a “pack” for SWI-Prolog)

[dtonhofer]

Thank you Peter.

But I would expect the program to continue as if dif(X,Y) had failed, and thus call the “else” goal.

Another example:

docut(X,Y) :- dif(X,Y),!,postdif(X,Y).
docut(X,Y) :- writeln(alternative),postdif(X,Y).
   
do(X,Y) :- dif(X,Y),postdif(X,Y).
do(X,Y) :- writeln(alternative),postdif(X,Y).

postdif(X,Y) :- 
   writeln(X), X = 1, writeln(Y), Y = 1, 
   writeln('end of clause').

After dif/2 “late failure” Prolog rolls back to where?

For do/2 it seems to behave as if dif(X,Y) had failed, and takes the alternative clause.

?- do(X,Y).
_13340
_13372
alternative
_12986
_12988
end of clause
X = Y, Y = 1.

For do_cut/2 it seems to behave as if dif(X,Y) had failed, but the cut traversed. The alternative clause is not taken:

?- docut(X,Y).
_12628
_12660
false.

This seems strange. Why has the cut been traversed already?

I will definitely check library(reif).

[ridgeworks]

My interpretation:

dif/2 does not fail unless X and Y cannot be unified at the point of call. It succeeds if they can never be unified. If that can’t yet be determined, e.g., X and Y are both variables, it succeeds AND enables a “constraint” that they can never be unified. On backtracking over the dif, this constraint is removed, but that’s it.

Whenever X or Y are unified, the constraint wakes up and checks that it still applies. It’s as if dif(X,Y) with new binding is executed again as part of the unification. But the thing that does fail when the constraint is violated is the unification, which, in your example is Y=1 in postdif.

So looking at ?- do(X,Y):

1. Apply the constraint dif(X,Y) and call postdif(X,Y).
2. Y=1 subsequently fails the dif test, postdif fails, backtracking over the original dif call, removing the constraint.
3. Try the second clause of do/2 which subsequently calls postdif again without the constraint, so it then succeeds.

docut works the same except the choicepoint for the second clause of docut has been removed when 'postdif` fails so the query fails.

Make any sense?

[dtonhofer]

Yes, makes sense.

But the fact that the choicepoint has been removed does not. What might be the rationale (it could be that that is the way of implementing it without having to fuss around with rare edge cases…)?

[ridgeworks]

Don’t think I follow you. The only choicepoint is the second clause of do/2 and it’s not removed (prints alternative and executes postdif again). What other choicepoint is there?

And in your first example try_again will never be executed due to the semantics of -> ; (see manual) as Peter says, i.e., nothing to do with dif.

[peter.ludemann]

Here’s a simple “reified” version of dif/2 (it requires its arguments to be fully ground rather than sufficiently ground):

%! test(X, Y, Result) is det.
% Result is 'dif'   when X and Y become ground and are not unifiable
% Result is 'equal' when X and Y become ground and are unifiable
test(X, Y, dif) :-
    when((ground(X),ground(Y)), X\=Y).
test(X, Y, equal) :-
    when((ground(X),ground(Y)), X==Y).

my_dif(X, Y) :- test(X, Y, dif).

And running it gets:

?- test(X, Y, Result), X=1, Y=1.
X = Y, Y = 1,
Result = equal.

15 ?- test(X, Y, Result), X=1, Y=2.
X = 1,
Y = 2,
Result = dif

You could then rewrite your if-then-else to not have a cut but instead have both the condition and its inverse – that is: if cond then A else B becomes (cond & A) | (~cond & B).

?- ( test(X, Y, dif), writeln(different) ; test(X, Y, equal), writeln(equal) ), X=1, Y=1.
different
equal
X = Y, Y = 1.

?- ( test(X, Y, dif), writeln(different) ; test(X, Y, equal), writeln(equal) ), X=1, Y=2.
different
X = 1,
Y = 2 

[jan]

The general rule of thumb is that constraints and cuts (and thus if-then-else and negation) do not play together. It only works if all relevant constraints are resolved before committing. That is in general hard to predict. Constraint solvers have in general incomplete propagation and thus may have pending constraints even in cases where all constraints can be resolved. At debug time, call_residue_vars/2 can be used to verify there are no pending constraints. The implementation is fairly costly in terms of additional bookkeeping that, for example, protects constraints against garbage collection. This may prohibit usage at runtime.

[dtonhofer]

And in your first example try_again will never be executed due to the semantics of -> ; (see manual) as Peter says, i.e., nothing to do with dif .

No, it has everything to do with dif/2. It’s new & undefined semantics: the whole ->/2 goal behaves as if it had already been run once upon dif/2 “late failure”. One can live with that behaviour of course, but it’s definitely not in the manual.

Would you really expect to not see a “no” and an “END” printed here in addition to “yes”?
I would not. The manual says nothing about that either way.

?- ( dif(X,Y) -> writeln(yes) ; writeln(no) ), X = 1, Y = 1, write(" END").
yes
false.

Or with alternative branches prior to the ->/2:

?- (write("START ");write("BACK ")), 
   ( dif(X,Y) -> writeln(yes) ; writeln(no) ), 
   X = 1, Y = 1, write(" END").
START yes
BACK yes
false.

[swi]

@dtonhofer

But the fact that the choicepoint has been removed does not

By the way, just as a side note, there is also *->/2 which doesn’t prune the choice points.

6 ?- between(1,3,N) -> A=yes; A=no.
N = 1,
A = yes. % -> prunes the choice points

7 ?- between(1,3,N) *-> A=yes; A=no.
N = 1,
A = yes ;
N = 2,
A = yes ;
N = 3,
A = yes. % *-> doesn't prune choice points.

EDIT: @EricGT The automatic doc-link for *->/2 produces a 500 HTTP return code (Internal Server error) when you click on it, but the summary tooltip is okay.

[ridgeworks]

@dtonhofer

Would you really expect to not see a “no” and an “END” printed here in addition to “yes”?
I would not. The manual says nothing about that either way.

Short answer: I would not expect to see a “no” and an “END” printed.

From the reference manual:
"
Condition -> Action ; Else
This construct implements the so-called‘soft-cut’. The control is defined as follows: If Condition succeeds at least once, the semantics is the same as ( call(Condition) , Action). If Condition does not succeed, the semantics is that of (\+ Condition, Else). In other words, if Condition succeeds at least once, simply behave as the conjunction of call(Condition) and Action, otherwise execute Else.
"

So once dif(X,Y) (or any goal), succeeds the Else is never executed so “no” is not printed. And since dif(X,Y) did succeed there is now a constraint between X and Y which fails when Y=1, the whole query fails and “END” is not printed. The only time I would expect to see “no” printed is when X and Y are bound to the same term as defined by ‘==’.

Furthermore dif(X,Y) is deterministic (see manual); it either fails or succeeds. When it succeeds it may leave a constraint on its arguments that causes a subsequent unification (note: not the call to dif) to fail. But dif never leaves a choicepoint.

[ridgeworks]

@jan

The general rule of thumb is that constraints and cuts (and thus if-then-else and negation) do not play together. It only works if all relevant constraints are resolved before committing. That is in general hard to predict.

Not sure I follow this. An application of a constraint may fail if the constraint is already “violated” at the that time. If the application succeeds, it may cause a unification failure at any time in the forward computation. It seems to me that this is independent of any cuts.

[jan]

@ridgeworks

An application of a constraint may fail if the constraint is already “violated” at the that time.

The clue is indeed in may fail. Most constraints can also succeed (with pending constraints) in situations where one can prove that the constraint can never hold. I’m quite sure this used to hold for dif/2 as well, but I couldn’t create a case. So possibly this is no longer true for dif/2.

[ridgeworks]

@jan

Most constraints can also succeed (with pending constraints) in situations where one can prove that the constraint can never hold.

Specifically for dif(X,Y) I see three cases:

1. if X==Y then dif(X,Y) fails.
2. if X\=Y then dif(X,Y) succeeds.
3. if X\==Y, not(not(X=Y)) then dif(X,Y) succeeds with dif constraint between X and Y. (Subsequent unification of X or Y may fail.)

dif is determistic so there are no choicepoints. Therefore, I don’t see how cut affects this at all.

Don’t all CLP systems work this way?

[jan]

It is a bit more complicated. dif/2 uses unifiable/3 to figure out what is needed to make two two terms equal and than creates constraints on these variables to prevent this. We can make it a bit hard though.

?- dif(x(X,X), x(1,Y)).
dif(f(X, Y), f(1, 1)).

?- dif(X, Y), dif(x(X,X), x(1,Y)).
dif(X, Y),
dif(f(X, Y), f(1, 1)).

The first show us that the two terms are different, unless both X and Y become 1. In the second, the dif(X,Y) prevents this, so this is logically false, but dif/2 nevertheless succeeds.

@ridgeworks

dif is determistic so there are no choicepoints. Therefore, I don’t see how cut affects this at all.

There surely are no choicepoints, so the cut does not prune any choicepoints. It does however cause the wrong branch (of an if-then-else) or wrong clause to be taken.

@ridgeworks

Don’t all CLP systems work this way?

AFAIK, yes. This is also why the people advocating wide use of constraints (for example replace normal arithmetic by clp(fd)) argue so strongly against using cuts.

[ridgeworks]

@jan

The first show us that the two terms are different, unless both X and Y become 1. In the second, the dif(X,Y) prevents this, so this is logically false , but dif/2 nevertheless succeeds.

But isn’t this a “meta” interpretation that detects the inconsistency? I think all dif claims to do is to ensure that any bindings of the the variables in ‘X’ and ‘Y’ do not violate the constraint. Constrained variables in the answer are still subject to the (in this case inconsistent) constraints. I suppose its theoretically possible that dif could detect a new dif constraint was mutually inconsistent with any existing dif constraints, but that’s a separate issue.

In any case, I’m not sure what this has to do with the original question. Even if mutually inconsistent constraints could cause immediate failure, the earlier dif (perhaps in another clause entirely) still behaves the same.

@jan

It does however cause the wrong branch (of an if-then-else) or wrong clause to be taken.

This is what I don’t see. The correct branch is taken depending on the success/failure of dif (the “condiition”). Subsequent unification failure due to the constraint doesn’t, and shouldn’t, affect this. Put another way, the else goal is only executed if the constraint can never be true given the current program state (early failure).

@jan

This is also why the people advocating wide use of constraints (for example replace normal arithmetic by clp(fd)) argue so strongly against using cuts.

Really don’t understand this. I’ll do some independent research but any references appreciated.

[jamesnvc]

@swi

The automatic doc-link for *->/2 produces a 500 HTTP return code (Internal Server error) when you click on it, but the summary tooltip is okay.

It looks like the proper link is supposed to have parens around it – e.g. (-*>)/2. Not sure how to handle that in general though.

[jan]

@jamesnvc

Not sure how to handle that in general though

I think it makes more sense to fix the website

[jan]

@ridgeworks

This is what I don’t see. The correct branch is taken depending on the success/failure of dif (the “condiition”).

The first post contains the snippet below. I could be wrong, but I read this as an attempt to choose between two branches depending on whether A and B are different. This code doesn’t branch on whether or not A and B are always different. The else branch is only taken if dif/2 can decide immediately that the two terms can never become the same. There are however terms for which this is true (always different), but which dif/2 cannot detect this. If you want to test what dif is doing I guess this is ok, but I cannot see any useful application in the real world. Then, I might have missed the essence of this topic …

@dtonhofer

(dif(A,B)
    -> 
    proceed_hoping_that_dif_will_turn_true(A,B,W)
    ;
    try_again(A,B))

@ridgeworks

I’ll do some independent research but any references appreciated.

Have a look at the questions and answers about pure Prolog on Stack Overflow.

[ridgeworks]

@jan

There are however terms for which this is true (always different), but which dif/2 cannot detect this.

In fact, this is unknowable in general. Consider a this variation of your example:

?- (dif(X, Y) -> write(then) ; write(else)), dif(x(X,X), x(1,Y)).
then
dif(X, Y),
dif(f(X, Y), f(1, 1)).

Would you ever expect the first dif to fail taking the else branch? Would you expect the if-then-else to behave differently due to the presence of the second dif? If so, by what magic?

If the original query was intended to do what you suggest, how about:

(dif(A,B)
    -> 
    (proceed_hoping_that_dif_will_turn_true(A,B,W)
     ;
     try_again(A,B)
    )
)

@jan

Have a look at the questions and answers about pure Prolog on Stack Overflow.

Thanks, I’ll check it out.