SWI-Prolog as a Test Bed for Copilots (Re: Humans are just overwhelmed by computers)

Hi,
Create a ChatGPT for cyclic terms? It seems
that the SWI-Prolog discourse contains a lot
of recent exploration of about cyclic terms.
Yet humans don’t remember them,
or are too lazy to recall them, look them
up again. Maybe to offload some of the cognitive
load and have a easier way forward, one might
use GPT builder and
create a cyclic term assistant. One could
then ask the artificial intelligece (AI) for
the following things:
- Automated Testing:
   please perform some monkey testing
   on my news compare/3 idea
- Automated Proving:
   please suggest a proof for my newest
   lemma about compare/3
- Code Refactor:
   please refactor my code, I would like to
   use (==)/2 instead of same_time/2
- Auto Comment:
   please auto comment my code, I was too
   lazy to write comments
- What else?
   ChatGPT itself gave me a list when I ask
   what will be between now and AGI. Could
   look it up, as a few interesting items as well
   mainly targeting automated summarizing ideas.
Is SWI-Prolog discourse part of the SWI-Prolog
assistant building process. Its less a static
resource, has ongoing discussions. Needs periodic
retraining of the AI.
Also the above vision includes some scenarios
where the Assistant would be better integrated
into an IDE, but these Assistants have usually
more expensive price plans.
Will this IDE be XPCE, who knows?
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

>