From: janburse@fastmail.fm   
      
   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-   
   rent-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)