**unify_with_occurs_check**(

`+Term1, +Term2`)

*sound unification*. That is, a variable only unifies to a term if this term does not contain the variable itself. To illustrate this, consider the two queries below.

1 ?- A = f(A). A = f(A). 2 ?- unify_with_occurs_check(A, f(A)). false.

The first statement creates a *cyclic
term*, also called a
*rational tree*. The second executes logically sound unification
and thus fails. Note that the behaviour of unification through
=/2 as well as implicit
unification in the head can be changed using the Prolog flag occurs_check.

The SWI-Prolog implementation of unify_with_occurs_check/2
is cycle-safe and only guards against *creating* cycles, not
against cycles that may already be present in one of the arguments. This
is illustrated in the following two queries:

?- X = f(X), Y = X, unify_with_occurs_check(X, Y). X = Y, Y = f(Y). ?- X = f(X), Y = f(Y), unify_with_occurs_check(X, Y). X = Y, Y = f(Y).

Some other Prolog systems interpret unify_with_occurs_check/2 as if defined by the clause below, causing failure on the above two queries. Direct use of acyclic_term/1 is portable and more appropriate for such applications.

unify_with_occurs_check(X,X) :- acyclic_term(X).