most general unifier: can a variable be substituted to a variable and a function?

407 Views Asked by At

i was wondering: when doing most general unifiers(MGU), can a variable be substituted to a variable and to a function?

examples that illustrates my question:

1)loves(girlfriend(x),x) , loves(y,y)

2)loves(girlfriend(x),x) , loves(girfriend(y), Suzzie)

?

can it be done or are they wrong both?

would appreciate your explanations regarding this tricky thing.

1

There are 1 best solutions below

4
On BEST ANSWER

I don't quite understand the question in your first paragraph, but assuming that you attempt to find an mgu for each of the sets 1) and 2):

Presupposing a stepwise algorithmic proedure where you work your way from left to right substituting differing terms until you arrive at an mgu that makes the two formulas identical:


1) is not unifiable at all.

A possible first substitution which identifies the terms $\text{girlfriend}(x)$ and $y$ is

$\sigma_1 = [y/\text{girlfriend}(x)]$

which gives you

$\{\text{love}(\text{girlfriend}(x),x), \text{love}(\text{girlfriend}(x),\text{girlfriend}(x))\}$.

At this point you see that the set is not unifiable: The next substitution step would be to identify $x$ and $\text{girlfriend}(x)$. The only variable available to undergo this substitution step is $x$, but $x$ occurs in the only other term avialable, which is $\text{girlfriend}(x)$, so any sustitution would just lead to an infinite recursion $\text{girlfriend}(\text{girlfriend}(...(x)))$, and hence there is no mgu.


2) is unifiable:

A first substitution that identifies the terms $\text{girlfriend}(x)$ and $\text{girlfriend}(y)$

is

$\sigma_1 = [x/y]$

which gives you

$\{\text{love}(\text{girlfriend}(y),y), \text{love}(\text{girlfriend}(y), \text{Suzzie})\}$

The second substitution which identifies $y$ and $\text{Suzzie}$ is

$\sigma_2 = [y/\text{Suzzie}]$

which yields the unified set

$\{\text{love}(\text{girlfriend(Suzzie)},\text{Suzzie}), \text{girlfriend(Suzzie)},\text{Suzzie})\} = \{\text{love}(\text{girlfriend(Suzzie)},\text{Suzzie})\} $

so your mgu is

$mgu = \sigma_1 \sigma_2 = [x/y][y/\text{Suzzie}] = [x/\text{Suzzie},y/\text{Suzzie}]$.