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

**URL:** <https://swi-prolog.discourse.group/t/dif-2-call-as-implication-premiss-is-the-implications-else-part-run-should-it-be/2486>\
**Category:** Help!\
**Tags:** discussion\
**Created:** [June 9, 2020, 5:19pm UTC](https://swi-prolog.discourse.group/t/dif-2-call-as-implication-premiss-is-the-implications-else-part-run-should-it-be/2486 "2020-06-09T17:19:12Z")\
**Posts on this page:** 20\
**Page:** 1

<div class="post-metadata">

**Author:** ![dtonhofer](https://yyz2.discourse-cdn.com/free1/user_avatar/swi-prolog.discourse.group/dtonhofer/32/902_2.png) [@dtonhofer](https://swi-prolog.discourse.group/u/dtonhofer)\
**Post date:** [June 9, 2020, 5:19pm UTC](https://swi-prolog.discourse.group/t/dif-2-call-as-implication-premiss-is-the-implications-else-part-run-should-it-be/2486/1 "2020-06-09T17:19:12Z")

</div>

I have tried to understand the behaviour of dif/2 (which leads to a [state diagram](https://raw.githubusercontent.com/dtonhofer/prolog_notes/master/swipl_notes/about_dif/about_dif_correct.svg?sanitize=true)) 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):

```prolog
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:

```prolog
?- 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?

```prolog
?- 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`?

---

<div class="post-metadata">

**Author:** ![peter.ludemann](https://yyz2.discourse-cdn.com/free1/user_avatar/swi-prolog.discourse.group/peter.ludemann/32/48_2.png) [@peter.ludemann](https://swi-prolog.discourse.group/u/peter.ludemann)\
**Post date:** [June 9, 2020, 5:44pm UTC](https://swi-prolog.discourse.group/t/dif-2-call-as-implication-premiss-is-the-implications-else-part-run-should-it-be/2486/2 "2020-06-09T17:44:56Z")

</div>

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:

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

```

compared to:

```prolog
?- 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](https://www.metalevel.at/prolog/metapredicates)  
(I’m in the process of turning this into a “pack” for SWI-Prolog)

---

<div class="post-metadata">

**Author:** ![dtonhofer](https://yyz2.discourse-cdn.com/free1/user_avatar/swi-prolog.discourse.group/dtonhofer/32/902_2.png) [@dtonhofer](https://swi-prolog.discourse.group/u/dtonhofer)\
**Post date:** [June 9, 2020, 6:18pm UTC](https://swi-prolog.discourse.group/t/dif-2-call-as-implication-premiss-is-the-implications-else-part-run-should-it-be/2486/3 "2020-06-09T18:18:23Z")

</div>

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:

```prolog
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.

```prolog
?- 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:

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

```

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

I will definitely check library(reif).

---

<div class="post-metadata">

**Author:** ![ridgeworks](https://yyz2.discourse-cdn.com/free1/user_avatar/swi-prolog.discourse.group/ridgeworks/32/886_2.png) [@ridgeworks](https://swi-prolog.discourse.group/u/ridgeworks)\
**Post date:** [June 9, 2020, 7:35pm UTC](https://swi-prolog.discourse.group/t/dif-2-call-as-implication-premiss-is-the-implications-else-part-run-should-it-be/2486/4 "2020-06-09T19:35:51Z")

</div>

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?

---

<div class="post-metadata">

**Author:** ![dtonhofer](https://yyz2.discourse-cdn.com/free1/user_avatar/swi-prolog.discourse.group/dtonhofer/32/902_2.png) [@dtonhofer](https://swi-prolog.discourse.group/u/dtonhofer)\
**Post date:** [June 9, 2020, 9:35pm UTC](https://swi-prolog.discourse.group/t/dif-2-call-as-implication-premiss-is-the-implications-else-part-run-should-it-be/2486/5 "2020-06-09T21:35:37Z")

</div>

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…)?

---

<div class="post-metadata">

**Author:** ![ridgeworks](https://yyz2.discourse-cdn.com/free1/user_avatar/swi-prolog.discourse.group/ridgeworks/32/886_2.png) [@ridgeworks](https://swi-prolog.discourse.group/u/ridgeworks)\
**Post date:** [June 9, 2020, 11:57pm UTC](https://swi-prolog.discourse.group/t/dif-2-call-as-implication-premiss-is-the-implications-else-part-run-should-it-be/2486/6 "2020-06-09T23:57:48Z")

</div>

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`.

---

<div class="post-metadata">

**Author:** ![peter.ludemann](https://yyz2.discourse-cdn.com/free1/user_avatar/swi-prolog.discourse.group/peter.ludemann/32/48_2.png) [@peter.ludemann](https://swi-prolog.discourse.group/u/peter.ludemann)\
**Post date:** [June 10, 2020, 12:45am UTC](https://swi-prolog.discourse.group/t/dif-2-call-as-implication-premiss-is-the-implications-else-part-run-should-it-be/2486/7 "2020-06-10T00:45:23Z")

</div>

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

```prolog
%! 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:

```prolog
?- 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_).

```prolog
?- ( 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 

```

---

<div class="post-metadata">

**Author:** ![jan](https://yyz2.discourse-cdn.com/free1/user_avatar/swi-prolog.discourse.group/jan/32/4_2.png) [@jan](https://swi-prolog.discourse.group/u/jan)\
**Post date:** [June 10, 2020, 8:02am UTC](https://swi-prolog.discourse.group/t/dif-2-call-as-implication-premiss-is-the-implications-else-part-run-should-it-be/2486/8 "2020-06-10T08:02:42Z")

</div>

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.

---

<div class="post-metadata">

**Author:** ![dtonhofer](https://yyz2.discourse-cdn.com/free1/user_avatar/swi-prolog.discourse.group/dtonhofer/32/902_2.png) [@dtonhofer](https://swi-prolog.discourse.group/u/dtonhofer)\
**Post date:** [June 10, 2020, 12:01pm UTC](https://swi-prolog.discourse.group/t/dif-2-call-as-implication-premiss-is-the-implications-else-part-run-should-it-be/2486/9 "2020-06-10T12:01:50Z")

</div>

> 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.

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

```

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

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

```

---

<div class="post-metadata">

**Author:** ![swi](https://avatars.discourse-cdn.com/v4/letter/s/51bf81/32.png) [@swi](https://swi-prolog.discourse.group/u/swi)\
**Post date:** [June 10, 2020, 12:14pm UTC](https://swi-prolog.discourse.group/t/dif-2-call-as-implication-premiss-is-the-implications-else-part-run-should-it-be/2486/10 "2020-06-10T12:14:58Z")

</div>

> [@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.

```prolog
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.

---

<div class="post-metadata">

**Author:** ![ridgeworks](https://yyz2.discourse-cdn.com/free1/user_avatar/swi-prolog.discourse.group/ridgeworks/32/886_2.png) [@ridgeworks](https://swi-prolog.discourse.group/u/ridgeworks)\
**Post date:** [June 10, 2020, 1:48pm UTC](https://swi-prolog.discourse.group/t/dif-2-call-as-implication-premiss-is-the-implications-else-part-run-should-it-be/2486/11 "2020-06-10T13:48:29Z")

</div>

> [@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.

---

<div class="post-metadata">

**Author:** ![ridgeworks](https://yyz2.discourse-cdn.com/free1/user_avatar/swi-prolog.discourse.group/ridgeworks/32/886_2.png) [@ridgeworks](https://swi-prolog.discourse.group/u/ridgeworks)\
**Post date:** [June 10, 2020, 2:04pm UTC](https://swi-prolog.discourse.group/t/dif-2-call-as-implication-premiss-is-the-implications-else-part-run-should-it-be/2486/12 "2020-06-10T14:04:09Z")

</div>

> [@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.

---

<div class="post-metadata">

**Author:** ![jan](https://yyz2.discourse-cdn.com/free1/user_avatar/swi-prolog.discourse.group/jan/32/4_2.png) [@jan](https://swi-prolog.discourse.group/u/jan)\
**Post date:** [June 10, 2020, 2:56pm UTC](https://swi-prolog.discourse.group/t/dif-2-call-as-implication-premiss-is-the-implications-else-part-run-should-it-be/2486/13 "2020-06-10T14:56:48Z")

</div>

> [@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.

---

<div class="post-metadata">

**Author:** ![ridgeworks](https://yyz2.discourse-cdn.com/free1/user_avatar/swi-prolog.discourse.group/ridgeworks/32/886_2.png) [@ridgeworks](https://swi-prolog.discourse.group/u/ridgeworks)\
**Post date:** [June 10, 2020, 3:31pm UTC](https://swi-prolog.discourse.group/t/dif-2-call-as-implication-premiss-is-the-implications-else-part-run-should-it-be/2486/14 "2020-06-10T15:31:19Z")

</div>

> [@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?

---

<div class="post-metadata">

**Author:** ![jan](https://yyz2.discourse-cdn.com/free1/user_avatar/swi-prolog.discourse.group/jan/32/4_2.png) [@jan](https://swi-prolog.discourse.group/u/jan)\
**Post date:** [June 10, 2020, 4:09pm UTC](https://swi-prolog.discourse.group/t/dif-2-call-as-implication-premiss-is-the-implications-else-part-run-should-it-be/2486/15 "2020-06-10T16:09:15Z")

</div>

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.

```prolog
?- 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.

---

<div class="post-metadata">

**Author:** ![ridgeworks](https://yyz2.discourse-cdn.com/free1/user_avatar/swi-prolog.discourse.group/ridgeworks/32/886_2.png) [@ridgeworks](https://swi-prolog.discourse.group/u/ridgeworks)\
**Post date:** [June 10, 2020, 6:28pm UTC](https://swi-prolog.discourse.group/t/dif-2-call-as-implication-premiss-is-the-implications-else-part-run-should-it-be/2486/16 "2020-06-10T18:28:50Z")

</div>

> [@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](https://www.swi-prolog.org/pldoc/doc_for?object=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.

---

<div class="post-metadata">

**Author:** ![jamesnvc](https://yyz2.discourse-cdn.com/free1/user_avatar/swi-prolog.discourse.group/jamesnvc/32/14_2.png) [@jamesnvc](https://swi-prolog.discourse.group/u/jamesnvc)\
**Post date:** [June 10, 2020, 6:48pm UTC](https://swi-prolog.discourse.group/t/dif-2-call-as-implication-premiss-is-the-implications-else-part-run-should-it-be/2486/17 "2020-06-10T18:48:12Z")

</div>

> [@swi](#):
>
> The automatic doc-link for [\*-\>/2](https://www.swi-prolog.org/pldoc/doc_for?object=*-%3E/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.

---

<div class="post-metadata">

**Author:** ![jan](https://yyz2.discourse-cdn.com/free1/user_avatar/swi-prolog.discourse.group/jan/32/4_2.png) [@jan](https://swi-prolog.discourse.group/u/jan)\
**Post date:** [June 10, 2020, 6:56pm UTC](https://swi-prolog.discourse.group/t/dif-2-call-as-implication-premiss-is-the-implications-else-part-run-should-it-be/2486/18 "2020-06-10T18:56:08Z")

</div>

> [@jamesnvc](#):
>
> Not sure how to handle that in general though

I think it makes more sense to fix the website 🙂

---

<div class="post-metadata">

**Author:** ![jan](https://yyz2.discourse-cdn.com/free1/user_avatar/swi-prolog.discourse.group/jan/32/4_2.png) [@jan](https://swi-prolog.discourse.group/u/jan)\
**Post date:** [June 10, 2020, 7:08pm UTC](https://swi-prolog.discourse.group/t/dif-2-call-as-implication-premiss-is-the-implications-else-part-run-should-it-be/2486/19 "2020-06-10T19:08:17Z")

</div>

> [@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](#):
>
> ```prolog
> (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.

---

<div class="post-metadata">

**Author:** ![ridgeworks](https://yyz2.discourse-cdn.com/free1/user_avatar/swi-prolog.discourse.group/ridgeworks/32/886_2.png) [@ridgeworks](https://swi-prolog.discourse.group/u/ridgeworks)\
**Post date:** [June 10, 2020, 9:41pm UTC](https://swi-prolog.discourse.group/t/dif-2-call-as-implication-premiss-is-the-implications-else-part-run-should-it-be/2486/20 "2020-06-10T21:41:35Z")

</div>

> [@jan](#):
>
> There are however terms for which this is true (always different), but which [dif/2](https://www.swi-prolog.org/pldoc/doc_for?object=dif/2) cannot detect this.

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

```prolog
?- (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:

```prolog
(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.

[Next page](https://swi-prolog.discourse.group/t/dif-2-call-as-implication-premiss-is-the-implications-else-part-run-should-it-be/2486.md?page=2)