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: =?UTF-8?Q?So_we_are_essentially_all_using_Trojan_Horses_?=
 =?UTF-8?B?8J+QjiBkYWlseT8gKFJlOiBGaXNoeSDwn5CfIGluIFNjcnllciBQcm9sb2cgYW5k?=
 =?UTF-8?Q?_SWI-Prolog=29?=
Date: Thu, 17 Jul 2025 10:58:55 +0200
Message-ID: <105ae0d$2dlfh$2@solani.org>
References: <1058lt5$2cep9$2@solani.org> <1058luf$2cep9$3@solani.org>
 <1058lvi$2cep9$4@solani.org> <105adhh$2dl43$1@solani.org>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Thu, 17 Jul 2025 08:58:53 -0000 (UTC)
Injection-Info: solani.org;
	logging-data="2545137"; 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:8S08LLfyEWO999iiBYFXPunrNik=
In-Reply-To: <105adhh$2dl43$1@solani.org>
X-User-ID: eJwNycEBwCAIA8CVBEOQcQRk/xHa+55tCstBI2xsMq0T6jqhc0S8QMl3Nw+U//Vqt4lCzOh0wCDQvrVOPeIDVk0VnQ==

You can answer such questions
to the negative via Fuzzy Testing:

 > However such relation induced above is transitive ?

Typical counter example, showing
the native compare/3 is not transitive:

/* SWI-Prolog 9.3.25 */
?- repeat, fuzzy(X), fuzzy(Y), compare(<,X,Y), fuzzy(Z),
     compare(<,Y,Z),  compare(>,X,Z).
X = f(f(f(X, 1), 1), 1),
Y = f(f(Y, 1), 0),
Z = f(f(f(Z, 1), 0), 1) .
Etc..

Works also for Trealla Prolog, so I
assume compare_expensive/3 also fails:

/* Trealla Prolog 2.78.5 */
?- repeat, fuzzy(X), fuzzy(Y), compare(<,X,Y), fuzzy(Z),
     compare(<,Y,Z),  compare(>,X,Z).
    X = f(f(f(...,0),0),1), Y = f(f(...,1),0), Z = f(f(...,0),1)
;  ... .
Etc..

In essence, my nasty fuzzer uses
variants of Matt Carlsons example.

P.S.: From a logic viewpoint you could view
Fuzzy Testing as a form of randomized model
checking. A little famous Fuzzy Tester was Sandsifter:

"The tool discovered undocumented instructions
in all major processors, shared bugs in nearly
every major assembler and disassembler, flaws in
enterprise hypervisors, and critical x86 hardware"
https://github.com/xoreaxeaxeax/sandsifter/blob/master/references/domas_breaking_the_x86_isa_wp.pdf

So we are essentially all using Trojan Horses 🐎 daily?

Mild Shock schrieb:
> 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-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
>>>
>>
========== REMAINDER OF ARTICLE TRUNCATED ==========