Szpilrajn Theorem and Suzumura Consistency

Nice to know
1

Now question is whether compare_rat/2 can
be extended to a total order or not. On the positive side
we find that a partial order can always be extended:

Szpilrajn Extension Theorem
https://en.wikipedia.org/wiki/Szpilrajn_extension_theorem

But what if compare_rat/2 by @kuniaki.mukai is not a partial
order? What if it is only a preorder, or even worse only
a binary relation. Returning 4 values doesn’t guarantee

that it is a partial order. We have help from here:

Szpilrajn, Arrow and Suzumura
https://onlinelibrary.wiley.com/doi/abs/10.1111/j.1467-999X.2011.04130.x

A binary relation needs to be Suzumura consistent,
so that it can be extended into a total preorder. And
compare_rat/2 is not Suzumura consistent, as

the following cycle a < c < b < a shows:

?- repeat, fuzzy(A), fuzzy(C), compare_rat(_X, A, C), _X = (<),
   fuzzy(B), compare_rat(_Y, C, B), _Y = (<),
   compare_rat(_Z, B, A), _Z = (<).
A = s(s(A, A), 1), _A = s(_A, s(_, 1)), C = s(_A, _), 
_B = s(1, _B), B = s(B, s(1, _B))

Was only testing with compare_rat/3, but the theorem applies
also to other compare proposals, and can be used to exclude
them, as soon as a Suzumura inconsistency is found.

2

I have been updating compare_rat/3 little by little repeatedly, and now have to say I lost the old one. compare_rat/3 has the exactly same idea on “incomparable”, and only differs in that
it is based on same_term/2 instead of ==/2. I am afraid it is not usable for others, because, first, it converts whole involved terms into a minimum system of equations in vector form with flat terms as elements (i.e. coalgebra in theory). It might be ultimate term_factorized, though I am not familiar with it.

5

I knew little of the incomparable relation R. But I am getting a list of elementary properties of R.

  • If R(x,y) there is no z such that R(x,z) and R(z, y).

  • For some x, there are infinitely many y such that R(x, y).

  • If R(x,y) then R(y,x). (Symmetric)

  • If R(x,y) and R(y,z), then R(x,z). (Transitive)

Hence it follows that the reflexive closure of R is an equivalence relation, though I am not 100 percent sure in the transitivity. This means that by identifying incomparable group (the quotient set modulo R) is linearly ordered by <. I didn’t imagine that I have to think about such basic things, and I hope it is a kind of folklore.

6

(Nothing of importance)

7

(Nothing of importance)

9

What I assert on comparing rational trees is simple. To compare A with B, assuming A \== B, walk down from the initial pair (A, B), keeping pairs of corresponding arguments on the history stack downward. If no pair of different arguments in the current branch then popup one step before and move to the pair of next right arguments. If the same pair is found in the history stack, then exit with “incomparable”. Otherwise, there must be found a pair of different arguments then apply the standard compare/3 to them, and exit with the result. As A and B are assumed to be different, such pair must be found. Otherwise by bisimulation argument it follows A = B, a contradiction.

Although for incomparable pairs A, B, order is not lifted from that of finite terms, forced order A<B works due to nice property of incomparable pairs, for sorting list of rational trees, for example which is lucky.

I think this might be possible best reply to your recent posts, which were really difficult for me to understand your thought on ordering rational trees. Sorry for my poor reading. I should wait the moment in the future when I would shout “Aha he did say this.”

10

(Nothing of importance)

12

I prepared the home work that seems to be solved by me also.
But the problem seems disappeared before I posted . Anyway it is an answer:

Let E be an equivalence relation on X and the quotient set of (X/E, \leq) is linearly ordered.
Suppose \leq_C is a total order on C\in X/E. Then \bigcup_{C\in X/E} E_C extends to a total order on E in obvious way, like from \{1,2 \} < \{3,4\}, and 1<2, 3<4 locally, then we can paste it to get a global 1<2<3<4.

13

(Nothing of importance)

14

What order do you give for Mats Carlsson’s pair X = f(Y,0), Y=f(X, 1) ? 
Is it X < Y because of comparing the second arguments 0 < 1 ?
I agree that bread-first comparison gives total order on the rational terms, even for irrational trees.
Perhaps I am missing on this. I wrote a definition of incomparable (implicitly < ). If it is not that easy one based bread-first search for rational trees, could you reproduce here the definition if it exists.

15

(Nothing of importance)

16

(Nothing of importance)

17

If I understand correctly, your idea is to convert frist rational tree X to its minimized DNF D_X. Then compare D_X and D_Y in their canonial forms. However properties of the canonical order is unclear for me it seems to forget completely the order of finite terms. Anyway I feel I understand your idea, and I think it depends on applications on rational tree orders. Thanks.

20

(Nothing of importance)