Although unification is mostly done implicitly while matching the head of a predicate, it is also provided by the predicate =/2.
\+Term1 = Term2
This predicate is logically sound if its arguments are sufficiently
instantiated. In other cases, such as
?- X ,
the predicate fails although there are solutions. This is due to the
incomplete nature of \+/1.
To make your programs work correctly also in situations where the arguments are not yet sufficiently instantiated, use dif/2 instead.
Comparison and unification of arbitrary terms. Terms are ordered in the so-called ``standard order''. This order is defined as follows:
\+Term1 == Term2
, 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(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).
a =@= A
A =@= B
x(A,A) =@= x(B,C)
x(A,A) =@= x(B,B)
x(A,A) =@= x(A,B)
x(A,B) =@= x(C,D)
x(A,B) =@= x(B,A)
x(A,B) =@= x(C,A)
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. 55The 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.56In many systems variant is implemented using two calls to subsumes_term/2.
`. See =@=/2 for details.
\+Term1 =@= Term2'
chkpostfix was considered to refer to determinism as in e.g., memberchk/2. This predicate respects constraints.
Term1 == Term2will not change due to further instantiation of either term. It behaves as if defined by
?=(X,Y) :- \+ unifiable(X,Y,[_|_]).