"That is, a variable only unifies to a term if this term does not contain the variable itself."
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")
vars: A ↓ term: a─b─☐ a(b( A ))
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.