Builtin predicates - Term unification

Predicates in this group take two terms as arguments and unifies them under various conditions.

(=)/2, (!=)/2, unifiable/2, unifiable_one_way/2, unify_one_way/2 unify_with_occurs_check/2

(=)/2 - unifies two terms.

Usage: Term1 = Term2

: unify_with_occurs_check(Term1, Term2)

Description: If Term1 and Term2 can be unified, then perform variable substitutions to unify them and succeed. Fails otherwise.

: An occurs check is performed to ensure that circular terms will not be created by the unification. Therefore, in this implementation the Standard Prolog predicate unify_with_occurs_check/2 is identical to (=)/2.

Examples

 f(X,b) = f(a,Y)      succeeds with X = a, Y = b
 f(X,b) = g(X,b)      fails
 X = f(X)             fails due to occurs check

Compatibility: Standard Prolog

See Also: (!=)/2, unifiable/2, unify_one_way/2, (:=)/2

(!=)/2 - tests if two terms are not unifiable.

Usage: Term1 != Term2

: Term1 \= Term2

Description: If Term1 and Term2 can not be unified, then succeed without modifying Term1 or Term2. Fails otherwise.

Examples

 f(X,b) != f(a,Y)     fails
 f(X,b) != g(X,b)     succeeds
 X != f(X)            succeeds

Compatibility: The (\=)/2 predicate is from Standard Prolog. The new name (!=)/2 is the recommended spelling.

See Also: (=)/2, unifiable/2, unify_one_way/2

unifiable/2 - tests if two terms are unifiable.

Usage: unifiable(Term1, Term2)

Description: If Term1 and Term2 can be unified, then succeed without modifying Term1 or Term2. Fails otherwise.

Examples

 unifiable(f(X,b), f(a,Y))    succeeds without modifying X or Y
 unifiable(f(X,b), g(X,b))    fails
 unifiable(X, f(X))           fails due to occurs check

See Also: (=)/2, (!=)/2, unifiable_one_way/2

unifiable_one_way/2 - tests if two terms are unifiable by only binding variables in the first term.

Usage: unifiable_one_way(Term1, Term2)

Description: If Term1 and Term2 can be unified without modifying Term2, then succeed without modifying Term1 or Term2. Fails otherwise.

Examples

 unifiable_one_way(X, Y + Z)  succeeds
 unifiable_one_way(Y + Z, X)  fails
 unifiable_one_way(X, Y)      succeeds

See Also: (=)/2, (!=)/2, unifiable/2, unify_one_way/2, Input-only arguments

unify_one_way/2 - unifies two terms, but only bind variables in the first term.

Usage: unify_one_way(Term1, Term2)

Description: If Term1 and Term2 can be unified without modifying Term2, then succeed. Fails otherwise.

Examples

 unify_one_way(X, Y + Z)      succeeds, binding X to Y + Z
 unify_one_way(Y + Z, X)      fails, would cause X to be modified
 unify_one_way(X, Y)          succeeds, binding X to Y

See Also: (=)/2, (!=)/2, unifiable_one_way/2, Input-only arguments