Although unification is mostly done implicitly while matching the head of a predicate, it is also provided by the predicate =/2.
=(Term, Term).
\+
Term1 = Term2
. See also dif/2.
Comparison and unification of arbitrary terms. Terms are ordered in the so called ``standard order''. This order is defined as follows:
\+
Term1 == Term2
.<
, >
or =
, with the obvious meaning.
This section describes special purpose variations on Prolog unification. The predicate unify_with_occurs_check/2 provides sound unification and is part of the ISO standard. The predicate subsumes_term/2 defines `one-sided-unification' and is part of the ISO proposal established in Edinburgh (2010). Finally, unifiable/3 is a `what-if' version of unification that is often used as a building block in constraint reasoners.
1 ?- A = f(A). A = f(f(f(f(f(f(f(f(f(f(...)))))))))) 2 ?- unify_with_occurs_check(A, f(A)). No
I.e. the first creates a cyclic-term,
which is printed as an infinitely nested f/1
term (see the max_depth
option of write_term/2).
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.
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.bugThe combination of sharing and cycles may produce false possitives. Its performance is comparable to ==/2, both on success and (early) failure. Unlike ==, the variant implementation does not benefit from sharing subterms.28The current implementation is based on ideas from 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.29In many systems variant is implemented using two calls to subsumes_term/2.
`\+
Term1 =@= Term2'
. See =@=/2
for details.Term1 == Term2
will not change due to further instantiation of either term. It behaves
as if defined by ?=(X,Y) :- \+ unifiable(X,Y,[_|_]).