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: Try this online Prolog (Was: --- OLCOTT BANNED ---)
Date: Wed, 10 Jul 2024 06:21:47 +0200
Message-ID: <v6l28r$ddn3$2@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> <v6l1q2$ddn3$1@solani.org>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 7bit
Injection-Date: Wed, 10 Jul 2024 04:21:47 -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:7kQx4ZMF+qafdmfvjg+MKxVKol8=
X-User-ID: eJwFwQEBACAIA7BKIv5IHAXfP4IbnMaKRXBB0ED0fs0jHdccSqH8KrhNFXFqm3X2yLrX0JzekbDSo1fGB3aIFjw=
In-Reply-To: <v6l1q2$ddn3$1@solani.org>
Bytes: 2440
Lines: 42

Hi,

 > - 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

An example of goal to head unification would be:

equal(X, X) :- write('You hit me!'), nl.

?- equal(foo(Y), Y).

You can try the same here with this online Prolog:

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

It will give you:

You hit me!
Y = <cyclic term> .

Bye

Mild Shock schrieb:
> 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.