Does SWI-Prolog's `foreach/2` involve `freeze/2`?

Question

On SWI Prolog's foreach/2, we read:

The compatibility of the "aggregate" library which contains the foreach/2 predicate is stated to be

Quintus, SICStus 4. The forall/2 is a SWI-Prolog built-in and term_variables/3 is a SWI-Prolog built-in with different semantics.

From the SICStus Prolog documentation:

foreach(:Generator, :Goal)

for each proof of Generator in turn, we make a copy of Goal with the appropriate substitution, then we execute these copies in sequence. For example, foreach(between(1,3,I), p(I)) is equivalent to p(1), p(2), p(3).

Note that this is not the same as forall/2. For example, forall(between(1,3,I), p(I)) is equivalent to

\+ \+ p(1), \+ \+ p(2), \+ \+ p(3).

The trick in foreach/2 is to ensure that the variables of Goal which do not occur in Generator are restored properly. (If there are no such variables, you might as well use forall/2.)

Like forall/2, this predicate does a failure-driven loop over the Generator. Unlike forall/2, the Goals are executed as an ordinary conjunction, and may succeed in more than one way.

Taking the example on the SWI Prolog page, without the final unification:

?- foreach(between(1,4,X), dif(X,Y)).
dif(Y, 4),
dif(Y, 3),
dif(Y, 2),
dif(Y, 1),
dif(Y, 1),
dif(Y, 2),
dif(Y, 1),
dif(Y, 1),
dif(Y, 3),
dif(Y, 2),
dif(Y, 1),
dif(Y, 1),
dif(Y, 2),
dif(Y, 1),
dif(Y, 1).

I'm not sure why there is the output of all the dif/2 instantiations and why there are repetitions of the same subgoal.

foreach/2 should be decide that the conjunction of multiple dif(Y,i) is true, as unbound variable Y is evidently dif from an integer i.

But now:

?- foreach(between(1,4,X), dif(X,Y)), Y = 5.
Y = 5.

Ok, so no output except for Y=5 because the goal succeeds. But what does the Y=5 change? After foreach/2, Prolog has already been able to decide to that foreach/2 is true (given the state of Y at the time foreach/2 was run), so adding Y=5 should not change anything.

But then:

?- foreach(between(1,4,X), dif(X,Y)), Y = 2.
false.

A later unification changes the outcome of foreach/2. How?

I thought that freeze/2 on Y might be involved to make the situation interesting, as in, we are really computing:

freeze(Y,foreach(between(1,4,X), dif(X,Y))).

This would more or less explain the printouts. For example:

?- freeze(Y,foreach(between(1,4,X), dif(X,Y))).
freeze(Y, foreach(between(1, 4, X), dif(X, Y))).

?- freeze(Y,foreach(between(1,4,X), dif(X,Y))), Y=5.
Y = 5.

?- freeze(Y,foreach(between(1,4,X), dif(X,Y))), Y=2.
false.

Is this what's going on?

Answer 1

The "freezing" behaviour that you observe is due to dif/2, not foreach/2.

The predicate dif/2 ensures that its two arguments are not identical and will not become identical. So if the two arguments might become identical, then dif/2 is suspended until it can decide whether they are identical or not.