# History dependent semi_lex_compare/3

Don’t use my random_cyclic/1 in place of @ridgeworks random_cyclic/1.
He modified it to return only ground. He posted about that. But the transitivity

violation in your code exists. It seems to be reproducible in the top-level of
SWI-Prolog. Maybe should double check with another Prolog system?

``````/* SWI-Prolog 9.1.7 */
?- T1 = s(s(T1, 0), T1), T2 = s(T2, 1), T3 = _S3, % where
_S1 = s(_S1, _S2),
_S2 = s(_S2, 0),
_S3 = s(_S1, _S3),
compare_with_stack(C1,T1,T2,[],F1), compare_with_stack(C2,T2,T3,F1,F2),
compare_with_stack(C3,T1,T3,F2,_), C1==C2, C1\==C3.
C1 = C2, C2 = (<),
C3 = (>).
``````

So `compare_with_stack/5` cannot be used for sort/2.

Edit 03.04.2023
But they are very few. They are much rarer than those for native compare/3 or
for `compare_stack/3`. When using 10’000’000 iterations I get:

``````?- aggregate_all(count, (between(1,10000000,_), random_cyclic(T1), ground(T1),
random_cyclic(T2), ground(T2), random_cyclic(T3), ground(T3),
compare_with_stack(C1,T1,T2,[],F1), compare_with_stack(C2,T2,T3,F1,F2),
compare_with_stack(C3,T1,T3,F2,_), C1==C2, C1\==C3), F).
F = 1.
``````

Hope its not a bug in SWI-Prolog itself. But if it were a bug, since I can reproduce an example
on the top-level, it would be a bug not related to the failure driven loop.

A different result: It shows only T1< T2, T2>T3, T1>T3,
Does this violate transitivity ?

``````% ?- T1 = s(s(T1, 0), T1), T2 = s(T2, 1), T3 = _S3,
%     _S1 = s(_S1, _S2),
%     _S2 = s(_S2, 0),
%     _S3 = s(_S1, _S3),
%     compare_with_stack(C1,T1,T2,[],F1), compare_with_stack(C2,T2,T3,F1,F2),
%     compare_with_stack(C3,T1,T3,F2,_).

%@ C1 = (<),
%@ C2 = C3, C3 = (>),
``````

Here is.

``````compare_with_stack(C, X, Y, H, H):- X == Y, !, C = (=).
compare_with_stack(C, X, Y, H, H0):- compare_with_stack(C0, X, Y),
(	C0 = (incomparable) -> force_order(C, X, Y, H, H0)
;	C = C0,
H0 = H
).
%
force_order(C, X, Y, H, H0):- functor(X, F, N),
(	select(F/N-G, H, H1) -> true
;	G = [],
H1 = H
),
force_order_in_arity_grouping(C, X, Y, G, G1),
H0 = [F/N-G1|H1].
%
force_order_in_arity_grouping(C, X, Y, G, G0):-
(	memberchk(X, G)->
(	memberchk(Y, G) ->
(	precede(X, Y, G) -> C = (<)
;	C = (>)
),
G0 = G
; 	C  = (>),
G0 = [Y|G]
)
;	memberchk(Y, G)->
C = (<),
G0 = [X|G]
;  	C = (<),
G0 = [X, Y|G]
).

%
precede(X, _, [X|_]):-!.
precede(X, Y, [U|L]):- Y\==U, precede(X, Y, L).

%
compare_with_stack(C, X, Y):- compare_with_stack(C, X, Y, []).
%
compare_with_stack(C, X, Y, P):-
( 	X = Y -> C = (=)
;	(atomic(X); atomic(Y)) -> compare(C, X, Y)
;	memberchk(X-Y, P) -> C = (incomparable)
;	functor(X, F, N),
functor(Y, G, M),
compare(D, N, M),
(	D = (=) ->
compare(E, F, G),
(	E = (=) ->
compare_args_with_stack(C, 1, X, Y, [X-Y|P])
;	C = E
)
;	C = D
)
).
%
compare_args_with_stack(C, K, A, B, P):- arg(K, A, X), arg(K, B, Y), !,
compare_with_stack(D, X, Y, P),
(	D = (=) ->
K0 is K+1,
compare_args_with_stack(C, K0, A, B, P)
;	C = D
).
compare_args_with_stack(=, _, _, _, _).
``````

Using my fuzzer I found a ground term transitivity violation:

``````?- T1 = s(_S1, 1), % where
_S1 = s(_S1, s(s(_S1, 1), s(1, 0))),
T2 = s(T2, 1),
T3 = _S3, % where
_S2 = s(_S2, 1),
_S3 = s(_S2, _S3),
compare_with_stack(C1,T1,T2,[],F1), compare_with_stack(C2,T2,T3,F1,F2),
compare_with_stack(C3,T1,T3,F2,_).
C1 = C2, C2 = (<),
C3 = (>).
``````

So your new predicate cannot be used for sort/2.

Thanks you for Monkey test, which should have been done by me as you say.

Yes, that is sureyly a bug, hopefully, a careless bug.
I changed meaning of order in the compare history, older is smaller, then the bug case fixed.
But not sure for other cases.

``````% ?- T1 = s(_S1, 1),
%     _S1 = s(_S1, s(s(_S1, 1), s(1, 0))),
% T2 = s(T2, 1),
% T3 = _S3,
%     _S2 = s(_S2, 1),
%     _S3 = s(_S2, _S3),
% compare_with_stack(C1,T1,T2,[],F1), compare_with_stack(C2,T2,T3,F1,F2),
% compare_with_stack(C3,T1,T3,F2,_).
%@ T1 = s(_S1, 1), % where
%@     _S1 = s(_S1, s(s(_S1, 1), s(1, 0))),
%@ _S1 = s(_S1, s(s(_S1, 1), s(1, 0))),
%@ T2 = _S2, _S2 = s(_S2, 1),
%@ T3 = _S3, _S3 = s(_S2, _S3),
%@ C1 = (>),
%@ F1 = F2, F2 = [s/2-[s(_S1, 1), _S4]], % where
%@     _S4 = s(_S4, 1),
%@ C2 = C3, C3 = (<).
``````

Since you didn’t post the new code, I cannot do your monkey testing.

I really appreciate if you would kindly do the Monkey test for me.

Below is the only predicate that I changed due to the bug found by Monkey test (Monkey is great !). I thought one could not make error on such a simple one, but I made error. This time I change so that for example, [a, b, c, d] means chronological ordering d<c<b<a.

``````force_order_in_arity_grouping(C, X, Y, G, G0):-
(	memberchk(X, G)->
(	memberchk(Y, G) ->
(	precede(X, Y, G) -> C = (>)
;	C = (<)
),
G0 = G
; 	C  = (<),
G0 = [Y|G]
)
;	memberchk(Y, G)->
C = (>),
G0 = [X|G]
;  	C = (>),
G0 = [X, Y|G]
).
``````

I have reproduced the similar result, which is still strange to me. I have to ask the Monkey seriously, and review also “incomparability” concept for cyclic terms, which is most fundamental for compare_with_stack. So far, I have no doubt for that.

If I will notice something related, I will post.

Thank you.

Rewrite as:
`T3<T1, T1<T2, T3<T2` or `T2>T1, T1>T3, T2>T3`

No violation, is there?

No, for this case. However, I am trying to find some bugs. which surely exist.
I am enjoying to find them.

The same history F1 should be shared with both queries, which prevents from violation.

``````% ?- T1=s(T1,0), T2=s(T2,1), compare_with_stack(C1,T1,T2,[],F1),
%  T1=s(T1,0), T2=s(T2,1), compare_with_stack(C2, T2,T1,F1,_).
%@ T1 = s(T1, 0),
%@ T2 = s(T2, 1),
%@ C1 = (>),
%@ F1 = [s/2-[s(T1, 0), s(T2, 1)]],
%@ C2 = (<).
``````

I met a strange error message below, which was issued by clpfd order.
My compare_with_stack never passes ‘incomparable’ to the standard compare/3.
To conentrate on compare_with_stack, is it possible to separate clpfd off. clpfd seems called
from Monkey.

``````% ?- between(1,1000000,_), random_cyclic(T1), ground(T1), random_cyclic(T2), ground(T2),
% random_cyclic(T3), ground(T3), compare_with_stack(Ct,T1,T2),
% compare_with_stack(Ct,T2,T3), compare_with_stack(C,T1,T3),C\=Ct.
%@ ERROR: Domain error: `order' expected, found `incomparable'
%@ ERROR: In:
%@ ERROR:    compare(incomparable,s(s(...,...),1),1)
%@ ERROR:    '<meta-call>'('<garbage_collected>') <foreign>
%@ ERROR:     toplevel_call('<garbage_collected>') at /Users/cantor/lib/swipl/boot/toplevel.pl:1173
%@ ERROR:
%@ ERROR: Note: some frames are missing due to last-call optimization.
%@ ERROR: Re-run your program in debug mode (:- debug.) to get more detail.

% ?- listing(order).
%@ clpfd:order(up).
%@ clpfd:order(down).
%@ clpfd:order(random_value(Seed)) :-
%@     must_be(integer, Seed),
%@     set_random(seed(Seed)).
%@
%@ true.
``````

I am struggling with the puzzle. However, so far I have found no bug in the `compare_with_stack/5`.
So I put back the order in the history as before, that is, a list as history [a,b,c,d] of
cyclic terms appearing as incomparable terms, represents the current linear (forced) order a<b<c<d.

As for your “violation” example, it seems normal as I expected:
History is growing

``````[] ->  [T1, T2] -> [T3, T1, T2]
``````

Note that the order grows T1< T2 ===> T3 < T1<T2

I found nothing wrong of the code. However, Monkey generates non zero violation counts cases.

This is the current state of debugging.

``````% ?- T1 = s(T1, T1),
% T2 = s(_S1, 1),
%     _S1 = s(_S1, 0),
% T3 = s(T3, 0),
%	compare_with_stack(C12, T1,T2, [], H0),
%	compare_with_stack(C23, T2,T3, H0, H1),
%	compare_with_stack(C13, T1,T3, H1, H2),
%	compare_with_stack(D12, T1,T2, H2, H3),
%	compare_with_stack(D23, T2,T3, H3, H4),
%	compare_with_stack(D13, T1,T3, H4, H5).

%@ T1 = s(T1, T1),
%@ T2 = s(_S1, 1), % where
%@     _S1 = s(_S1, 0),
%@ _S1 = T3, T3 = s(T3, 0),
%@ C12 = D12, D12 = (<),
%@ H0 = H1, H1 = [s/2-[s(T1, T1), s(_S1, 1)]],
%@ C23 = C13, C13 = D23, D23 = D13, D13 = (>),
%@ H2 = H3, H3 = H4, H4 = H5, H5 = [s/2-[s(T3, 0), s(T1, T1), s(_S1, 1)]].
``````

Sorry, but they are just reverse order to each other.

Take, for example, a list [a,b,c] as a<b, a<c, b<c. It is obviously transitive.

As you informed us that @< is no more total ordering on rational trees
by introducing the Carllson’s pair x=f(y,0), y=f(x, 1).
My idea is to keep a list of such cyclic terms by “chronologicall order” only which has been
decided to be incomparable with some other cyclic terms. The cyclic term x is not
put in the list as far as x is compared only with finite terms.

I don’t think by any means it is smart to bring such compare-history, buit it is only one of ways of keeping @< as a locally total linear ordering.

EDIT. 2023/04/05

I used a wrong predicate for Monkey tes. Sorry for that. This time it is done with corret one.

`compare_with_stack/3,5` has passed Monkey test on transitivity, which I take as symptone that
it now works as I intended. The standard `@<` got violation count 158．

``````semi_lex_compare(C, X, Y):- b_getval(compare_history, H),
compare_with_stack(C, X, Y, H, H0),
b_setval(compare_history, H0).

% ?- b_setval(compare_history, []), aggregate_all(count,
% (between(1,10000000,_), random_cyclic(A), ground(A), random_cyclic(B), ground(B),
% random_cyclic(C), ground(C), semi_lex_compare(>, A,B), semi_lex_compare(>, B,C),
% semi_lex_compare(<, A,C)), F).
%@ F = 0.

% ?- b_setval(compare_history, []), aggregate_all(count,
% (between(1,100000000,_), random_cyclic(A), ground(A), random_cyclic(B), ground(B),
% random_cyclic(C), ground(C), A @<B, B @<C, \+ A @< C), F).
%@ F = 158.
``````

I am sad to report that increasing stress for Monkey test, it returns violation on semi_lex_compare on transitivity. Although I am still fairy sure on the semi_lex_compare transitivity , I have to re-re-rereview that simple codes. Please let me take time to enjoy the puzzle.

``````non_transitive_pattern(<, <, >).
non_transitive_pattern(>, >, <).

% ?- b_setval(compare_history, []), aggregate_all(count,
%	( between(1,100000000,_),
%	random_cyclic(T1), ground(T1),
%	random_cyclic(T2), ground(T2),
%	random_cyclic(T3), ground(T3),
%	semi_lex_compare(C,T1,T2),
%	semi_lex_compare(D,T2,T3),
%	semi_lex_compare(E,T1,T3),
%	non_transitive_pattern(C, D, E)), F).
%@ F = 113.
``````

The discussion here has languished, but I thought it was too important to just let it fade away so I raised an issue (for posterity) - see system:compare/3 violates transitive ordering for rational trees (cyclic terms) · Issue #1159 · SWI-Prolog/swipl-devel · GitHub.

Feel free to add your own comments to this issue if you think I’ve misrepresented anything or left out something important.

Although I know nothing `compare/3` of other Prolog’s, let me summarize what I have thought and done about comparing cyclic terms, most of which have been posted somewhere related threads.

First, I reviewed fixed-point based construction on the following things from scratch.

• H: Herebrand Universe (the standard ground terms.)

• @< : The sandard lexcical order on H, which is linear and total on H.

• R: Rational Terms

• @@<<: lexical order, which is transitive and total on R.

However `@@<<` is NOT ANTI-SYMMETRIC. `x\=y`, `x @@<< y`, and `y@@<< x` are possible together. A counter example is the Matts Carllsons pair `x=s(y,0)`, `y=s(x,1)`.

These results are easy by really simple fixpint argument of monotone increasing
operations on sets theoretical encoding for H and R. These encoding are easy but tedious to write down so that I preferred to write some prolog codes, which is for escaping from such boring jobs.

In fact, in spite of these theoretical but easy consideration, I wrote a several `compare/3` friends on the rational trees with stack, heap or arity-path-trees, though two of them I did not post.

And the Monkey test correctly destroyed all my trials showing counter examples. I should thank J. Burse for his great Monky test, which now takes me to think that the experiment shows that my theoretical consideration is sadly correct.

However, I think another `@@<<` like `compare/3` might be possible which is free from the anti-symmetricity with some sophistcated monotone operations usable for prolog cyclic terms, though I have no idea about it at all for now.

This summary might explain why SWI-Prolog document carefully(?) does not mention to compareing rational trees, because theoretically it is impossible in the sense of the fixpoint I used.

No objection to opening a second ticket for `term_factorized`; I also wasn’t sure whether the problem was due to `rbtree`’s use of the broken `compare/3` or whether it was some other issue with cyclic terms.

And even if `term_factorize` was fixed, is there any reason (other than performance tradeoffs) for preferring it rather than your “custom” `factorize/3` for comparing cyclic terms?

`factorize/3` is already yesterday’s snow, check out `naish/2`.
But anything should work that doesn’t give a stack overflow.

No use confusing things with variations; let’s focus on `naish/2` as the prototypical predicate going forward.