(Nothing of importance)
I see 
I think they would agree on two terms that have no sharing, no? And a little more aggressive, compare agrees with mercio if it decides before using any tricks that make it terminate on cyclic terms (and more efficient on terms with internal sharing).
If that were true, the big question is what impact that would have on realistic Prolog programs? I suspect not much, but, it is not very hard to craft a counter example where the result is pretty bad.
(Nothing of importance)
Forgot about that. I fear that makes it rather impractical. A fast C implementation could be useful for some applications, but I fear there is no sensible way to make this the default without paying a high price. I understand that the C implementation must also do breath-first, which makes it quite a bit more complicated.
My instantaneous proposal is to introduce 4-values compare, say @compare4values.
For example
@compare4value(C, X, Y):- compare_with_stack(C, X, Y).
compare_with_stack/3 is just the standard compare/3 except watching same pairs appearing in the current branch of the compared terms in the history stack.
One of merits of such @compare_with_stack, it is flexible when applying to predsort/3, because incomparable could be interpreted as any of =, <, > safely, I believe. One could identify incomparable pairs as indistinguishable objects, if one wants. Currently compare_with_stack/3 relies on ==/2, which, I think, should be replaced something same_term like primitives. I wrote a prototype toward the efficient compare_with_stack, but it needs preparations for applying to predsort, which smashes invoved terms into a minimum system of flat equations x=f(x1,x2,…,xn). ( I like the prototype itself as it was interesting as prolog programming.)
BTW, I remember that you posted two years(?) ago something compare_rep/3,
which I thought it is clever, efficient and final solution on comaparing rational trees. But I heard recently in this forum there exists a monkey that found a counter example against compare_rep/3’. I was surprised at the monkey. However I have now a small question whether the efficient compare_rep/3 could be extended to 4-valued compare like compare_with_stack.
I do not remember. In any case, sort/2 and pretty much all algorithms based on ordering require ordering to be stable and transitive. I guess there would be nice in compare/3 being able to decide it is comparing two values for which it is unsafe and, if so, throw an exception if we could do so with minimal impact on performance.
That stops a lot of things one can do with cyclic terms. We cannot even do efficient sets of them using hash tables as term_hash/2 only handles ground terms and variant_sha1/2 raises an exception on cyclic terms (and would otherwise lead to different hashes for equivalent cyclic terms). So, the only set that works is a list
Transitivity of compare will be kept after incomparable is introduced.
Define the standard compare/3 like this.
compare(C, X, Y):- @compare4vaue(D, X, Y), !,
( D = incomaparable ->
compare address of structure X and Y
( like compareing variables) ,
then depending the result unify with result =, <, >
; ....
).
Also @< must be changed for rational trees comparison just like compare/3.
X==Y means that X and Y are expanded to the same rational trees, right ?
If X==Y then X and Y belongs to the same incomparable group. I think there is technique like
dereferencing to give the same physical address for isomorphic ones.
(Nothing of importance)
Aso I did already in collect_subterms (posted earlier) very similar to your canonical to
prepare minimum set of DAFs. So I could say I am familiar with what you are doing, though I am afraid missing something important. However I am completely missing relations between the standard order on the finite terms (@< ?) and the one derived from your canonical predicate. You seem interested in only giving total order on the set of proper rational trees (ignoring finite terms). As for me perhaps as others, I am trying to extend the standard order on rational trees at minimum cost . The notion of incomparable is the minimum extra cost I am paying. If you find the link between DFA and the standard compare, certainly it is great !
(Nothing of importance)
(Nothing of importance)
(Nothing of importance)
EDIT The original post below is completely error from my mis-reading the Mercio’s post. He explicitly his algorithm is based on bread-first search. Thanks @Burse for pointing this. So totality of the order on rational trees is almost obvious, and I think also it works as semi-algorithm on even irrational trees of finite branching. As Mercio’s idea is so simple, I wrote a small codes below to compare rational trees and use it for sorting rational trees. Although it surely have bugs, it works as expected as for small tests. If the codes might look too much simple, perhaps it comes from its using minimum coalgebra for given set of terms. Sorry for wasting your time due to my misreading, though it is not rare on me.
bread-first search based compare on rational trees
% Bread-First search based sorting.
% ?- numlist(1, 100, Ns), reverse(Ns, Rs), bfs_sort(Rs, U).
% ?- bfs_sort([f(b,a), f(a,b), f(g(a,b), c)], R), reverse(R, R0),
% ?- In = [f(b,a), f(a,b), f(g(a,b), c)], reverse(In, In0),
% bfsreverse(R, R0),
bfs_sort(X, Y):- minimum_coa(X, Is, Mcoa),
predsort(bfs_compare(Mcoa), Is, Js),
zipper(Is, X, Assoc),
subst_list_by_assoc(Js, Assoc, Y).
%
bfs_compare(Mcoa, C, I, J):- fpl_compare(C, I, J, Mcoa).
% ?- X= f(Y, 0), Y=f(X, 1), reciprocal_list(1000, [X,Y], R),
% time(bfs_sort(R, R0)).
%@ % 82,660 inferences, 0.005 CPU in 0.005 seconds (95% CPU, 16469416 Lips)
%@ X = f(f(X, 1), 0),
%@ Y = f(X, 1),
%@ R = [f(f(X, 1), 0), f(X, 1), f(f(X, 1), 0), f(X, 1), f(f(X, 1), 0), f(X, 1), f(f(X, 1), 0), f(X, 1), f(..., ...)|...],
%@ R0 = [f(f(X, 1), 0), f(X, 1)] .
% ?- reciprocal_list(3, [a,b], R).
%@ R = [a, b, a, b, a, b] .
reciprocal_list(_, [], []):-!.
reciprocal_list(N, R, L):- length(R, K),
NK is N*K,
length(L, NK),
reciprocal_unify(R, L).
% ?- reciprocal_unify([a, b], [A,B,C,D]).
reciprocal_unify(_, []).
reciprocal_unify(R, L):- append(R, L0, L),
reciprocal_unify(R, L0).
% ?- minimum_coa([a,b],[I,J], Mcoa),
% fpl_compare(C, I, J, Mcoa).
% ?- X= f(Y, 0), Y=f(X, 1), minimum_coa([X, Y],[I,J], Mcoa),
% fpl_compare(C, I, J, Mcoa).
% ?- X= f(Y, 0), Y=f(X, 1), minimum_coa([X, Y],[I,J], Mcoa), fpl_compare(C, I, J, Mcoa).
% ?- X= f(Y, 0), Y=f(X, 1), minimum_coa([X, Y],[I,J], Mcoa), fpl_compare(C, J, I, Mcoa).
% FPL; frontier pair list
% The frontier pair list is the sequence of corresponding leaf pairs
% obtained from the left-to-right leaf traversal of two isomorphic% trees.
% ?- fpl_compare(C, 2, 1, v(A, B)).
fpl_compare(=, I, I, _):-!.
fpl_compare(C, I, J, Mcoa):- fpl_compare(D, [I-J], [], FPL, Mcoa),
( D = (=) -> fpl_compare(C, FPL, [], _, Mcoa)
; C = D
).
%
fpl_compare(=, [], FPL, FPL, _):-!.
fpl_compare(C, [I-J|F], FPL, FPL0, Mcoa):-
( I = J -> fpl_compare(C, F, FPL, FPL0, Mcoa)
; arg(I, Mcoa, U),
arg(J, Mcoa, V),
( \+ ( compound(U), compound(V)) ->
compare(D, U, V),
( D = (=) -> fpl_compare(C, F, FPL, FPL0, Mcoa)
; C = D,
FPL0 = FPL
)
; compare_arity(D, U, V),
( D = (=) ->
add_pair_of_args(1, U, V, FPL, FPL1),
fpl_compare(C, F, FPL1, FPL0, Mcoa)
; C = D,
FPL0 = FPL
)
)
).
%
add_pair_of_args(I, U, V, FPL, FPL0):-
arg(I, U, A),
!,
arg(I, V, B),
J is I + 1,
add_pair_of_args(J, U, V, [A-B|FPL], FPL0).
add_pair_of_args(_, _, _, FPL, FPL).
END of edit.
Original post
Urgent question: What is the output of Mercio algorithm applied to Mats Carlson’s pair X=f(Y, 0), Y=f(X,1) ? As far as I have read Mercio’s short post quoted, the output might be at least “undefined” because it does not terminate for Mats Carlsson pair, in my observation.
Also Mercio algorithm seems rather very like compare_with_stack/3 and probably the standard compare/3 except that Mercio does not say incomparable as output.
Very sorry for another wasting your time. Of course I see that Mercio is based on breadth-first search, but I realized that Mercio is really on the standard order for terms.
END
(Nothing of importance)
I posted recently elsewhere something like this.
If two terms A, B of same arity are different, there is at lest their argument pairs C, D which are different, select first such pair C, D. Write (A,B)\to (C,D) for this.
Marcio in his post responds to a question. From his answer, I am afraid that he assumes wrongly that if for any pair A\ne B, the sequence
(A,B)\to (C,D)\to \cdots
must terminate in finite steps. However, for Mats Carlsson’s pair X=f(Y,0), Y=f(X, 1),
we have non terminated sequence.
(X, Y)\to (Y,X)\to (X, Y) \to \cdots.
So I still think Mats Carlsson’s pair should be defined as incomparable. As the termination is base of total ordering of rational trees, I am lost. But I think I should not waste your time any more. Thanks.
(Nothing of importance)
(Nothing of importance)
(Nothing of importance)