How to define (and name) the corresponding safe te

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

In this answer we present the predicate safe_term_less_than/2, a monotonic analogue to the iso-prolog built-in predicate (@<)/2 (§8.4.1, "term less than"). Its main properties are:

• Explicit traversal of recursive terms.

• Based on prolog-coroutining facilities, in particular when/2.

  • The comparison may progress gradually:

    • "freeze" whenever instantiation is not sufficient
    • "wake up" whenever the instantiation of the most significant terms change

  • The current frontline of the comparison is represented as an explicit (LIFO) stack.

  • The current state is directly passed around the residual goals.

---

The following code has been developed and tested on sicstus-prolog version 4.3.2:

safe_term_less_than(L, R) :-                    % exported predicate
   i_less_than_([L-R]).

Above definition of safe_term_less_than/2 is based on the following auxiliary predicates:

i_less_than_([L-R|LRs]) :-
   Cond = (?=(L,R) ; nonvar(L),nonvar(R)),
   when(Cond, i_lt_step_(L,R,LRs)).

i_lt_step_(L, R, LRs) :-
   (  L == R
   -> i_less_than_(LRs)
   ;  term_itype(L, L_type),
      term_itype(R, R_type),
      compare(Ord, L_type, R_type),
      ord_lt_step_(Ord, L, R, LRs)
   ).

term_itype(V, T) :-
   (  var(V)      -> throw(error(instantiation_error,_))
   ;  float(V)    -> T = t1_float(V)
   ;  integer(V)  -> T = t2_integer(V)
   ;  callable(V) -> T = t3_callable(A,F), functor(V, F, A)
   ;                 throw(error(system_error,_))
   ).

ord_lt_step_(<, _, _, _).
ord_lt_step_(=, L, R, LRs) :-
   (  compound(L)
   -> L =.. [_|Ls],
      R =.. [_|Rs],
      phrase(args_args_paired(Ls,Rs), LRs0, LRs),
      i_less_than_(LRs0)
   ;  i_less_than_(LRs)
   ).

args_args_paired([], [])         --> [].
args_args_paired([L|Ls], [R|Rs]) --> [L-R], args_args_paired(Ls, Rs).

Sample queries:

| ?- safe_term_less_than(X, 3).
prolog:trig_nondif(X,3,_A,_B),
prolog:trig_or([_B,X],_A,_A),
prolog:when(_A,(?=(X,3);nonvar(X),nonvar(3)),user:i_lt_step_(X,3,[])) ? 
yes
| ?- safe_term_less_than(X, 3), X = 4.
no
| ?- safe_term_less_than(X, 3), X = 2.
X = 2 ? ;
no
| ?- safe_term_less_than(X, a).
prolog:trig_nondif(X,a,_A,_B),
prolog:trig_or([_B,X],_A,_A),
prolog:when(_A,(?=(X,a);nonvar(X),nonvar(a)),user:i_lt_step_(X,a,[])) ? ;
no
| ?- safe_term_less_than(X, a), X = a.
no
| ?- safe_term_less_than(X+2, Y+1), X = Y.
no

In comparison to previous answers, we observe:

• The "text volume" of residual goals appears kind of "bloated".
• The query ?- safe_term_less_than(X+2, Y+1), X = Y. fails—just like it should!

Answer 2

Here is a sketch of what I believe might be a working approach. Consider the goal lt(X, Y) and term_variables(X, XVars), term_variables(Y, YVars).

The purpose of the definition is to determine whether or not a further instantiation might change the term order (7.2). So we might want to find out the responsible variables directly. Since term_variables/2 traverses a term in the very same way that is of relevance to term order, the following holds:

If there is an instantiation that changes the term order, then the variables that have to be instantiated to witness that change are in the list prefixes XCs, YCs of XVars and YVars respectively, and either

1. XCs, YCs, XVars, and YVars are identical, or

2. XCs and YCs are identical up to the last element, or

3. XCs and YCs are identical up to the end where one list has a further element, and the other list is identical to its corresponding variable list XVars or YVars.

As an interesting special case, if the first elements in XVars and YVars differ, then those are the only variables to be tested for relevance. So this includes the case where there is no common variable, but it is even more general than that.