From: janburse@fastmail.fm   
      
   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-a   
   d-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   
   >>   
   >   
      
   --- SoupGate-Win32 v1.05   
    * Origin: you cannot sedate... all the things you hate (1:229/2)