Is the following a unifier, but not a most general unifier?

894 Views Asked by At

So I have the following pair of terms $p(q(A),r(A))$ and $p(q(A),r(B))$

I understand the most general unifier for this would be $B/A$. i.e. replace $B$ with $A$.

But I am also aware that there is not necessarily only one most general unifier, and that there also exist unifiers with are not the most general unifier.

Am I right in thinking $A/B$ is a unifier but not a most general unifier? So we end up with $p(q(A),r(B))$ as there is no indication that $A = B$?

1

There are 1 best solutions below

0
On

A less general unifier here would consist of a substitutition for both A and B with some term which is not a literal, such as $f(X, Y)$. Such a unifier upon substitution would yield the less general formula: $$ p(q(f(X, Y)), r(f(X, Y))) $$

It qualifies as less general than say $p(q(A), r(A))$, since you can obtain it from $p(q(A), r(A))$ by substitution alone, and you can't obtain $p(q(A), r(A))$ from $p(q(f(X, Y)), r(f(X, Y)))$.

You could replace A with B and also obtain another most general unifier. The unifier $A/B$ yields: $$ p(q(B), r(B)) $$ from which we can obtain $p(q(A),r(A))$ by substitution alone and conversely we can obtain $p(q(A), r(A))$ from $p(q(B), r(B))$ by substitution alone. Thus, the unifiers $A/B$ and $B/A$ for $p(q(A),r(A))$ and $p(q(A),r(B))$ both yield a most general formulas and both qualify as a most general unifiers.

In other words, a substitution qualifies as a most general unifier if upon substitution we obtain a most general common formula. All other common forms of the two terms can get derived from any most general formula by substitution alone. Thus, if two unifiers yield two formulas each of which can get derived from the other by substitution alone, both of those unifiers qualify as most general unifiers.

Another way to see if two unifiers qualify as most general unifier involves replacing all variables in the formulas obtainable from the unifiers uniformly with ordinal numbers according to where they appear in the formula. If upon such ordinal substitution both formulas match each other, and one of them got obtained via a most general unifier, then both qualify as most general unifiers.

For instance, if we have $c(A, B)$ and $c(c(c(X, Y), Z), c(Y, Z))$ and use the substitution $A / c(c(X, Y), Z), B / c(Y, Z)$ we obtain $$ \qquad c(c(c(X, Y), Z), c(Y, Z)) \tag{1} $$

if we used the substitution $X / C$, $Y / B$, $Z / A$, $A / c(c(C, B), A)$, $B / c(B, A)$ we obtain $$ c(c(c(C, B), A), c(B, A))\tag{2} $$

Now in 1. $X$ is the first variable, $Y$ the second variable and $Z$ the third variable. Thus, upon ordinal substitution we obtain $$ c(c(c(1, 2), 3), c(2, 3)) $$ In 2. $C$ is the first variable, $Y$ the second variable, and $Z$ the third variable, so upon ordinal substitution in 2. we obtain $$ c(c(c(1, 2), 3), c(2, 3)) $$ So, both unifiers qualify as equivalent. And since one of them consists of a most general unifier, both qualify as most general unifiers.