Unification algorithm with examples

Unification is essentially a process of substitution. I have seen it called "two-way matching". In Prolog, in other logic programming languages and in languages directly based on rewriting logic (Maude, Elan, etc...) is the mechanism by which free (logical) variables are bind to terms/values. In Concurrent Prolog these variables are interpreted as communication channels. IMO, the better way to understand it is with some examples from mathematics (unification was/is a base key mechanism, for example, in the context of automated theorem provers research, a sub-field of AI; another use in in type inference algorithms). The examples that follow are taken from the context of computer algebra systems (CAS): First example: given a set Q and two binary operations * and + on it, then * is left-distributive over + if: X * (Y + Z)   =   (X * Y) + (X * Z)   |1| this is a rewrite rule (a set of rewrite rules is a rewriting system). If we want to apply this rewrite rule to a specific case, say: a * (1 + b)   |2| we unify (via a unification algorithm) this term, |2|, with the left-hand side (lhs) of |1| and we have this (trivial on purpose) substitution (the most general unifier, mgu): {X/a, Y/1, Z/b}   |3| Now, applying |3| to the right-hand side (rhs) of |1|, we have, finally: (a * 1) + (a * b) This was simple and to appreciate what unification can do I will show a little more complex example. Second example: Given this rewrite rule: log(X,Y) + log(X,Z)   =>   log(X,Y*Z)   |4| we apply it to this equation: log(e,(x+1)) + log(e,(x-1)) = k   |5| (lhs of |5| unify to lhs of |4|), so we have this mgu: {X/e, Y/(x+1), Z/(x-1)}   |6| Note that X and x are two different variables. Here we have two variables, X and Y, which match two compound terms, (x+1) and (x-1), not simple values or variables. We apply this mgu, |6|, to rhs of |4| then and we put back this in |5|; so we have: log(e,(x+1)*(x-1)) = k   |7| and so on.