Most general unifier - "infinite loop" - failure?

Question

Lets say I have the following expressions where $x,y$ are both variables:

$p(x,y)$

$p(y,x)$

Is there a most general unifier in this case? since $x,y$ are both variables do I get stuck in an infinite loop while trying to run the basic MGU algorithm?

Answer 1

As suggested, transcribing my comments to an answer:

The MGU algorithm that I learned starts with the desired equation $(,)=(,)$, and first adjoins the required equations between the arguments, i.e., $=$ and $=$. Then, having the equation $=$, it removes $$ from its vocabulary, removes the equation $=$, and replaces $$ with $$ in the remaining equations. So now it has $(,)=(,)$ and $=$. Then there's some cleaning up, but you already see the MGU: convert $$ to $$ to get unified $(,)$. If you re-order the equations, you might end up converting $$ to $$ and getting $(,)$, but that's OK, since MGU's are only defined up to renaming anyway. The only way I see to get an infinite loop is to try to execute both versions of the algorithm in parallel --- converting $$ to $$ and also converting $$ to $$. Don't do that; execute the algorithm one step at a time.