I don&#x27;t know if I understand unification well or not; I feel like the control flow in Algorithm W is still a bit of a mystery to me, but I suspect that this is more a function of the effort I&#x27;ve put into understanding it than of the adequacy of the explanations I&#x27;ve found.  <a href="http:&#x2F;&#x2F;canonical.org&#x2F;~kragen&#x2F;sw&#x2F;dev3&#x2F;term-rewriting.scm" rel="nofollow">http:&#x2F;&#x2F;canonical.org&#x2F;~kragen&#x2F;sw&#x2F;dev3&#x2F;term-rewriting.scm</a> was the last time I implemented unification, in August, and sort of represented my understanding of unification at the time — but looking at it now, I see that it only does pattern-matching, which is really only kind of half of unification.  I think I did a more general first-order vaguely unificationy thing for queries on triple stores some years back, but the details are now fuzzy in this thing of mine that I flatter by calling it a mind.<p>So, yes!  I&#x27;d love a detailed tutorial of unification step-by-step (or perhaps recursive function by recursive function, if that turns out to be simpler).  Maybe it already exists somewhere, perhaps in a textbook, and I just haven&#x27;t found it.  Or maybe I got intimidated and need to calm down and work some exercises instead of going off to read Facebook and HN.