Thanks. I have missed these unstableness in my test, but I noticed similar cases with my experimental lazy_compare. My lazy_compare keeps history of pairs of cyclic terms during sorting.
In fact, I noticed at least one problematic part of codes with regard to the book keeping.
Just to confirm your example:
?- X=(X-b(X)), predsort(comparable,[X-b(X), X-a(X)], L).
X = X-b(X),
L = [X-b(X), X-a(X)].
?- X=(X-b(X)), predsort(comparable,[b(X), a(X)], L).
X = X-b(X),
L = [a(X), b(X)].
Or is it an issue with the top level output. X = X-b(x) so L in the first query is equivalent to [X, X-a(X)]; is the ascending order property broken?
Is this an equivalent query:
?- X=(X-b(X)), predsort(comparable,[X, X-a(X)], L).
X = X-b(X),
L = [X-b(X), X-a(X)].
And if X isn’t one of the list members:
?- X=(X-b(X)), predsort(comparable,[X-c(X), X-a(X)], L).
X = X-b(X),
L = [X-a(X), X-c(X)].
?- X=(X+b(X)), predsort(comparable,[X-b(X), X-a(X)], L).
X = X+b(X),
L = [X-a(X), X-b(X)].
Yes, since you’ve exposed a problem using SWIP’s term compare, my version of sorted/1 uses comparable/3:
?- X=(X-b(X)), predsort(comparable,[X-b(X), X-a(X)], L), sorted(L).
X = X-b(X),
L = [X-b(X), X-a(X)].
?- X=(X-b(X)), predsort(comparable,[X-a(X), X-b(X)], L), sorted(L).
X = X-b(X),
L = [X-b(X), X-a(X)].
Using X=X-b(X) as a key and an element in a list to be key-sorted is a bit beyond my abstract thinking capability. (Why would you choose ‘-’ as the functor for this term?) But I guess it is unexpected; to what extent is it a problem?
At least to me the two cyclic terms X = [a,b|X] and Y = [b,a|Y] look identical. It is an arbitrary choice where you choose to start writing them down. I am trying to say that cyclic terms are comparable syntactically (maybe, in the source code) but definitely not structurally (or as they are represented in the machine), unless we want to use accidental properties like how it was written or where in memory it resides.
None of what I wrote is rigorous enough to be taken seriously.
This is all what I think I know about extending order @< onto rational trees. Also I attach codes compare_roughly/3 and queries on predsort for around Matt Carlson’s example.
(compare_roughly should be named useless_compare. )
First, definition of the extension of @< written < for simplicity. Let R be the set of rational trees,
and H is the set of Herbrand terms (H\subset R). (H, <) is the standard totally ordered set. Note that (H, <) is defined inductively.
Let F be an operation on relations on R.
F(P) = \{(U, V) \mid \mbox{ $U$ lexically goes before $V$ wrt $P$}\},
where U=f(a_1,\ldots, a_n) lexically goes before V=g(b_1, \ldots, b_m) wrt P
when one of the conditions holds.
- n<m
- n=m, f lexicallly goes before g
-
n=m, f=g, for some k\leq n,
a_i = b_i ( i < k) and (a_k, b_k) \in P.
As F is clealy monotone there is the largest fixpoint Q of F.
Q=F(Q). Clearly Q is an extension of @< on H. However,
Carlson’s example is a counter example against that Q is order (reflexive, transitive, anti-symmetric).
Q seems complex, at least for me, more than it looks simple as for the definition. It seems to
interesting to investigate Q, but also far beyond me
Before dropping out of this thread, I have written codes compare_roughly/3, which uses ==/2, cyclic_term/1, compare/3 for limited case, and somewhat ad hoc limit of depths.
% ?- A=f(A, 0), B=f(B, 1), compare_roughly(R, A, B).
%@ A = f(A, 0),
%@ B = f(B, 1),
%@ R = (<).
% ?- A=f(A, 0), B=f(B, 1), C=f(C, 2), predsort(compare_roughly, [A, B, C], R).
%@ A = f(A, 0),
%@ B = f(B, 1),
%@ C = f(C, 2),
%@ R = [f(A, 0), f(B, 1), f(C, 2)].
% ?- A=f(A, 0), B=f(B, 1), C=f(C, 2), predsort(compare_roughly, [A, B, A, B, C, A], R).
%@ A = f(A, 0),
%@ B = f(B, 1),
%@ C = f(C, 2),
%@ R = [f(A, 0), f(B, 1), f(C, 2)].
compare_roughly(C, X, Y):- compare_roughly(10, C, X, Y). % default depth = 10.
%
compare_roughly(_, =, X, Y):- X == Y, !.
compare_roughly(N, C, _, _):- N<0, !, C = (=).
compare_roughly(N, C, X, Y):- compare_cyclic_terms_with_depth_limit(N, C, X, Y), !.
compare_roughly(_, C, X, Y):- compare(C, X, Y).
%
compare_cyclic_terms_with_depth_limit(N, C, X, Y):- cyclic_term(X),
cyclic_term(Y),
functor(X, F, I),
functor(Y, G, J),
compare(D, I, J),
( D = (=) ->
compare(E, F, G),
( E = (=) ->
X=..[_|As],
Y=..[_|Bs],
N0 is N-1,
compare_list(N0, C, As, Bs)
; C = E
)
; C = D
).
%
compare_list(_, =, [], []).
compare_list(N, C, [A|As], [B|Bs]):- A == B, !, compare_list(N, C, As, Bs).
compare_list(N, C, [A|As], [B|Bs]):- compare_roughly(N, D, A, B),
( D = (=) ->
compare_list(N, C, As, Bs)
; C = D
).
Dict was out of my thought. I am not sure on dict syntax.
As is, dicts are just compound terms with a non-atom functor. All you need to do is to give this functor a place among the atoms. Actually, ordering blobs (the super type of atoms) is defined.
I have checked that compare_roughly works also for @j4n_bur53 dict sampl, though I understand only half of your comments. Anyway, as I used basically what SWI-Prolog provides with my minior limited use of them for not going looping, it is quite natural it works so.
% ?- A = _{bar:B,baz:0}, B = _{bar:A,baz:1}, compare_roughly(X, A, B).
%@ A = _{bar:_A{bar:A, baz:1}, baz:0},
%@ B = _A{bar:A, baz:1},
%@ X = (<).
Unfortunately, despite of useful information flowing in this thread, still I am unclear about spcification of limited but useufl lexical ordering on rational trees. Maybe I am lazy for digesting new things.
Not sure why you think they look identical. Rational trees (cyclic terms) are still trees and they have roots. In this case the roots are different [a|_] for X and [b|_] for Y.
From another perspective: would you say X=[a,b|TX] and Y=[b,a|TY] look identical? Does subsequent unification (X=TX and Y=TY) change that?
That’s an invalid construct, due to the cyclic term X, so… why is it discussed?
I get the feeling I’m missing something obvious 
Google search for “rational tree” returns 61,800,000 hits. It is used to represent
directed graph with cycles, stream, perpetual process, …
Yes, so the only thing that is different is where your handle is, at some given moment. But it doesn’t have a root since it is a cycle.
In the same vein, I understand perfectly well that under some interpretation, X = [a|X] and Y = [a,a|Y] are different terms. But length/2 refuses to tell me how “big” or “deep” they are and for any predicate that needs to iterate through the list they are defacto identical. Try member/2, for example.
And I have no idea what sort/2 is doing 
check this out:
?- X = [a|X], Y = [a,a|Y], sort([X,Y], Sorted).
X = Y, Y = [a, a|Y],
Sorted = [_S1], % where
_S1 = [a|_S1].
?- X = [a,a|X], Y = [a|Y], sort([X,Y], Sorted).
X = Y, Y = [a|Y],
Sorted = [_S1], % where
_S1 = [a, a|_S1].
?- X = [a|X], Y = [a,a|Y], sort([Y,X], Sorted).
X = Y, Y = [a, a|Y],
Sorted = [[a, a|Y]].
?- X = [a,a|X], Y = [a|Y], sort([Y,X], Sorted).
X = Y, Y = [a|Y],
Sorted = [[a|Y]].
EDIT
Ok I think I see now, the difference between the first two and the last two queries is again something about how the top-level reports it, most probably.
no in fact I have no idea what this means.
EDIT2
Hmm… so contrary to my expectations sort/2 seems to attempt to do something like unification? Because:
?- X = [a|X], Y = [a,a|Y], X = Y.
X = Y, Y = [a, a|Y].
?- X = [a,a|X], Y = [a|Y], X = Y.
X = Y, Y = [a|Y].
In other words, I take back everything I said, those two cyclic terms are clearly unifiable so they are indeed the same term. Not sure which one but since they are the same it doesn’t matter. Case closed, sorry for the noise.
Last EDIT I promise they also compare equal, not sure what decides how the answer is printed, with one or two "a"s.
?- X = [a|X], Y = [a,a|Y], compare(Order, X, Y).
X = Y, Y = [a, a|Y],
Order = (=).
?- X = [a,a|X], Y = [a|Y], compare(Order, X, Y).
X = Y, Y = [a|Y],
Order = (=).
Not invalid in most Prolog’s but varying degrees of support. A quote from a paper referenced earlier in this thread by @j4n_bur53:
From as early as (Colmerauer 1982; Jaffar and Stuckey 1986), Prolog implementers have chosen to omit the occurs check in unification. This has resulted in generating cyclic terms known as rational terms or rational trees in Prolog. While the introduction of cyclic terms in Prolog was unintentional, soon after applications for cyclic terms emerged in fields such as definite clause grammars (Colmerauer 1982; Giannesini and Cohen 1984), constraint programming (Meister and Frühwirth 2006; Bagnara et al. 2001) and coinduction (Gupta et al. 2007).
Perhaps a bit unfortunate that your original post concerning comparing non-ground terms got expanded to include comparing rational trees. But it does seem to have exposed a flaw in the current (standard order) compare/3.
IIRC printing them was the subject of two papers @j4n_bur53 referenced previously in this thread. I think there’s a minimal form but SWIP doesn’t enforce it for top level output.
I’ve written code which heavily depends on cyclic terms but I never try to compare, print or walk them, let alone assert or table them. Custom hooks (portray, attr_portray_hook and project_attributes) are used to minimize (not eliminate) their exposure to the “outside world”.
I have changed codes of compare_roughly/3. The new codes compare_with_stack/3,
which can be used instead of compare/3 for predsort for a list of ground possiby cyclic terms.
It is still experimental, but for now I am seeing high possiblity that it could give one of final solutions to what disscussed in this thread.
I appreciate for any comment. The codes is short and hopefully clear.
compare_with_stack/3 is actually 4 value version of compare, <, =, >, and unstable.
% ?- compare_with_stack(C, a, a).
%@ C = (=).
% ?- A=f(A), compare_with_stack(C, A, A).
%@ A = f(A),
%@ C = (=).
% ?- A=f(A), B=f(B), compare_with_stack(C, A, B).
%@ A = B, B = f(B),
%@ C = (=).
% ?- A=f(A,0), B=f(B,1), compare_with_stack(C, A, B).
%@ A = f(A, 0),
%@ B = f(B, 1),
%@ C = (<).
% ?- A=f(B,0), B=f(A,1), compare_with_stack(C, A, B).
%@ A = f(f(A, 1), 0),
%@ B = f(A, 1),
%@ C = (>).
% ?- A=f(B,0), B=f(A,1), compare_with_stack(C, B, A).
%@ A = f(f(A, 1), 0),
%@ B = f(A, 1),
%@ C = (<).
% ?- A=f(A, 0), B=f(B, 1), C=f(C, 2), predsort(compare_with_stack, [A, B, C], R).
%@ A = f(A, 0),
%@ B = f(B, 1),
%@ C = f(C, 2),
%@ R = [f(A, 0), f(B, 1), f(C, 2)].
% ?- A=f(A, 0), B=f(B, 1), C=f(C, 2), predsort(compare_with_stack, [A, B, A, B, C, A], R).
%@ A = f(A, 0),
%@ B = f(B, 1),
%@ C = f(C, 2),
%@ R = [f(A, 0), f(B, 1), f(C, 2)].
% ?- A = _{bar:B,baz:0}, B = _{bar:A,baz:1}, compare_with_stack(X, A, B).
%@ A = _S1, % where
%@ _S1 = _S1{bar:_S2, baz:0},
%@ _S2 = _S2{bar:_S1, baz:1},
%@ B = _S2{bar:_S1, baz:1},
%@ X = (>).
% ?- H = H-9-7-6-5-4-3-2-1-0, Z = H-9-7-6-5-4-3-2-1,
% Y = Y-7-5-8-2-4-1, compare_with_stack(<, Z, Y).
%@ H = H-9-7-6-5-4-3-2-1-0,
%@ Z = H-9-7-6-5-4-3-2-1,
%@ Y = Y-7-5-8-2-4-1.
% ?- X = X-0-9-7-6-5-4-3-2-1, Y = Y-7-5-8-2-4-1, compare_with_stack(<, X, Y).
%@ X = X-0-9-7-6-5-4-3-2-1,
%@ Y = Y-7-5-8-2-4-1.
% ?- H = H-9-7-6-5-4-3-2-1-0, Z = H-9-7-6-5-4-3-2-1,
% Y = Y-7-5-8-2-4-1, compare_with_stack(<, Z, Y).
%@ H = H-9-7-6-5-4-3-2-1-0,
%@ Z = H-9-7-6-5-4-3-2-1,
%@ Y = Y-7-5-8-2-4-1.
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=(=)
; functor(X, F, N),
functor(Y, G, M),
compare(D, N, M),
( D == (=) ->
compare(E, F, G),
( E == (=) ->
X=..[_|Xs],
Y=..[_|Ys],
compare_with_stack_list(C, Xs, Ys, [X-Y|P])
; C = E
)
; C = D
)
).
%
compare_with_stack_list(C, [], [], _):-!, C = (=).
compare_with_stack_list(C, [X|Xs], [Y|Ys], P):-
compare_with_stack(D, X, Y, P),
( D = (=) -> compare_with_stack_list(C, Xs, Ys, P)
; C = D
).
The toplevel finds variable that have the same value (==), and as X = [a|X] and Y = [a,a|Y] are the same terms, it will print X = Y and print more or less randomly ether X or Y. The toplevel printing for a single term factorizes the term if it is cyclic, but on the internal structure rather than by finding equivalent subterms. In other words, it prints the physical cycle in memory rather than the logical one.
I think I am far from saying something difficult more than written
in Lloyd book on foundation of logic programming.
BTW, my lesson on the operator F teachs me that although F is simple and expected useful
to define some lexical order on rational trees, the largest fixpoint F contains
Matts Carllson’s pair, which is not good I think. Maybe F is too simple.
I am revising F so that largest fixpoint is semi-lexcical total order on rational trees, of course without
the Matt Carllson’s pairs. I am afraid that a revised F would look similar to my codes compare_with_stack (sigh)
I am looking forward to see someone would propose relevant smart operators, or, anything else
to manage lexcai order on cyclic terms.
Of course, its impossible. So far, no one seems against.
However, fortunately for rational terms it is decidable whether they are comparable in the sense of lexical order or not. I think, with a little change, comapare_with_stack could be such a decision predicate.
Giving order between two incomparable terms in a conservative way, it could be used
to sort lists (sort only locally coherent ). comapare_with_stack together with semi_lex_sort are for such direction, which was pushed by accepting Matt Carllson’s pairs positively.
Change compare_with_stack/3 to return ‘incomparable’ when
given terms are incomparable.
I know. This is why I let = include incomparable case.