Fixing the compare/3 mirror anomaly in SWI-Prolog?

General
1

I was too optimistic about the native compare/3. It has also the
mirror anomaly. I find very quickly a violation of the mirror law:

/* SWI-Prolog 9.1.7 */
?- repeat, random_cyclic(A), random_cyclic(B), 
compare(X,A,B), X = (<), \+ (compare(Y,B,A), Y = (>)).
A = s(A, A),
B = s(_S1, 1), % where
    _S1 = s(_S1, s(1, _S1)),
X = (<) .

Its indeed a violation of this law:

It can be reproduced on the top-level:

/* SWI-Prolog 9.1.7 */
?- A = s(A, A),
B = s(_S1, 1), % where
_S1 = s(_S1, s(1, _S1)), compare(X,A,B), compare(Y,B,A).
%%% answer
X = Y, Y = (<).

This could explain why the native compare/3 has transitivity violations?
But where does the SWI-Prolog implementation make a decision,
which violates the mirror law?

Edit 05.04.2023
Interestingly Scryer-Prolog doesn’t have the mirror anomaly. I neverthless
found somewhere a transitivity violation, but the mirror anomaly seems not
to be there. So there is no guarantee if the mirror anomaly is fixed, that

the native compare/3 works correctly. But for the mirror anomaly here the
same in Scryer Prolog, it doesn’t yield anything:

/* Scryer-Prolog 0.9.1-218 */
?- repeat, random_cyclic(A), random_cyclic(B),
compare(X,A,B), X = (<), \+ (compare(Y,B,A), Y = (>)).
%%% runs and runs and runs

Was using the below fuzzer version. This fuzzer only generates ground
cyclic terms. So the mirror law is violated by two ground terms. Couldn’t
find a violation yet in Scryer-Prolog though.

fuzzer_20230405.p.log (1,7 KB)

3

Assuming mirror anomaly means anti_symmetricity,
IMO, transitivity is not problem because in general, binary relation becomes transitive by taking
simply transitive closure. The origin of problem seems mirror anomaly, which requires
detecting closed paths of comparing. Using your random-cyclic and generating
anomaly triples of terms which violates transitivity I often observed something long closed paths, which discouraged me to find new compare/3 to sort list of cyclic terms. I feel I am getting
into negative to apply compare on rational trees.

I am not familiar with the state of art of comparing rational terms in other languages.

EDIT.

For the first time for me, I have tried a little bit to generate a universe of rational trees without mirror anomaly by trying to find operations which transform binary relations to mirror-anomaly-free ones.
However any of them seems not monotone increasing because of including set-minus operations.
As a very personal feeling, still I am pessimistic to find a “constructive” universe of mirror-anomaly-free universe of rational trees.

5

@kuniaki.mukai did you study @ridgeworks proposal already or what considers
your research in an universe of rational trees equipped with compare/3? Basically
this would be structure, since compare/3 can be bootstrapped from (@<)/2:

/* Structure Signature */
<R, (==)/2, (@<)/2>

Maybe people are not aware, that @ridgeworks proposal of representation
based comparison is a total order. It only violates lexical ordering, but total order
laws will obviously not be violated.

What are total order laws (not violated by all terms):

  • Not A @< A (irreflexiv)
  • If A @< B then not B @< A (asymmetric)
  • if A @< B and B @< C then A @< C (transitive)
  • if not A == B, then A @< B or B @< A (connected)

What is lexical ordering (violated by some cyclic terms):

  • (A,B) @< (C,D) iff A @< C or (A ==C and B @< D) (lexical)
6

It was out of my sight, but it is good news that he found a solution to mirror anomaly problem
loosening lexical order.

7

To get a slightly quicker rep_compare/3, you could partially
evaluate its definition, so that the two naish/2 calls get eliminated
and merged into the compare/3 call, giving some recursive

definition of rep_compare/3 with behaviour as specified here:

rep_compare(C, X, Y) :-
    naish(X, A), naish(Y, B),
    compare(C, X, Y).

So you would make a predicate that does everything at once,
with the following benefit:

  • Fast Failure: It would not anymore first materialize A and B
    through the two nasih/2 calls, but diretly takle the comparison
    roblem. Leading to fast failure if it allready sees that terms are
    different at the root.

  • ‘\a’(N) Not Needed: Since it doesn’t anymore materialize
    A and B, you also don’t need to generate some currious
    compound for a Naish reference. Just deal with the Naish
    reference case inside rep_compare/3.

  • ‘\a’(N) Flexibly Ordered: You might also modify the code,
    and not anymore rely on compare/3 of your Nasih references,
    and impose some other order at your will.

  • naish/2 Obsolete: We can spare us the hussle in developing
    a naive naish/2, by for example forking copy_term/2. It would
    totally disappear.

8

That was exactly what I was thinking. I came to this. Just finished 100M tests in 5 minutes. It can be optimized
a bit further, but it is mostly a demonstrator that can be used as basis for an implementation in the core.

rep_compare(C, X, Y) :-
    rep_compare(C, X, [], Y, []).

rep_compare(C, X, SX, Y, SY), compound(X), compound(Y) =>
    naish_lookup(X, SX, X2, Flag),
    naish_lookup(Y, SY, Y2, Flag),
    (   Flag == true
    ->  compare(C, X2, Y2)
    ;   compound_name_arity(X, NX, AX),
        compound_name_arity(Y, NY, AY),
        (   NX == NY, AX == AY
        ->  compare_args(C, 1, AX, X, [X|SX], Y, [Y|SY])
        ;   compare(C, AX-NX, AY-NY)
        )
    ).
rep_compare(C, X, _, Y, _) =>
    compare(C, X, Y).

compare_args(C, I, Arity, X, SX, Y, SY), I =< Arity =>
    arg(I, X, AX),
    arg(I, Y, AY),
    rep_compare(C0, AX, SX, AY, SY),
    (   C0 == (=)
    ->  I1 is I+1,
        compare_args(C, I1, Arity, X, SX, Y, SY)
    ;   C = C0
    ).
compare_args(C, _I, _Arity, _X, _SX, _Y, _SY) =>
    C = (=).

naish_lookup(Term, Stack, Naish, true) :-
    nth1(N, Stack, Term2),
    Term2 == Term,
    !,
    Naish = N.
naish_lookup(Term, _, Term, _).

With test code like this (should check transitivity as well).

test(N, Pred) :-
    N > 0,
    !,
    (   N mod 10000 =:= 0
    ->  format(user_error, '\r~t~D~20|', [N])
    ;   true
    ),
    random_cyclic(X),
    random_cyclic(Y),
    call(Pred, C1, X, Y),
    call(Pred, C2, Y, X),
    (   consistent(C1, C2)
    ->  N2 is N - 1,
        test(N2, Pred)
    ;   format(user_error, 'FAILED:~n\t~q~n\t~q~n', [X, Y])
    ).
test(_, _).

consistent(=, =).
consistent(<, >).
consistent(>, <).

% random_cyclic(-Term)
random_cyclic(T) :-
   random_cyclic([T], T).

% random_cyclic(+List, -Term)
random_cyclic(L, T) :-
   length(L, M),
   random(R),
   N is truncate(R*(M+3)),
   (   N = 0
   ->  T = 0
   ;   N = 1
   ->  T = 1
   ;   N = 2
   ->  T = s(P,Q),
       random_cyclic([P|L], P),
       random_cyclic([Q|L], Q)
   ;   K is N-3,
       nth0(K, L, S),
       S = T
   ).
9

Possibly a viable implemenation, if the Prolog system has SSU (=>)/2.
Would need some redesign for a Prolog system without SSU (=>)/2.
What do we know about the rest of SWI-Prolog. Now I find an

interesting library,used by distinct/1 for example:

add_nb_set(+Key, !Set, ?New)
Computing the hash for cyclic terms is performed with the help of
term_factorized/3, which performs rather poorly.
nb_set.pl

It uses term_factorized/3. So its possible to create a stack overflow?
See other thread for this bug. Besides that, is the hash key calculation
realiable. Maybe can use some fuzzing and also

find that some essential properties are violated? Can the partial
evaluator approach be used to also derive a more direct hash key?