I am currently doing a re-evaluation of an old
Prolog system, checking what features I could adopt.
This is unlike the current trend where people have
turned their focus on GUIs, like XPCE,
or a are stuck in an endless loop of parser
problems, like in Trealla. But I would nevertheless
share my finding. Take this simple example of
a list append:
app([], X, X).
app([X|Y], Z, [X|T]) :- app(Y, Z, T).
ECLiPSe Prolog gives me, only one redo question
in the top-level:
/* ECLiPSe Prolog 7.1beta #13 */
[eclipse 2]: app(X,Y,[1]).
X = []
Y = [1]
Yes (0.00s cpu, solution 1, maybe more) ? ;
X = [1]
Y = []
Yes (0.00s cpu, solution 2)
In SWI-Prolog I find, two redo questions
in the top.level:
/* SWI-Prolog 9.3.25 */
?- app(X,Y,[1]).
X = [],
Y = [1] ;
X = [1],
Y = [] ;
false.
I know SWI-Prolog handles lists differently
than other Prolog terms during indexing. Could
this be the reason? Or maybe that the call is
not “hot” enough, so it doesn’t get JIT-ed.
ECLiPSe Prolog does it on the very first call,
and I assume its due to a kind of index on
the 3rd argument.
Interestingly, DCG is also affect. Here a
DCG take of an append app/3, it has the 2nd
and 3rd argument swapped:
?- [user].
app([]) --> [].
app([X|Y]) --> [X], app(Y).
^D
Looks like an append, taking the argument swap
into account, the A=B is redundant, could
be optimized away:
/* SWI-Prolog 9.3.25 */
?- listing(app/3).
app([], A, B) :-
A=B.
app([A|B], [A|C], D) :-
app(B, C, D).
And works like an append, again taking the
argument swap into account:
?- app([1],X,[2,3]).
X = [1, 2, 3].
Now the multi-argument indexing test, still
taking the argument swap into account;
/* ECLiPSe Prolog 7.1beta #13 */
[eclipse 3]: app(X, [1], Y).
X = []
Y = [1]
Yes (0.00s cpu, solution 1, maybe more) ? ;
X = [1]
Y = []
Yes (0.00s cpu, solution 2)
Versus:
/* SWI-Prolog 9.3.25 */
?- app(X, [1], Y).
X = [],
Y = [1] ;
X = [1],
Y = [] ;
false.
Mild Shock schrieb:
I am currently doing a re-evaluation of an old
Prolog system, checking what features I could adopt.
This is unlike the current trend where people have
turned their focus on GUIs, like XPCE,
or a are stuck in an endless loop of parser
problems, like in Trealla. But I would nevertheless
share my finding. Take this simple example of
a list append:
app([], X, X).
app([X|Y], Z, [X|T]) :- app(Y, Z, T).
ECLiPSe Prolog gives me, only one redo question
in the top-level:
/* ECLiPSe Prolog 7.1beta #13 */
[eclipse 2]: app(X,Y,[1]).
X = []
Y = [1]
Yes (0.00s cpu, solution 1, maybe more) ? ;
X = [1]
Y = []
Yes (0.00s cpu, solution 2)
In SWI-Prolog I find, two redo questions
in the top.level:
/* SWI-Prolog 9.3.25 */
?- app(X,Y,[1]).
X = [],
Y = [1] ;
X = [1],
Y = [] ;
false.
I know SWI-Prolog handles lists differently
than other Prolog terms during indexing. Could
this be the reason? Or maybe that the call is
not “hot” enough, so it doesn’t get JIT-ed.
ECLiPSe Prolog does it on the very first call,
and I assume its due to a kind of index on
the 3rd argument.
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
Mild Shock schrieb:
Interestingly, DCG is also affect. Here a
DCG take of an append app/3, it has the 2nd
and 3rd argument swapped:
?- [user].
app([]) --> [].
app([X|Y]) --> [X], app(Y).
^D
Looks like an append, taking the argument swap
into account, the A=B is redundant, could
be optimized away:
/* SWI-Prolog 9.3.25 */
?- listing(app/3).
app([], A, B) :-
A=B.
app([A|B], [A|C], D) :-
app(B, C, D).
And works like an append, again taking the
argument swap into account:
?- app([1],X,[2,3]).
X = [1, 2, 3].
Now the multi-argument indexing test, still
taking the argument swap into account;
/* ECLiPSe Prolog 7.1beta #13 */
[eclipse 3]: app(X, [1], Y).
X = []
Y = [1]
Yes (0.00s cpu, solution 1, maybe more) ? ;
X = [1]
Y = []
Yes (0.00s cpu, solution 2)
Versus:
/* SWI-Prolog 9.3.25 */
?- app(X, [1], Y).
X = [],
Y = [1] ;
X = [1],
Y = [] ;
false.
Mild Shock schrieb:
I am currently doing a re-evaluation of an old
Prolog system, checking what features I could adopt.
This is unlike the current trend where people have
turned their focus on GUIs, like XPCE,
or a are stuck in an endless loop of parser
problems, like in Trealla. But I would nevertheless
share my finding. Take this simple example of
a list append:
app([], X, X).
app([X|Y], Z, [X|T]) :- app(Y, Z, T).
ECLiPSe Prolog gives me, only one redo question
in the top-level:
/* ECLiPSe Prolog 7.1beta #13 */
[eclipse 2]: app(X,Y,[1]).
X = []
Y = [1]
Yes (0.00s cpu, solution 1, maybe more) ? ;
X = [1]
Y = []
Yes (0.00s cpu, solution 2)
In SWI-Prolog I find, two redo questions
in the top.level:
/* SWI-Prolog 9.3.25 */
?- app(X,Y,[1]).
X = [],
Y = [1] ;
X = [1],
Y = [] ;
false.
I know SWI-Prolog handles lists differently
than other Prolog terms during indexing. Could
this be the reason? Or maybe that the call is
not “hot” enough, so it doesn’t get JIT-ed.
ECLiPSe Prolog does it on the very first call,
and I assume its due to a kind of index on
the 3rd argument.
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(02345679)
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
Mild Shock schrieb:
Interestingly, DCG is also affect. Here a
DCG take of an append app/3, it has the 2nd
and 3rd argument swapped:
?- [user].
app([]) --> [].
app([X|Y]) --> [X], app(Y).
^D
Looks like an append, taking the argument swap
into account, the A=B is redundant, could
be optimized away:
/* SWI-Prolog 9.3.25 */
?- listing(app/3).
app([], A, B) :-
A=B.
app([A|B], [A|C], D) :-
app(B, C, D).
And works like an append, again taking the
argument swap into account:
?- app([1],X,[2,3]).
X = [1, 2, 3].
Now the multi-argument indexing test, still
taking the argument swap into account;
/* ECLiPSe Prolog 7.1beta #13 */
[eclipse 3]: app(X, [1], Y).
X = []
Y = [1]
Yes (0.00s cpu, solution 1, maybe more) ? ;
X = [1]
Y = []
Yes (0.00s cpu, solution 2)
Versus:
/* SWI-Prolog 9.3.25 */
?- app(X, [1], Y).
X = [],
Y = [1] ;
X = [1],
Y = [] ;
false.
Mild Shock schrieb:
I am currently doing a re-evaluation of an old
Prolog system, checking what features I could adopt.
This is unlike the current trend where people have
turned their focus on GUIs, like XPCE,
or a are stuck in an endless loop of parser
problems, like in Trealla. But I would nevertheless
share my finding. Take this simple example of
a list append:
app([], X, X).
app([X|Y], Z, [X|T]) :- app(Y, Z, T).
ECLiPSe Prolog gives me, only one redo question
in the top-level:
/* ECLiPSe Prolog 7.1beta #13 */
[eclipse 2]: app(X,Y,[1]).
X = []
Y = [1]
Yes (0.00s cpu, solution 1, maybe more) ? ;
X = [1]
Y = []
Yes (0.00s cpu, solution 2)
In SWI-Prolog I find, two redo questions
in the top.level:
/* SWI-Prolog 9.3.25 */
?- app(X,Y,[1]).
X = [],
Y = [1] ;
X = [1],
Y = [] ;
false.
I know SWI-Prolog handles lists differently
than other Prolog terms during indexing. Could
this be the reason? Or maybe that the call is
not “hot” enough, so it doesn’t get JIT-ed.
ECLiPSe Prolog does it on the very first call,
and I assume its due to a kind of index on
the 3rd argument.
Julio Di Egidio schrieb:
But we must thank MS for the nail in that coffin, too: they can't
be satisfied with just a Lean broken by design, they must own the
whole compartment: only poisoned meatballs for the public...
-Julio
Corr.: Small typo in the number
expansion itself, should read:
10/81 = 0.(123456790) = 0.12345679(012345679)
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(02345679)
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
Mild Shock schrieb:
Interestingly, DCG is also affect. Here a
DCG take of an append app/3, it has the 2nd
and 3rd argument swapped:
?- [user].
app([]) --> [].
app([X|Y]) --> [X], app(Y).
^D
Looks like an append, taking the argument swap
into account, the A=B is redundant, could
be optimized away:
/* SWI-Prolog 9.3.25 */
?- listing(app/3).
app([], A, B) :-
A=B.
app([A|B], [A|C], D) :-
app(B, C, D).
And works like an append, again taking the
argument swap into account:
?- app([1],X,[2,3]).
X = [1, 2, 3].
Now the multi-argument indexing test, still
taking the argument swap into account;
/* ECLiPSe Prolog 7.1beta #13 */
[eclipse 3]: app(X, [1], Y).
X = []
Y = [1]
Yes (0.00s cpu, solution 1, maybe more) ? ;
X = [1]
Y = []
Yes (0.00s cpu, solution 2)
Versus:
/* SWI-Prolog 9.3.25 */
?- app(X, [1], Y).
X = [],
Y = [1] ;
X = [1],
Y = [] ;
false.
Mild Shock schrieb:
I am currently doing a re-evaluation of an old
Prolog system, checking what features I could adopt.
This is unlike the current trend where people have
turned their focus on GUIs, like XPCE,
or a are stuck in an endless loop of parser
problems, like in Trealla. But I would nevertheless
share my finding. Take this simple example of
a list append:
app([], X, X).
app([X|Y], Z, [X|T]) :- app(Y, Z, T).
ECLiPSe Prolog gives me, only one redo question
in the top-level:
/* ECLiPSe Prolog 7.1beta #13 */
[eclipse 2]: app(X,Y,[1]).
X = []
Y = [1]
Yes (0.00s cpu, solution 1, maybe more) ? ;
X = [1]
Y = []
Yes (0.00s cpu, solution 2)
In SWI-Prolog I find, two redo questions
in the top.level:
/* SWI-Prolog 9.3.25 */
?- app(X,Y,[1]).
X = [],
Y = [1] ;
X = [1],
Y = [] ;
false.
I know SWI-Prolog handles lists differently
than other Prolog terms during indexing. Could
this be the reason? Or maybe that the call is
not “hot” enough, so it doesn’t get JIT-ed.
ECLiPSe Prolog does it on the very first call,
and I assume its due to a kind of index on
the 3rd argument.
Hi,
Maybe AGI should take over proving.
Just take the humans out of the loop
of any programming, it leads to nowhere.
Bye
Julio Di Egidio schrieb:
But we must thank MS for the nail in that coffin, too: they can't
be satisfied with just a Lean broken by design, they must own the
whole compartment: only poisoned meatballs for the public...
-Julio
Mild Shock schrieb:
Corr.: Small typo in the number
expansion itself, should read:
10/81 = 0.(123456790) = 0.12345679(012345679)
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(02345679)
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
Mild Shock schrieb:
Interestingly, DCG is also affect. Here a
DCG take of an append app/3, it has the 2nd
and 3rd argument swapped:
?- [user].
app([]) --> [].
app([X|Y]) --> [X], app(Y).
^D
Looks like an append, taking the argument swap
into account, the A=B is redundant, could
be optimized away:
/* SWI-Prolog 9.3.25 */
?- listing(app/3).
app([], A, B) :-
A=B.
app([A|B], [A|C], D) :-
app(B, C, D).
And works like an append, again taking the
argument swap into account:
?- app([1],X,[2,3]).
X = [1, 2, 3].
Now the multi-argument indexing test, still
taking the argument swap into account;
/* ECLiPSe Prolog 7.1beta #13 */
[eclipse 3]: app(X, [1], Y).
X = []
Y = [1]
Yes (0.00s cpu, solution 1, maybe more) ? ;
X = [1]
Y = []
Yes (0.00s cpu, solution 2)
Versus:
/* SWI-Prolog 9.3.25 */
?- app(X, [1], Y).
X = [],
Y = [1] ;
X = [1],
Y = [] ;
false.
Mild Shock schrieb:
I am currently doing a re-evaluation of an old
Prolog system, checking what features I could adopt.
This is unlike the current trend where people have
turned their focus on GUIs, like XPCE,
or a are stuck in an endless loop of parser
problems, like in Trealla. But I would nevertheless
share my finding. Take this simple example of
a list append:
app([], X, X).
app([X|Y], Z, [X|T]) :- app(Y, Z, T).
ECLiPSe Prolog gives me, only one redo question
in the top-level:
/* ECLiPSe Prolog 7.1beta #13 */
[eclipse 2]: app(X,Y,[1]).
X = []
Y = [1]
Yes (0.00s cpu, solution 1, maybe more) ? ;
X = [1]
Y = []
Yes (0.00s cpu, solution 2)
In SWI-Prolog I find, two redo questions
in the top.level:
/* SWI-Prolog 9.3.25 */
?- app(X,Y,[1]).
X = [],
Y = [1] ;
X = [1],
Y = [] ;
false.
I know SWI-Prolog handles lists differently
than other Prolog terms during indexing. Could
this be the reason? Or maybe that the call is
not “hot” enough, so it doesn’t get JIT-ed.
ECLiPSe Prolog does it on the very first call,
and I assume its due to a kind of index on
the 3rd argument.
Hi,
Having 2544 issues is probably a bad sign.
I find this many issues here:
https://github.com/rocq-prover/rocq/issues
Mostlikely 90% of the issues can be move to
the new discussion feature of GitHub.
LoL
Bye
P.S.: Same holds for Scryer Prolog with 406 issues.
Mild Shock schrieb:
Hi,
Maybe AGI should take over proving.
Just take the humans out of the loop
of any programming, it leads to nowhere.
Bye
Julio Di Egidio schrieb:
But we must thank MS for the nail in that coffin, too: they can't;
be satisfied with just a Lean broken by design, they must own the
whole compartment: only poisoned meatballs for the public...
-Julio
Mild Shock schrieb:
Corr.: Small typo in the number
expansion itself, should read:
10/81 = 0.(123456790) = 0.12345679(012345679)
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(02345679)
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
Mild Shock schrieb:
Interestingly, DCG is also affect. Here a
DCG take of an append app/3, it has the 2nd
and 3rd argument swapped:
?- [user].
app([]) --> [].
app([X|Y]) --> [X], app(Y).
^D
Looks like an append, taking the argument swap
into account, the A=B is redundant, could
be optimized away:
/* SWI-Prolog 9.3.25 */
?- listing(app/3).
app([], A, B) :-
A=B.
app([A|B], [A|C], D) :-
app(B, C, D).
And works like an append, again taking the
argument swap into account:
?- app([1],X,[2,3]).
X = [1, 2, 3].
Now the multi-argument indexing test, still
taking the argument swap into account;
/* ECLiPSe Prolog 7.1beta #13 */
[eclipse 3]: app(X, [1], Y).
X = []
Y = [1]
Yes (0.00s cpu, solution 1, maybe more) ? ;
X = [1]
Y = []
Yes (0.00s cpu, solution 2)
Versus:
/* SWI-Prolog 9.3.25 */
?- app(X, [1], Y).
X = [],
Y = [1] ;
X = [1],
Y = [] ;
false.
Mild Shock schrieb:
I am currently doing a re-evaluation of an old
Prolog system, checking what features I could adopt.
This is unlike the current trend where people have
turned their focus on GUIs, like XPCE,
or a are stuck in an endless loop of parser
problems, like in Trealla. But I would nevertheless
share my finding. Take this simple example of
a list append:
app([], X, X).
app([X|Y], Z, [X|T]) :- app(Y, Z, T).
ECLiPSe Prolog gives me, only one redo question
in the top-level:
/* ECLiPSe Prolog 7.1beta #13 */
[eclipse 2]: app(X,Y,[1]).
X = []
Y = [1]
Yes (0.00s cpu, solution 1, maybe more) ? ;
X = [1]
Y = []
Yes (0.00s cpu, solution 2)
In SWI-Prolog I find, two redo questions
in the top.level:
/* SWI-Prolog 9.3.25 */
?- app(X,Y,[1]).
X = [],
Y = [1] ;
X = [1],
Y = [] ;
false.
I know SWI-Prolog handles lists differently
than other Prolog terms during indexing. Could
this be the reason? Or maybe that the call is
not “hot” enough, so it doesn’t get JIT-ed.
ECLiPSe Prolog does it on the very first call,
and I assume its due to a kind of index on
the 3rd argument.
Hi,
1. Everybody’s a programmer now
The barrier to entry dropped dramatically — you can
become a "developer" with a few online tutorials
and a GitHub account.
2. Everybody’s an academic now
Academia expanded, but standards often fell. In
some places, it's publish or perish, so paper
mills and fake research flourish.
3. Signal Collapse ↔ Systemic Uncertainty
Credentials lose meaning, No reliable markers of
skill, Fragile systems built on shallow knowledge
4. Signal Collapse ↔ Systemic Uncertainty
Quantity overwhelms quality, Important truths get
buried, Bad signals drown good ones
Etc..
Bye
Mild Shock schrieb:
Hi,
Having 2544 issues is probably a bad sign.
I find this many issues here:
https://github.com/rocq-prover/rocq/issues
Mostlikely 90% of the issues can be move to
the new discussion feature of GitHub.
LoL
Bye
P.S.: Same holds for Scryer Prolog with 406 issues.
Mild Shock schrieb:
Hi,
Maybe AGI should take over proving.
Just take the humans out of the loop
of any programming, it leads to nowhere.
Bye
Julio Di Egidio schrieb:
But we must thank MS for the nail in that coffin, too: they can't;
be satisfied with just a Lean broken by design, they must own the
whole compartment: only poisoned meatballs for the public...
-Julio
Mild Shock schrieb:
Corr.: Small typo in the number
expansion itself, should read:
10/81 = 0.(123456790) = 0.12345679(012345679)
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(02345679)
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
Mild Shock schrieb:
Interestingly, DCG is also affect. Here a
DCG take of an append app/3, it has the 2nd
and 3rd argument swapped:
?- [user].
app([]) --> [].
app([X|Y]) --> [X], app(Y).
^D
Looks like an append, taking the argument swap
into account, the A=B is redundant, could
be optimized away:
/* SWI-Prolog 9.3.25 */
?- listing(app/3).
app([], A, B) :-
A=B.
app([A|B], [A|C], D) :-
app(B, C, D).
And works like an append, again taking the
argument swap into account:
?- app([1],X,[2,3]).
X = [1, 2, 3].
Now the multi-argument indexing test, still
taking the argument swap into account;
/* ECLiPSe Prolog 7.1beta #13 */
[eclipse 3]: app(X, [1], Y).
X = []
Y = [1]
Yes (0.00s cpu, solution 1, maybe more) ? ;
X = [1]
Y = []
Yes (0.00s cpu, solution 2)
Versus:
/* SWI-Prolog 9.3.25 */
?- app(X, [1], Y).
X = [],
Y = [1] ;
X = [1],
Y = [] ;
false.
Mild Shock schrieb:
I am currently doing a re-evaluation of an old
Prolog system, checking what features I could adopt.
This is unlike the current trend where people have
turned their focus on GUIs, like XPCE,
or a are stuck in an endless loop of parser
problems, like in Trealla. But I would nevertheless
share my finding. Take this simple example of
a list append:
app([], X, X).
app([X|Y], Z, [X|T]) :- app(Y, Z, T).
ECLiPSe Prolog gives me, only one redo question
in the top-level:
/* ECLiPSe Prolog 7.1beta #13 */
[eclipse 2]: app(X,Y,[1]).
X = []
Y = [1]
Yes (0.00s cpu, solution 1, maybe more) ? ;
X = [1]
Y = []
Yes (0.00s cpu, solution 2)
In SWI-Prolog I find, two redo questions
in the top.level:
/* SWI-Prolog 9.3.25 */
?- app(X,Y,[1]).
X = [],
Y = [1] ;
X = [1],
Y = [] ;
false.
I know SWI-Prolog handles lists differently
than other Prolog terms during indexing. Could
this be the reason? Or maybe that the call is
not “hot” enough, so it doesn’t get JIT-ed.
ECLiPSe Prolog does it on the very first call,
and I assume its due to a kind of index on
the 3rd argument.
I checked that your examples are not counter
examples for my compare_with_stack/3.
Hi,
Maybe AGI should take over proving.
Just take the humans out of the loop
of any programming, it leads to nowhere.
Bye
Julio Di Egidio schrieb:
But we must thank MS for the nail in that coffin, too: they can't
be satisfied with just a Lean broken by design, they must own the
whole compartment: only poisoned meatballs for the public...
-Julio
Mild Shock schrieb:
Corr.: Small typo in the number
expansion itself, should read:
10/81 = 0.(123456790) = 0.12345679(012345679)
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(02345679)
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
Mild Shock schrieb:
Interestingly, DCG is also affect. Here a
DCG take of an append app/3, it has the 2nd
and 3rd argument swapped:
?- [user].
app([]) --> [].
app([X|Y]) --> [X], app(Y).
^D
Looks like an append, taking the argument swap
into account, the A=B is redundant, could
be optimized away:
/* SWI-Prolog 9.3.25 */
?- listing(app/3).
app([], A, B) :-
A=B.
app([A|B], [A|C], D) :-
app(B, C, D).
And works like an append, again taking the
argument swap into account:
?- app([1],X,[2,3]).
X = [1, 2, 3].
Now the multi-argument indexing test, still
taking the argument swap into account;
/* ECLiPSe Prolog 7.1beta #13 */
[eclipse 3]: app(X, [1], Y).
X = []
Y = [1]
Yes (0.00s cpu, solution 1, maybe more) ? ;
X = [1]
Y = []
Yes (0.00s cpu, solution 2)
Versus:
/* SWI-Prolog 9.3.25 */
?- app(X, [1], Y).
X = [],
Y = [1] ;
X = [1],
Y = [] ;
false.
Mild Shock schrieb:
I am currently doing a re-evaluation of an old
Prolog system, checking what features I could adopt.
This is unlike the current trend where people have
turned their focus on GUIs, like XPCE,
or a are stuck in an endless loop of parser
problems, like in Trealla. But I would nevertheless
share my finding. Take this simple example of
a list append:
app([], X, X).
app([X|Y], Z, [X|T]) :- app(Y, Z, T).
ECLiPSe Prolog gives me, only one redo question
in the top-level:
/* ECLiPSe Prolog 7.1beta #13 */
[eclipse 2]: app(X,Y,[1]).
X = []
Y = [1]
Yes (0.00s cpu, solution 1, maybe more) ? ;
X = [1]
Y = []
Yes (0.00s cpu, solution 2)
In SWI-Prolog I find, two redo questions
in the top.level:
/* SWI-Prolog 9.3.25 */
?- app(X,Y,[1]).
X = [],
Y = [1] ;
X = [1],
Y = [] ;
false.
I know SWI-Prolog handles lists differently
than other Prolog terms during indexing. Could
this be the reason? Or maybe that the call is
not “hot” enough, so it doesn’t get JIT-ed.
ECLiPSe Prolog does it on the very first call,
and I assume its due to a kind of index on
the 3rd argument.
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?
However such relation induced above is transitive ?
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?
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,
Maybe AGI should take over proving.
Just take the humans out of the loop
of any programming, it leads to nowhere.
Bye
Julio Di Egidio schrieb:
But we must thank MS for the nail in that coffin, too: they can't;
be satisfied with just a Lean broken by design, they must own the
whole compartment: only poisoned meatballs for the public...
-Julio
Mild Shock schrieb:
Corr.: Small typo in the number
expansion itself, should read:
10/81 = 0.(123456790) = 0.12345679(012345679)
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(02345679)
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
Mild Shock schrieb:
Interestingly, DCG is also affect. Here a
DCG take of an append app/3, it has the 2nd
and 3rd argument swapped:
?- [user].
app([]) --> [].
app([X|Y]) --> [X], app(Y).
^D
Looks like an append, taking the argument swap
into account, the A=B is redundant, could
be optimized away:
/* SWI-Prolog 9.3.25 */
?- listing(app/3).
app([], A, B) :-
A=B.
app([A|B], [A|C], D) :-
app(B, C, D).
And works like an append, again taking the
argument swap into account:
?- app([1],X,[2,3]).
X = [1, 2, 3].
Now the multi-argument indexing test, still
taking the argument swap into account;
/* ECLiPSe Prolog 7.1beta #13 */
[eclipse 3]: app(X, [1], Y).
X = []
Y = [1]
Yes (0.00s cpu, solution 1, maybe more) ? ;
X = [1]
Y = []
Yes (0.00s cpu, solution 2)
Versus:
/* SWI-Prolog 9.3.25 */
?- app(X, [1], Y).
X = [],
Y = [1] ;
X = [1],
Y = [] ;
false.
Mild Shock schrieb:
I am currently doing a re-evaluation of an old
Prolog system, checking what features I could adopt.
This is unlike the current trend where people have
turned their focus on GUIs, like XPCE,
or a are stuck in an endless loop of parser
problems, like in Trealla. But I would nevertheless
share my finding. Take this simple example of
a list append:
app([], X, X).
app([X|Y], Z, [X|T]) :- app(Y, Z, T).
ECLiPSe Prolog gives me, only one redo question
in the top-level:
/* ECLiPSe Prolog 7.1beta #13 */
[eclipse 2]: app(X,Y,[1]).
X = []
Y = [1]
Yes (0.00s cpu, solution 1, maybe more) ? ;
X = [1]
Y = []
Yes (0.00s cpu, solution 2)
In SWI-Prolog I find, two redo questions
in the top.level:
/* SWI-Prolog 9.3.25 */
?- app(X,Y,[1]).
X = [],
Y = [1] ;
X = [1],
Y = [] ;
false.
I know SWI-Prolog handles lists differently
than other Prolog terms during indexing. Could
this be the reason? Or maybe that the call is
not “hot” enough, so it doesn’t get JIT-ed.
ECLiPSe Prolog does it on the very first call,
and I assume its due to a kind of index on
the 3rd argument.
Let (H, <) be the standard total oder an the
Prolog finite terms. Let R be the set of rational
term. H c R. Then there is total order
extention (R, <') of (H, <).
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?
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?
| Sysop: | DaiTengu |
|---|---|
| Location: | Appleton, WI |
| Users: | 1,090 |
| Nodes: | 10 (0 / 10) |
| Uptime: | 158:13:31 |
| Calls: | 13,922 |
| Files: | 187,021 |
| D/L today: |
224 files (59,514K bytes) |
| Messages: | 2,457,273 |