What is a unifier?

Currently I read up on unifiers, however have some problem understanding its concept. Thus far I found an example of an equation:

add(suc(x); y) $\stackrel{.}{=}$ add(y; suc(z))

and unifiers to it:

$\omicron$ = [suc(x)/y; x/z],

$\omicron'$ = [suc(suc(z))/y; suc(z)/z; suc(z)/x] and

$\omicron'$ = $\omicron$[suc(z)=x]

However I do not understand how one generally derives these unifiers from the equation above. Any construcive comment/answer would be appreciated.

A unifier of a set of terms is just any substitution that, when applied to each of the terms, makes them all equal. There's also the concept of a "most general unifier" (MGU), which is a unifier $\sigma$ of the terms such that any other unifier can be written as $\sigma\circ\tau$ for some substitution $\tau$: in other words any other unifier can be written as "first do an MGU and then do some more substitutions, which were kinda unnecessary because you'd already made the terms equal."
• $[a/b]$ means "replace every instance of $a$ with $b$". Whether or not commutativity of addition and so on are taken into account depends on whether you're looking for a syntactic unifier (one that makes the strings literally the same, without trying to assign any meaning to them) or a semantic unifier (one that makes the strings evaluate to the same thing). Nov 6 '16 at 15:23
• @DavidRicherby You meant "replace every instance of $b$ with $a$". Nov 7 '16 at 5:08
• @DerekElkins Sorry, you're right. I hate that notation. The way to remember which way it goes is that, just like fractions, $b[a/b]=a$, but that didn't help me. Nov 7 '16 at 8:17
• Agreed. I usually use the less common $[b \mapsto a]$, so the original example would be $[y \mapsto \text{suc}(x), z \mapsto x]$. It's less compact, but I feel (I haven't verified this in any way) that it is more self-explanatory. It's certainly less amenable to mixing things up. I actually hadn't made the connection to fractions. Mentally, I usually keep track by visualizing $[a/b]$ as $a/$ looming over $b$ like a wave about to crash. 'still easy to flip things around though. Nov 7 '16 at 10:45