How to define (and name) the corresponding safe term comparison predicates in ISO Prolog?

Question

Standard term order (ISO/IEC 13211-1 7.2 Term order) is defined over all terms — including variables. While there are good uses for this — think of the implementation of setof/3, this makes many otherwise clean and logical uses of the built-ins in 8.4 Term comparison a declarative nightmare with imps (short form for imperative constructs) all around. 8.4 Term comparison features:

8.4 Term comparison

8.4.1 (@=<)/2, (==)/2, (\==)/2, (@<)/2, (@>)/2, (@>=)/2.
8.4.2 compare/3.
8.4.3 sort/2.
8.4.4 keysort/2.

To give an example, consider:

?- X @< a. true. 

This succeeds, because

7.2 Term order

An ordering term_precedes (3.181) defines whether or
not a term X term-precedes a term Y.

If X and Y are identical terms then X term_precedes Y
and Y term_precedes X are both false.

If X and Y have different types: X term_precedes Y iff the
type of X precedes the type of Y in the following order:
variable precedes floating point precedes integer
precedes atom precedes compound.

NOTE — Built-in predicates which test the ordering of terms
are defined in 8.4.
...

And thus all variables are smaller than a. But once X is instantiated:

?- X @< a, X = a. X = a. 

the result becomes invalid.

So that is the problem. To overcome this, one might either use constraints, or stick to core behavior only and therefore produce an instantiation_error.

7.12.2 Error classification

Errors are classified according to the form of Error_term:

a) There shall be an Instantiation Error when an
argument or one of its components is a variable, and an
instantiated argument or component is required. It has
the form instantiation_error.

In this manner we know for sure that a result is well defined as long as no instantiation error occurs.

For (\==)/2, there is already either dif/2 which uses constraints or iso_dif/2 which produces a clean instantiation error.

iso_dif(X, Y) :-    X \== Y,    ( X \= Y -> true    ; throw(error(instantiation_error,iso_dif/2))    ). 

So what my question is about: How to define (and name) the corresponding safe term comparison predicates in ISO Prolog? Ideally, without any explicit term traversal. Maybe to clarify: Above iso_dif/2 does not use any explicit term traversal. Both (\==)/2 and (\=)/2 traverse the term internally, but the overheads for this are extremely low compared to explicit traversal with (=..)/2 or functor/3, arg/3.

Answer 1

iso_dif/2 is much simpler to implement than a comparison:

• The built-in \= operator is available
• You now exactly what arguments to provide to\=

Definition

Based on your comments, the safe comparison means that the order won't change if variables in both subterms are instanciated. If we name the comparison lt, we have for example:

• lt(a(X), b(Y)) : always holds for all any X and Y, because a @< b
• lt(a(X), a(Y)) : we don't know for sure: intanciation_error
• lt(a(X), a(X)) : always fails, because X @< X fails

As said in the comments, you want to throw an error if, when doing a side-by-side traversing of both terms, the first (potentially) discriminating pair of terms contains:

• two non-identical variables (lt(X,Y))
• a variable and a non-variable (lt(X,a), or lt(10,Y))

But first, let's review the possible approaches that you don't want to use:

• Define an explicit term-traversal comparison function. I known you'd prefer not to, for performance reason, but still, this is the most straightforward approach. I'd recommend to do it anyway, so that you have a reference implementation to compare against other approaches.

• Use constraints to have a delayed comparison: I don't know how to do it using ISO Prolog, but with e.g. ECLiPSe, I would suspend the actual comparison over the set of uninstanciated variables (using term_variables/2), until there is no more variables. Previously, I also suggested using the coroutine/0 predicate, but I overlooked the fact that it does not influence the @< operator (only <).

  This approach does not address exactly the same issue as you describe, but it is very close. One advantage is that it does not throw an exception if the eventual values given to variables satisfy the comparison, whereas lt throws one when it doesn't know in advance.

Explicit term traversal (reference implementation)

Here is an implementation of the explicit term traversal approach for lt, the safe version of @<. Please review it to check if this is what you expect. I might have missed some cases. I am not sure if this is conform to ISO Prolog, but that can be fixed too, if you want.

lt(X,Y) :- X == Y,!,     fail.  lt(X,Y) :- (var(X);var(Y)),!,     throw(error(instanciation_error)).  lt(X,Y) :- atomic(X),atomic(Y),!,     X @< Y.  lt([XH|XT],[YH|YT]) :- !,     (XH == YH ->          lt(XT,YT)      ;   lt(XH,YH)).  lt(X,Y) :-     functor(X,_,XA),     functor(Y,_,YA),     (XA == YA ->        X =.. XL,        Y =.. YL,        lt(XL,YL)     ;  XA < YA). 

(Edit: taking into account Tudor Berariu's remarks: (i) missing var/var error case, (ii) order by arity first; moreover, fixing (i) allows me to remove subsumes_term for lists. Thanks.)

Implicit term traversal (not working)

Here is my attempt to achieve the same effect without destructuring terms.

every([],_). every([X|L],X) :-     every(L,X).  lt(X,Y) :-     copy_term(X,X2),     copy_term(Y,Y2),     term_variables(X2,VX),     term_variables(Y2,VY),     every(VX,1),     every(VY,0),     (X @< Y ->          (X2 @< Y2 ->               true           ;   throw(error(instanciation_error)))      ;   (X2 @< Y2 ->               throw(error(instanciation_error))           ;   false)). 

Rationale

Suppose that X @< Y succeeds. We want to check that the relation does not depend on some uninitialized variables. So, I produce respective copies X2 and Y2 of X and Y, where all variables are instanciated:

• In X2, variables are unified with 1.
• In Y2, variables are unified with 0.

So, if the relation X2 @< Y2 still holds, we know that we don't rely on the standard term ordering between variables. Otherwise, we throw an exception, because it means that a 1 @< 0 relation, that previously was not occuring, made the relation fail.

Shortcomings

(based on OP's comments)

• lt(X+a,X+b) should succeed but produce an error.

  At first sight, one may think that unifying variables that occur in both terms with the same value, say val, may fix the situation. However, there might be other occurences of X in the compared terms where this lead to an errorneous judgment.

• lt(X,3) should produce an error but succeeds.

  In order to fix that case, one should unify X with something that is greater than 3. In the general case, X should take a value that is greater than other any possible term¹. Practical limitations aside, the @< relation has no maximum: compound terms are greater than non-compound ones, and by definition, compound terms can be made arbitrarly great.

So, that approach is not conclusive and I don't think it can be corrected easily.

---

1: Note that for any given term, however, we could find the locally maximal and minimal terms, which would be sufficient for the purpose of the question.