History dependent semi_lex_compare/3

General
29

Ha Ha, I am everybodies monkey. Why do people not test?

Here is result of stress testing compare_with_stack/5:

?- between(1,1000000,_), 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.
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),
C1 = C2, C2 = (<),
F1 = F2, F2 = [],
C3 = (>)

So it has also a transitivity violation. Right?

30 
% ?- between(1,1000000,_), random_cyclic(T1), random_cyclic(T2),
% random_cyclic(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:   [13] compare(incomparable,s(s(...,0),1),1)
%@ ERROR:   [10] '<meta-call>'(compstack:compstack: ...) <foreign>
%@ ERROR:    [9] toplevel_call(compstack:compstack: ...) 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.
31

Yes. So compare_with_stack/3,5 must not be called compare predicate. I agree.

32

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.
% answer:
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.

33

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 = (>),
35

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(=, _, _, _, _).
36

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,_).
% answer
C1 = C2, C2 = (<),
C3 = (>).

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

37

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 = (<).
38

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

39

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]
	).
41

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.

42

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

No violation, is there?

43

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

46

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 = (<).
47

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:   [13] compare(incomparable,s(s(...,...),1),1)
%@ ERROR:   [10] '<meta-call>'('<garbage_collected>') <foreign>
%@ ERROR:    [9] 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.
49

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)]].
52

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.
55

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.
56

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.

57

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.