rebis-dev: Top level: unusual ordering of new variable names

[UWN]

?- [user].
est(Z,Z):-Z=[_,_].
est([A,B],[A,B]).
est(Z,Y):-Z=[_|X],X=[_], Z=Y.
est(Z,Z):-Z=[_|X],X=[_].
est(Z,Z):-X=[_],Z=[_|X].

?- est(A,B).
   A = [_B,_A], B = [_B,_A]    % unexpected
;  A = [_A,_B], B = [_A,_B]
;  A = [_A,_B], B = [_A,_B]
;  A = [_A,_B], B = [_A,_B].
;  A = [_B,_A], B = [_B,_A].    % unexpected

Regardless of the way how a term has been created, new variable names in an answer (-substitution) should always be used in the very same left-to-right order.

[UWN]

In master they are all the same

[UWN]

Please note that this is serious.

[triska]

I think it is worth appreciating why this issue, which may appear unimportant at first, is in fact important:

If I understand correctly, the reason is that with a reliable order of variables in answer substitutions, we can easily obtain any order we want on the toplevel.

For instance, suppose I get solutions that show the binding for N before the one for F:

?- n_factorial(N, F).
   N = 0, F = 1
;  N = 1, F = 1
;  N = 2, F = 2
;  N = 3, F = 6
;  N = 4, F = 24
;  ...

Then I can easily enforce a variable order in answer substitutions that first emits the binding for F, and then that for N, by simply adding a semantically irrelevant goal of the form _=[F,N] in front of the query:

?- _=[F,N], n_factorial(N, F).
   F = 1, N = 0
;  F = 1, N = 1
;  F = 2, N = 2
;  F = 6, N = 3
;  F = 24, N = 4
;  F = 120, N = 5
;  F = 720, N = 6
;  ...

In this way, we can reliably show the most interesting variable bindings first.

[UWN]

@triska , yes this is one aspect, but more importantly is the actual comparison of different answers containing variables and quite often attached to it, constraints. By having one precise numbering, alternate answers can be much easier compared.

Also, I wonder how this different ordering happens anyway, in any case term_variables/2 does not seem to be used for it as this is definitely independent of variable age.

[triska]

@mthom: Could list_to_set/2 from library(lists) be useful for this? This would allow retaining more of the toplevel logic in Prolog.

[UWN]

term_variables/2.