If you are only armed with Fuzz(y) Testing or Engineering trial and
error, then you are very badly prepared for computer science.
There is balance between testing and proving in computer science.
You could say there is balance between Inductive and Deductive science:
Thanks for the reference. IMHO I am afraid you will not find a counter example of transitivity.
On of the reason is this: Rational trees A and B are the same if and only if both of truncations of A and B at depth n are the same finite trees for any n.
How about applying to Matts Carlson’s pair X =f(Y,0), Y = f(X, 1) ? Do they become comparable ?
(Nothing of importance)
On finite terms comparison, top-down lift-to-right search for conflicting subterm pair is the principal, and it is the same on rational trees, I though, though possibly endless search happens like Matts Carlson’s pair. Mercio’s algorithm sounds like based on breadth-first search, which is not compatible with finite terms, I think.
I have found that for any incomparable pairs X, Y like Matts Carlsons pair there is no other rational tree Z in between X and Y, i.e., X < Z < Y. This is intuitively wrong, but a consequence of transitivity on rational trees. Now I should suspect that my lifting argument for the transitivity has a gap.
However, if my observation were correct, it means two incomparable pairs could be identified in sorting rational trees. I am curious to write such sorting codes with 1 % hope.
(Nothing of importance)
(Nothing of importance)
Rational trees A, B are incomparable if (modified) compare_with_stack/3 detects same pairs
in the stack, that is, so far, it is procedural notion. However, I think it could be defined as follows: distinct X and Y are incomparable if neither X< Y nor Y< X. A binary relation < on rational trees is defined first, It follows that < is transitive, < is not total, if X<Y then X<Z<Y for some Z.
EDIT I remember lengthy definition of mine.
Let A, B, C, D be terms with A\ne B, C\ne D. Define (A, B) \to (C, D) if A = f(A_1,A_2,\ldots,A_i, \ldots,A_n), B = f(B_1,B_2,\ldots,B_i, \ldots,B_n), A_j=B_j (1\leq j<i) A_i\neq B_i, for some n, f, 1\leq i\leq n.
Two cyclic terms X, Y are incomparable if there are infinite series of pairs
Let X=f(Y,0), Y=f(X, 1) (Mats Carlsson). Note that X\ne Y. X,Y are incomparable because of infinite series
END
The following is just for curiosity, where incomparable pairs are identified, though still I can’t imagine situations in which sorting rational trees are useful.
% ?- predsort(x_compare, [c, b, b, a], R).
%@ R = [a, b, c].
% ?- X=f(Y, 0), Y=f(X, 1), predsort(x_compare, [X, Y, X, Y], R).
%@ X = f(f(X, 1), 0),
%@ Y = f(X, 1),
%@ R = [f(f(X, 1), 0)].
x_compare(C, X, Y):- compare_with_stack(C0, X, Y),
( C0 = incomparable -> C = (=)
; C = C0
).
(Nothing of importance)
(Nothing of importance)
(Nothing of importance)
How about to make it total by force, which seems work for toy query below.
As incomparable pairs can not be separated by another rational tree I think it works for sorting
rational trees in conservative way with the standard sorting finite terms.
x_compare(C, X, Y):- compare_with_stack(C0, X, Y),
( C0 = incomparable -> C = (<) % Was (=), but better.
; C = C0
).
As compare_with_stack/3 is based heavily on ==/2 for simplicity, it should be revised of course.
% ?- X=f(Y, 0), Y=f(X, 1), predsort(x_compare, [X, a, Y, b, X, Y], R).
%@ X = f(f(X, 1), 0),
%@ Y = f(X, 1),
%@ R = [a, b, f(f(X, 1), 0), f(X, 1)].
(Nothing of importance)
compare_with_stack/3 is total, which returns four values =, < , > , incomparable.
x-compare passes to presort < for the incomparable. This is within what is allowed for use of predsort, I think.
(Nothing of importance)
If I understand correctly, this is a crucial point. I thought top-down left-to-right walking on trees solves such critical questions, but I should justify the use of pair-mem. However my definition of < is independent to such procedural definition, but relies on basic graph theory notions as I mentioned elsewhere.
(Nothing of importance)
A built-in implementation could simply do what compare/3 does except for not using the structure sharing trick and using a depth-limit. So, it performs a depth-first left-to-right comparison with a depth horizon. That is fairly trivial to implement.
Having a complete ordering that includes cyclic terms is surely worth considering.
The most important question to turn this into a practical implementation is whether we can decide that the current compare is unsafe. I guess it would suffice to figure out it decides on non-equal on a sub-term based on the modified pointer and then prove that the sub-term is cyclic? So, if we compare p(A1,B1,C1) to p(A2,B2,C2) where the variables are arbitrary subterms. If now we compare B1/B2 and they have the same functor and it returns non-equal, we need to check that B1 and B2 are both (?) cyclic and decide we cannot compare. Now we can use mercio on B1 and B2?
If that would work, the overhead and complexity look bearable. Iterative deepening should not be too bad if there is some branching (i.e., the arity of the terms that are compared is 2 or more) as the price of the failed attempts is still low. On terms with one argument and long cycles we would get quadratic complexity. Unless we can find something smarter here? We could double the depth limit rather than adding one?
(Nothing of importance)