Path: utzoo!utgpu!news-server.csri.toronto.edu!mailrus!ames!rex!samsung!uunet!brunix!mj
From: mj@cs.brown.edu (Mark Johnson)
Newsgroups: comp.lang.prolog
Subject: Re: Does It Unify?
Message-ID: <41083@brunix.UUCP>
Date: 28 May 90 16:03:15 GMT
References: <1990May7.132305.15989@agate.berkeley.edu> <189@qt.cs.utexas.edu> <24861@pasteur.Berkeley.EDU> <191@qt.cs.utexas.edu> <10809@alice.UUCP> <194@qt.cs.utexas.edu> <40089@brunix.UUCP> <10838@alice.UUCP>
Sender: news@brunix.UUCP
Reply-To: mj@cs.brown.edu (Mark Johnson)
Distribution: usa
Organization: Brown University Department of Computer Science
Lines: 29


pereira@alice.UUCP (Fernando Pereira) writes:
> mj@cs.brown.edu (Mark Johnson) writes:
> >It is computationally cheaper to implement safe unification
> >than to implement the occurs check.
> 
> Unfortunately, the real problem is constant factors; every rational term
> unification algorithm I know requires far more (and more complex) trailing
> of side-effects to terms than the usual Prolog unification. No free lunch...

True enough.  But not having a safe unification can lead to some nasty bugs.
In e.g. C-Prolog, see what happens with the following query:

	X = f(X,X), Y = f(Y,Y), X = Y, fail.

Most debuggers I know of can't identify this sort of bug; they just
drop dead on you.

I also wonder how much more trailing rational term unification
requires.  After all, half of the nodes of a binary tree are leaf
nodes.  Also, as I understand it, rational term unification makes 
unified structures eq, so it should help reduce heap size.  

Finally, to obtain a safe unification algorithm it's only necessary to 
redirect (and hence trail) one term node in every cycle, so term nodes
that the compiler can identify as part of an acyclic term don't need
to be trailed at all.

Mark Johnson.