Occurs check flag and setarg/3

Help!
1

I wonder whether some Prolog system ever considered
extending the scope of the occurs check flag. Currently
there are two ways to create cycles:

?- X = f(X).
X = f(X).

?- X = f(0), setarg(1,X,X).
X = f(X).

The occurs check only bars creation of cycles from unification.
But cycles from setarg/3 are still allowed:

?- set_prolog_flag(occurs_check, true).
true.

?- X = f(X).
false.

?- X = f(0), setarg(1,X,X).
X = f(X).

A setarg/3 check would be more difficult, since we cannot
check whether a variable occurs in a term. We would need
to see whether we reach the to be modified compound.

Is there such a check already available? It would possibly make
use of same_term/2, which is stronger than (==)/2?

2

Surely true that you can still create cycles through setarg/3. Full occur check is mostly there to support sound logical inferences though and that is gone using setarg/3 anyway. The flag is there such that we can cover all unification, everywhere. That is pretty hard otherwise. For destructive modifications there are only a couple of predicates and anyone can add explicit tests using cyclic_term/1, etc.

There is a small price. unify_with_occurs_check/2 only guarantees no new cycles are created (in SWI-Prolog), a cyclic_term/1 test would also impact cases where the original term was already cyclic. That seems to be how most Prolog systems implement unify_with_occurs_check/2 though :slight_smile: