I'm trying to trace the algorithm for getting the most general unifier, and I'm a bit confused. Can there be more than one solution? (although the adjective 'most' suggests otherwise) found online: https://courses.cs.washington.edu/courses/cse415/02sp/slides.0/Unification/sld009.htm
This is the solution provided:
$L1 = P(a, f(x,a))$
$L2 = P(a,f(g(y),y)$
$S: \{\}$
$S: \{g(y)/x\}$
$S: \{g(a)/x, a/y\}$
I'll use v and t as cursors so its easier to follow.
Step 1: the cursors are in a, in L1 and L2. Since theyre are equal we move to the next term. $$ t = a, v = a$$
Step 2: both cursors in both literals are in a function symbol so we move to the next one in which the cursor t is in the variable x and the cursor v is in another function symbol. We add $v/t$ which is $g(y)/x$ $$S:\{g(y)/x\}$$
Step 3: now this is where I start to get confused, we move the cursor t to a. But should we move the cursor v to the y inside g(..) or the final y? I assumed that we should move it to the y closest to the current position of the cursor v.
another thing that confuses me is should I try adding both y/a and a/y in my solution set? Why couldn't be the final solution set be S: {g(y)/x, y/a}
btw, another factor why I got confused probably because I have no idea what elementary substitution is, and how its different from regular substition. (They used the word elementary substitution in the algorithm)
The substitution that results from the MGU algorithm is unique apart from the choice of variable names in the term that results after you apply it to the terms being unified.
The author is using "elementary substitution" to mean substitution for a single variable according to an earlier slide in the set of slides your link points to.
The description of the algorithm you are looking at is deficient in not saying where to move the cursor next in the case when you add a term-variable pair to the substitution. It should say that you skip past the term rather than move the cursor inside it. (You will look inside the term while you are making the occurs check.)
In the example given, I expect $a$ is intended to be a constant. In any case, the description of the algorithm doesn't make it clear that in the variable-variable case, you have to make an arbitrary choice of how to extend the substitution.
I think you will be able to find clearer descriptions of the unification algorithm. The one in http://en.wikipedia.org/wiki/Unification_(computer_science) is pretty good, but is rather different in style from the one you are looking at.