Did you know ... Search Documentation:
Predicate unify_with_occurs_check/2
Availability:built-in
[ISO]unify_with_occurs_check(+Term1, +Term2)
As =/2, but using 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).
Tags are associated to your profile if you are logged in
Tags:
LogicalCaptain said (2020-06-17T13:27:32):0 upvotes 0 0 downvotes
Picture of user LogicalCaptain.

"That is, a variable only unifies to a term if this term does not contain the variable itself."

Another example:

Arbitrarily choosing LHS and RHS of "LHS = RHS":

Remembering that terms are trees and variables can only name leaves of such a tree:

  • You have the LHS term/tree with A naming some leaf node.
  • You have the RHS term/tree with the same A naming some leaf node.
  • A is a freshvar (i.e. the leaf nodes are "holes")

LHS:

vars:      A
           ↓
term:  a─b─☐            a(b( A ))

RHS:

vars:            A
                 ↓
term:  a─b─x─y─z─☐      a(b( x(y(z(A))) ))

A on the LHS will be unified with x─y─z─☐ which contains a place named by A.

This yields an infinite (cyclic) subterm.

vars:      A     A     A      The term named by A now has a beginning but no end
           ↓     ↓     ↓
term:  a─b─x─y─z─x─y─z─x─y─z-...
?- a(b(A)) = a(b(x(y(z(A))))).
A = x(y(z(A))).

?- unify_with_occurs_check(a(b(A)) , a(b(x(y(z(A)))))).
false.

Note that unify_with_occurs_check/2 does not veto the unification if the structure involved is already cyclic:

?- a(b(A)) = a(b(x(y(z(A))))), unify_with_occurs_check(A,x(y(B))).
A = x(y(z(A))),
B = z(A).

See also:

See also: Unification at Wikipedia)

See also: Occurs Check at Wikipedia