Path: utzoo!attcan!uunet!munnari!mulga!wcc!latcs1!ditmela!murtoa.cs.mu.oz.au!munnari.oz!lee
From: lee@munnari.oz (Lee Naish)
Newsgroups: comp.lang.prolog
Subject: Re: Determining order of argument unification
Message-ID: <1028@murtoa.cs.mu.oz.au>
Date: 7 Nov 88 00:35:07 GMT
References: <8192@burdvax.PRC.Unisys.COM>
Sender: news@cs.mu.oz.au
Reply-To: lee@munmurra.UUCP (Lee Naish)
Organization: University of Melbourne, Comp Sci Dept
Lines: 44

With right to left unification the following fails.  With left to
right unification without the occurs check creates two infinite terms
then tries to unify them, which will (probably) loop.

?- p(C-C, A-A, A, a).

p(D-f(D), B-f(B), D, b).


It seems that most systems use left to right ordering but POPLOG uses
right to left (thanks Chris Moss, who ran lots of examples on lots of
systems).  My guess is that POPLOG pushes unifications onto a stack at
some point.  Richard is right in saying that you can never tell for
sure of course.  I also disagree with the original assertion that the
only two reasonable orders are L to R and R to L.  See the paper by
Janssens Demoen and Marien in the latest ICLP/SLP on optimizing
register allocation.

There are also some other subtle differences in the way cyclic terms
are handled by the various implementations (not to mention the
unsubtle differences of systems which handle infinite terms properly).
The following example will loop in some but not all L to R
implementations:

?- p(A-A, A, a).

p(f(B)-B, B, b).

The difference between this and the example above is that only one
cyclic term is created and it is unified with itself.  Many unification
procedures first check if the addresses of the two terms are the same
and succeed if that is the case.

Another difference is whether the infinite loops are interruptable and
whether they consume memory (due to recursion in unification).
Running out of space in the unification stack causes user-unfriendly
behaviour in many systems.  It occurs less often if the unification
procedure is tail recursive, so it doesn't consume memory if an
infinite (sub)term is always in the "last" argument of a term (last
with respect to the unification order of course).  Assuming the
system uses tail recursion, this is another way to find out the
unification order!

	lee