| Deutsch English Français Italiano |
|
<v6k34o$dpc7$1@solani.org> View for Bookmarking (what is this?) Look up another Usenet article |
Path: ...!news.mixmin.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: Re: --- OLCOTT BANNED --- Date: Tue, 9 Jul 2024 21:30:32 +0200 Message-ID: <v6k34o$dpc7$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> 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: <v6k2kf$dp3g$1@solani.org> 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 = <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 ========== REMAINDER OF ARTICLE TRUNCATED ==========