From ok@atlas.otago.ac.nz  Mon Aug 21 01:49:43 2000
Received: from atlas.otago.ac.nz (atlas.otago.ac.nz [139.80.32.250])
	by swi.psy.uva.nl (8.9.3/8.9.3) with ESMTP id BAA19854
	for <prolog@swi.psy.uva.nl>; Mon, 21 Aug 2000 01:49:42 +0200 (MET DST)
Received: (from ok@localhost)
	by atlas.otago.ac.nz (8.9.3/8.9.3) id LAA21776;
	Mon, 21 Aug 2000 11:49:48 +1200 (NZST)
Date: Mon, 21 Aug 2000 11:49:48 +1200 (NZST)
From: "Richard A. O'Keefe" <ok@atlas.otago.ac.nz>
Message-Id: <200008202349.LAA21776@atlas.otago.ac.nz>
To: p.singleton@keele.ac.uk, prolog@swi.psy.uva.nl
Subject: Re: representing terms canonically

Paul Singleton wrote:

	I note (empirically) that ==/2 succeeds when comparing a cyclic term with
	itself, which is half of what I need, but (understandably) it doesn't
	terminate when comparing some cyclic terms which don't "match up", e.g.
	
	  T1 = f(f(T1)),
	  T2 = f(T1),
	  T1 == T2.
	
	T1 and T2, although identical, can never be found to be identical by ==/2,
	as their f/2 nodes are forever out-of-step.
	
Surely that's a bug?  When I tried
	?- T1 = f(f(T1)), T2 = f(T2), T1 == T2, write(yes), !, fail.
at the top level loop of SWI 3.3.8, it didn't fail to terminate, it did
	Segmentation Fault (core dumped)
instead.

If you do
	T1 = f(f(T1)), T2 = f(T2), T1 = T2
ISO Prolog is supposed to require that to succeed, and one way to
implement (==)/2 is as (=)/2 with the ability to bind variables taken away.
Instead it never came back with any kind of answer.

	What I think I need, is a (distinctly non-logical :-) term comparison which
	immediately (without any recursive searching) reports whether two terms are
	the same actual compound "cell" (or whatever Prolog implementors call it).
	
No, what you need is versions of (=)/2 and (==)/2 that work the way they
did in SICStus Prolog back in the early 80s.  I was once told that the
method went something like this:

    start by assuming that the two terms you're comparing *are* equal
    until you get evidence against it.  variable/non-variable is such
    evidence, differing functors is evidence.  If two terms aren't
    obviously different, *temporarily* bend one of them to point to
    the other.  When you eventually make your mind up either way,
    restore the original values of the bent cells.

Let's see how that would work for this example.

	 +-------+
    A1:	 |  f/1  |		
    A1+1:|A2|cmpd|
	 +-------+
    A2:  |  f/1  |		+--------+
    A2+1:|A1|cmpd|<-------------^A2+1|bnd| : T1
         +-------+		+--------+
    A3:  |  f/1  |		+--------+
    A3+1:|A3|cmpd|<-------------^A3+1|bnd| : T2
	 +-------+		+--------+

    Compare T1 == T2
	W1 := T1
	deref(W1) % W1 := [A1|cmpd]
	W2 := T2
	deref(W2) % W2 := [A3|cmpd]
	tag(W1) == tag(W2) && functor(W1-cmpd) == functor(W2-cmpd)
	    W1 := arg(W1,1) % = [A1|cmpd]
	    W2 := arg(W2,1) % = [A3|cmpd]
	    arg(old W2,1) := W1 % A3[1] := [A1|cmpd]

	    deref(W1) % W1 = [A2|cmpd]
	    deref(W2) % W2 = [A1|cmpd]
	    tag(W1) == tag(W2) && functor(W1-cmpd) == functor(W2-cmpd)
	        W1 := arg(W1,1) % = [A1|cmpd]
	        W2 := arg(W2,1) % = [A2|cmpd]
		arg(old W2,1) := W1 % A1[1] := [A2|cmpd]

		deref(W1) % W1 := [A1|cmpd]
		deref(W2) % W2 := [A2|cmpd]
		tag(W1) == tag(W2) && functor(W1-cmpd) == functor(W2-cmpd)
		    arg(W1,1) = [A2|cmpd]
		    arg(W2,1) = [A2|cmpd]
		    identical, so no more to do

At the end of this, three cells have been smashed and are on the trail.
The interesting thing is, if the terms _were_ identical, the changes
that have been made have only made loops shorter, they haven't introduced
any equalities they shouldn't have, so with a certain about of care in
choosing which cells to bind to what, you don't need to undo anything
on success (but you can if you want to) just like shortening variable
reference chains.  On failure, you do have to restore things, so you
had to push (which word, what old contents) pairs on the trail.


This is something that really belongs in the Prolog implementation
so that we can be sure of = and == always terminating.

(Obviously, you can pull the same trick in compare/3 and its relatives,
ensuring that _they_ terminate too.  It would be nice to be able to trust
them.  It would be even better to have a logic programming language like
Mercury that does the occurs check at compile time so we don't have to
worry about this nonsense.)

