Path: nntp.eternal-september.org!news.eternal-september.org!eternal-september.org!feeder3.eternal-september.org!weretis.net!feeder8.news.weretis.net!reader5.news.weretis.net!news.solani.org!.POSTED!not-for-mail
From: Mild Shock <janburse@fastmail.fm>
Newsgroups: sci.logic
Subject: Humans are just overwhelmed by computers (Re: Wait till they find out
 about compare/3)
Date: Wed, 16 Jul 2025 19:02:43 +0200
Message-ID: <1058lvi$2cep9$4@solani.org>
References: <1058lt5$2cep9$2@solani.org> <1058luf$2cep9$3@solani.org>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Wed, 16 Jul 2025 17:02:42 -0000 (UTC)
Injection-Info: solani.org;
	logging-data="2505513"; mail-complaints-to="abuse@news.solani.org"
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:128.0) Gecko/20100101
 Firefox/128.0 SeaMonkey/2.53.21
Cancel-Lock: sha1:3UKUNwUAeLP6pDLM1KBt/Fg51z0=
X-User-ID: eJwVy8ERACEIBLCWQGCRclCX/ku4ufwTBsVNR8BjYnTlvOLIKa12Qia1dwvNVdB9soyUqwzawj/fgz7h3gV8VUIVOQ==
In-Reply-To: <1058luf$2cep9$3@solani.org>


 > 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
>