4.6.2 Special unification and comparison predicates

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.

[ISO]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 queries below.

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).

+Term1 =@= +Term2

True if Term1 is a variant of (or structurally equivalent to) Term2. Testing for a variant is weaker than equivalence (==/2), but stronger than unification (=/2). Two terms A and B are variants iff there exists a renaming of the variables in A that makes A equivalent (==) to B and vice versa.^{69Row 7 and 8 of this table may come as a surprise, but row 8 is satisfied by (left-to-right) A→, B→ and (right-to-left) C→, A→. If the same variable appears in different locations in the left and right term, the variant relation can be broken by consistent binding of both terms. E.g., after binding the first argument in row 8 to a value, both terms are no longer variant.} Examples:

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. Its performance is comparable to ==/2, both on success and (early) failure. ^{70The 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.^{71In many systems variant is implemented using two calls to subsumes_term/2.}

+Term1 \=@= +Term2

Equivalent to ‘\+Term1 =@= Term2’. See =@=/2 for details.

[ISO]subsumes_term(@Generic, @Specific)

True if Generic can be made equivalent to Specific by only binding variables in Generic. The current implementation performs the unification and ensures that the variable set of Specific is not changed by the unification. On success, the bindings are undone.^{72This predicate is often named subsumes_chk/2 in older Prolog dialects. The current name was established in the ISO WG17 meeting in Edinburgh (2010). The 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.

term_subsumer(+Special1, +Special2, -General)

General is the most specific term that is a generalisation of Special1 and Special2. The implementation can handle cyclic terms.

unifiable(@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.^{73This predicate was introduced for the implementation of dif/2 and when/2 after discussion with Tom Schrijvers and Bart Demoen. None of us is really happy with the name and therefore suggestions for a new name are welcome.} This predicate can handle cyclic terms. Attributed variables are handled as normal variables. Associated hooks are not executed.

?=(@Term1, @Term2)

Succeeds if the syntactic equality of Term1 and Term2 can be decided safely, i.e. if the result of Term1 == Term2 will not change due to further instantiation of either term. It behaves as if defined by ?=(X,Y) :- \+ unifiable(X,Y,[_|_]).