(Nothing of importance)
% ?- 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.
Yes. So compare_with_stack/3,5 must not be called compare predicate. I agree.
(Nothing of importance)
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(=, _, _, _, _).
(Nothing of importance)
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 = (<).
(Nothing of importance)
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: [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.
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.