🚀 go-pugleaf

I have some comments and questions on the term comparison operator @<.

The behavior of setof
---------------------

Consider the following predicate:

	a(X,X).
	a(Y,Z).
	a(W,T).
	a(a,b).

The query

	| ?- setof(a(X,Y), a(X,Y), S).

gives the result (slightly edited for readability):

	S = [a(A,B),a(C,D),a(E,E),a(a,b)]

It would be better if one of a(A,B) and a(C,D) were deleted from this result.
In order to do this, two terms such as a(X,X) and a(Y,Y) which have the
same pattern of bound variables should be considered equal.
This requires a new meaning for the equality of two terms.

Modified term comparison
------------------------

Term comparison should do a structural comparison for all terms, including
those containing variables.  It should impose an ordering between terms
that also depends on the pattern of variable binding.  Terms such as a(X,X)
and a(Y,Z) should have a place in this ordering.  To solve the setof
problem mentioned above, a structural equality predicate @== is needed,
since a(X,X)==a(Y,Y) fails, whereas they are structurally equal.
To summarize, the following comparisons succeed:

	a(X,X) @== a(Y,Y)
	a(X,Y) @== a(A,B)

Structural comparison is easy to implement.  One possibility is to instantiate
all variables in each term temporarily to unique atoms in a sequence, do a
term comparison between the resulting ground terms, and then uninstantiate the
variables.
Structural comparison can be defined as follows in Prolog:

	:- op( 700, xfx, [@@<, @==]).
	:- dynamic copy_term/1.

	A @@< B :- inst_vars(A, CA), inst_vars(B, CB), CA@<CB.

	A @== B :- inst_vars(A, CA), inst_vars(B, CB), CA==CB.

	inst_vars(A, CA) :- copy(A, CA), inst_vars(CA, 0, _).

	inst_vars(V) --> {var(V)}, !, inc(I), {gen_atom(I, V)}.
	inst_vars(A) --> {atomic(A)}, !.
	inst_vars(S) --> {S=..L}, inst_vars_list(L).

	inst_vars_list([]) --> [].
	inst_vars_list([H|T]) --> inst_vars(H), inst_vars_list(T).

	inc(I, I, I1) :- I1 is I+1.

	gen_atom(I, A) :-
		name(I, IL),
		append("$$$", IL, AL),
		name(A, AL).

	append([], L, L).
	append([X|L1], L2, [X|L3]) :- append(L1, L2, L3).

	copy(A, C) :-
		assert(copy_term(A)),
		retract(copy_term(C)).

There is a slight bug in this version: it assumes that the atom '$$$n' for any
integer will never be used elsewhere in the program.  If the algorithm is
implemented as a part of the system then this can be ensured.
Some comments about this method:
	1. The relative order of two terms is independent of the order of the
	   variables in memory.
	2. Two terms that are equal will still be equal if they are unified
	   together.
	3. Two terms that are equal can become unequal if one of them becomes
	   more instantiated.  This is never true for ==.

A logically sound term comparison
---------------------------------

To be logically sound, if the result of a term comparison cannot be determined
solely by looking at the instantiated portion of the terms then the operation
should do one of two things:
	1. It should delay until the instantiation is done elsewhere, or
	2. It should terminate with an error condition.

Peter Van Roy
vanroy@ji.Berkeley.edu