projog

3.38. unify_with_occurs_check(X, Y) - an equality test using sound unification.

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