Instability of standard order

Request For Comments
1

The discussion has been here before: standard order of terms is complete (except cyclic terms :frowning: ), but unstable, i.e.,

X @< a, X = b

succeeds, but a @< b rather than a @> b. I wonder whether we should have a variant of compare/3 that fixes this. I see two sensible behaviours: a compare/3 variant that raises an instantiation exception and one that tells us which comparison decides. The implementation of compare/3 at some point stumbles on a variable. That means we cannot decide (unless the other side is the same variable, e.g., X==X). We can return a pair indicating the undecidable comparison, so we get

?- compare_ex(Diff, f(a), f(X)).
Diff = compare(a, X)

The sad thing is that instantiation_error has no culprit. Else, we could also consider

?- catch(compare_ex(Diff, f(a), f(X)), E, true).
E = error(instantiation_error(compare(a,X), _).

I know we can use the second argument. That is nice for a message, but not for something you want to act upon. Of course, the disadvantage is that normal computation may need to use catch/3, something I’ve never liked.

Opinions? Existing practice?

2

I found compare/3 to be disappointingly illogical as a learner :grinning_face:

Exceptions are a last resort, for when there are no other reasonable actions… how about, for a point-in-time comparison:

compare_sound(C, X, Y) :-
    (   X \= Y
    ->  compare(S, X, Y),
        % Will be < or > sign
        C = comp(S)
    ;   X == Y
    ->  C = comp(=)
        % Insufficiently instantiated for sound comparison
    ;   C = insuf
    ).

Results:

?- compare_sound(C, A, A).
C = comp(=).

?- compare_sound(C, b(_), a(_)).
C = comp(>).

?- compare_sound(C, A, B).
C = insuf.

I think these results would be the least surprising for a learner.

3

hm, I heavily rely on being able to compare 2 variables and ground terms with variables in my egraph implementations.
In my case, the current status quo is okay I found…

4

I thought about this as well. It is not correct. consider compare(D, f(X, a), f(x, b)). These do not unify, but their comparison is unstable. The current working hypothesis is to introduce

 partial_compare(?Dif, @T1, @T2)

Which will unify Dif with one of >, =. < or undefined(X,Y), which expresses that we can not decide, but Dif is the same as compare(X,Y) when we can compare. Related, there is a proposal for

must_compare(Dif, T1, T2)

which raises an instantiation_error if the above returns undefined(,). Finally,

compare_when(Dif, T1, T2)

Which could act as a constraint, i.e., delays if we cannot decide now.