Path: utzoo!utgpu!jarvis.csri.toronto.edu!clyde.concordia.ca!uunet!cs.utexas.edu!yale!cs.yale.edu
From: Duchier-Denys@cs.yale.edu (Denys Duchier)
Newsgroups: comp.lang.prolog
Subject: Re: unification in Prolog II
Message-ID: <11752@cs.yale.edu>
Date: 16 Jan 90 21:41:03 GMT
References: <11740@csli.Stanford.EDU>
Sender: news@cs.yale.edu
Reply-To: Duchier-Denys@cs.yale.edu (Denys Duchier)
Organization: Computer Science, Yale University, New Haven, CT 06520-2158
Lines: 22
In-reply-to: schuetze@csli.Stanford.EDU (Hinrich Schuetze)

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