Occurs check flag and setarg/3

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?

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:

Maybe some Prolog systems have a setarg_with_occurs_check/3. But the occurs check would not be the traditional v ∈ t check, but s ∈ t where s is the target compound. But it would not help somebody who anyway uses setarg/3 to create a cyclic data structure, like for example a double linked list. But sometimes setarg/3 is used for non cyclic data structures.

If a Prolog systems can implement setarg_with_occurs_check/3, it might also respect occurs_check flag in setarg/3. But I don’t know whether for example SWI-Prolog uses setarg/3 already internally with some cyclic data structure. So when we would make occurs_check=true and if it had the extended semantic, maybe it would paralyze the Prolog system?