As =/2, but using sound
unification. That is, a variable only unifies to a term if this
term does not contain the variable itself. To illustrate this, consider
the two queries below.
1 ?- A = f(A).
A = f(A).
2 ?- unify_with_occurs_check(A, f(A)).
false.
The first statement creates a cyclic
term, also called a
rational tree. The second executes logically sound unification
and thus fails. Note that the behaviour of unification through
=/2 as well as implicit
unification in the head can be changed using the Prolog flag occurs_check.
The SWI-Prolog implementation of unify_with_occurs_check/2
is cycle-safe and only guards against creating cycles, not
against cycles that may already be present in one of the arguments. This
is illustrated in the following two queries:
?- X = f(X), Y = X, unify_with_occurs_check(X, Y).
X = Y, Y = f(Y).
?- X = f(X), Y = f(Y), unify_with_occurs_check(X, Y).
X = Y, Y = f(Y).
Some other Prolog systems interpret unify_with_occurs_check/2
as if defined by the clause below, causing failure on the above two
queries. Direct use of acyclic_term/1
is portable and more appropriate for such applications.
unify_with_occurs_check(X,X) :- acyclic_term(X).
True if Term1 is a variant
of (or structurally equivalent to) Term2. Testing
for a variant is weaker than equivalence (==/2),
but stronger than unification (=/2).
Two terms A and B are variants iff there exists a
renaming of the variables in A that makes A
equivalent (==) to B and vice versa.69Row 7
and 8 of this table may come as a surprise, but row 8 is satisfied
by (left-to-right) A→, B→ and
(right-to-left) C→, A→. If the same
variable appears in different locations in the left and right term, the
variant relation can be broken by consistent binding of both terms.
E.g., after binding the first argument in row 8 to a value, both
terms are no longer variant. Examples:
| 1 | a =@= A | false |
| 2 | A =@= B | true |
| 3 | x(A,A) =@= x(B,C) | false |
| 4 | x(A,A) =@= x(B,B) | true |
| 5 | x(A,A) =@= x(A,B) | false |
| 6 | x(A,B) =@= x(C,D) | true |
| 7 | x(A,B) =@= x(B,A) | true |
| 8 | x(A,B) =@= x(C,A) | true |
A term is always a variant of a copy of itself. Term copying takes
place in, e.g., copy_term/2, findall/3
or proving a clause added with
asserta/1.
In the pure Prolog world (i.e., without attributed variables), =@=/2
behaves as if defined below. With attributed variables, variant of the
attributes is tested rather than trying to satisfy the constraints.
A =@= B :-
copy_term(A, Ac),
copy_term(B, Bc),
numbervars(Ac, 0, N),
numbervars(Bc, 0, N),
Ac == Bc.
The SWI-Prolog implementation is cycle-safe and can deal with
variables that are shared between the left and right argument. Its
performance is comparable to ==/2,
both on success and (early) failure.
70The current implementation is
contributed by Kuniaki Mukai.
This predicate is known by the name variant/2
in some other Prolog systems. Be aware of possible differences in
semantics if the arguments contain attributed variables or share
variables.71In many systems
variant is implemented using two calls to subsumes_term/2.
True if Generic can be made equivalent to Specific
by only binding variables in Generic. The current
implementation performs the unification and ensures that the variable
set of Specific is not changed by the unification. On
success, the bindings are undone.72This
predicate is often named subsumes_chk/2
in older Prolog dialects. The current name was established in the ISO
WG17 meeting in Edinburgh (2010). The chk postfix was
considered to refer to determinism as in e.g., memberchk/2.
This predicate respects constraints.
See section 5.6 for
defining clauses whose head is unified using
single sided unification.
