🚀 go-pugleaf

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