Path: ...!feeds.phibee-telecom.net!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:13:53 +0200
Message-ID: <v6l1q2$ddn3$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>
 <v6k2kf$dp3g$1@solani.org> <v6k34o$dpc7$1@solani.org>
 <v6k43h$1ga5f$4@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Wed, 10 Jul 2024 04:13:54 -0000 (UTC)
Injection-Info: solani.org;
	logging-data="440035"; 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:J6TYDUVcMSwuhGmTD2h0mgZo3n0=
In-Reply-To: <v6k43h$1ga5f$4@dont-email.me>
X-User-ID: eJwFwYEBwDAEBMCVIuXFODz2H6F39kFAVxjU1vZqhp9CSSNmOlLgsuRtJg/VdW8xYOrzgpzyk3jZp+K9+QFrUxZg
Bytes: 8250
Lines: 220

Hi,

You wrote:

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

But for soundness you have to perform it sometimes!
So what is the solution? The solution is simple:

- Its not performed in the goal to head unification
- Its not performed in (=)/2 buit-in
- It is performed in unify_with_occurs_check/2 built-in

The ISO core standard requires both (=)/2 and
unify_with_occurs_check/2. You need unify_with_occurs_check/2
when you want an occurs check, which is need

for example in rewriting or type inference
to get correct results.

olcott schrieb:
> 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
>>
> 
> 
> 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).
>>>>
========== REMAINDER OF ARTICLE TRUNCATED ==========