Path: ...!news.mixmin.net!weretis.net!feeder8.news.weretis.net!reader5.news.weretis.net!news.solani.org!.POSTED!not-for-mail From: Mild Shock Newsgroups: sci.logic Subject: Re: --- OLCOTT BANNED --- Date: Tue, 9 Jul 2024 21:30:32 +0200 Message-ID: References: MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8; format=flowed Content-Transfer-Encoding: 8bit Injection-Date: Tue, 9 Jul 2024 19:30:32 -0000 (UTC) Injection-Info: solani.org; logging-data="451975"; 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:o3F2w/4ylF48tZjoHjMymTagh4w= X-User-ID: eJwdytEVwCAIA8CVjEIk4xQq+49gX7/vfBGsbXSat3co4h2gW4+cEs1QRmTW7zmL+wR69VOJhRK/dKZcQ/tcNHIUwg== In-Reply-To: Bytes: 6935 Lines: 189 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 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 = . > > 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 ========== REMAINDER OF ARTICLE TRUNCATED ==========