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.
--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)