From Newsgroup: comp.lang.prolog

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

--- Synchronet 3.20a-Linux NewsLink 1.114

From Newsgroup: comp.lang.prolog

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

--- Synchronet 3.20a-Linux NewsLink 1.114

From Newsgroup: comp.lang.prolog

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.
--- Synchronet 3.20a-Linux NewsLink 1.114

From Newsgroup: comp.lang.prolog

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.

--- Synchronet 3.20a-Linux NewsLink 1.114

From Newsgroup: comp.lang.prolog

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.

--- Synchronet 3.20a-Linux NewsLink 1.114

From Newsgroup: comp.lang.prolog

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)
--- Synchronet 3.20a-Linux NewsLink 1.114

From Newsgroup: comp.lang.prolog

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)

--- Synchronet 3.20a-Linux NewsLink 1.114

From Newsgroup: comp.lang.prolog

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)

--- Synchronet 3.20a-Linux NewsLink 1.114

From Newsgroup: comp.lang.prolog

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)

--- Synchronet 3.20a-Linux NewsLink 1.114

From Newsgroup: comp.lang.prolog

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>)
--- Synchronet 3.20a-Linux NewsLink 1.114

From Newsgroup: comp.lang.prolog

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>)

--- Synchronet 3.20a-Linux NewsLink 1.114

From Newsgroup: comp.lang.prolog

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>)

--- Synchronet 3.20a-Linux NewsLink 1.114

From Newsgroup: comp.lang.prolog

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).
--- Synchronet 3.20a-Linux NewsLink 1.114