Most General Unification in Prolog-EBG algorithm

Question

I am reading the algorithm of prolog-EBG in Machine Learning by Tom Mitchell, and the following algorithm has a step to compute a most general unification:

$\theta_{hl}:$ the most general unifier of $head$ with $Literal$ such that there exists a substitution $\theta_{li}$ for which: $$\theta_{li} (\theta_{hl} (head))= \theta_{hi}(head)$$

Here head means the head of a rule, Literal is a selected literal. In the example given:

$$head=Weight (z,5)$$ $$Literal = Weight(y,wy)$$ $$\theta_{hi} = \{z/Obj_2\}$$ $$\theta_{hl}= \{z/y, wy/5\}, where\ \theta_{li} = \{y/Obj2\}$$

Here the book states that:

The notation {z/y} denotes the substitution of y in place of z.

I am doing this unification on my own following Martelli, Montanari's algorithm and I feel quite confused.

$\{Weight(y,wy)/ Weight(z,5)\}$:

Since weight is the same predicate with same arity 2, do $\{z/y, 5/wy \}$.

Then I find confused at:

1. Which is the Variable, z, y, wy?
2. How to unify when we have constants here?

Answer 1

Comment : a substitution $\theta = \{ v_1/t_1,\ldots,v_n/t_n \ \}$ acts on an expression $E$ and $\theta(E)$ is the expression obtained from $E$ by replacing simultaneously each occurrence of the variable $v_i$ with term $t_i$.

Thus, if we assume that $\text {Weight}(z,5)$ is an atomic formula (or literal) expressing the fact that the Weight of $z$ is $5$, it is not a term and we have to apply substitutions to it.

Having said that, using the substitutions defined above we have :

$θ_{hi} (\text {head}) = θ_{hi} (\text {Weight}(z,5)) = \text {Weight}(\text {Obj}_2,5)$.

And : $θ_{hl} (\text {head}) = \text {Weight}(y,5)$.

Thus,

$θ_{li} (θ_{hl} (\text {head})) = θ_{li} (\text {Weight} (y,5)) = \text {Weight} (\text {Obj}_2 ,5)$.

Conclusion :

$θ_{li} (θ_{hl} (\text {head})) = θ_{hi} (\text {head})$.

---

If instead we want to unify $\text {head}$ with $\text {Literal}$, what we need is to apply the substitution $θ_{hl}$ to both to get :

$\text {Weight} (y,5)$.