According to Wikipedia:
Implementations offering sound unification for all unifications are Qu-Prolog and Strawberry Prolog and (optionally, via a runtime flag): XSB, SWI-Prolog and Tau Prolog.
However, when I do apropos(occur)
it only finds unify_with_occurs_check/2
. The man page doesn't mention "occur" either. How can the occurs check be enabled for all unifications in SWI-Prolog?
In the section on Environment Control, it lists the flags of the system. The occurs_check
flag is the one that controls occurs checks for unification.
You can set the flag with:
:- set_prolog_flag(occurs_check, true).
For example:
?- X = f(X).
X = f(X).
?- set_prolog_flag(occurs_check, true).
true.
?- X = f(X).
false.
So first it unifies X
with f(X)
. If we later set the occurs_check
to true
, then if we try to unify X
again with f(X)
, it fails.