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).