"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