
Chapter 14: Logic Programming and Parallel Complexity 577
1.
The root of T, node u, is mapped by ρ to v.
2.
For all nodes w of T, w and p(w) are labeled by the same function, or w
is labeled by a variable.
3. For all nodes w and w' of T, if there is an arc in Τ labeled i from wtow'
then there is an arc in dag ν labeled i from p(w) to p(w').
If there is no embedding, then clearly t
u
and t
v
are not unifiable.
M3 The embedding ρ gives a substitution for all the variables of t
u
. Specifi-
cally, if variable χ is the label of (the unique) node w in dag u then the subdag
rooted at p(w) represents the term substituted for x. The substitution is per