markh@csd4.milw.wisc.edu (Mark William Hopkins) (12/28/88)
If you are given two patterns:
f ?x (g ?x a) (h ?y) and f (h ?z) ?y (h ?z)
then you may have been taught that the Unification of these two patterns is
derived by making appropriate substitutions for the pattern variables ?x and ?y
in the first pattern, ?y and ?z in the second in such a way that the two
results match. There is an algorithm to do this procedure which is called
Pattern Unification. Yet there is a completely different type of "unification"
which is never mentioned in that context. I am going to compare the two
algorithms here.
This is a simple illustration of how Pattern Unification works. Take the
two patterns
f ?x (g ?x a) (h ?y) f (h ?z) ?y (h ?z)
and parse them:
f ?x (g ?x a) (h ?y) f (h ?z) ?y (h ?z)
becomes (0), where: becomes (5), where:
(0) = f (3) (1) (2) (5) = f (6) (7) (6)
(1) = g (3) a (6) = h (8)
(2) = h (4) (7) = ?y
(3) = ?x (8) = ?z
(4) = ?y
The labels (1), (2), etc. inside each string represents pointers to the string
with the given label. Pattern variables are represented as empty parses in
such a way that distinct variables have distinct labels. Each of these two
parses is a graph, and the unification algorithm is a particular kind of graph
traversal algorithm. I choose to represent it here is a Breadth First Search
traversal.
The algorithm goes as follows: to unify (0) and (5), unify each of the
components of the corresponding strings. When two patterns fail to unify,
we represent the result by the "null-pattern" (), (my terminology) which
satisfies the axiom:
if S = a1 ... an and ai = () for and i, then S = ().
that is, any string containing the null pattern reduces to the null pattern.
So we match (0) and (5). As a result we are required to match (3)/(6),
(1)/(7) and (2)/(6). When we get to (3), we see that (3) is a "more general"
pattern than (6) ... it can be reduced to (6) by an appropriate substitution
for the variable ?x. So we set (3) to (6). The new table entry becomes:
(3) = (6).
Matching (1) to (7) creates a new table entry:
(7) = (1).
When we match (2) to (6), we find that we have to match (4) to (8). Both
entries are equally general and so either can be bound to the other. We'll
bind (8) to (4) to create the new entry:
(8) = (4).
The final result is the table:
(0) = f (3) (1) (2) (5) = f (6) (7) (6)
(1) = g (3) a (6) = h (8)
(2) = h (4) (7) = (1)
(3) = (6) (8) = (4)
(4) = ?y
Pattern unification does not allow for recursively defined patterns, so we need
to check to ensure that the graph does not have any cycles in it. In the
process we may eliminate those vertices that cannot be reached from (0) to get
and "dereference" the bound variables (3), (7) and (8) to get:
(0) = f (6) (1) (2)
(1) = g (6) a
(2) = h (4)
(6) = h (4)
(4) = ?y
The final result of the unification of the two patterns:
f ?x (g ?x a) (h ?y) f (h ?z) ?y (h ?z)
is:
f (h ?y) (g (h ?y) a) (h ?y)
Yet there is another kind of unification algorithm. This other algorithm
attempts to derive the most specific pattern C that is more general than two
given patterns A or B. A and B can both be derived from C by substituting
appropriate variables in C, for example:
if A = f ?x a and B = f b ?y
then
C = f ?x ?y
Unification does the opposite. The algorithm uses the same parse table as
above but performs the bindings in a slightly different way. To apply the
other algorithm on the two patterns:
f ?x (g ?x a) (h ?y) f (h ?z) ?y (h ?z)
we proceed in the following way. We form the parse tables:
f ?x (g ?x a) (h ?y) f (h ?z) ?y (h ?z)
becomes (0), where: becomes (5), where:
(0) = f (3) (1) (2) (5) = f (6) (7) (6)
(1) = g (3) a (6) = h (8)
(2) = h (4) (7) = ?y
(3) = ?x (8) = ?z
(4) = ?y
and then match (0) to (5). This entails matching (3)/(6), (1)/(7) and (2)/(6)
as before. In the first match, (6) is less general than (3). The binding will
occur in the opposite direction. However, the entry (6) is left untouched.
What will be changed is only the label (6) which occurs in the string (5), not
the string (6), itself. The new table entry is thus:
(5) = f (3) (7) (6)
Matching (1)/(7) entails a similar change for the entry (0):
(0) = f (3) (7) (2)
Finally, matching (2)/(6) entails matching (4)/(8). As before, since both
patterns are equally general, we can bind either to the other. We choose to
bind (8) to (4). Thus, the new table entry for (6) is:
(6) = h (4).
This leaves us with the table:
(0) = f (3) (7) (2) (5) = f (3) (7) (6)
(1) = g (3) a (6) = h (4)
(2) = h (4) (7) = ?y
(3) = ?x (8) = ?z
(4) = ?y
which, when reduced, gives us:
(0) = f (3) (7) (2)
(3) = ?x
(7) = ?y
(2) = h (4)
(4) = ?z
(since (4) and (7) are distinct labels that thereofre represent distinct
variables, one of them has been rewritten)
The final result of this other unification algorithm on
f ?x (g ?x a) (h ?y) f (h ?z) ?y (h ?z)
is
f ?x ?y (h ?z)