Unification Functions

Question

I need to apply the unification function to unify the following expression:

foo(X,X,Y) and foo(Z,p(Z),w)

So far, I've determined that I must substitute 'w's for occurances of 'Y', making

foo(X,X,w) and foo(Z,p(Z),w)

Then, I can saw X/Z (replaces 'Z' with 'X'), making:

foo(X,X,w) and foo(X,p(X),w)

Now all that's left is making p(X) equivalent to X

My question here is, is it allowed to replace this P(X) with X using the substitution X/p(X)? Or am I going about the question in the wrong pattern?

Thank you!

Answer 1

Rather than thinking about this in terms of substitutions, you might find it useful to think about this in terms of equalities that you can infer.

In the first step, you inferred that $w=Y$.

In the second step, you inferred that $X=p(Z)$.

In the third step, you inferred that $X=Z$.

It follows that you can infer $Z=p(Z)$. So we know $X=Z=p(Z)$ and $w=Y$.

Of course, if you can infer that two things are equal, you can substitute one for the other. But maybe it's easier to think about unification as being a way to keep track of which things are equal (which in turn helps you know which substitutions you can make). Hope this helps make this kind of situation feel more intuitive.