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

Help!
#3

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

#4

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?

2 Likes
#5

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

#6

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.

#7

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
1 Like
#8

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.

2 Likes
Bug hunting toolbox
#9

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

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.

#11

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.

1 Like
#12

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.

#13

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.

#14

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?

#15

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.

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.

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.

1 Like
#16

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.

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

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

#17

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.

#18

I think it makes more sense to fix the website :slight_smile:

3 Likes
#19

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 …

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

1 Like
#20

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

Thanks, I’ll check it out.

#21

No. That is precisely my point, you never know whether a constraint succeeds with pending constraints that can either never be satisfied or that can already be resolved to a single solution. The only way to know is to label the result.

1 Like
#22

This construct implements the so-called‘soft-cut’. T

That’s the wrong manual page, namely this one:

https://eu.swi-prolog.org/pldoc/doc_for?object=(*->)/2

instead of this

https://eu.swi-prolog.org/pldoc/doc_for?object=(->)/2

But I get it now! Simply

?- (writeln("It begins"); (writeln("Backtracked to before ->"),fail)),
|    (dif(X,Y) -> writeln("YES") ; writeln("NO")), 
|    X=1,
|    (writeln("Past X=1"); (writeln("Backtracked to before Y=1"),fail)),
|    (Y=1 ; (writeln("Y=1 failed"),fail)),  % because the constraint fails
|    writeln("END").

It begins
YES
Past X=1
Y=1 failed
Backtracked to before Y=1
Backtracked to before ->
false.

That’s actually pretty simple.