Path: ...!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: --- OLCOTT BANNED ---
Date: Wed, 10 Jul 2024 06:52:24 +0200
Message-ID: <v6l429$devq$1@solani.org>
References: <v6iufa$cd7u$4@solani.org> <v6l2sg$deia$1@solani.org>
 <v6l3lv$deu2$1@solani.org>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Wed, 10 Jul 2024 04:52:25 -0000 (UTC)
Injection-Info: solani.org;
	logging-data="441338"; mail-complaints-to="abuse@news.solani.org"
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101
 Firefox/91.0 SeaMonkey/2.53.18.2
Cancel-Lock: sha1:SpuKUBj+yBBJ+i3mIG7UvF3TrmU=
X-User-ID: eJwFwYEBwDAEBMCVeHwYRxP2H6F3YVTe4wx6bOyYlFZT+qavFUBwazpDF88nLEsz+D7QQUr6JMrlFFXxAypwE5w=
In-Reply-To: <v6l3lv$deu2$1@solani.org>
Bytes: 3964
Lines: 108

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