🚀 go-pugleaf

In article <11740@csli.Stanford.EDU>, schuetze@csli (Hinrich Schuetze) writes:
> Does anyone know a good description of the unification
> algorithm used in prolog II? I'm interested in how
> circular structures are dealt with. 
> 
> Thanks a lot!
> 
> Hinrich

If memory serves, they keep a stack of equations during unification.
Think of them as assumptions. Whenever, they are about to unify 2
trees they first check the stack of assumptions; if the two trees have
been postulated equal, the recursive call succeeds immediately;
otherwise, they enter a new equation in the stack postulating that the
2 trees are equal, then proceed with regular unification (think of the
subsequent computation as either showing the set of assumptions to be
inconsistent, in which case it fails, or returning a unifier if it
succeeds).

It's a bit sketchy, but you get the general idea...

--Denys