This never gets old, especially since even seasoned Prologers
might not be aware of it. But it made it even into Prolog system
documentation, like here:

"Please note : the standard order is only well-defined for finite (acyclic) terms.
There are infinite (cyclic) terms for which no order relation holds."
https://sicstus.sics.se/sicstus/docs/3.12.11/html/sicstus/Term-Compare.html

And here is a funny disagreement between two Prolog systems,
an old lady (SWI-Prolog) and a youngster (Scryer Prolog):

/* SWI-Prolog 9.1.7 */
?- X=f(X,a(X)), Y=f(Y,b(Y)), Z=f(Y,c(Y)),
compare(A,X,Y), compare(B,Y,Z), compare(C,X,Z).
A = B, B = (<),
C = (>).

/* Scryer Prolog 0.9.1-194 */
?- X=f(X,a(X)), Y=f(Y,b(Y)), Z=f(Y,c(Y)),
compare(A,X,Y), compare(B,Y,Z), compare(C,X,Z).
A = (<), B = (<), C = (<).

Mats Carlsson schrieb am Dienstag, 16. Juli 1996 um 09:00:00 UTC+2:
> In the '80s, Alain Comerauer, Joxan Jaffar and others published
> algorithms for unification without occurs check that could work
> with infinite (cyclic) terms with termination guaranteed.
> Until yesterday, I always believed that the standard total order for
> finite Prolog terms readily extended to include infinite terms as
> well. However, the following example shows two terms that can't be
> ordered.
> Consider the terms A and B defined by the equations
> [1] A = s(B,0).
> [2] B = s(A,1).
> Clearly, A and B are not identical, so is A @< B or A @> B?
> Assume A @< B. But then s(A,1) @< s(B,0) i.e. B @< A. Contradiction.
> Assume A @> B. But then s(A,1) @> s(B,0) i.e. B @> A. Contradiction.
> So the standard order of Prolog terms cannot include (some) infinite
> terms. On reflection, the same is true for the integers---infinity
> minus infinity is not defined.
> Perhaps this is all obvious, but I was a bit jarred at first.
> Mats Carlsson, PhD
> Computing Science Department tel: +46 18 187691
> Uppsala University fax: +46 18 511925
> P.O. Box 311 Email: m...@csd.uu.se
> S-751 05 Uppsala, Sweden

Hurray, I found a new counter example, derived from
my X,Y,Z tripple. This is a counter example for unstable
keysort, using @ridgeworks new_compare/2.

Lets define unstable_keysort/2 as follows:

unstable_keysort(L, R) :- predsort(new_compare, L, R).

I can now use unstable_keysort/2 and as expected and
useful for setof/3 implementation, it gives me ascending
order of the values for equal keys:

?- unstable_keysort([x-3,x-1,x-2,x-1], L).
L = [x-1, x-2, x-3].

?- predsort(new_compare, [3,1,2,1], L).
L = [1, 2, 3].

Now using the new counter example. The key X is such
that it mimics a pair, confusing acyclic_rep/2 inside
new_compare/2. It breaks the ascending order property:

?- X=(X-b(X)), unstable_keysort([X-b(X), X-a(X)], L).
X = X-b(X),
L = [X-b(X), X-a(X)].

?- X=(X-b(X)), predsort(new_compare, [b(X), a(X)], L).
X = X-b(X),
L = [a(X), b(X)].

Mostowski Collapse schrieb am Mittwoch, 22. März 2023 um 16:51:31 UTC+1:
> This never gets old, especially since even seasoned Prologers
> might not be aware of it. But it made it even into Prolog system
> documentation, like here:
>
> "Please note : the standard order is only well-defined for finite (acyclic) terms.
> There are infinite (cyclic) terms for which no order relation holds."
> https://sicstus.sics.se/sicstus/docs/3.12.11/html/sicstus/Term-Compare.html
>
> And here is a funny disagreement between two Prolog systems,
> an old lady (SWI-Prolog) and a youngster (Scryer Prolog):
>
> /* SWI-Prolog 9.1.7 */
> ?- X=f(X,a(X)), Y=f(Y,b(Y)), Z=f(Y,c(Y)),
> compare(A,X,Y), compare(B,Y,Z), compare(C,X,Z).
> A = B, B = (<),
> C = (>).
>
> /* Scryer Prolog 0.9.1-194 */
> ?- X=f(X,a(X)), Y=f(Y,b(Y)), Z=f(Y,c(Y)),
> compare(A,X,Y), compare(B,Y,Z), compare(C,X,Z).
> A = (<), B = (<), C = (<).
>
> Mats Carlsson schrieb am Dienstag, 16. Juli 1996 um 09:00:00 UTC+2:
> > In the '80s, Alain Comerauer, Joxan Jaffar and others published
> > algorithms for unification without occurs check that could work
> > with infinite (cyclic) terms with termination guaranteed.
> > Until yesterday, I always believed that the standard total order for
> > finite Prolog terms readily extended to include infinite terms as
> > well. However, the following example shows two terms that can't be
> > ordered.
> > Consider the terms A and B defined by the equations
> > [1] A = s(B,0).
> > [2] B = s(A,1).
> > Clearly, A and B are not identical, so is A @< B or A @> B?
> > Assume A @< B. But then s(A,1) @< s(B,0) i.e. B @< A. Contradiction.
> > Assume A @> B. But then s(A,1) @> s(B,0) i.e. B @> A. Contradiction.
> > So the standard order of Prolog terms cannot include (some) infinite
> > terms. On reflection, the same is true for the integers---infinity
> > minus infinity is not defined.
> > Perhaps this is all obvious, but I was a bit jarred at first.
> > Mats Carlsson, PhD
> > Computing Science Department tel: +46 18 187691
> > Uppsala University fax: +46 18 511925
> > P.O. Box 311 Email: m...@csd.uu.se
> > S-751 05 Uppsala, Sweden

Here is a formal proof of Matt Carlsons counter example.
Wiithout loss of generality its enough to handle the case
Lab, although Matt Carlson mentioned both proofs:

/* Lexical Ordering */
∀x∀y∀z∀t(Ls(x,y)s(z,t) ↔ (Lxz ∨ (x=z ∧ Lyt))),

/* Example A,B satisfies A @< B and ~(B @< A) */
Lab, ¬Lba,

/* Example A,B is A=s(B,c) and B=s(A,d), proof works for any c,d */
a=s(b,c), b=s(a,d)

/* We can derive a Contradiction */
entails p∧¬p.
https://www.umsu.de/trees/#~6x~6y~6z~6t(Ls(x,y)s(z,t)~4Lxz~2(x=z~1Lyt)),Lab,~3Lba,a=s(b,c),b=s(a,d)

The consistency means unless hell freezes over,
we can never find a less than relationship L.

Corr.:

The inconsistency means unless hell freezes over,
we can never find a less than relationship L.

Mostowski Collapse schrieb am Freitag, 31. März 2023 um 00:32:28 UTC+2:
> Here is a formal proof of Matt Carlsons counter example.
> Wiithout loss of generality its enough to handle the case
> Lab, although Matt Carlson mentioned both proofs:
>
> /* Lexical Ordering */
> ∀x∀y∀z∀t(Ls(x,y)s(z,t) ↔ (Lxz ∨ (x=z ∧ Lyt))),
>
> /* Example A,B satisfies A @< B and ~(B @< A) */
> Lab, ¬Lba,
>
> /* Example A,B is A=s(B,c) and B=s(A,d), proof works for any c,d */
> a=s(b,c), b=s(a,d)
>
> /* We can derive a Contradiction */
> entails p∧¬p.
> https://www.umsu.de/trees/#~6x~6y~6z~6t(Ls(x,y)s(z,t)~4Lxz~2(x=z~1Lyt)),Lab,~3Lba,a=s(b,c),b=s(a,d)
>
> The consistency means unless hell freezes over,
> we can never find a less than relationship L.

Link of the proof:
https://www.umsu.de/trees/#~6x~6y~6z~6t(Ls(x,y)s(z,t)~4Lxz~2(x=z~1Lyt)),Lab,~3Lba,a=s(b,c),b=s(a,d)|=p~1~3p

Got somehow cropped, hope this one works now?

Mostowski Collapse schrieb am Freitag, 31. März 2023 um 00:33:27 UTC+2:
> Corr.:
>
> The inconsistency means unless hell freezes over,
> we can never find a less than relationship L.
> Mostowski Collapse schrieb am Freitag, 31. März 2023 um 00:32:28 UTC+2:
> > Here is a formal proof of Matt Carlsons counter example.
> > Wiithout loss of generality its enough to handle the case
> > Lab, although Matt Carlson mentioned both proofs:
> >
> > /* Lexical Ordering */
> > ∀x∀y∀z∀t(Ls(x,y)s(z,t) ↔ (Lxz ∨ (x=z ∧ Lyt))),
> >
> > /* Example A,B satisfies A @< B and ~(B @< A) */
> > Lab, ¬Lba,
> >
> > /* Example A,B is A=s(B,c) and B=s(A,d), proof works for any c,d */
> > a=s(b,c), b=s(a,d)
> >
> > /* We can derive a Contradiction */
> > entails p∧¬p.
> > https://www.umsu.de/trees/#~6x~6y~6z~6t(Ls(x,y)s(z,t)~4Lxz~2(x=z~1Lyt)),Lab,~3Lba,a=s(b,c),b=s(a,d)
> >
> > The consistency means unless hell freezes over,
> > we can never find a less than relationship L.

Here is a relatively cheap compare for cyclic terms that satisfies the
laws, except lexical order. It is based on the idea to define:

S @<' T :<=> rep(S) @< rep(T)
The only requirement to the function rep is that it is injective,
then the laws, except for lexical order, are automatically satisfied.
The proof is not so difficult. Here is an example proof, showing

irreflexivity of @<’ based on irreflexivity of @<:

/* I am using r for the function rep,
R for the relation @<' and L for the relation @< */
/* Injectivity */
∀x∀y(r(x)=r(y) → x=y),

/* Bootstrapping */
∀x∀y(Rxy ↔ Lr(x)r(y)),

/* Irreflexivity */
∀x¬Lxx

/* Irreflexivity */
entails ∀x¬Rxx.

https://www.umsu.de/trees/#~6x~6y(r(x)=r(y)~5x=y),~6x~6y(Rxy~4Lr(x)r(y)),~6x(~3Lxx)%7C=~6x(~3Rxx)

Here is a suggestion:

rep(X, Y-Z) :-
term_factorized(X, Y, Z),
numberassoc(Z, 0).

numberassoc([], _).
numberassoc(['$VAR'(N)=_|L], N) :-
M is N+1,
numberassoc(L, M).

And then the comparator:

rep_compare(C, X, Y) :-
rep(X, A), rep(Y, B),
compare(C, A, B).

Any bugs? It requires that term_factorized/3 is stable and it works
only for terms that don’t have already ‘$VAR’/1 in it. Might need to
use something else, but with ‘$VAR’/1 rep/2 can be easily inspected.

Mostowski Collapse schrieb am Freitag, 31. März 2023 um 23:08:55 UTC+2:
> Here is a relatively cheap compare for cyclic terms that satisfies the
> laws, except lexical order. It is based on the idea to define:
>
> S @<' T :<=> rep(S) @< rep(T)
> The only requirement to the function rep is that it is injective,
> then the laws, except for lexical order, are automatically satisfied.
> The proof is not so difficult. Here is an example proof, showing
>
> irreflexivity of @<’ based on irreflexivity of @<:
>
> /* I am using r for the function rep,
> R for the relation @<' and L for the relation @< */
> /* Injectivity */
> ∀x∀y(r(x)=r(y) → x=y),
>
> /* Bootstrapping */
> ∀x∀y(Rxy ↔ Lr(x)r(y)),
>
> /* Irreflexivity */
> ∀x¬Lxx
>
> /* Irreflexivity */
> entails ∀x¬Rxx.
>
> https://www.umsu.de/trees/#~6x~6y(r(x)=r(y)~5x=y),~6x~6y(Rxy~4Lr(x)r(y)),~6x(~3Lxx)%7C=~6x(~3Rxx)

Here is a sort example, the Matt Carlsson pairs can be easily sorted:

?- A=(B,0), B=(A,1), predsort(rep_compare, [A,B], X),
term_factorized(X, P, Q).
P = [_A, _B],
Q = [_B=(_A, 0), _A=(_B, 1)].

?- A=(B,0), B=((B,0),1), predsort(rep_compare, [B,A], X),
term_factorized(X, P, Q).
P = [_A, _B],
Q = [_B=(_A, 0), _A=(_B, 1)].

And the tripple X,Y,Z that has a bug in native compare/3, the bug is gone:

?- X=f(X,a(X)), Y=f(Y,b(Y)), Z=f(Y,c(Y)),
rep_compare(A,X,Y), rep_compare(B,Y,Z), rep_compare(C,X,Z).
A = B, B = C, C = (<)

Mostowski Collapse schrieb am Freitag, 31. März 2023 um 23:08:55 UTC+2:
> Here is a relatively cheap compare for cyclic terms that satisfies the
> laws, except lexical order. It is based on the idea to define:
>
> S @<' T :<=> rep(S) @< rep(T)
> The only requirement to the function rep is that it is injective,
> then the laws, except for lexical order, are automatically satisfied.
> The proof is not so difficult. Here is an example proof, showing
>
> irreflexivity of @<’ based on irreflexivity of @<:
>
> /* I am using r for the function rep,
> R for the relation @<' and L for the relation @< */
> /* Injectivity */
> ∀x∀y(r(x)=r(y) → x=y),
>
> /* Bootstrapping */
> ∀x∀y(Rxy ↔ Lr(x)r(y)),
>
> /* Irreflexivity */
> ∀x¬Lxx
>
> /* Irreflexivity */
> entails ∀x¬Rxx.
>
> https://www.umsu.de/trees/#~6x~6y(r(x)=r(y)~5x=y),~6x~6y(Rxy~4Lr(x)r(y)),~6x(~3Lxx)%7C=~6x(~3Rxx)

Ok, half of the proofs don't need injectivity. But connectedness
shows me a proof using injectivity in Wolfgang Schwartz tree tool:

/* I am using r for the function rep,
R for the relation @<' and L for the relation @< */
/* Injectivity */
∀x∀y(r(x)=r(y) → x=y),

/* Bootstrapping */
∀x∀y(Rxy ↔ Lr(x)r(y)),

/* Connectedness */
∀x∀y(¬x=y → (Lyx ∨ Lxy))

/* Connectedness */
entails ∀x∀y(¬x=y → Ryx ∨ Rxy)

https://www.umsu.de/trees/#~6x~6y(r(x)=r(y)~5x=y),~6x~6y(Rxy~4Lr(x)r(y)),~6x~6y(~3x=y~5Lyx~2Lxy)%7C=~6x~6y(~3x=y~5Ryx~2Rxy)

Mostowski Collapse schrieb am Freitag, 31. März 2023 um 23:10:58 UTC+2:
> Here is a sort example, the Matt Carlsson pairs can be easily sorted:
>
> ?- A=(B,0), B=(A,1), predsort(rep_compare, [A,B], X),
> term_factorized(X, P, Q).
> P = [_A, _B],
> Q = [_B=(_A, 0), _A=(_B, 1)].
>
> ?- A=(B,0), B=((B,0),1), predsort(rep_compare, [B,A], X),
> term_factorized(X, P, Q).
> P = [_A, _B],
> Q = [_B=(_A, 0), _A=(_B, 1)].
>
> And the tripple X,Y,Z that has a bug in native compare/3, the bug is gone:
>
> ?- X=f(X,a(X)), Y=f(Y,b(Y)), Z=f(Y,c(Y)),
> rep_compare(A,X,Y), rep_compare(B,Y,Z), rep_compare(C,X,Z).
> A = B, B = C, C = (<)
> Mostowski Collapse schrieb am Freitag, 31. März 2023 um 23:08:55 UTC+2:
> > Here is a relatively cheap compare for cyclic terms that satisfies the
> > laws, except lexical order. It is based on the idea to define:
> >
> > S @<' T :<=> rep(S) @< rep(T)
> > The only requirement to the function rep is that it is injective,
> > then the laws, except for lexical order, are automatically satisfied.
> > The proof is not so difficult. Here is an example proof, showing
> >
> > irreflexivity of @<’ based on irreflexivity of @<:
> >
> > /* I am using r for the function rep,
> > R for the relation @<' and L for the relation @< */
> > /* Injectivity */
> > ∀x∀y(r(x)=r(y) → x=y),
> >
> > /* Bootstrapping */
> > ∀x∀y(Rxy ↔ Lr(x)r(y)),
> >
> > /* Irreflexivity */
> > ∀x¬Lxx
> >
> > /* Irreflexivity */
> > entails ∀x¬Rxx.
> >
> > https://www.umsu.de/trees/#~6x~6y(r(x)=r(y)~5x=y),~6x~6y(Rxy~4Lr(x)r(y)),~6x(~3Lxx)%7C=~6x(~3Rxx)

Instead of using the verification path, and making
mathematical proofs, one can also use the validation path.
What helps is this fuzzer:

% random_cyclic(-Term)
random_cyclic(T) :-
random_cyclic([T], T).

% random_cyclic(+List, -Term)
random_cyclic(L, T) :-
length(L, M),
random(R),
N is truncate(R*(M+3)),
(N = 0 -> T = 0;
N = 1 -> T = 1;
N = 2 -> T = s(P,Q), random_cyclic([P|L], P), random_cyclic([Q|L], Q);
K is N-3, nth0(K, L, S), S=T).

Now I found that term_factorized/3 might run into
a stack overflow. The reason could be the buggy
compare/3, in case it is used in rbtrees:

?- aggregate_all(count, (between(1,1000000,_), random_cyclic(A),
random_cyclic(B), random_cyclic(C), rep_less(A,B),
rep_less(B,C), \+ rep_less(A,C)), F).
ERROR: Stack limit (1.0Gb) exceeded
ERROR: Stack sizes: local: 0.7Gb, global: 0.2Gb, trail: 1Kb
ERROR: Stack depth: 12,882,088, last-call: 50%, Choice points: 6
ERROR: In:
ERROR: [12,882,088] rbtrees:lookup(<compound s/2>,
_64416492, <compound black/4>)
ERROR: [12,882,086] terms:insert_vars(<compound s/2>,
_64416526, <compound t/2>)

There is a new surprise. I get the same stack
overflow when I use a ground term:

/* SWI-Prolog 9.1.7 */
?- T = _S1, % where
_S1 = s(s(_S1, _S2), 0),
_S2 = s(_S2, _S1), term_factorized(T, Y, L).
ERROR: Stack limit (1.0Gb) exceeded

The stack overflow glitch is not only present in non-ground
terms, it sadly happens for ground terms as well.

Mostowski Collapse schrieb am Samstag, 1. April 2023 um 20:23:06 UTC+2:
> Instead of using the verification path, and making
> mathematical proofs, one can also use the validation path.
> What helps is this fuzzer:
>
> % random_cyclic(-Term)
> random_cyclic(T) :-
> random_cyclic([T], T).
>
> % random_cyclic(+List, -Term)
> random_cyclic(L, T) :-
> length(L, M),
> random(R),
> N is truncate(R*(M+3)),
> (N = 0 -> T = 0;
> N = 1 -> T = 1;
> N = 2 -> T = s(P,Q), random_cyclic([P|L], P), random_cyclic([Q|L], Q);
> K is N-3, nth0(K, L, S), S=T).
>
> Now I found that term_factorized/3 might run into
> a stack overflow. The reason could be the buggy
> compare/3, in case it is used in rbtrees:
>
> ?- aggregate_all(count, (between(1,1000000,_), random_cyclic(A),
> random_cyclic(B), random_cyclic(C), rep_less(A,B),
> rep_less(B,C), \+ rep_less(A,C)), F).
> ERROR: Stack limit (1.0Gb) exceeded
> ERROR: Stack sizes: local: 0.7Gb, global: 0.2Gb, trail: 1Kb
> ERROR: Stack depth: 12,882,088, last-call: 50%, Choice points: 6
> ERROR: In:
> ERROR: [12,882,088] rbtrees:lookup(<compound s/2>,
> _64416492, <compound black/4>)
> ERROR: [12,882,086] terms:insert_vars(<compound s/2>,
> _64416526, <compound t/2>)

I was too optimistic about the native compare/3. It has also the
mirror anomaly. I find very quickly a violation of the mirror law:

/* SWI-Prolog 9.1.7 */
?- repeat, random_cyclic(A), random_cyclic(B),
compare(X,A,B), X = (<), \+ (compare(Y,B,A), Y = (>)).
A = s(A, A),
B = s(_S1, 1), % where
_S1 = s(_S1, s(1, _S1)),
X = (<) .

Mostowski Collapse schrieb am Montag, 3. April 2023 um 14:09:16 UTC+2:
> There is a new surprise. I get the same stack
> overflow when I use a ground term:
>
> /* SWI-Prolog 9.1.7 */
> ?- T = _S1, % where
> _S1 = s(s(_S1, _S2), 0),
> _S2 = s(_S2, _S1), term_factorized(T, Y, L).
> ERROR: Stack limit (1.0Gb) exceeded
> The stack overflow glitch is not only present in non-ground
> terms, it sadly happens for ground terms as well.
> Mostowski Collapse schrieb am Samstag, 1. April 2023 um 20:23:06 UTC+2:
> > Instead of using the verification path, and making
> > mathematical proofs, one can also use the validation path.
> > What helps is this fuzzer:
> >
> > % random_cyclic(-Term)
> > random_cyclic(T) :-
> > random_cyclic([T], T).
> >
> > % random_cyclic(+List, -Term)
> > random_cyclic(L, T) :-
> > length(L, M),
> > random(R),
> > N is truncate(R*(M+3)),
> > (N = 0 -> T = 0;
> > N = 1 -> T = 1;
> > N = 2 -> T = s(P,Q), random_cyclic([P|L], P), random_cyclic([Q|L], Q);
> > K is N-3, nth0(K, L, S), S=T).
> >
> > Now I found that term_factorized/3 might run into
> > a stack overflow. The reason could be the buggy
> > compare/3, in case it is used in rbtrees:
> >
> > ?- aggregate_all(count, (between(1,1000000,_), random_cyclic(A),
> > random_cyclic(B), random_cyclic(C), rep_less(A,B),
> > rep_less(B,C), \+ rep_less(A,C)), F).
> > ERROR: Stack limit (1.0Gb) exceeded
> > ERROR: Stack sizes: local: 0.7Gb, global: 0.2Gb, trail: 1Kb
> > ERROR: Stack depth: 12,882,088, last-call: 50%, Choice points: 6
> > ERROR: In:
> > ERROR: [12,882,088] rbtrees:lookup(<compound s/2>,
> > _64416492, <compound black/4>)
> > ERROR: [12,882,086] terms:insert_vars(<compound s/2>,
> > _64416526, <compound t/2>)

Can we produce Naish pointers without relying on
term_factorized/3 which unfortunately gives a stack
overflow sometimes? Of course:

% naish(+Term, -Termt)
naish(T, S) :-
naish(T, [], S).

% naish(+Term, +Map, -Term)
naish(T, _, T) :- \+ compound(T), !.
naish(T, C, '\a'(N)) :- nth0(N, C, S), S == T, !.
naish(T, C, S) :-
T =.. [F|L],
naish_list(L, [T|C], R),
S =.. [F|R].

% naish_list(+List, +Map, -List)
naish_list([], _, []).
naish_list([X|L], C, [Y|R]) :-
naish(X, C, Y),
naish_list(L, C, R).

Works fine:

?- A=(B,0), B=(A,1), naish(A, X).
X = (('\a'(1), 1), 0).