So we are essentially all using Trojan Horses 🐎 daily? (Re: Fishy 🐟 in Scryer Prolog and SWI-Prolog)

You can answer such questions
to the negative via Fuzzy Testing:
 > However such relation induced above is transitive ?
Typical counter example, showing
the native compare/3 is not transitive:
/* SWI-Prolog 9.3.25 */
?- repeat, fuzzy(X), fuzzy(Y), compare(<,X,Y), fuzzy(Z),
     compare(<,Y,Z),  compare(>,X,Z).
X = f(f(f(X, 1), 1), 1),
Y = f(f(Y, 1), 0),
Z = f(f(f(Z, 1), 0), 1) .
Etc..
Works also for Trealla Prolog, so I
assume compare_expensive/3 also fails:
/* Trealla Prolog 2.78.5 */
?- repeat, fuzzy(X), fuzzy(Y), compare(<,X,Y), fuzzy(Z),
     compare(<,Y,Z),  compare(>,X,Z).
    X = f(f(f(...,0),0),1), Y = f(f(...,1),0), Z = f(f(...,0),1)
;  ... .
Etc..
In essence, my nasty fuzzer uses
variants of Matt Carlsons example.
P.S.: From a logic viewpoint you could view
Fuzzy Testing as a form of randomized model
checking. A little famous Fuzzy Tester was Sandsifter:
"The tool discovered undocumented instructions
in all major processors, shared bugs in nearly
every major assembler and disassembler, flaws in
enterprise hypervisors, and critical x86 hardware"
https://github.com/xoreaxeaxeax/sandsifter/blob/master/references/domas_breaking_the_x86_isa_wp.pdf
So we are essentially all using Trojan Horses 🐎 daily?
Mild Shock schrieb:

Hi,
 The same example values also create fishy 🐟
sorting using native sorting in Scryer Prolog:
 /* Scryer Prolog 0.9.4-417 */
?- values([z,x,y], A), sort(A, B),
    values([x,y,z], C), sort(C, D), B == D.
    false. /* fishy 🐟 */
 Or using native sorting in SWI-Prolog:
 /* SWI-Prolog 9.3.25 */
?- values([z,x,y], A), sort(A, B),
    values([x,y,z], C), sort(C, D), B == D.
false. /* fishy 🐟 */
 Bye
 Mild Shock schrieb:

>
 > I checked that your examples are not counter
 > examples for my compare_with_stack/3.
>
What makes you think the values I show, X, Y
and Z, are possible in a total linear ordering?
The values also break predsort/3, you can easily
verify that sort([x,y,z]) =\= sort([y,x,z]):
>
value(x, X) :- X = X-0-9-7-6-5-4-3-2-1.
value(y, Y) :- Y = Y-7-5-8-2-4-1.
value(z, Z) :- H = H-9-7-6-5-4-3-2-1-0, Z = H-9-7-6-5-4-3-2-1.
>
values(L, R) :- maplist(value, L, R).
>
?- values([x,y,z], A), predsort(compare_with_stack, A, B),
    values([y,x,z], C), predsort(compare_with_stack, C, D),
    B == D.
false.
>
But expectation would be sort([x,y,z]) ==
sort([y,x,z]) since sort/2 should be immune
to permutation. If this isn’t enough proof that
there is something fishy in compare_with_stack/3 ,
>
well then I don’t know, maybe the earth is indeed flat?
>
Mild Shock schrieb:

Hi,
>
Now somebody was so friendly to spear head
a new Don Quixote attempt in fighting the
windmills of compare/3. Interestingly my
>
favorite counter example still goes through:
>
?- X = X-0-9-7-6-5-4-3-2-1, Y = Y-7-5-8-2-4-1,
    compare_with_stack(C, X, Y).
X = X-0-9-7-6-5-4-3-2-1,
Y = Y-7-5-8-2-4-1,
C = (<).
>
?- H = H-9-7-6-5-4-3-2-1-0, Z = H-9-7-6-5-4-3-2-1, Y = Y-7-5-8-2-4-1,
    compare_with_stack(C, Z, Y).
H = H-9-7-6-5-4-3-2-1-0,
Z = H-9-7-6-5-4-3-2-1,
Y = Y-7-5-8-2-4-1,
C = (>).
>
?- H = H-9-7-6-5-4-3-2-1-0, Z = H-9-7-6-5-4-3-2-1, X = X-0-9-7-6-5-4-3-2-1,
    compare_with_stack(C, Z, X).
H = H-9-7-6-5-4-3-2-1-0,
Z = X, X = X-0-9-7-6-5-4-3-2-1,
C = (=).
>
I posted it here in March 2023:
>
Careful with compare/3 and Brent algorithm
https://swi-prolog.discourse.group/t/careful-with-compare-3-and-brent-algorithm/6413 >
>
Its based that rational terms are indeed in
some relation to rational numbers. The above
terms are related to:
>
10/81 = 0.(123456790) = 0.12345679(012345679)
>
Bye
>
Mild Shock schrieb:

Hi,
>
That false/0 and not fail/0 is now all over the place,
I don't mean in person but for example here:
>
?- X=f(f(X), X), Y=f(Y, f(Y)), X = Y.
false.
>
Is a little didactical nightmare.
>
Syntactic unification has mathematical axioms (1978),
to fully formalize unifcation you would need to
formalize both (=)/2 and (≠)/2 (sic!), otherwise you
rely on some negation as failure concept.
>
Keith L. Clark, Negation as Failure
https://link.springer.com/chapter/10.1007/978-1-4684-3384-5_11
>
You can realize a subset of a mixture of (=)/2
and (≠)/2 in the form of a vanilla unify Prolog
predicate using some of the meta programming
facilities of Prolog, like var/1 and having some
>
negation as failure reading:
>
/* Vanilla Unify */
unify(V, W) :- var(V), var(W), !, (V \== W -> V = W; true).
unify(V, T) :- var(V), !, V = T.
unify(S, W) :- var(W), !, W = S.
unify(S, T) :- functor(S, F, N), functor(T, F, N),
      S =.. [F|L], T =.. [F|R], maplist(unify, L, R).
>
I indeed get:
>
?- X=f(f(X), X), Y=f(Y, f(Y)), unify(X,Y).
false.
>
If the vanilla unify/2 already fails then unify
with and without subject to occurs check, will also
fail, and unify with and without ability to
handle rational terms, will also fail:
>
Bye

>

>