Although unification is mostly done implicitly while matching the head of a predicate, it is also provided by the predicate =/2.
=(Term, Term).
For behaviour on cyclic terms see the Prolog flag occurs_check. Calls to =/2 in a clause body are compiled and may be (re)moved depending on the Prolog flag optimise_unify. See also section 2.17.3.
\+Term1 = Term2This 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.
\= Y.
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:
-inf. If the comparison
is equal, the float is considered the smaller value. If the Prolog flag
iso is defined, all
floating point numbers precede all rationals.
Although variables are ordered, there are some unexpected properties
one should keep in mind when relying on variable ordering. This applies
to the predicates below as to predicate such as sort/2
as well as libraries that reply on ordering such as library library(assoc)
and library
library(ordsets). Obviously, an established relation A @<
As stated above, variables are sorted by address, which implies that they are sorted by ‘age’, where ‘older’ variables are ordered before ‘newer’ variables. If two variables are unified their ‘shared’ age is the age of oldest variable. This implies we can examine a list of sorted variables with ‘newer’ (fresh) variables without invalidating the order. Attaching an attribute, see section 8.1, turns an ‘old’ variable into a ‘new’ one as illustrated below. Note that the first always succeeds as the first argument of a term is always the oldest. This only applies for the first attribute, i.e., further manipulation of the attribute list does not change the ‘age’.
?- T = f(A,B), A @< B. T = f(A, B). ?- T = f(A,B), put_attr(A, name, value), A @< B. false.
The above implies you can use e.g., an assoc (from library
library(assoc), implemented as an AVL tree) to maintain
information about a set of variables. You must be careful about what you
do with the attributes though. In many cases it is more robust to use
attributes to register information about variables.
Note that the standard order is not well defined on rational trees, also known as cyclic terms. This issue was identified by Mats Carlsson, quoted below. See also issue#1162 on GitHub.
Consider the terms A and B defined by the equations[1] A = s(B,0). [2] B = s(A,1).
- Clearly, A and B are not identical, so either
A @< BorA @> Bmust hold.
- Assume
A @< B. But then,s(A,1) @> s(B,0)i.e.,B @< A. Contradiction.
- Assume
A @> B. But then,s(A,1) @< s(B,0)i.e.,B @< A. Contradiction.
By default, comparing such terms returns an arbitrary order, which
breaks predicates that rely on a consistent order such as sort/2,
library library(assoc) and library library(ordsets).
Setting the Prolog flag incomparable
to error raises an exception instead. The predicate partial_compare/3
reports such pairs as
incomparable(Sub1, Sub2).
\+Term1 == Term2<>=undecided(Sub1, Sub2), where Sub1
and
Sub2 are the first pair of subterms of Term1 and Term2
that could not be compared. Because the standard order compares terms
lexicographically, this pair decides the entire comparison: after any
further instantiation, compare(Order, Term1, Term2) gives
the same result as compare(Order, Sub1, Sub2), unless Sub1
and
Sub2 become equal (==/2), in which case the comparison must
continue with the remaining subterms.
If the two terms are cyclic and have no order (see
section 4.6.1), Order
is unified with
incomparable(Sub1, Sub2), where Sub1 and Sub2
are a pair of subterms at which the lexicographic comparison runs into a
cycle. Unlike undecided(Sub1, Sub2), further instantiation
cannot make the terms comparable.
?- partial_compare(Order, f(a,1), f(a,2)). Order = (<). ?- partial_compare(Order, f(a,X), f(a,b)). Order = undecided(X, b). ?- partial_compare(Order, f(X,1), f(X,2)). Order = (<). ?- partial_compare(Order, f(_,1), g(_,2)). Order = (<). ?- A = s(B,0), B = s(A,1), partial_compare(Order, A, B). A = s(s(A, 1), 0), B = s(A, 1), Order = incomparable(s(s(A, 1), 0), s(A, 1)).
The last two queries illustrate that a variable only makes the comparison undecided if it is actually reached: the first of these compares the same variable to itself and continues with the second argument, while the second is decided by the functor name before the arguments are examined at all.
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).
1 a =@= Afalse 2 A =@= Btrue 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. 72The 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.73In many systems variant is implemented using two calls to subsumes_term/2.
‘\+Term1 =@= Term2’.
See =@=/2 for details.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.
Term1 == Term2
will not change due to further instantiation of either term. It behaves
as if defined by ?=(X,Y) :- \+ unifiable(X,Y,[_|_]).