* Unification and Entailment
Basic operation in logic programming.
Recall that Store: Partition of k variables x1, ..., xk as follows.
(1) Sets of unbound variables that are equal.
(2) Variables bound to a value: number, record or procedure.
Unification is an operation that takes an assignment of the form
= and makes the two terms equal, if possible, by adding zero or
more bindings to the store. If it is not possible to equate the terms,
the operation raises a "failure" exception.
(In logic programming, unification can also deliberately fail using a
"fail" statement.)
Entailment == is an operation that checks whether two partial valu-
es are identical given the store bindings. Disentailment \= is an
operation that returns true if the partial values are different. If neit-
her is true, then both the operations block.
Store variables in this context are called logical variables.
** Primitive Bind Operation
bind(ES:EquivalenceSet, :Number|Record)
Binds all variables in ES to
The variables in ES are no longer in any equivalence set
(Case 2 of the store).
bind(ES1:EquivalenceSet, ES2:EquivalenceSet)
Merges the two equivalence sets.
** Unify(x:StoreVariable, y:StoreVariable) (Operation: =)
*** Algorithm for Acyclic structures
If x and y are in separate equivalence sets, then merge the sets with
the primitive bind operation. If x and y are in the same equivalence
set, then nothing needs to be done.
If x is in the equivalence set ES and y is determined, bind(ES,y).
If y is in the equivalence set ES and x is determined, bind(ES,x).
If x is bound to a(a1:x1 ... an:xn) and y to b(b1:y1 ... bm:ym), with
a \= b or {a1 a2 ... an} \= {b1 ... bm} then raise a failure exception.
If x is bound to a(a1:x1 ... an:xn) and y to a(a1:y1 ... an:yn), that
is x and y are bound to the same type of record, then for all i= 1 .. n,
we unify(xi, yi).
*** Unification of Cyclic Structures
--------------------------
local X in
X=[1 X]
{Browse X}
end
--------------------------
--------------------------
local X Y in
X=Y
Y=[1 a(X)]
end
--------------------------
They lead to an infinite loop in the above recursion.
We can remember the pair of unified values in a table. The table is ini-
tialized to empty. If a pair is being unified for the first time, we uni-
fy them, and add the pair to the table. If the pair of values has been
unified before, that is, they are in the table, then we skip the unifica-
tion.
Remembering the state in this way is a technique known as *memoization*.
** Entailment and Disentailment (Operations:== and \=)
==:
return true if the graphs starting from X and Y have the same struc-
ture: all pairwise corresponding nodes have identical values, or are
the same.
\=:
return NOT(==)
Both operations block when the pairwise corresponding nodes are differnt,
but at least one of them is unbound.