• =?UTF-8?Q?Fishy_=f0=9f=90=9f_in_Scryer_Prolog_and_SWI-Prolog_=28Re:?= =?UTF-8?Q?_Humans_are_just_overwhelmed_by_computers=29?=

    From Mild Shock@janburse@fastmail.fm to sci.physics on Thu Jul 17 10:52:28 2025
    From Newsgroup: sci.physics

    Hi,

    The same example values also create fishy EfEf
    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 EfEf */

    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 EfEf */

    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),
    -a-a values([y,x,z], C), predsort(compare_with_stack, C, D),
    -a-a 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 isnrCOt enough proof that
    there is something fishy in compare_with_stack/3 ,

    well then I donrCOt 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,
    -a-a-a 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,
    -a-a-a 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,
    -a-a-a 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 (rea)/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 (rea)/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),
    -a-a-a-a-a 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



    --- Synchronet 3.21a-Linux NewsLink 1.2