How to unify a pair of atomic formulas?

Question

Unify the pair of atomic formulas $p(a,x,f(g(y))),\ p(z,h(z,u),f(u))$.

Attempt following the alogrithm described below.

We have \begin{align} \begin{aligned} a &=z\\ x &=h(z,u)\\ f(g(y))&=f(u) \end{aligned} \implies \begin{aligned} z&=a\\ x&=h(z,u)\\ f(g(y))&=f(u) \end{aligned} \end{align}

Now here I could apply 3. to get $g(y)=u$ and hence $u=g(y)$.

And I don't know how to proceed from here.

The thing is I'm confused on how the algorithm works, $u$ and $z$ variables have another occurrence in $x=h(z,u)$ so we should use step 4. but I don't understand what this means

"If $x$ occurs in $t$ and $x$ differs from $t$".

For the example above we have $z=a,$ i.e. $t=a$, thus $z$ occurs in $a$ means $z=a$?

Also, what does step 3 mean?

"If the outermost function symbols of $t$ and $t'$ are not identical, terminate the algorithm and report not unifiable".

Outermost respect to what? Note that there is no problem when there is just one function.

---

Algorithm 10.15 (Unification algorithm) (See Ben-Ari page 190)

Input: A set of term equations.

Output: A set of term equations in solved form or report not unifiable.

Perform the following transformations on the set of equations as long as any one of them is applicable:

1. Transform $t = x$, where $t$ is not a variable, to $x = t$.
2. Erase the equation $x = x$.

3. Let $t = t'$ be an equation where $t$, $t'$ are not variables.

   • If the outermost function symbols of $t$ and $t'$ are not identical, terminate the algorithm and report not unifiable.
   • Otherwise, replace the equation $f (t_1, \dots , t_k) = f (t_1' , \dots , t_k')$ by the $k$ equations $t_1 = t_1' , \dots , t_k = t_k'$.

4. Let $x = t$ be an equation such that $x$ has another occurrence in the set.

   • If $x$ occurs in $t$ and $x$ differs from $t$, terminate the algorithm and report not unifiable.
   • Otherwise, transform the set by replacing all occurrences of $x$ in other equations by $t$.

Answer 1

You are almost done!

You have to iterate the steps of the unification algorithm until you get:

• either an equation $x = t$ such that $x$ occurs in $t$ but $x \neq t$ (step 4), and this means that you cannot unify the formulas;
• or an equation $f(t_1, \dots t_k) = g(s_1, \dots, s_n)$ with $f \neq g$ (step 3), and this means that you cannot unify the formulas (this is the meaning of step 3 that you don't understand);
• or a set of term equations in solved form, and this means that you can unify the formulas by applying the substitutions defined in these equations.

You have obtained the equations $\ z = a$, $\ x = h(z,u)$, $\ u = g(y)$ and then you have to apply the second item of step 4 for $z = \dots$ and $u = \dots$.

The following is a step-to-step description of the execution of the unification algorithm, starting from the beginning:

1. First round:
   • step 3 (second item): $\ a = z$, $\ x = h(z,u)$, $\ f(g(y)) = f(u)$
2. Second round:
   • step 1: $\ z = a$, $\ x = h(z,u)$, $\ f(g(y)) = f(u)$
   • step 3 (second item): $\ z = a$, $\ x = h(z,u)$, $\ g(y) = u$
   • step 4 (second item): $\ z = a$, $\ x = h(a,u)$, $\ g(y) = u$
3. Third round:
   • step 1: $\ z = a$, $\ x = h(a,u)$, $\ u = g(y)$
   • step 4 (second item): $\ z = a$, $\ x = h(a,g(y))$, $\ u = g(y)$

After this last step, we have obtained a set of term equations in solved form, which unify the atomic formulas $p(a, x, f(g(y)))$ and $p(z, h(z,u), f(u))$. Indeed: \begin{align} &p(a, x, f(g(y))) [z = a,\ x = h(a,g(y)), \ u = g(y)] \\= \ &p(a, h(a,g(y)), f(g(y))) \\= \ &p(z, h(z,u), f(u))[z = a, \ x = h(a,g(y)), \ u = g(y)] \end{align}