--- OLCOTT BANNED ---

Hi,
This one is also nice, succeeds as well, both:
/* SWI-Prolog 9.3.2 */
?- A = [f,g|A], B = [g,f|B], A = [f|B].
A = [f, g|A],
B = [g, f|B].
?- A = [f,g|A], B = [g,f|B], B = [g|A].
A = [f, g|A],
B = [g, f|B].
You cannot use unify_with_occurs_check/2 in the
above case, to ban it, since A and B are already
cyclic. When the input is already cyclic,
in SWI-Prolog, unify_with_occurs_check/2 lets
pass the unification, turns it into a kind
of bisimulation basically:
?- A = [f,g|A], B = [g,f|B], unify_with_occurs_check(A, [f|B]).
A = [f, g|A],
B = [g, f|B].
?- A = [f,g|A], B = [g,f|B], unify_with_occurs_check(B, [g|A]).
A = [f, g|A],
B = [g, f|B].
The above two examples never lead to an instantiation,
V = T, where an occurs check would be needed.
Because A and B are already ground, they don't have
any uninstantiated variables anymore:
?- A = [f,g|A], ground(A).
A = [f, g|A].
?- B = [g,f|B], ground(B).
B = [g, f|B].
Bye
Mild Shock schrieb:

Hi,
 Here you see SWI-Prolog deal with cyclic terms:
 /* SWI-Prolog 9.3.2 */
?- X = [f,f|X], Y = [f|Y], X = Y.
X = Y, Y = [f|Y].
 Clocksin & Mellish refer to the formal
definition of Unification in Resolution Theorem
proving, and not in Prolog. They write:
  > According to the formal definition of Unification,
 > this kind of "infinite term" should never come to exist.
 > Thus Prolog systems that allow a term to match an
 > uninstantiated subterm of itself do not act correctly
 > as Resolution theorem provers.
 Thats from page 254 of this Clocksin and Mellish:
 Programming in Prolog - Using the ISO Standard
Fifth Edition - See PDF page 268
Clocksin & Mellish - 2003
https://athena.ecs.csus.edu/~mei/logicp/Programming_in_Prolog.pdf
 Bye
 Mild Shock schrieb:

Hi,
>
Pete Olcott is full of bullshit. He writes
nonsense like for example:
>
"According to the formal definition of Unification, this
kind of “infinite term” should never come to exist"
https://philarchive.org/archive/OLCPDPv4
>
Thats not true. There are different formal definitions
of Unification. There is Unification with and without
occurs check.
>
There are algorithms that can make Unification without
occurs check terminate, and such an algorithm is
for example implemented in SWI-Prolog.
>
They were pioneered by Alain Colmerauer himself, the
co-inventor of Prolog, who even wrote a paper about
the subject:
>
PROLOG AND INFINITE TREES
Alain Colmerauer - 1982
Universite Aix-Marseille
https://www.softwarepreservation.org/projects/prolog/marseille/doc/Colmerauer-InfTree-1982.pdf >
Bye
>
Mild Shock schrieb:

>
The full time idiot olcott should be
put in jail, and the key should be thrown away.
All he can do is spam other peoples threads
with his crazy lovebird chirping.

>