Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]
| From | Mild Shock <janburse@fastmail.fm> |
|---|---|
| Newsgroups | sci.math |
| Subject | Mercios decidability was already attested in 2012 (Re: Mercio’s Algorithm for Rational Tree Compare in Prolog) |
| Date | 2025-08-14 20:40 +0200 |
| Message-ID | <107lai9$1hn9$2@solani.org> (permalink) |
| References | <106p0ct$3b6se$3@solani.org> |
Mercios decidability was already attested in 2012,
you find it in the original SE post. But it could
be that the two persons that didn't understand the
SE post, are @jp-diegidio and mercio. Especially since
decidability was explicitly asked in the SE post back then,
- Is it decidable for rational trees?
user4414, October 12, 2012
The question was asked by myself back in 2012, I
am also the author of the original SE post question.
Nevertheless the contrarian @jp-diegidio suddently
claims semi-decidabilty! So I have doubts that
mercio didn't understand his SE post,
since he correctly states:
- If two trees are distincts then there is a level
that distinguishes them, and so you don't need to
look infinitely far down the tree to decide how
they are ordered. You just need to check level
after level until you find the difference. So it
boils down to deciding equality among rational trees
mercio, October 12, 2012
Do you @jp-diegidio have a pair `X` and `Y` where
this here in SWI-Prolog does not properly terminate,
making the comment by mercio ultimately useless for
the implementation of `mercio/3` ?
?- X == Y.
%%% hangs or aborts ?
Here is `mercio/3` again, it uses (==)/2, and shows
decidability of a total order on rational trees,
although the order is not a natural order. I placed
comments into the code, so that the
gifted computer scientists and the blessed
mathematicians likewise understand what is going on
in Mercio's as described on the SE post. You see the
yellow highlight passages now placed into
the beautiful Prolog code:
/* equality among rational trees */
mercio(C, X, Y) :- X == Y, !,
/* boils down */
C = (=).
/* if two trees are distinct */
mercio(C, X, Y) :-
/* level that distinguishes them */
mercio(0, X, Y, C).
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?
Back to sci.math | Previous | Next — Previous in thread | Next in thread | Find similar | Unroll thread
Mercio’s Algorithm for Rational Tree Compare in Prolog Mild Shock <janburse@fastmail.fm> - 2025-08-04 02:54 +0200
The Original Ganster (OG) of Gameification: IEEE 1044.1-1995 (Re: Mercio’s Algorithm for Rational Tree Compare in Prolog) Mild Shock <janburse@fastmail.fm> - 2025-08-04 13:50 +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 13:57 +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:12 +0200
Szpilrajn Theorem and Suzumura Consistency (Re: Mercio’s Algorithm for Rational Tree Compare in Prolog Mild Shock <janburse@fastmail.fm> - 2025-08-06 01:53 +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:09 +0200
Hopcroft and Karp’s is just Contraction (Re: The good thing is we have at least Mercio’s Algorithm) Mild Shock <janburse@fastmail.fm> - 2025-08-06 08:16 +0200
Re: Hopcroft and Karp’s is just Contraction (Re: The good thing is we have at least Mercio’s Algorithm) Mild Shock <janburse@fastmail.fm> - 2025-08-06 08:23 +0200
Mercios decidability was already attested in 2012 (Re: Mercio’s Algorithm for Rational Tree Compare in Prolog) Mild Shock <janburse@fastmail.fm> - 2025-08-14 20:40 +0200
Performance of Mercio’s Total Order (Re: Mercios decidability was already attested in 2012) Mild Shock <janburse@fastmail.fm> - 2025-08-15 23:51 +0200
Fuzzy Testing is your Swiss Knife (Was: Performance of Mercio’s Total Order) Mild Shock <janburse@fastmail.fm> - 2025-08-15 23:54 +0200
Yeah, we have another name! (Re: Fuzzy Testing is your Swiss Knife) Mild Shock <janburse@fastmail.fm> - 2025-08-16 12:40 +0200
Monte Carlo sampling the frontier version (Re: Yeah, we have another name!) Mild Shock <janburse@fastmail.fm> - 2025-08-16 12:44 +0200
An NPU could give 1000x more LIPS (Re: Mercio’s Algorithm for Rational Tree Compare in Prolog) Mild Shock <janburse@fastmail.fm> - 2025-11-27 14:23 +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:02 +0100
100% serious Giga Logical Inferences per Second (GLIPS) (Re: An NPU could give 1000x more LIPS (Re: Mercio’s Algorithm for Rational Tree Compare in Prolog) Mild Shock <janburse@fastmail.fm> - 2025-11-28 14:53 +0100
csiph-web