Path: ...!2.eu.feeder.erje.net!feeder.erje.net!eternal-september.org!feeder3.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail
From: olcott <polcott333@gmail.com>
Newsgroups: sci.logic
Subject: Please quit disrespecting me
Date: Tue, 9 Jul 2024 14:46:57 -0500
Organization: A noiseless patient Spider
Lines: 203
Message-ID: <v6k43h$1ga5f$4@dont-email.me>
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>
 <v6k2kf$dp3g$1@solani.org> <v6k34o$dpc7$1@solani.org>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Tue, 09 Jul 2024 21:46:58 +0200 (CEST)
Injection-Info: dont-email.me; posting-host="b5da22ad5ca0d0ccd5a9478202582a44";
	logging-data="1583279"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX1/6oMGJp4FlxxhklVxkEYm2"
User-Agent: Mozilla Thunderbird
Cancel-Lock: sha1:OtBT9aohrbVJ4pUJAHrHO+yEOwY=
In-Reply-To: <v6k34o$dpc7$1@solani.org>
Content-Language: en-US
Bytes: 7641

On 7/9/2024 2:30 PM, Mild Shock wrote:
> You can define unify_with_occurs_check/2 in terms
> of MGU Θ it finds. The definition is such that for
> two acyclic terms X and Y, it finds an MGU Θ such that:
> 
> - 1. It equals the two terms X Θ = Y Θ
> - 2. It is most general
> - 3. The new instance X Θ is acyclic
> 
> So in the end never a cyclic graph is created in
> memory. To have a cyclic graph in memory a
> variable V with V ∈ T would need to be instantiated
> 

Yet C&M say that this test is only performed when run
thus almost never performed because it is too expensive.

If you didn't top post then context could be more accurate.
By top posting I am only responding to the gist of what
you said and not your exact words.

> to T. This would be the edge in the graph that
> participates in a cycle. But such an edge is never
> created in memory when you use unify_with_occurs_check/2.
> 
> The occurs check "prevents" that, it doesn't detect that.
> 
> Mild Shock schrieb:
>> 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
========== REMAINDER OF ARTICLE TRUNCATED ==========