Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]

Groups > sci.physics > #894017 > unrolled thread

The headache an eGovernment might get from Prolog

Back to article view | Back to sci.physics

Contents

  The headache an eGovernment might get from Prolog Mild Shock <janburse@fastmail.fm> - 2025-07-16 19:05 +0200
    Wait till they find out about compare/3 (Re: The headache an eGovernment might get from Prolog) Mild Shock <janburse@fastmail.fm> - 2025-07-16 19:06 +0200
      Fishy 🐟 in Scryer Prolog and SWI-Prolog (Re: Humans are just overwhelmed by computers) Mild Shock <janburse@fastmail.fm> - 2025-07-17 10:52 +0200

#894017 — The headache an eGovernment might get from Prolog

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

[toc] | [next] | [standalone]

#894018 — 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

[toc] | [prev] | [next] | [standalone]

#894029 — Fishy 🐟 in Scryer Prolog and SWI-Prolog (Re: Humans are just overwhelmed by computers)

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

[toc] | [prev] | [standalone]

Back to top | Article view | sci.physics

csiph-web