Find the MGU in the following set of expressions
$bar(1,Y,X,Y),bar(X,X,1,Z),bar(1,g(Y),1,f(W))$
Attempt
I do not know if you can work with the 3 functions at the same time. So I did for 2 functions first. So consider (1) and (2) $bar(1,Y,X,Y),bar(X,X,1,Z)$ first.
Using Algorithm 10.15 I found that MGU $\theta\ is\ \{X\leftarrow1,Y\leftarrow1,Z\leftarrow1\}$.
Then I considered (2) and (3) $bar(X,X,1,Z),bar(1,g(Y),1,f(W))$
Applying $\theta$ in (2) yields
$$1=1\\ 1=g(Y)\\ 1=1\\ 1=f(W)$$ which implies by the Algorithm $$1=g(Y)\\ 1=f(W)$$
But in this equations you cannot apply the algorithm, hence can we conclude that MGU does not exist?
Or what can be done here?
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:
- Transform $t = x$, where $t$ is not a variable, to $x = t$.
- Erase the equation $x = x$.
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'$.
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$.