Counterexample to most general unifier example

Question

I am reading these slides about unifiers and most general unifiers (MGUs): https://artint.info/2e/slides/ch13/lect3.pdf

In particular, an MGU is defined as follows. A substitution $\sigma$ is an MGU of $e_1$ and $e_2$ if

• $\sigma$ is a unifier of $e_1$ and $e_2$ and
• If a substitution $\sigma'$ also unifies $e_1$ and $e_2$, then $e\sigma'$ is an instance of $e\sigma$ for all atoms $e$.

Let $e_1 = p(A, b, C, D)$ and $e_2 = p(X, Y, Z, e)$.

In the slides it is stated that $\sigma_7 = \{ A/V, X/V, Y/b, C/W, Z/W, D/e \}$ is an MGU of $e_1$ and $e_2$, but I cannot understand why the following counterexample to this statement does not work:

• Let $\sigma' = \{ X/A, Y/b, Z/C, D/e, V/f \}$, which also unfies $e_1$ and $e_2$
• Let $e = q(V, X)$, which is such that $e\sigma' = q(f, A)$ and $e\sigma_7 = q(V, V)$, but $q(f, A)$ is not an instance of $q(V, V)$, since there is no substitution $\sigma''$ such that $q(f, A) = q(V, V)\sigma''$.

I feel like I'm missing something obvious. Thank you for any answer.

Answer 1

You’re right that under the given definition this is not a most general unifier.

Here’s a quote from Term Rewriting and All That by Franz Baader and Tobias Nipkow (pp. $71$–$72$):

A substitution $\sigma$ is more general than a substitution $\sigma'$ if there is a substitution $\delta$ such that $\sigma'=\delta\sigma$. [...] We also say that $\sigma'$ is an instance of $\sigma$.

[...]

$\sigma':=\{x\mapsto z,y\mapsto z\}$ is a unifier of $x=^?y$, but not an mgu: $\sigma=\{x\mapsto y\}$ is not an instance of $\sigma'$ because $\{z\mapsto y\}\sigma'$ is $\{x\mapsto y,z\mapsto y\}$ but not $\sigma$. There are more complex definitions of mgu (see Chapter $10$) that take into account that $\sigma$ and $\{z\mapsto y\}\sigma'$ only differ on variables $(z)$ not present in the unification problem. For the time being we prefer the simpler definition.

This is precisely your scenario: $\sigma_7$ fails to be a most general unifier only because it introduces variables $V$ and $W$ that don’t occur in the unification problem. Perhaps the authors of the slides had one of the “more complex definitions” in mind in writing that example. Note that the algorithm they give on p. $12$ for finding a most general unifier never introduces new variables; in your example it would return the most general unifier $\sigma_4=\{A/X,Y/b,C/Z,D/E\}$.