"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.
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: Unification at Wikipedia)
See also: Occurs Check at Wikipedia