Wait till they find out about compare/3 (Re: The headache an eGovernment might get from Prolog)

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