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: Re: --- OLCOTT BANNED ---
Date: Tue, 9 Jul 2024 21:21:51 +0200
Message-ID: <v6k2kf$dp3g$1@solani.org>
References: <v6iufa$cd7u$4@solani.org> <v6jk49$1ctoi$13@dont-email.me>
 <v6jkfa$1ctoi$14@dont-email.me> <v6jnhj$dij7$1@solani.org>
 <v6jp3e$1er0g$1@dont-email.me> <v6k1li$dolj$1@solani.org>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Tue, 9 Jul 2024 19:21:51 -0000 (UTC)
Injection-Info: solani.org;
	logging-data="451696"; 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:maPulKCUCaxmGgBvMBQCyU4cwCs=
X-User-ID: eJwFwQkBwDAIA0BLLYQAcjoe/xJ2Z8rLctAIW1v9MnJuPxFlXczMSRNfiDRaCK9z6Dt8kckxlLZHq2kS+gM/hRSP
In-Reply-To: <v6k1li$dolj$1@solani.org>
Bytes: 5971
Lines: 168

Only a complete nut head can write nonsense like:

 >> It detects cycles in the directed graph of the expression's
 >> evaluation sequence as a paraphrase of Clocksin & Mellish indicates.

You can try yourself and see that it is a "prevent"
and not a "detect" of cyclic terms. Just go online,
and you will find:

Example 02: Website Sandbox
https://www.xlog.ch/runtab/doclet/docs/04_tutor/reference/example02/package.html

And now you can try unify_with_occurs_check/2,
it will never allow a cyclic structure in memory,
if the two arguments are already acyclic,

so it does a "prevent" and not a "detect":

/* Import Richard O'Keefes METUTL */
:- ensure_loaded(library(compat)).

/* Will not detect something but prevent something */
?- unify_with_occurs_check(X, [f|X]).
fail.

On the other hand the predicate acyclic_term/1 is made to
detect something, but and doesn't prevent something.
You can try in the Website Sandbox:

/* Will not prevent something but detect something */
?- X = [f|X], \+ acyclic_term(X).
X = <cyclic term> .

Also to the best of my knowledge its not possible
to bootstrap detect from prevention. So there is
no way to define:

/* not possible derive detect from prevent */
acyclic_term(X) :-
     ...
     /* make use of unify_with_occurs_check/2 */
     ...

Mild Shock schrieb:
> In unification with occurs check cycles in a graph
> are prevented before they happen. You are such a moron.
> The "occurs check" does that. It checks V ∈ T, BEFORE
> a variable V gets instantiated to T.
> 
> On the other hand acyclic_term/1 can figure out whether
> a term as variable V instantiated to T, where V ∈ T,
> AFTER a cycle allowing unification has been performed,
> i.e. the ordinary (=)/2.
> 
> You are an idiot, you confuse these predicate:
> 
> - acyclic_term/1
> 
> With this predicate:
> 
> - unify_with_occurs_check/2.
> 
> Usually unify_with_occurs_check/2 is not implemented as:
> 
> /* not how it is done */
> unify_with_occurs_check(X,Y) :-
>      X = Y,
>      acyclic_term(X).
> 
> The problem is the above wouldn't allow enough fast failure.
> 
> Instead it is usually implemented as follows,
> Just consult Rihcard O'Keefes File METUTL.PL :
> 
> % unify(?X, ?Y)
> % Try to unify X and Y, wih occurs check.
> % Further down in this file is the Occurs Check.
> 
> unify(X, Y) :-
>      var(X),
>      var(Y),
>      !,
>      X = Y.                %  want unify(X,X)
> unify(X, Y) :-
>      var(X),
>      !,
>      occurs_check(Y, X),        %  X is not in Y
>      X = Y.
> unify(X, Y) :-
>      var(Y),
>      !,
>      occurs_check(X, Y),        %  Y is not in X
>      X = Y.
> unify(X, Y) :-
>      atomic(X),
>      !,
>      X = Y.
> unify(X, Y) :-
>      functor(X, F, N),
>      functor(Y, F, N),
>      unify(N, X, Y).
> 
> unify(0, _, _) :- !.
> unify(N, X, Y) :-
>      arg(N, X, Xn),
>      arg(N, Y, Yn),
>      unify(Xn, Yn),
>      M is N-1,
>      !,
>      unify(M, X, Y).
> 
> occurs_check(Term, Var) :-
>      var(Term),
>      !,
>      Term \== Var.
> occurs_check(Term, Var) :-
>      functor(Term, _, Arity),
>      occurs_check(Arity, Term, Var).
> occurs_check(0, _, _) :- !.
> occurs_check(N, Term, Var) :-
>      arg(N, Term, Arg),
>      occurs_check(Arg, Var),
>      M is N-1,
>      !,
>      occurs_check(M, Term, Var).
> 
> http://www.picat-lang.org/bprolog/publib/metutl.html
> 
> Bye
> 
> olcott schrieb:
>> On 7/9/2024 11:12 AM, Mild Shock wrote:
>>>
>>> Fuck off asshole. Prolog is irrelevant for
>>> the minimal logic posts. I only made this
>>> joke, but it has nothing to do with occurs check:
>>>
>>>  > Meanwhile I am going back to my tinkering with my
>>>  > Prolog system, which even provides a more primitive
>>>  > logic than minimal logic, pure Prolog is minimal
>>>  >
>>>  > logic without embedded implication.
>>>
>>> You even don't know what the occurs check is,
>>> and for what it is used.
>>>
>>
>> It detects cycles in the directed graph of the expression's
>> evaluation sequence as a paraphrase of Clocksin & Mellish indicates.
>>
>>> If the occurs check is used, then
>>> olcott schrieb:
>>>> On 7/9/2024 10:14 AM, olcott wrote:
>>>>> On 7/9/2024 4:04 AM, Mild Shock wrote:
>>>>>>
>>>>>> 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.
>>>>>
>>>>> I initially thought that you would agree with me
>>>>> about Prolog and not dismiss what I said out-of-hand
>>>>> without review.
>>>>>
>>>>
>>>
>>
>