How are Queries submitted to Pengine in SWISH

Is there something that interfers in parsing a query? Like submitting
an alphabetically sorted variable names list before the query, and
thus establish a different variable order?

I get in SWISH:

?- X @< A.
false

In the ordinary SWI-Prolog top-level:

?- X @< A.
true.

I am struggling with different results in SWISH and SWI-Prolog
for an algorithm that uses (@<)/2.

As you probably know, ordering of two unrelated variables is undefined. The only thing that is guaranteed is that they are not equal and that the ordering is stable as long as you do not unify the variables to anything except for variables that have been created later than the oldest of the pair.

In this case the behavior depends on the order reading the query creates the two variables. As that works different in SWISH compared to the normal toplevel you may end up with this result.

I don’t see much of a problem. Such things are simply undefined and SWISH is not just an online SWI-Prolog shell. It behaves quite different in many ways.

From the ISO core standard:

7.2.1 Variable

If x and Y are variables which are not identical then
x term-precedes Y shall be implementation dependent
except that during the creation of a sorted list (7.1.6.5,
8.10.3.1 j) the ordering shall remain constant.

That is not much. You know there is more. I’d assume most (all?) implementations dereference variables and compare their (final) addresses. Prolog implementations generally also make more recently created variables reference older variables rather than the other way around such that backtracking can simply reset the top of the stack and only bindings in older parts of the stack need to be trailed. Since 8.3.7 references between variables only exist on the global stack (heap). As the heap is contiguous and garbage collection does not reorder terms on the global stack, we have a few more guarantees. One could also imagine other stack models that may break this picture.

Jan W.’ s explanation seems reasonable for me, who is far from familiar with such internal thing in Prolog. In theory, ordering on variables should be that on equivalence classes of variables with respect to current states in the unification history. Conventionally, each class is idenfitified with a reprensentative of the class. Thus, the ordering depends on a way of choosing the representative, and the current way of SWI_Prolog of choosing representatives sounds reasonable. Of course, every one knows this, but for just in case.

I think that works in SWI-Prolog. As I read the ISO docs, the only promise is that sort/2 is sort of atomic to variable ordering and doesn’t get confused by changes to the order during its execution. I fear there is not even a guarantee that @< applies between every consecutive members of the result list as the stability is only demanded during the creation of a sorted list.

From  curiosity, also I tested to see.
% ?- length(X, 4), length(Y, 3), append(X, Y, Z), sort(Z, Z0), Z==Z0.
%@ X = [_10534, _10540, _10546, _10552],
%@ Y = [_10562, _10568, _10574],
%@ Z = Z0, Z0 = [_10534, _10540, _10546, _10552, _10562, _10568, _10574].

% ?- X=[A,B,C], Y=[A, D, C], append(X, Y, Z), sort(Z, Z0),
%	  B = D, sort(Z, Z1),  Z0 == Z1.
%@ false.

Hmmm. Anyway, we should be careful to sort lists with variables to be unified with some other.

Sounds strange. According to app/3, no unification occurs between X and Y. I think both should be true.

I see. Thanks. Tau-prolog, I guess, gives to each newly generated variable cell a field to hold inherited equivalence class id to keep the ordering compatible with ancestors.

I see. Thank you for explanation.

My rough understanding your question is this:

Prolog “=” should have the following property (ISO requirement ?)

P(X), X = X0 ==> p(X0)

(example) X @< Y, X=X0 ==> X0 @< Y

Your question is: So far SWI-Prolog/Jekejeke-Prolog satisfy this “good” property, but is this “universally” true ?

Is this right ?

It is definitely not an ISO requirement. Even in the conjunction below, according the ISO the first may succeed while the second may fail.

X @< Y, X @< Y,

In most concrete Prolog systems the above is probably guaranteed.

Also in concrete Prolog systems I would not trust your example. I would not guarantee it.

Only, if at some point X @< Y and you call some predicate that unifies X and/or Y with variables that are introduced in this predicate, you should be safe (in SWI-Prolog).

Wow! I will try to find such an example myself.

I feel at ease. For my applications, it is enough.

You won’t. It is just that ISO doesn’t guarantee this. We could imagine a Prolog system with a segmented heap where garbage collection may result in variables being moved into different segments causing the ordering to change. Even there it is highly unlikely that a GC happens between these two calls, but if you call something non-trivial between the two comparisons it gets more likely.

Coincident ! Also I suspected that GC can cause such abnormal thing unless it keeps physical order of variables during gc. Also I imagined “idempotent watcher” which monitor to inhibit the program doing the same thing twice.

Anyway now I respect prolog developers much more than ever.

Thank you for valuable information. Once a long time ago I was taught that non-ground goals should be carefully treated when used with extra logical predicates. Since then, I was careful for variables. For example, we know \ + p(X, Y) (negation of uninstantiated goal) tends to cause logical bugs. BTW, I never met a situation where sorting variables is necessary, and, I felt something dangerous in sorting variables.

library(ordsets) works with sufficiently ground terms, such that the uninstantiated variables don’t participate in the comparisons. For example, f(X) @< g(Y) succeeds for all possible values of X and Y.

(This is also true for sort/2: the list elements merely need to be sufficiently ground.)

PS: I don’t understand what you meant by “There is doubt that this is true.” Did you mean “I doubt that this is true”?

1 Like

The ISO text is quite explicit “shall be implementation dependent except that during the creation of a sorted list”. I haven’t been involved, but my guess is that people wanted to allow for GC to reorder variables. I’m not aware if any system actually doing that.

Note that groundness is not really required. Just a term ordering that does not depend on variables. Thus, [a(_), b(_)] is perfectly fine as the standard order can be decided before a variable is reached.

That said, ordered variables can be useful to get rid of duplicates using sort/2 (which is probably why this is an exception). If order is preserved you can use variables as keys in e.g., library(assoc) to store information about variables, e.g., for abstract interpretation. In my experience such cases are more elegantly and efficiently handled using attributed variables. Given attributed variables there are few cases left where stable variable ordering is useful.

SWI-Prolog’s library(ordsets) follows (AFAIK) pretty much established practices. As it is BSD licensed, you can just copy it :slight_smile: . ord_intersection/3 and related predicates are indeed useful to get scalable access to how variables in different subterms are related. For example:

shared_vars(T1, T2, Vars) :-
    term_variables(T1, V1), sort(V1, SV1),
    term_variables(T2, V2), sort(V2, SV2),
    ord_intersection(SV1, SV2, Vars).

As I read it, the ISO standard does not guarantee this to work. None of library(ordsets) seems to be guaranteed for sets holding multiple plain variables.

Well, probably the above works in all current Prolog systems and anyone considering implementing a Prolog system where this is not guaranteed to work should think at least twice.

I vote

  1. gc must keep the ordering on variables.
  2. The ordering on variables X, Y must be preserved as far as both of the equivalence class w.r.t unification of X and Y are kept. Otherwise, it is implementation dependent.

The pack/unpack case may violates condition 2 due to possible fresh variables.

As a prolog user, if the ordering of variables matters, it may not difficult to guarantee condition 2. But as for condition 1 surely it is out of his control to keep the ordering.

SWI-Prolog guarantees that ordering doesn’t change unless a variable is unified with an older variable (or a non-variable, but nobody is surprised about that). As last remark is that setting the first attribute on a variable changes its location in the variable ordering. Adding more attributes or changing an attribute value has no impact on the ordering.

I only claim that the ISO standard only demands sort/2 on a set of variables to remove the duplicates and make all variables appear before all non-variables.

sortq/3 is beautiful !

BTW, although I wrote this,

rethinking from the equivalence classes of unbound variables and
applications of sorting variables like term_variables, now I am inclined to think that gc needs not keep the ordering of variables. As far as variables are concerned, an important role of sort/2 is not to keep the ordering variables but to eliminate multiple occurrences of variables in the list. In other word, as far as sorting lists of variables, we should think such practical functions of sort/2 under “modulo” ordering of variables. Prolog variables are definitely different from variables in polynomials (Groebner base calculus, for example). Prolog variables are open and has no natural good ordering like Groebner base. I am not enough confident of such “modulo choice of representative” semantics is allowed in the logic programming. I may change my mind tomorrow.