4.6 Comparison and Unification or Terms

4.6.1 Standard Order of Terms

Comparison and unification of arbitrary terms. Terms are ordered in the so called ``standard order''. This order is defined as follows:

1. Variables < Atoms < Strings < Numbers < Terms (20)
2. Old Variable < New Variable (21)
3. Atoms are compared alphabetically.
4. Strings are compared alphabetically.
5. Numbers are compared by value. Integers and floats are treated identically.
6. Compound terms are first checked on their arity, then on their functor-name (alphabetically) and finally recursively on their arguments, leftmost argument first.

If the prolog_flag (see current_prolog_flag/2) iso is defined, all floating point numbers precede all integers.

+Term1 == +Term2

Succeeds if Term1 is equivalent to Term2. A variable is only identical to a sharing variable.

+Term1 \== +Term2

Equivalent to \+Term1 == Term2.

+Term1 = +Term2

Unify Term1 with Term2. Succeeds if the unification succeeds.

unify_with_occurs_check(+Term1, +Term2)

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 goals below:

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.

+Term1 \= +Term2

Equivalent to \+Term1 = Term2.

+Term1 =@= +Term2

Succeeds if Term1 is `structurally equal' to Term2. Structural equivalence is weaker than equivalence (==/2), but stronger than unification (=/2). Two terms are structurally equal if their tree representation is identical and they have the same `pattern' of variables. Examples:

a	=@=	A	false
A	=@=	B	true
x(A,A)	=@=	x(B,C)	false
x(A,A)	=@=	x(B,B)	true
x(A,B)	=@=	x(C,D)	true

The predicates =@=/2 and \=@=/2 are cycle-safe. Attributed variables are considered structurally equal iff their attributes are structurally equal.

+Term1 \=@= +Term2

Equivalent to `\+Term1 =@= Term2'.

+Term1 @< +Term2

Succeeds if Term1 is before Term2 in the standard order of terms.

+Term1 @=< +Term2

Succeeds if both terms are equal (==/2) or Term1 is before Term2 in the standard order of terms.

+Term1 @> +Term2

Succeeds if Term1 is after Term2 in the standard order of terms.

+Term1 @>= +Term2

Succeeds if both terms are equal (==/2) or Term1 is after Term2 in the standard order of terms.

compare(?Order, +Term1, +Term2)

Determine or test the Order between two terms in the standard order of terms. Order is one of <, > or =, with the obvious meaning.

?=(@Term1, @Term2)

Decide whether the equality of Term1 and Term2 can be compared safely, i.e. whether the result of Term1 == Term2 can change due to further instantiation of either term. It is defined as by ?=(A,B) :- (A==B ; A B), !.. See also dif/2.

unifyable(@X, @Y, -Unifier)

If X and Y can unify, unify Unifier with a list of Var = Value, representing the bindings required to make X and Y equivalent. (22) This predicate can handle cyclic terms. Attributed variables are handles as normal variables. Associated hooks are not executed.