vanroy@ji.Berkeley.EDU (Peter Van Roy) (09/08/88)
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.edulee@mulga.oz (Lee Naish) (09/09/88)
In article <25985@ucbvax.BERKELEY.EDU> vanroy@ji.Berkeley.EDU (Peter Van Roy) writes: >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. > :- op( 700, xfx, [@@<, @==]). > <code> I think the sentiments expressed are reasonable, but there are some improvements which could be made. Firstly, the @< term ordering should be preserved as much as possible (Vars @< ints @< atoms etc). In the implementation presented: X @@< a succeeds X @@< ' ' fails X @@< 1 fails The problem it that vars are turned into atoms before comparison (it could be fixed in the implementation by wrapping a functor around nonvars in the terms - this also fixes the bug mentioned previously). Secondly, I think the subsumption (partial) ordering should be preserved as much as possible also. With @<, if terms dont contain repeated vars, A sumbsumes (is more general than) B implies A @< B. Unfortunately, with the implementation of @@< given, f(X, X) @@< f(Y, Z). It could be changed by using a decreasing sequence of atoms instead of an increasing sequence. I think a reasonable specification of this kind of term comparison would (almost) be: new_compare(Result, A, B) :- if A subsumes B, B subsumes A then Result = (=) else if A subsumes B then Result = (<) else if B subsumes A then Result = (>) else compare(Result, A, B). The reason why its not quite what we want is that new_compare(R, f(A+A, 1), f(C+D, 2)) may return R = (<) but new_compare(R, A+A, C+D) must return R = (>). The reason is that because the second arguments dont unify, compare is used for everything, rather than subsumption. A proper specification/ implementation is much more complex, but I hope you get the idea. Thirdly (a minor efficiency gripe), this is a perfect example of where not to use =.. (and where to use functor and arg). >To be logically sound,... > 1. It should delay until the instantiation is done elsewhere, or This is what NU-Prolog termCompare/3 does. As was pointed out in "Negation and quantifiers in NU-Prolog", a sound inequality predicate which returns a result is useful for implementing logical termCompare: termCompare(Result, A, B) :- is_equal(A, B, R), % delays until A,B sufficiently % instantiated (if R = true then % delays until R instantiated Result = (=) else compare(Result, A, B) ). Sound inequality is used in MU-Prolog to implement == also (using an awful hack): A == B :- \+ A ~= B. % ~= fails iff A == B The "funny quantifiers" of NU-Prolog can be used in an even more horrible hack to implement subsumption efficiently: % gAll A A ~= B fails if and only if A and B can be unified % without binding any variables in B (otherwise it may succeed % or delay - we don't care which since its inside \+ anyway) subsumes(A, B) :- \+ (gAll A A ~= B). lee
ok@quintus.uucp (Richard A. O'Keefe) (09/10/88)
In article <25985@ucbvax.BERKELEY.EDU> vanroy@ji.Berkeley.EDU (Peter Van Roy) writes: >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. [Shouldn't that be "same pattern of UNbound variables"?] The basic problem here is not really a problem with term comparison. There are two ways of looking at these variables (A,B,C,D,E). (1) Since the variables are really "copies" of the original X,Y, we should have delayed until X and Y were sufficiently instantiated to ensure that duplicate elimination never had to compare a variable with a variable. In this view, the mistake is returning any answer at all: if we were to say | ?- all_solutions(a(X,Y), a(X,Y), S), X=foo, Y=baz. the answer should be S=[a(foo,baz)]. (2) The other view is that the variables which came back are METAVARIABLES, and the list S is really at the meta-level: is_a_solution(X) <-> (exists E) member(E, S) & instance_of(X, E) In this view, the set S *really* means [a($1,$1),a($1,$2),a(a,b)] But note that in order to reduce redundancy, we should not just drop an element E when it is *equivalent to* another element of S, but we should also drop E if it is *subsumed by* another element of S. That is to say, a($1,$1) should ALSO be dropped, and a non-redundant result is [a($1,$2),a(a,b)]. Note that in neither case do we have any reason to retain a(E,E). Since a(p,p) is an instance of both a($1,$1) and a($1,$2), it is implicitly present *twice* in [a(A,B),a(E,E),a(a,b)]. If we are willing to tolerate that, we have lost our excuse for demanding that a(C,D) be deleted. Van Roy's proposal (which I heard a couple of days before from Herve' Touati) is simply to compare terms by comparing "standardised" alphabetic variants of them. >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. Note that you have to standardise the terms *separately*, because they might share variables. {Instead of van Roy's "inst_vars/2", you would do well to use number_vars/3, which binds variables to '$VAR'(Int) terms.} Note that the desired effect can be obtained for the special case of setof/3 by doing touati_setof(Template, Generator, Set) :- quantify_and_number(Generator, Template, Goal), bagof(Template, Goal, Bag), sort(Bag, Temp), varnumbers_list(Temp, Set). quantify_and_number(Q^Generator, Template, Q^Goal) :- !, quantify_and_number(Generator, Template, Goal). quantify_and_number(Goal, Template, N^(Goal,numbervars(Template,0,N))). varnumbers_list([], []). varnumbers_list([T|Ts], [S|Ss]) :- varnumbers(T, S), varnumbers_list(Ts, Ss). where varnumbers/2 is an inverse of numbervars(_, 0, _). The query | ?- touati_setof(a(X,Y), a(X,Y), S). gave S = [a(a,b),a(A,A),a(B,C)] as the answer, with X and Y still unbound. >Some comments about this method: > 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 ==. Note that unifying two terms which are alphabetic variants of each other can change the relative order of two OTHER terms. Part of sort/2 looks like this: sort(2, [X,Y|Rest], Answer, Rest) :- !, compare(R, X, Y), sort2(R, X, Y, Answer). sort2(<, X, Y, [X,Y]). sort2(>, X, Y, [Y,X]). sort2(=, X, X, [X]). <----- The last clause may indifferently be written sort2(=, X, X, [X]), sort(=, X, _, [X]), or sort(=, _, X, [X]), because with the standard ordering, unifying two identical terms has no effect. With the "alphabetic variant" ordering, unifying term equivalent terms may change the relative order of OTHER terms, so it MUST NOT be done by sort/2. So one of the other alternative versions of the last clause must be used. But there are two choices, and they yield distinguishable results. Note also that maintaining two binding environments during term comparison (should there be any variables which have to be compared) is intrinsically more costly than maintaining none.