6.6 Unification and Comparison of Terms

The predicates described in this section allow unification and comparison of terms ^6.4.

Like most Prologs, default unification in XSB does not perform a so-called occurs check -- it does not handle situations where a variable X may be bound to a structure containing X as a proper subterm. For instance, in the goal

X = f(X) % incorrect!

X is bound to f(X) creating a term that is either cyclic or infinite, depending on one's point of view. Prologs in general perform unification without occurs check since without occurs check unification is linear in the size of the largest term to be unified, while unification with occurs check may be exponential in the size of the largest term to be unified. Still, unification with occurs check can be important for certain applications, in particular when Prolog is used to implement theorem provers or sophisticated constraint handlers. As a result XSB provides an ISO-style implementation of the predicate unify_with_occurs_check/2 described below.

As opposed to unification predicates, term comparison predicates described below take into account a standard total ordering of terms, which has as follows:

$$variables {\tt @<} floating point numbers {\tt @<} integers {\tt @<} atoms {\tt @<} compound terms$$

Within each one of the categories, the ordering is as follows:

• ordering of variables is based on their address within the SLG-WAM -- the order is not related to the names of variables. Thus note that two variables are identical only if they share the same address - only if they have been unified or are the same variable to begin with. As a corollary, note that two anonymous variables will not have the same address and so will not be considered identical terms. As with most WAM-based Prologs, the order of variables may change as variables become bound to one another. If the order is expected to be invariant across variable bindings, other mechanisms, such as attributed variables, should be used.
• floating point numbers and integers are put in numeric order, from $-\infty$ to $+\infty$. Note that a floating point number is always less than an integer, regardless of their numerical values. If comparison is needed, a conversion should be performed (e.g. through float/1).
• atoms are put in alphabetical (i.e. ASCII) order;
• compound terms are ordered first by arity, then by the name of their principal functor and then by their arguments (in a left-to-right order).
• lists are compared as ordinary compound terms having arity 2 and functor '.'.

For example, here is a list of terms sorted in increasing standard order:

[ X, 3.14, -9, fie, foe, fum(X), [X], X = Y, fie(0,2), fie(1,1) ]

The basic predicates for unification and comparison of arbitrary terms are:

X = Y

Unifies X and Y without occur check.

unify_with_occurs_check(One,Two)

Unifies One and Two using an occur check, and failing if One is a proper subterm of Two or if Two is a proper subterm of One.

Example:

                | ?- unify_with_occurs_check(f(1,X),f(1,a(X))).

                no
                | ?- unify_with_occurs_check(f(1,X),f(1,a(Y))).

                X = a(_h165)
                Y = _h165

                yes
                | ?- unify_with_occurs_check(f(1,a(X)),f(1,a(X))).

                X = _h165

                yes

T1 == T2

Tests if the terms currently instantiating T1 and T2 are literally identical (in particular, variables in equivalent positions in the two terms must be identical). For example, the goal:

$\vert$ ?- X == Y.

fails (answers no) because X and Y are distinct variables. However, the question

$\vert$ ?- X = Y, X == Y.

succeeds because the first goal unifies the two variables.

X $\backslash$= Y

Succeeds if X and Y are not unifiable, fails if X and Y are unifiable. It is thus equivalent to $\backslash$+(X = Y).

T1 $\backslash$== T2

Tests if the terms currently instantiating T1 and T2 are not literally identical.

Term1 ?= Term2

Succeeds if 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), !.

unifiable(X, Y, -Unifier)

constraintLib
If X and Y can unify, succeeds unifying Unifier with a list of terms of the form Var = Value representing a most general unifier of X and Y. unifiable/3 can handle cyclic terms. Attributed variables are handles as normal variables. Associated hooks are not executed ^6.5.

T1 @$<$ T2

Succeeds if term T1 is before term T2 in the standard order.

T1 @$>$ T2

Succeeds if term T1 is after term T2 in the standard order.

T1 @$=<$ T2

Succeeds if term T1 is not after term T2 in the standard order.

T1 @$>=$ T2

Succeeds if term T1 is not before term T2 in the standard order.

T1 @$=$ T2

Succeeds if T1 and T2 are identical variables, or if the main structure symbols of T1 and T2 are identical.

compare(?Op, +T1, +T2)

Succeeds if the result of comparing terms T1 and T2 is Op, where the possible values for Op are:

`='

if T1 is identical to T2,

`$<$'

if T1 is before T2 in the standard order,

`$>$'

if T1 is after T2 in the standard order.

Thus compare(=, T1, T2) is equivalent to T1==T2. Predicate compare/3 has no associated error conditions.