Works like X = Y but with an additional check to avoid cyclic terms. When using unify_with_occurs_check a variable can only be unified with a term if that term does not contain the variable.
Examples
?- unify_with_occurs_check(A, f(A)).
no
?- unify_with_occurs_check(f(A), A).
no
?- unify_with_occurs_check(A, [1, A, 3]).
no
?- unify_with_occurs_check([1, A, 3], A).
no
?- unify_with_occurs_check(A, f([1, A, 3])).
no
?- unify_with_occurs_check(f([1, A, 3]), A).
no
?- unify_with_occurs_check(A, [1, f(A), 3]).
no
?- unify_with_occurs_check([1, f(A), 3], A).
no
?- unify_with_occurs_check(f(A), f([1, A, 3])).
no
?- unify_with_occurs_check(f([1, A, 3]), f(A)).
no
?- unify_with_occurs_check(X, X).
X = UNINSTANTIATED VARIABLE
yes
?- unify_with_occurs_check(X, Y).
X = UNINSTANTIATED VARIABLE
Y = UNINSTANTIATED VARIABLE
yes
?- X=1, unify_with_occurs_check(X, Y).
X = 1
Y = 1
yes
?- unify_with_occurs_check(X, Y), Y=2.
X = 2
Y = 2
yes
?- unify_with_occurs_check(X, f(Y)).
X = f(Y)
Y = UNINSTANTIATED VARIABLE
yes
?- unify_with_occurs_check(f(X), Y).
X = UNINSTANTIATED VARIABLE
Y = f(X)
yes
?- unify_with_occurs_check(X, [1, Y, 3]).
X = [1,Y,3]
Y = UNINSTANTIATED VARIABLE
yes
?- unify_with_occurs_check([1, X, 3], Y).
X = UNINSTANTIATED VARIABLE
Y = [1,X,3]
yes
?- unify_with_occurs_check(a, a).
yes
?- unify_with_occurs_check(1, 1).
yes
?- unify_with_occurs_check(1.0, 1.0).
yes
?- unify_with_occurs_check(1.5, 1.5).
yes
?- unify_with_occurs_check([], []).
yes
?- unify_with_occurs_check([a], [a]).
yes
?- unify_with_occurs_check([a, b, c], [a, b, c]).
yes
?- unify_with_occurs_check(p(a), p(a)).
yes
?- unify_with_occurs_check(p(a, b, c), p(a, b, c)).
yes
?- unify_with_occurs_check(a, b).
no
?- unify_with_occurs_check(1, 2).
no
?- unify_with_occurs_check(1, -1).
no
?- unify_with_occurs_check(1, '1').
no
?- unify_with_occurs_check(1, 1.0).
no
?- unify_with_occurs_check(1.0, -1.0).
no
?- unify_with_occurs_check(1.0, 1.5).
no
?- unify_with_occurs_check(2, 1+1).
no
?- unify_with_occurs_check([a], [x]).
no
?- unify_with_occurs_check([a, b, c], [a, b, x]).
no
?- unify_with_occurs_check([a, b, c], [a, x, c]).
no
?- unify_with_occurs_check([a, b, c], [x, b, c]).
no
?- unify_with_occurs_check([a, b, c], [a, c, b]).
no
?- unify_with_occurs_check([a, b, c], [b, a, c]).
no
?- unify_with_occurs_check([a, b, c], [b, c, a]).
no
?- unify_with_occurs_check([a, b, c], [c, a, b]).
no
?- unify_with_occurs_check([a, b, c], [c, b, a]).
no
?- unify_with_occurs_check(p(a), p(x)).
no
?- unify_with_occurs_check(p(a, b), p(a)).
no
?- unify_with_occurs_check(p(a), p(a, b)).
no
?- unify_with_occurs_check(p(a, b, c), p(a, b, x)).
no
?- unify_with_occurs_check(p(a, b, c), p(a, x, c)).
no
?- unify_with_occurs_check(p(a, b, c), p(x, b, c)).
no
?- unify_with_occurs_check(p(a, b, c), p(a, c, b)).
no
?- unify_with_occurs_check(p(a, b, c), p(b, a, c)).
no
?- unify_with_occurs_check(p(a, b, c), p(b, c, a)).
no
?- unify_with_occurs_check(p(a, b, c), p(c, a, b)).
no
?- unify_with_occurs_check(p(a, b, c), p(c, b, a)).
no