Hi,

Nope, stack overflow didn't invent Gameification.
This was already quite fun:

IEEE Guide to Classificaton of Software Anomalies https://github.com/Orthant/IEEE/blob/master/1044.1-1995.pdf

Here some examples:

- Boing Airplane lost in the Maledives:
No problem, severity 7

- Salary Payed twice by Booking Software:
No problem, severity 0

LoL

Bye

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?

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)

Hi,

But who would have thought that Gameification leads to
Bitrot? I mean I asked the question when I had user4414,
until somebody mobbed me on MSE.

Now there is a nonsense answer accepted, and I will
not correct it. Since I don't use Bitrot anymore:

https://math.stackexchange.com/a/210730

The question "What is a natural one that is closest
to the lexical order?" of course wants "Conservativity".
Because by "lexical order" we mean (@<)/2 from Prolog.

But Mercio’s Algorithm doesn't satisfy Mats Carlsons appeal,
so we find a counter example to "Conservativity", which
is quite interesting:

problem(X, Y) :-
repeat, fuzzy(X), acyclic_term(X),
fuzzy(Y), acyclic_term(Y),
mercio(<, X, Y), \+ X @< Y.

?- problem(X, Y).
X = s(s(1, 1), 1),
Y = s(s(1, _), s(_, 1))

It is interesting, since it is now an a) an acyclic term,
and that b) violates Mats Carlsons appeal:

?- X = s(s(1, 1), 1), Y = s(s(1, _), s(_, 1)), mercio(C, X, Y).
X = s(s(1, 1), 1),
Y = s(s(1, _), s(_, 1)),
C = (<).

?- X1 = s(1,1), Y1 = s(1,_), mercio(C, X1, Y1).
X1 = s(1, 1),
Y1 = s(1, _),
C = (>).

This is kind of an independence proof of total
order and Mats Carlsons appeal.

Cool!

Bye

Mild Shock schrieb:

Hi,

Nope, stack overflow didn't invent Gameification.
This was already quite fun:

IEEE Guide to Classificaton of Software Anomalies https://github.com/Orthant/IEEE/blob/master/1044.1-1995.pdf

Here some examples:

- Boing Airplane lost in the Maledives:
  No problem, severity 7

- Salary Payed twice by Booking Software:
  No problem, severity 0

LoL

Bye

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?

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)

I guess its back to Hopcroft and Karp. And say
goodby to Mercio’s. What would work for sorting
and conservativity is a certain normal form of a DFA.
I was researching creating a minimal DFA,

but didn’t found yet a good paper. A O(N^2)
algorithm is rather straight forward, but I
wonder what a O(N log(N)) algorithm does. I only
find a good paper detailing bisimulation.

Especially from an implementation point of view,
still forming an arc to mathematical theory as well:

Hopcroft and Karp’s algorithm for Non-deterministic Finite Automata https://hal.science/hal-00639716v1/file/hkc.pdf

You might be surprised that your algorithms
compare_with_stack/3, escentially contain what
is know by the name “Naive Hopcroft and Karp
for Equality of DFA”. Whereby what SWI-Prolog

internally uses with Union Find, ist called the
“Non-Naive Hopcroft and Karp for Equality of DFA”.

Mild Shock schrieb:

Hi,

But who would have thought that Gameification leads to
Bitrot? I mean I asked the question when I had user4414,
until somebody mobbed me on MSE.

Now there is a nonsense answer accepted, and I will
not correct it. Since I don't use Bitrot anymore:

https://math.stackexchange.com/a/210730

The question "What is a natural one that is closest
to the lexical order?" of course wants "Conservativity".
Because by "lexical order" we mean (@<)/2 from Prolog.

But Mercio’s Algorithm doesn't satisfy Mats Carlsons appeal,
so we find a counter example to "Conservativity", which
is quite interesting:

problem(X, Y) :-
   repeat, fuzzy(X), acyclic_term(X),
   fuzzy(Y), acyclic_term(Y),
   mercio(<, X, Y), \+ X @< Y.

?- problem(X, Y).
X = s(s(1, 1), 1),
Y = s(s(1, _), s(_, 1))

It is interesting, since it is now an a) an acyclic term,
and that b) violates Mats Carlsons appeal:

?- X = s(s(1, 1), 1), Y = s(s(1, _), s(_, 1)), mercio(C, X, Y).
X = s(s(1, 1), 1),
Y = s(s(1, _), s(_, 1)),
C = (<).

?- X1 = s(1,1), Y1 = s(1,_), mercio(C, X1, Y1).
X1 = s(1, 1),
Y1 = s(1, _),
C = (>).

This is kind of an independence proof of total
order and Mats Carlsons appeal.

Cool!

Bye

Mild Shock schrieb:

Hi,

Nope, stack overflow didn't invent Gameification.
This was already quite fun:

IEEE Guide to Classificaton of Software Anomalies
https://github.com/Orthant/IEEE/blob/master/1044.1-1995.pdf

Here some examples:

- Boing Airplane lost in the Maledives:
   No problem, severity 7

- Salary Payed twice by Booking Software:
   No problem, severity 0

LoL

Bye

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?

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)