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.

There are more discrepancies, making it difficult to write tutorials that show something for SWI-Prolog and SWISH. For example I get in SWISH:

?- X \== A, X = 1, A = 2.
A = 2,
X = 1

Whereby I get in ordinary SWI-Prolog top-level:

?- X \== A, X = 1, A = 2.
X = 1,
A = 2.

Maybe this can be fixed with a little intervention into the messages that are exchanged between the browser client and the SWISH server.

Edit 16.11.2020:
It seems ordinary SWI-Prolog toplevel uses input order:

?- X \== A, X = 1, A = 2.
X = 1,
A = 2.

?- A \== X, X = 1, A = 2.
A = 2,
X = 1.

Whereby SWISH seems to sort:

?- X \== A, X = 1, A = 2.
A = 2,
X = 1

?- A \== X, X = 1, A = 2.
A = 2,
X = 1

Maybe the normal SWI-Prolog top-level should also start sorting? Or SWISH keeps the sorting for answer substitution but not for query execution?

I don’t think this is in the ISO core standard. Have to check whether this creates one more issue with pack/unpack. Do you apply the notion “created” to plain head variables as well?

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 am now checking whether ord_union/3 behaves as if bootstrapped from sort/2:

ord_union(X, Y, Z) :-
    append(X, Y, H),
    sort(H, Z).

Assuming append/3 doesn’t change the ordering as well. But I am lacking with my testing a little bit, busy with other stuff.

I need only a few invariants, and of course a coherent SWISH and SWI-Prolog top-level would be also a nice to have.

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.

This is result for append/3. I used this code:

app([], L, L).
app([H|T], L, [H|R]) :- app(T, L, R).

In SWI-Prolog (I mean SWI-Prolog top-level and not SWISH):

?- X @< Y.
true.

?- X @< Y, app([Y],[X],_), X @< Y.
true.

?- X @< Y, app([X],[Y],_), X @< Y.
true.

In TauProlog I get, it has a pack/unpack problem:

?- X @< Y.
true.

?- X @< Y, app([Y],[X],_), X @< Y.
true.

?- X @< Y, app([X],[Y],_), X @< Y.
false.

For TauProlog was expecting the second query to fail and not the third.

My system behaves well for app/3, like SWI-Prolog.

Edit 17.11.2020:
Probably can also create a pack/unpack problem for SWI-Prolog or my system.
For example coding append/3 differently with (=)/2. Not sure.

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

You can try yourself here:

http://tau-prolog.org/sandbox/
Screenshot is here: GitHub Issue #229

If a clause gets instantiated during execution new variables are created.
Its enough to have X instantiated to a new variable _1 and if it
also happens that Y @< _1.

One can avoid this when local variables like _1, _2, etc… are instantiated
and not argument variables. This doesn’t work always, but in most cases
and is easy to solve by a carefully crafted sorting-free head unify.

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.

Do you mean fresh variable gets fresh id? But this is not
the problem. Its rather that variable variable unification X = Y
where X \== Y can have two outcomes:

      X ---> Y: X is bound to Y

      Y ---> X: Y is bound to X

In append, the second clause, does this unfication when
the first argument is called with [X]:

      [H|T] = [X]

Which leads to a unfication:

      H = X

This unpacking can have two different outcomes,
thats implementation dependent.

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.

Not, I am not assuming that the ISO core standard mandates a certain
behaviour. But I am also not sure whether ISO core standard has
even identified this implementation dependency.

Somehow I guess they were aware, because of the sort/2 remark
that Jan W. found. But because the behaviour of X = Y is implementation
dependent, it can have these two outcomes:

The behaviour respectively whether the below is an invariant is
also implementation dependent (your statement rephrase):

    if     ?- Q(X), P(X)     then  ?- Q(X), X = Y, P(Y)

The phrase “implementation dependent” means it can be either way.
It means the above can be “true” sometimes or the above can be “false”
sometimes. The phrase “implementation dependent” means a feature

is not mandated, and likely not uniformly solved along implementations
aka different Prolog systems from different vendors.

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.