Szpilrajn Theorem and Suzumura Consistency (Was: Mercio’s Algorithm for Rational Tree Compare in Prolog)

From	Mild Shock <janburse@fastmail.fm>
Newsgroups	comp.lang.prolog
Subject	Szpilrajn Theorem and Suzumura Consistency (Was: Mercio’s Algorithm for Rational Tree Compare in Prolog)
Date	2025-08-06 01:50 +0200
Message-ID	<106u5bj$3bpia$1@solani.org> (permalink)
References	<106p08a$3b6se$1@solani.org>

Show all headers | View raw

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 order. And compare_rat/2 is

not Suzumura consistent, as the following
cycle a < c < b < a shows:

/* Not SWI, Windows Console is SNAFU */
?- 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.

Mild Shock schrieb:
> Mercio’s Algorithm (2012) for Rational
> Tree Compare is specified here mathematically.
> It is based on computing truncations A' = (A_0,
> A_1, etc..) of a rational tree A:
> 
> A < B ⟺ A′ <_lex B′
> 
> https://math.stackexchange.com/a/210730
> 
> Here is an implementation in Prolog.
> First the truncation:
> 
> trunc(_, T, T) :- var(T), !.
> trunc(0, T, F) :- !, functor(T, F, _).
> trunc(N, T, S) :-
>     M is N-1,
>     T =.. [F|L],
>     maplist(trunc(M), L, R),
>     S =.. [F|R].
> 
> And then the iterative deepening:
> 
> mercio(N, X, Y, C) :-
>     trunc(N, X, A),
>     trunc(N, Y, B),
>     compare(D, A, B),
>     D \== (=), !, C = D.
> mercio(N, X, Y, C) :-
>     M is N + 1,
>     mercio(M, X, Y, C).
> 
> The main entry first uses (==)/2 for a
> terminating equality check and if the
> rational trees are not equal, falls back
> to the iterative deepening:
> 
> mercio(C, X, Y) :- X == Y, !, C = (=).
> mercio(C, X, Y) :- mercio(0, X, Y, C).
> 
> I couldn’t find yet a triple that violates
> transitivity. But I am also not much happy
> with the code. Looks a little bit expensive
> to create a truncation copy iteratively.
> 
> Provided there is really no counter example,
> maybe we can do mit more smart and faster? It
> might also stand the test of conservativity?

Thread

Mercio’s Algorithm for Rational Tree Compare in Prolog Mild Shock <janburse@fastmail.fm> - 2025-08-04 02:52 +0200
  The Original Ganster (OG) of Gameification: IEEE 1044.1-1995 (Was: Mercio’s Algorithm for Rational Tree Compare in Prolog) Mild Shock <janburse@fastmail.fm> - 2025-08-04 13:48 +0200
    The Bitrot called Math Stack Exchange (Re: The Original Ganster (OG) of Gameification: IEEE 1044.1-1995) Mild Shock <janburse@fastmail.fm> - 2025-08-04 14:00 +0200
      I guess its back to Hopcroft and Karp.Re: The Bitrot called Math Stack Exchange) Mild Shock <janburse@fastmail.fm> - 2025-08-04 14:11 +0200
  Szpilrajn Theorem and Suzumura Consistency (Was: Mercio’s Algorithm for Rational Tree Compare in Prolog) Mild Shock <janburse@fastmail.fm> - 2025-08-06 01:50 +0200
    The good thing is we have at least Mercio’s Algorithm (Re: Szpilrajn Theorem and Suzumura Consistency) Mild Shock <janburse@fastmail.fm> - 2025-08-06 08:10 +0200
      Hopcroft and Karp’s is just Contraction (Was: The good thing is we have at least Mercio’s Algorithm) Mild Shock <janburse@fastmail.fm> - 2025-08-06 08:13 +0200
        Re: Hopcroft and Karp’s is just Contraction (Was: The good thing is we have at least Mercio’s Algorithm) Mild Shock <janburse@fastmail.fm> - 2025-08-06 08:23 +0200
      Should we use minimum_coa/3 ? (Was: The good thing is we have at least Mercio’s Algorithm) Mild Shock <janburse@fastmail.fm> - 2025-08-08 23:45 +0200
        Perfectly balanced , as all things should be! (Was: Should we use minimum_coa/3 ?) Mild Shock <janburse@fastmail.fm> - 2025-08-08 23:49 +0200
  Mercios decidability was already attested in 2012 (Was: Mercio’s Algorithm for Rational Tree Compare in Prolog) Mild Shock <janburse@fastmail.fm> - 2025-08-14 20:26 +0200
    Performance of Mercio’s Total Order (Was: Mercios decidability was already attested in 2012) Mild Shock <janburse@fastmail.fm> - 2025-08-15 23:49 +0200
      Fuzzy Testing is your Swiss Knife (Re: Performance of Mercio’s Total Order) Mild Shock <janburse@fastmail.fm> - 2025-08-15 23:55 +0200
        Yeah, we have another name! (Was: Fuzzy Testing is your Swiss Knife) Mild Shock <janburse@fastmail.fm> - 2025-08-16 12:38 +0200
        Monte Carlo sampling the frontier version (Was: Yeah, we have another name!) Mild Shock <janburse@fastmail.fm> - 2025-08-16 12:42 +0200
        AI most hated by formal verification (Was: Fuzzy Testing is your Swiss Knife) Mild Shock <janburse@fastmail.fm> - 2025-11-26 17:02 +0100
  An NPU could give 1000x more LIPS (Was: Mercio’s Algorithm for Rational Tree Compare in Prolog) Mild Shock <janburse@fastmail.fm> - 2025-11-27 14:19 +0100
    Neural Network based dif/2 respectively (#\=)/2 (Re: An NPU could give 1000x more LIPS) Mild Shock <janburse@fastmail.fm> - 2025-11-27 14:51 +0100
      Zeus: A Language for Expressing Algorithms in Hardware (Re: Neural Network based dif/2 respectively (#\=)/2) Mild Shock <janburse@fastmail.fm> - 2025-11-27 15:03 +0100
        Googles TPU muscle in 2017 [Prolog Community is Sleepy Joe] (Re: Zeus: A Language for Expressing Algorithms in Hardware) Mild Shock <janburse@fastmail.fm> - 2025-11-27 15:23 +0100
    100% serious Giga Logical Inferences per Second (GLIPS) (Was: An NPU could give 1000x more LIPS) Mild Shock <janburse@fastmail.fm> - 2025-11-28 14:50 +0100
      The tables have turned: GigaLIP on the Laptop? (Re: 100% serious Giga Logical Inferences per Second (GLIPS) Mild Shock <janburse@fastmail.fm> - 2025-11-28 15:12 +0100

csiph-web