Term unification

These predicates are concerned with the unification of two terms.

1. `=/2` (Prolog unify)

If X and Y are not subject to occurs check, then '='(X, Y) is true iff X and Y are unifiable.

Templates and modes for the predicate are as follows:

'='(?term, ?term)

Note that = is a predefined operator.

Let's start with some simple tests verifying success of failure of single goals.

alice.tuprolog.SimpleGoalFixture
goal	success()
'='(1, 1).	true
'='(_, _).	true
'='(1, 2).	false
'='(1, 1.0).	false
'='(g(X), f(f(X))).	false
'='(f(X, 1), f(a(X))).	false
'='(f(X, Y, X), f(a(X), a(Y), Y, 2)).	false
'='(X, a(X)).
'='(f(X, 1), f(a(X), 2)).
'='(f(1, X, 1), f(2, a(X), 2)).
'='(f(1, X), f(2, a(X))).
'='(f(X, Y, X, 1), f(a(X), a(Y), Y, 2)).

Now we run some tests also verifying the unification for some of the variables in goals.

First of all, let's start an appropriate fixture containing an engine.

fit.ActionFixture
start	alice.tuprolog.EngineFixture

Then, ask the engine to solve a query, and check variable bindings.

Note that there are no error or exception cases for this predicate.

unify_with_occurs_check(X, Y) attempts to compute and apply a most general unifier of the two terms X and Y.

Templates and modes for the predicate are as follows:

unify_with_occurs_check(?term, ?term)

Let's start with some simple tests verifying success of failure of single goals.

alice.tuprolog.SimpleGoalFixture
goal	success()
unify_with_occurs_check(1, 1).	true
unify_with_occurs_check(_, _).	true
unify_with_occurs_check(1, 2).	false
unify_with_occurs_check(1, 1.0).	false
unify_with_occurs_check(g(X), f(f(X))).	false
unify_with_occurs_check(f(X, 1), f(a(X))).	false
unify_with_occurs_check(f(X, Y, X), f(a(X), a(Y), Y, 2)).	false
unify_with_occurs_check(X, a(X)).	false
unify_with_occurs_check(f(X, 1), f(a(X), 2)).	false
unify_with_occurs_check(f(1, X, 1), f(2, a(X), 2)).	false
unify_with_occurs_check(f(1, X), f(2, a(X))).	false
unify_with_occurs_check(f(X, Y, X, 1), f(a(X), a(Y), Y, 2)).	false

Let's now start an appropriate fixture containing an engine to run tests and verify the unification for some of the variables in goals.

fit.ActionFixture
start	alice.tuprolog.EngineFixture

Then, ask the engine to solve a query, and check variable bindings.

fit.ActionFixture
enter	query	unify_with_occurs_check(X, 1).
check	hasSolution	true
enter	variable	X
check	binding	1
enter	query	unify_with_occurs_check(X, Y).
check	hasSolution	true
enter	variable	X
check	binding	Y
enter	query	unify_with_occurs_check(X, Y), unify_with_occurs_check(X, abc).
check	hasSolution	true
enter	variable	X
check	binding	abc
enter	variable	Y
check	binding	abc
enter	query	unify_with_occurs_check(f(X, def), f(def, Y)).
check	hasSolution	true
enter	variable	X
check	binding	def
enter	variable	Y
check	binding	def

Note that there are no error or exception cases for this predicate.

If X and Y are not subject to occurs check, then \=(X, Y) is true iff X and Y are not unifiable.

Templates and modes for the predicate are as follows:

'\\='(@term, @term)

Note that \= is a predefined operator.

Let's start with some simple tests verifying success of failure of single goals.

alice.tuprolog.SimpleGoalFixture
goal	success()
'\\='(1, 1).	false
\=(X, 1).	false
'\\='(X, Y).	false
\=(_, _).	false
\=(f(X, def), f(def, Y)).	false
'\\='(1, 2).	true
\=(1, 1.0).	true
'\\='(g(X), f(f(X))).	true
\=(f(X, 1), f(a(X))).	true
'\\='(f(X, Y, X), f(a(X), a(Y), Y, 2)).	true
\=(X, a(X)).
'\\='(f(X, 1), f(a(X), 2)).
'\\='(f(1, X, 1), f(2, a(X), 2)).
\=(f(1, X), f(2, a(X))).
'\\='(f(X, Y, X, 1), f(a(X), a(Y), Y, 2)).

Note that there are no error or exception cases for this predicate.

Run the tests!

The results of the tests for Term unification are as follows:

fit.Summary