These predicates are concerned with the unification of two terms.
=/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)). | false |
'='(f(X, 1), f(a(X), 2)). | false |
'='(f(1, X, 1), f(2, a(X), 2)). | false |
'='(f(1, X), f(2, a(X))). | false |
'='(f(X, Y, X, 1), f(a(X), a(Y), Y, 2)). | false |
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.
fit.ActionFixture | ||
enter | query | '='(X, 1). |
check | hasSolution | true |
enter | variable | X |
check | binding | 1 |
enter | query | '='(X, Y). |
check | hasSolution | true |
enter | variable | X |
check | binding | Y expected X actual |
enter | query | '='(X, Y), '='(X, abc). |
check | hasSolution | true |
enter | variable | X |
check | binding | abc |
enter | variable | Y |
check | binding | abc |
enter | query | '='(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.
unify_with_occurs_check/2
(unify)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 expected X actual |
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.
\=/2
(not Prolog unifiable)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). | falsealice.tuprolog.MalformedGoalException |
'\\='(X, Y). | false |
\=(_, _). | falsealice.tuprolog.MalformedGoalException |
\=(f(X, def), f(def, Y)). | falsealice.tuprolog.MalformedGoalException |
'\\='(1, 2). | true expected false actual |
\=(1, 1.0). | truealice.tuprolog.MalformedGoalException |
'\\='(g(X), f(f(X))). | true expected false actual |
\=(f(X, 1), f(a(X))). | truealice.tuprolog.MalformedGoalException |
'\\='(f(X, Y, X), f(a(X), a(Y), Y, 2)). | true expected false actual |
\=(X, a(X)). | error |
'\\='(f(X, 1), f(a(X), 2)). | false |
'\\='(f(1, X, 1), f(2, a(X), 2)). | false |
\=(f(1, X), f(2, a(X))). | error |
'\\='(f(X, Y, X, 1), f(a(X), a(Y), Y, 2)). | false |
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 | |
counts | 39 right, 5 wrong, 0 ignored, 5 exceptions |
input file | D:\Silvia\Merge_Tesi\Tesi\test\termUnification.html |
input update | Tue Dec 23 03:02:00 CET 2008 |
output file | D:\Silvia\Merge_Tesi\Tesi\test\report_Montanari\termUnification.html |
run date | Wed Sep 28 12:47:52 CEST 2011 |
run elapsed time | 0:01.18 |